Step | Hyp | Ref
| Expression |
1 | | segcon2 31382 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ∃𝑥 ∈ (𝔼‘𝑁)((𝐵 Btwn 〈𝐴, 𝑥〉 ∨ 𝑥 Btwn 〈𝐴, 𝐵〉) ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉)) |
2 | | andir 908 |
. . . . 5
⊢ (((𝐵 Btwn 〈𝐴, 𝑥〉 ∨ 𝑥 Btwn 〈𝐴, 𝐵〉) ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) ↔ ((𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) ∨ (𝑥 Btwn 〈𝐴, 𝐵〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉))) |
3 | | simpl1 1057 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ) |
4 | | simpl2l 1107 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐴 ∈ (𝔼‘𝑁)) |
5 | | simpr 476 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁)) |
6 | | simpl3 1059 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) |
7 | | cgrcom 31267 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉 ↔ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉)) |
8 | 3, 4, 5, 6, 7 | syl121anc 1323 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉 ↔ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉)) |
9 | 8 | anbi2d 736 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑥 Btwn 〈𝐴, 𝐵〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) ↔ (𝑥 Btwn 〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉))) |
10 | 9 | orbi2d 734 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (((𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) ∨ (𝑥 Btwn 〈𝐴, 𝐵〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉)) ↔ ((𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) ∨ (𝑥 Btwn 〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉)))) |
11 | 2, 10 | syl5bb 271 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (((𝐵 Btwn 〈𝐴, 𝑥〉 ∨ 𝑥 Btwn 〈𝐴, 𝐵〉) ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) ↔ ((𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) ∨ (𝑥 Btwn 〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉)))) |
12 | 11 | rexbidva 3031 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (∃𝑥 ∈ (𝔼‘𝑁)((𝐵 Btwn 〈𝐴, 𝑥〉 ∨ 𝑥 Btwn 〈𝐴, 𝐵〉) ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) ↔ ∃𝑥 ∈ (𝔼‘𝑁)((𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) ∨ (𝑥 Btwn 〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉)))) |
13 | | brsegle2 31386 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ↔ ∃𝑥 ∈ (𝔼‘𝑁)(𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉))) |
14 | | brsegle 31385 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (〈𝐶, 𝐷〉 Seg≤ 〈𝐴, 𝐵〉 ↔ ∃𝑥 ∈ (𝔼‘𝑁)(𝑥 Btwn 〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉))) |
15 | 14 | 3com23 1263 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐶, 𝐷〉 Seg≤ 〈𝐴, 𝐵〉 ↔ ∃𝑥 ∈ (𝔼‘𝑁)(𝑥 Btwn 〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉))) |
16 | 13, 15 | orbi12d 742 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ∨ 〈𝐶, 𝐷〉 Seg≤ 〈𝐴, 𝐵〉) ↔ (∃𝑥 ∈ (𝔼‘𝑁)(𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) ∨ ∃𝑥 ∈ (𝔼‘𝑁)(𝑥 Btwn 〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉)))) |
17 | | r19.43 3074 |
. . . 4
⊢
(∃𝑥 ∈
(𝔼‘𝑁)((𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) ∨ (𝑥 Btwn 〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉)) ↔ (∃𝑥 ∈ (𝔼‘𝑁)(𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) ∨ ∃𝑥 ∈ (𝔼‘𝑁)(𝑥 Btwn 〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉))) |
18 | 16, 17 | syl6bbr 277 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ∨ 〈𝐶, 𝐷〉 Seg≤ 〈𝐴, 𝐵〉) ↔ ∃𝑥 ∈ (𝔼‘𝑁)((𝐵 Btwn 〈𝐴, 𝑥〉 ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) ∨ (𝑥 Btwn 〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝑥〉)))) |
19 | 12, 18 | bitr4d 270 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (∃𝑥 ∈ (𝔼‘𝑁)((𝐵 Btwn 〈𝐴, 𝑥〉 ∨ 𝑥 Btwn 〈𝐴, 𝐵〉) ∧ 〈𝐴, 𝑥〉Cgr〈𝐶, 𝐷〉) ↔ (〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ∨ 〈𝐶, 𝐷〉 Seg≤ 〈𝐴, 𝐵〉))) |
20 | 1, 19 | mpbid 221 |
1
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ∨ 〈𝐶, 𝐷〉 Seg≤ 〈𝐴, 𝐵〉)) |