| Step | Hyp | Ref
| Expression |
| 1 | | segcon2 36106 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ∃𝑥 ∈ (𝔼‘𝑁)((𝑅 Btwn 〈𝐴, 𝑥〉 ∨ 𝑥 Btwn 〈𝐴, 𝑅〉) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉)) |
| 2 | 1 | adantr 480 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶)) → ∃𝑥 ∈ (𝔼‘𝑁)((𝑅 Btwn 〈𝐴, 𝑥〉 ∨ 𝑥 Btwn 〈𝐴, 𝑅〉) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉)) |
| 3 | | simpl1 1192 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ) |
| 4 | | simpl2l 1227 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐴 ∈ (𝔼‘𝑁)) |
| 5 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁)) |
| 6 | | simpl2r 1228 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑅 ∈ (𝔼‘𝑁)) |
| 7 | | broutsideof2 36123 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝐴OutsideOf〈𝑥, 𝑅〉 ↔ (𝑥 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉)))) |
| 8 | 3, 4, 5, 6, 7 | syl13anc 1374 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝐴OutsideOf〈𝑥, 𝑅〉 ↔ (𝑥 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉)))) |
| 9 | 8 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ ((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉)) → (𝐴OutsideOf〈𝑥, 𝑅〉 ↔ (𝑥 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉)))) |
| 10 | | simp3 1139 |
. . . . . . . . . . 11
⊢ ((𝑥 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉)) → (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉)) |
| 11 | | simpllr 776 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉)) → 𝐵 ≠ 𝐶) |
| 12 | 11 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉))) → 𝐵 ≠ 𝐶) |
| 13 | | simprlr 780 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉))) → 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) |
| 14 | | simp2l 1200 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁)) |
| 15 | 14 | anim1i 615 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁))) |
| 16 | | simpl3 1194 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) |
| 17 | | cgrdegen 36005 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉 → (𝐴 = 𝑥 ↔ 𝐵 = 𝐶))) |
| 18 | 3, 15, 16, 17 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉 → (𝐴 = 𝑥 ↔ 𝐵 = 𝐶))) |
| 19 | 18 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉))) → (〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉 → (𝐴 = 𝑥 ↔ 𝐵 = 𝐶))) |
| 20 | 13, 19 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉))) → (𝐴 = 𝑥 ↔ 𝐵 = 𝐶)) |
| 21 | 20 | necon3bid 2985 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉))) → (𝐴 ≠ 𝑥 ↔ 𝐵 ≠ 𝐶)) |
| 22 | 12, 21 | mpbird 257 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉))) → 𝐴 ≠ 𝑥) |
| 23 | 22 | necomd 2996 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉))) → 𝑥 ≠ 𝐴) |
| 24 | | simplll 775 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉)) → 𝑅 ≠ 𝐴) |
| 25 | 24 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉))) → 𝑅 ≠ 𝐴) |
| 26 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉))) → (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉)) |
| 27 | 23, 25, 26 | 3jca 1129 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉))) → (𝑥 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉))) |
| 28 | 27 | expr 456 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ ((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉)) → ((𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉) → (𝑥 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉)))) |
| 29 | 10, 28 | impbid2 226 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ ((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉)) → ((𝑥 ≠ 𝐴 ∧ 𝑅 ≠ 𝐴 ∧ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉)) ↔ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉))) |
| 30 | 9, 29 | bitrd 279 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ ((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉)) → (𝐴OutsideOf〈𝑥, 𝑅〉 ↔ (𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉))) |
| 31 | | orcom 871 |
. . . . . . . . 9
⊢ ((𝑥 Btwn 〈𝐴, 𝑅〉 ∨ 𝑅 Btwn 〈𝐴, 𝑥〉) ↔ (𝑅 Btwn 〈𝐴, 𝑥〉 ∨ 𝑥 Btwn 〈𝐴, 𝑅〉)) |
| 32 | 30, 31 | bitrdi 287 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ ((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉)) → (𝐴OutsideOf〈𝑥, 𝑅〉 ↔ (𝑅 Btwn 〈𝐴, 𝑥〉 ∨ 𝑥 Btwn 〈𝐴, 𝑅〉))) |
| 33 | 32 | expr 456 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶)) → (〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉 → (𝐴OutsideOf〈𝑥, 𝑅〉 ↔ (𝑅 Btwn 〈𝐴, 𝑥〉 ∨ 𝑥 Btwn 〈𝐴, 𝑅〉)))) |
| 34 | 33 | pm5.32rd 578 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶)) → ((𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ↔ ((𝑅 Btwn 〈𝐴, 𝑥〉 ∨ 𝑥 Btwn 〈𝐴, 𝑅〉) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉))) |
| 35 | 34 | an32s 652 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶)) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ↔ ((𝑅 Btwn 〈𝐴, 𝑥〉 ∨ 𝑥 Btwn 〈𝐴, 𝑅〉) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉))) |
| 36 | 35 | rexbidva 3177 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶)) → (∃𝑥 ∈ (𝔼‘𝑁)(𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ↔ ∃𝑥 ∈ (𝔼‘𝑁)((𝑅 Btwn 〈𝐴, 𝑥〉 ∨ 𝑥 Btwn 〈𝐴, 𝑅〉) ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉))) |
| 37 | 2, 36 | mpbird 257 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶)) → ∃𝑥 ∈ (𝔼‘𝑁)(𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉)) |
| 38 | | simpl1 1192 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) |
| 39 | | simpl2l 1227 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁)) |
| 40 | | simpl2r 1228 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝑅 ∈ (𝔼‘𝑁)) |
| 41 | | simpl3l 1229 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁)) |
| 42 | 39, 40, 41 | 3jca 1129 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) |
| 43 | | simpl3r 1230 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁)) |
| 44 | | simprl 771 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝑥 ∈ (𝔼‘𝑁)) |
| 45 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → 𝑦 ∈ (𝔼‘𝑁)) |
| 46 | 43, 44, 45 | 3jca 1129 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) |
| 47 | 38, 42, 46 | 3jca 1129 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)))) |
| 48 | | simpr 484 |
. . . . . . 7
⊢ (((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ ((𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝐴OutsideOf〈𝑦, 𝑅〉 ∧ 〈𝐴, 𝑦〉Cgr〈𝐵, 𝐶〉))) → ((𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝐴OutsideOf〈𝑦, 𝑅〉 ∧ 〈𝐴, 𝑦〉Cgr〈𝐵, 𝐶〉))) |
| 49 | | outsideofeq 36131 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) → (((𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝐴OutsideOf〈𝑦, 𝑅〉 ∧ 〈𝐴, 𝑦〉Cgr〈𝐵, 𝐶〉)) → 𝑥 = 𝑦)) |
| 50 | 49 | imp 406 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) ∧ ((𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝐴OutsideOf〈𝑦, 𝑅〉 ∧ 〈𝐴, 𝑦〉Cgr〈𝐵, 𝐶〉))) → 𝑥 = 𝑦) |
| 51 | 47, 48, 50 | syl2an 596 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁))) ∧ ((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) ∧ ((𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝐴OutsideOf〈𝑦, 𝑅〉 ∧ 〈𝐴, 𝑦〉Cgr〈𝐵, 𝐶〉)))) → 𝑥 = 𝑦) |
| 52 | 51 | an4s 660 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶)) ∧ ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ ((𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝐴OutsideOf〈𝑦, 𝑅〉 ∧ 〈𝐴, 𝑦〉Cgr〈𝐵, 𝐶〉)))) → 𝑥 = 𝑦) |
| 53 | 52 | exp32 420 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶)) → ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (((𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝐴OutsideOf〈𝑦, 𝑅〉 ∧ 〈𝐴, 𝑦〉Cgr〈𝐵, 𝐶〉)) → 𝑥 = 𝑦))) |
| 54 | 53 | ralrimivv 3200 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶)) → ∀𝑥 ∈ (𝔼‘𝑁)∀𝑦 ∈ (𝔼‘𝑁)(((𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝐴OutsideOf〈𝑦, 𝑅〉 ∧ 〈𝐴, 𝑦〉Cgr〈𝐵, 𝐶〉)) → 𝑥 = 𝑦)) |
| 55 | | opeq1 4873 |
. . . . . 6
⊢ (𝑥 = 𝑦 → 〈𝑥, 𝑅〉 = 〈𝑦, 𝑅〉) |
| 56 | 55 | breq2d 5155 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐴OutsideOf〈𝑥, 𝑅〉 ↔ 𝐴OutsideOf〈𝑦, 𝑅〉)) |
| 57 | | opeq2 4874 |
. . . . . 6
⊢ (𝑥 = 𝑦 → 〈𝐴, 𝑥〉 = 〈𝐴, 𝑦〉) |
| 58 | 57 | breq1d 5153 |
. . . . 5
⊢ (𝑥 = 𝑦 → (〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉 ↔ 〈𝐴, 𝑦〉Cgr〈𝐵, 𝐶〉)) |
| 59 | 56, 58 | anbi12d 632 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ↔ (𝐴OutsideOf〈𝑦, 𝑅〉 ∧ 〈𝐴, 𝑦〉Cgr〈𝐵, 𝐶〉))) |
| 60 | 59 | reu4 3737 |
. . 3
⊢
(∃!𝑥 ∈
(𝔼‘𝑁)(𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ↔ (∃𝑥 ∈ (𝔼‘𝑁)(𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ ∀𝑥 ∈ (𝔼‘𝑁)∀𝑦 ∈ (𝔼‘𝑁)(((𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉) ∧ (𝐴OutsideOf〈𝑦, 𝑅〉 ∧ 〈𝐴, 𝑦〉Cgr〈𝐵, 𝐶〉)) → 𝑥 = 𝑦))) |
| 61 | 37, 54, 60 | sylanbrc 583 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶)) → ∃!𝑥 ∈ (𝔼‘𝑁)(𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉)) |
| 62 | 61 | ex 412 |
1
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) → ∃!𝑥 ∈ (𝔼‘𝑁)(𝐴OutsideOf〈𝑥, 𝑅〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐵, 𝐶〉))) |