Step | Hyp | Ref
| Expression |
1 | | segcon2 31382 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ∃𝑥 ∈ (𝔼‘𝑁)((𝑅 Btwn 〈𝐴, 𝑥〉 ∨ 𝑥 Btwn 〈𝐴, 𝑅〉) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉)) |
2 | 1 | adantr 480 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶)) → ∃𝑥 ∈ (𝔼‘𝑁)((𝑅 Btwn 〈𝐴, 𝑥〉 ∨ 𝑥 Btwn 〈𝐴, 𝑅〉) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉)) |
3 | | simpl1 1057 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ) |
4 | | simpl2l 1107 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐴 ∈ (𝔼‘𝑁)) |
5 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁)) |
6 | | simpl2r 1108 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑅 ∈ (𝔼‘𝑁)) |
7 | | broutsideof2 31399 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝐴OutsideOf〈𝑥, 𝑅〉 ↔ (𝑥 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉)))) |
8 | 3, 4, 5, 6, 7 | syl13anc 1320 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝐴OutsideOf〈𝑥, 𝑅〉 ↔ (𝑥 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉)))) |
9 | 8 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ ((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉)) → (𝐴OutsideOf〈𝑥, 𝑅〉 ↔ (𝑥 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉)))) |
10 | | simp3 1056 |
. . . . . . . . . . 11
⊢ ((𝑥 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉)) → (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉)) |
11 | | simpllr 795 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉)) → 𝐵 ≠ 𝐶) |
12 | 11 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉))) → 𝐵 ≠ 𝐶) |
13 | | simprlr 799 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉))) → 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) |
14 | | simp2l 1080 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁)) |
15 | 14 | anim1i 590 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) |
16 | | simpl3 1059 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) |
17 | | cgrdegen 31281 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉 → (𝐴 = 𝑥 ↔ 𝐵 = 𝐶))) |
18 | 3, 15, 16, 17 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉 → (𝐴 = 𝑥 ↔ 𝐵 = 𝐶))) |
19 | 18 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉))) → (〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉 → (𝐴 = 𝑥 ↔ 𝐵 = 𝐶))) |
20 | 13, 19 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉))) → (𝐴 = 𝑥 ↔ 𝐵 = 𝐶)) |
21 | 20 | necon3bid 2826 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉))) → (𝐴 ≠ 𝑥 ↔ 𝐵 ≠ 𝐶)) |
22 | 12, 21 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉))) → 𝐴 ≠ 𝑥) |
23 | 22 | necomd 2837 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉))) → 𝑥 ≠ 𝐴) |
24 | | simplll 794 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉)) → 𝑅 ≠ 𝐴) |
25 | 24 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉))) → 𝑅 ≠ 𝐴) |
26 | | simprr 792 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉))) → (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉)) |
27 | 23, 25, 26 | 3jca 1235 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉))) → (𝑥 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉))) |
28 | 27 | expr 641 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ ((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉)) → ((𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉) → (𝑥 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉)))) |
29 | 10, 28 | impbid2 215 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ ((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉)) → ((𝑥 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉)) ↔ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉))) |
30 | 9, 29 | bitrd 267 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ ((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉)) → (𝐴OutsideOf〈𝑥, 𝑅〉 ↔ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉))) |
31 | | orcom 401 |
. . . . . . . . 9
⊢ ((𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉) ↔ (𝑅 Btwn 〈𝐴, 𝑥〉 ∨ 𝑥 Btwn 〈𝐴, 𝑅〉)) |
32 | 30, 31 | syl6bb 275 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ ((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉)) → (𝐴OutsideOf〈𝑥, 𝑅〉 ↔ (𝑅 Btwn 〈𝐴, 𝑥〉 ∨ 𝑥 Btwn 〈𝐴, 𝑅〉))) |
33 | 32 | expr 641 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶)) → (〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉 → (𝐴OutsideOf〈𝑥, 𝑅〉 ↔ (𝑅 Btwn 〈𝐴, 𝑥〉 ∨ 𝑥 Btwn 〈𝐴, 𝑅〉)))) |
34 | 33 | pm5.32rd 670 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶)) → ((𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ↔ ((𝑅 Btwn 〈𝐴, 𝑥〉 ∨ 𝑥 Btwn 〈𝐴, 𝑅〉) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉))) |
35 | 34 | an32s 842 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ↔ ((𝑅 Btwn 〈𝐴, 𝑥〉 ∨ 𝑥 Btwn 〈𝐴, 𝑅〉) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉))) |
36 | 35 | rexbidva 3031 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶)) → (∃𝑥 ∈ (𝔼‘𝑁)(𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ↔ ∃𝑥 ∈ (𝔼‘𝑁)((𝑅 Btwn 〈𝐴, 𝑥〉 ∨ 𝑥 Btwn 〈𝐴, 𝑅〉) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉))) |
37 | 2, 36 | mpbird 246 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶)) → ∃𝑥 ∈ (𝔼‘𝑁)(𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉)) |
38 | | simpl1 1057 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) |
39 | | simpl2l 1107 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁)) |
40 | | simpl2r 1108 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝑅 ∈ (𝔼‘𝑁)) |
41 | | simpl3l 1109 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁)) |
42 | 39, 40, 41 | 3jca 1235 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) |
43 | | simpl3r 1110 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁)) |
44 | | simprl 790 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝑥 ∈ (𝔼‘𝑁)) |
45 | | simprr 792 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝑦 ∈ (𝔼‘𝑁)) |
46 | 43, 44, 45 | 3jca 1235 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) |
47 | 38, 42, 46 | 3jca 1235 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)))) |
48 | | simpr 476 |
. . . . . . 7
⊢ (((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ ((𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝐴OutsideOf〈𝑦, 𝑅〉 ∧ 〈𝐴, 𝑦〉Cgr〈𝐵, 𝐶〉))) → ((𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝐴OutsideOf〈𝑦, 𝑅〉 ∧ 〈𝐴, 𝑦〉Cgr〈𝐵, 𝐶〉))) |
49 | | outsideofeq 31407 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (((𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝐴OutsideOf〈𝑦, 𝑅〉 ∧ 〈𝐴, 𝑦〉Cgr〈𝐵, 𝐶〉)) → 𝑥 = 𝑦)) |
50 | 49 | imp 444 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) ∧ ((𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝐴OutsideOf〈𝑦, 𝑅〉 ∧ 〈𝐴, 𝑦〉Cgr〈𝐵, 𝐶〉))) → 𝑥 = 𝑦) |
51 | 47, 48, 50 | syl2an 493 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) ∧ ((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ ((𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝐴OutsideOf〈𝑦, 𝑅〉 ∧ 〈𝐴, 𝑦〉Cgr〈𝐵, 𝐶〉)))) → 𝑥 = 𝑦) |
52 | 51 | an4s 865 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶)) ∧ ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ ((𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝐴OutsideOf〈𝑦, 𝑅〉 ∧ 〈𝐴, 𝑦〉Cgr〈𝐵, 𝐶〉)))) → 𝑥 = 𝑦) |
53 | 52 | exp32 629 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶)) → ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (((𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝐴OutsideOf〈𝑦, 𝑅〉 ∧ 〈𝐴, 𝑦〉Cgr〈𝐵, 𝐶〉)) → 𝑥 = 𝑦))) |
54 | 53 | ralrimivv 2953 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶)) → ∀𝑥 ∈ (𝔼‘𝑁)∀𝑦 ∈ (𝔼‘𝑁)(((𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝐴OutsideOf〈𝑦, 𝑅〉 ∧ 〈𝐴, 𝑦〉Cgr〈𝐵, 𝐶〉)) → 𝑥 = 𝑦)) |
55 | | opeq1 4340 |
. . . . . 6
⊢ (𝑥 = 𝑦 → 〈𝑥, 𝑅〉 = 〈𝑦, 𝑅〉) |
56 | 55 | breq2d 4595 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐴OutsideOf〈𝑥, 𝑅〉 ↔ 𝐴OutsideOf〈𝑦, 𝑅〉)) |
57 | | opeq2 4341 |
. . . . . 6
⊢ (𝑥 = 𝑦 → 〈𝐴, 𝑥〉 = 〈𝐴, 𝑦〉) |
58 | 57 | breq1d 4593 |
. . . . 5
⊢ (𝑥 = 𝑦 → (〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉 ↔ 〈𝐴, 𝑦〉Cgr〈𝐵, 𝐶〉)) |
59 | 56, 58 | anbi12d 743 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ↔ (𝐴OutsideOf〈𝑦, 𝑅〉 ∧ 〈𝐴, 𝑦〉Cgr〈𝐵, 𝐶〉))) |
60 | 59 | reu4 3367 |
. . 3
⊢
(∃!𝑥 ∈
(𝔼‘𝑁)(𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ↔ (∃𝑥 ∈ (𝔼‘𝑁)(𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ ∀𝑥 ∈ (𝔼‘𝑁)∀𝑦 ∈ (𝔼‘𝑁)(((𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝐴OutsideOf〈𝑦, 𝑅〉 ∧ 〈𝐴, 𝑦〉Cgr〈𝐵, 𝐶〉)) → 𝑥 = 𝑦))) |
61 | 37, 54, 60 | sylanbrc 695 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶)) → ∃!𝑥 ∈ (𝔼‘𝑁)(𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉)) |
62 | 61 | ex 449 |
1
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) → ∃!𝑥 ∈ (𝔼‘𝑁)(𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉))) |