| Step | Hyp | Ref
| Expression |
| 1 | | opex 5469 |
. . 3
⊢
〈𝐴, 𝐵〉 ∈ V |
| 2 | | opex 5469 |
. . 3
⊢
〈𝐶, 𝐷〉 ∈ V |
| 3 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑝 = 〈𝐴, 𝐵〉 → (𝑝 = 〈𝑎, 𝑏〉 ↔ 〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉)) |
| 4 | | eqcom 2744 |
. . . . . . . 8
⊢
(〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ↔ 〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉) |
| 5 | 3, 4 | bitrdi 287 |
. . . . . . 7
⊢ (𝑝 = 〈𝐴, 𝐵〉 → (𝑝 = 〈𝑎, 𝑏〉 ↔ 〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉)) |
| 6 | 5 | 3anbi1d 1442 |
. . . . . 6
⊢ (𝑝 = 〈𝐴, 𝐵〉 → ((𝑝 = 〈𝑎, 𝑏〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)) ↔ (〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)))) |
| 7 | 6 | rexbidv 3179 |
. . . . 5
⊢ (𝑝 = 〈𝐴, 𝐵〉 → (∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = 〈𝑎, 𝑏〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)) ↔ ∃𝑑 ∈ (𝔼‘𝑛)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)))) |
| 8 | 7 | 2rexbidv 3222 |
. . . 4
⊢ (𝑝 = 〈𝐴, 𝐵〉 → (∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = 〈𝑎, 𝑏〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)) ↔ ∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)))) |
| 9 | 8 | 2rexbidv 3222 |
. . 3
⊢ (𝑝 = 〈𝐴, 𝐵〉 → (∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = 〈𝑎, 𝑏〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)) ↔ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)))) |
| 10 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑞 = 〈𝐶, 𝐷〉 → (𝑞 = 〈𝑐, 𝑑〉 ↔ 〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉)) |
| 11 | | eqcom 2744 |
. . . . . . . 8
⊢
(〈𝐶, 𝐷〉 = 〈𝑐, 𝑑〉 ↔ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉) |
| 12 | 10, 11 | bitrdi 287 |
. . . . . . 7
⊢ (𝑞 = 〈𝐶, 𝐷〉 → (𝑞 = 〈𝑐, 𝑑〉 ↔ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉)) |
| 13 | 12 | 3anbi2d 1443 |
. . . . . 6
⊢ (𝑞 = 〈𝐶, 𝐷〉 → ((〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)) ↔ (〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)))) |
| 14 | 13 | rexbidv 3179 |
. . . . 5
⊢ (𝑞 = 〈𝐶, 𝐷〉 → (∃𝑑 ∈ (𝔼‘𝑛)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)) ↔ ∃𝑑 ∈ (𝔼‘𝑛)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)))) |
| 15 | 14 | 2rexbidv 3222 |
. . . 4
⊢ (𝑞 = 〈𝐶, 𝐷〉 → (∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)) ↔ ∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)))) |
| 16 | 15 | 2rexbidv 3222 |
. . 3
⊢ (𝑞 = 〈𝐶, 𝐷〉 → (∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)) ↔ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)))) |
| 17 | | df-segle 36108 |
. . 3
⊢
Seg≤ = {〈𝑝, 𝑞〉 ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = 〈𝑎, 𝑏〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉))} |
| 18 | 1, 2, 9, 16, 17 | brab 5548 |
. 2
⊢
(〈𝐴, 𝐵〉 Seg≤
〈𝐶, 𝐷〉 ↔ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉))) |
| 19 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑎 ∈ V |
| 20 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑏 ∈ V |
| 21 | 19, 20 | opth 5481 |
. . . . . . . 8
⊢
(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ↔ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵)) |
| 22 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑐 ∈ V |
| 23 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑑 ∈ V |
| 24 | 22, 23 | opth 5481 |
. . . . . . . 8
⊢
(〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ↔ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) |
| 25 | | biid 261 |
. . . . . . . 8
⊢
(∃𝑦 ∈
(𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉) ↔ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)) |
| 26 | 21, 24, 25 | 3anbi123i 1156 |
. . . . . . 7
⊢
((〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)) ↔ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉))) |
| 27 | 26 | 2rexbii 3129 |
. . . . . 6
⊢
(∃𝑐 ∈
(𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)) ↔ ∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉))) |
| 28 | 27 | 2rexbii 3129 |
. . . . 5
⊢
(∃𝑎 ∈
(𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)) ↔ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉))) |
| 29 | 28 | rexbii 3094 |
. . . 4
⊢
(∃𝑛 ∈
ℕ ∃𝑎 ∈
(𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)) ↔ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉))) |
| 30 | | simpl2l 1227 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ (𝔼‘𝑁)) |
| 31 | 30 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 = 𝐴 ∧ (𝑏 = 𝐵 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷))) ∧ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑛 ∈ ℕ) ∧ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛)) ∧ (𝐶 ∈ (𝔼‘𝑛) ∧ 𝐷 ∈ (𝔼‘𝑛))))) → 𝐴 ∈ (𝔼‘𝑁)) |
| 32 | | eleenn 28911 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ (𝔼‘𝑁) → 𝑁 ∈ ℕ) |
| 33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 = 𝐴 ∧ (𝑏 = 𝐵 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷))) ∧ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑛 ∈ ℕ) ∧ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛)) ∧ (𝐶 ∈ (𝔼‘𝑛) ∧ 𝐷 ∈ (𝔼‘𝑛))))) → 𝑁 ∈ ℕ) |
| 34 | | simprlr 780 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 = 𝐴 ∧ (𝑏 = 𝐵 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷))) ∧ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑛 ∈ ℕ) ∧ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛)) ∧ (𝐶 ∈ (𝔼‘𝑛) ∧ 𝐷 ∈ (𝔼‘𝑛))))) → 𝑛 ∈ ℕ) |
| 35 | | simprll 779 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑛 ∈ ℕ) ∧ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛)) ∧ (𝐶 ∈ (𝔼‘𝑛) ∧ 𝐷 ∈ (𝔼‘𝑛)))) → 𝐴 ∈ (𝔼‘𝑛)) |
| 36 | 35 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 = 𝐴 ∧ (𝑏 = 𝐵 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷))) ∧ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑛 ∈ ℕ) ∧ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛)) ∧ (𝐶 ∈ (𝔼‘𝑛) ∧ 𝐷 ∈ (𝔼‘𝑛))))) → 𝐴 ∈ (𝔼‘𝑛)) |
| 37 | | axdimuniq 28928 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁)) ∧ (𝑛 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑛))) → 𝑁 = 𝑛) |
| 38 | 33, 31, 34, 36, 37 | syl22anc 839 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 = 𝐴 ∧ (𝑏 = 𝐵 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷))) ∧ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑛 ∈ ℕ) ∧ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛)) ∧ (𝐶 ∈ (𝔼‘𝑛) ∧ 𝐷 ∈ (𝔼‘𝑛))))) → 𝑁 = 𝑛) |
| 39 | 38 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 = 𝐴 ∧ (𝑏 = 𝐵 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷))) ∧ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑛 ∈ ℕ) ∧ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛)) ∧ (𝐶 ∈ (𝔼‘𝑛) ∧ 𝐷 ∈ (𝔼‘𝑛))))) → (𝔼‘𝑁) = (𝔼‘𝑛)) |
| 40 | 39 | rexeqdv 3327 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 = 𝐴 ∧ (𝑏 = 𝐵 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷))) ∧ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑛 ∈ ℕ) ∧ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛)) ∧ (𝐶 ∈ (𝔼‘𝑛) ∧ 𝐷 ∈ (𝔼‘𝑛))))) → (∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ↔ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
| 41 | 40 | exbiri 811 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = 𝐴 ∧ (𝑏 = 𝐵 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷))) → ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑛 ∈ ℕ) ∧ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛)) ∧ (𝐶 ∈ (𝔼‘𝑛) ∧ 𝐷 ∈ (𝔼‘𝑛)))) → (∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) → ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)))) |
| 42 | 41 | anassrs 467 |
. . . . . . . . . . . 12
⊢ (((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑛 ∈ ℕ) ∧ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛)) ∧ (𝐶 ∈ (𝔼‘𝑛) ∧ 𝐷 ∈ (𝔼‘𝑛)))) → (∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) → ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)))) |
| 43 | | eleq1 2829 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝐴 → (𝑎 ∈ (𝔼‘𝑛) ↔ 𝐴 ∈ (𝔼‘𝑛))) |
| 44 | | eleq1 2829 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = 𝐵 → (𝑏 ∈ (𝔼‘𝑛) ↔ 𝐵 ∈ (𝔼‘𝑛))) |
| 45 | 43, 44 | bi2anan9 638 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛)) ↔ (𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛)))) |
| 46 | | eleq1 2829 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = 𝐶 → (𝑐 ∈ (𝔼‘𝑛) ↔ 𝐶 ∈ (𝔼‘𝑛))) |
| 47 | | eleq1 2829 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = 𝐷 → (𝑑 ∈ (𝔼‘𝑛) ↔ 𝐷 ∈ (𝔼‘𝑛))) |
| 48 | 46, 47 | bi2anan9 638 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → ((𝑐 ∈ (𝔼‘𝑛) ∧ 𝑑 ∈ (𝔼‘𝑛)) ↔ (𝐶 ∈ (𝔼‘𝑛) ∧ 𝐷 ∈ (𝔼‘𝑛)))) |
| 49 | 45, 48 | bi2anan9 638 |
. . . . . . . . . . . . 13
⊢ (((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → (((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛)) ∧ (𝑐 ∈ (𝔼‘𝑛) ∧ 𝑑 ∈ (𝔼‘𝑛))) ↔ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛)) ∧ (𝐶 ∈ (𝔼‘𝑛) ∧ 𝐷 ∈ (𝔼‘𝑛))))) |
| 50 | 49 | anbi2d 630 |
. . . . . . . . . . . 12
⊢ (((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑛 ∈ ℕ) ∧ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛)) ∧ (𝑐 ∈ (𝔼‘𝑛) ∧ 𝑑 ∈ (𝔼‘𝑛)))) ↔ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑛 ∈ ℕ) ∧ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛)) ∧ (𝐶 ∈ (𝔼‘𝑛) ∧ 𝐷 ∈ (𝔼‘𝑛)))))) |
| 51 | | opeq12 4875 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → 〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉) |
| 52 | 51 | breq1d 5153 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉 ↔ 〈𝐴, 𝐵〉Cgr〈𝑐, 𝑦〉)) |
| 53 | 52 | anbi2d 630 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ((𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉) ↔ (𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝑐, 𝑦〉))) |
| 54 | | opeq12 4875 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉) |
| 55 | 54 | breq2d 5155 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → (𝑦 Btwn 〈𝑐, 𝑑〉 ↔ 𝑦 Btwn 〈𝐶, 𝐷〉)) |
| 56 | | opeq1 4873 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 = 𝐶 → 〈𝑐, 𝑦〉 = 〈𝐶, 𝑦〉) |
| 57 | 56 | breq2d 5155 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = 𝐶 → (〈𝐴, 𝐵〉Cgr〈𝑐, 𝑦〉 ↔ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) |
| 58 | 57 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → (〈𝐴, 𝐵〉Cgr〈𝑐, 𝑦〉 ↔ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) |
| 59 | 55, 58 | anbi12d 632 |
. . . . . . . . . . . . . . 15
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → ((𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝑐, 𝑦〉) ↔ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
| 60 | 53, 59 | sylan9bb 509 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → ((𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉) ↔ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
| 61 | 60 | rexbidv 3179 |
. . . . . . . . . . . . 13
⊢ (((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → (∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉) ↔ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
| 62 | 61 | imbi1d 341 |
. . . . . . . . . . . 12
⊢ (((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → ((∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉) → ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) ↔ (∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) → ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)))) |
| 63 | 42, 50, 62 | 3imtr4d 294 |
. . . . . . . . . . 11
⊢ (((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑛 ∈ ℕ) ∧ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛)) ∧ (𝑐 ∈ (𝔼‘𝑛) ∧ 𝑑 ∈ (𝔼‘𝑛)))) → (∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉) → ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)))) |
| 64 | 63 | com12 32 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑛 ∈ ℕ) ∧ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛)) ∧ (𝑐 ∈ (𝔼‘𝑛) ∧ 𝑑 ∈ (𝔼‘𝑛)))) → (((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → (∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉) → ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)))) |
| 65 | 64 | expd 415 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑛 ∈ ℕ) ∧ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛)) ∧ (𝑐 ∈ (𝔼‘𝑛) ∧ 𝑑 ∈ (𝔼‘𝑛)))) → ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → (∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉) → ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))))) |
| 66 | 65 | 3impd 1349 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑛 ∈ ℕ) ∧ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛)) ∧ (𝑐 ∈ (𝔼‘𝑛) ∧ 𝑑 ∈ (𝔼‘𝑛)))) → (((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)) → ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
| 67 | 66 | expr 456 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑛 ∈ ℕ) ∧ (𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛))) → ((𝑐 ∈ (𝔼‘𝑛) ∧ 𝑑 ∈ (𝔼‘𝑛)) → (((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)) → ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)))) |
| 68 | 67 | rexlimdvv 3212 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑛 ∈ ℕ) ∧ (𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛))) → (∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)) → ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
| 69 | 68 | rexlimdvva 3213 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑛 ∈ ℕ) → (∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)) → ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
| 70 | 69 | rexlimdva 3155 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷) ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)) → ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
| 71 | 29, 70 | biimtrid 242 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)) → ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
| 72 | | simpl1 1192 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) → 𝑁 ∈ ℕ) |
| 73 | | simpl2l 1227 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) → 𝐴 ∈ (𝔼‘𝑁)) |
| 74 | | simpl2r 1228 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) → 𝐵 ∈ (𝔼‘𝑁)) |
| 75 | | simpl3l 1229 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) → 𝐶 ∈ (𝔼‘𝑁)) |
| 76 | | simpl3r 1230 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) → 𝐷 ∈ (𝔼‘𝑁)) |
| 77 | | eqidd 2738 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) → 〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉) |
| 78 | | eqidd 2738 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) → 〈𝐶, 𝐷〉 = 〈𝐶, 𝐷〉) |
| 79 | | simpr 484 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) → ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) |
| 80 | | opeq1 4873 |
. . . . . . . . . 10
⊢ (𝑐 = 𝐶 → 〈𝑐, 𝑑〉 = 〈𝐶, 𝑑〉) |
| 81 | 80 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (𝑐 = 𝐶 → (〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ↔ 〈𝐶, 𝑑〉 = 〈𝐶, 𝐷〉)) |
| 82 | 80 | breq2d 5155 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝐶 → (𝑦 Btwn 〈𝑐, 𝑑〉 ↔ 𝑦 Btwn 〈𝐶, 𝑑〉)) |
| 83 | 82, 57 | anbi12d 632 |
. . . . . . . . . 10
⊢ (𝑐 = 𝐶 → ((𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝑐, 𝑦〉) ↔ (𝑦 Btwn 〈𝐶, 𝑑〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
| 84 | 83 | rexbidv 3179 |
. . . . . . . . 9
⊢ (𝑐 = 𝐶 → (∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝑐, 𝑦〉) ↔ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝑑〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
| 85 | 81, 84 | 3anbi23d 1441 |
. . . . . . . 8
⊢ (𝑐 = 𝐶 → ((〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝑐, 𝑦〉)) ↔ (〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝑑〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)))) |
| 86 | | opeq2 4874 |
. . . . . . . . . 10
⊢ (𝑑 = 𝐷 → 〈𝐶, 𝑑〉 = 〈𝐶, 𝐷〉) |
| 87 | 86 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (𝑑 = 𝐷 → (〈𝐶, 𝑑〉 = 〈𝐶, 𝐷〉 ↔ 〈𝐶, 𝐷〉 = 〈𝐶, 𝐷〉)) |
| 88 | 86 | breq2d 5155 |
. . . . . . . . . . 11
⊢ (𝑑 = 𝐷 → (𝑦 Btwn 〈𝐶, 𝑑〉 ↔ 𝑦 Btwn 〈𝐶, 𝐷〉)) |
| 89 | 88 | anbi1d 631 |
. . . . . . . . . 10
⊢ (𝑑 = 𝐷 → ((𝑦 Btwn 〈𝐶, 𝑑〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ↔ (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
| 90 | 89 | rexbidv 3179 |
. . . . . . . . 9
⊢ (𝑑 = 𝐷 → (∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝑑〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ↔ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
| 91 | 87, 90 | 3anbi23d 1441 |
. . . . . . . 8
⊢ (𝑑 = 𝐷 → ((〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝑑〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) ↔ (〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)))) |
| 92 | 85, 91 | rspc2ev 3635 |
. . . . . . 7
⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ (〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉 ∧ 〈𝐶, 𝐷〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) → ∃𝑐 ∈ (𝔼‘𝑁)∃𝑑 ∈ (𝔼‘𝑁)(〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝑐, 𝑦〉))) |
| 93 | 75, 76, 77, 78, 79, 92 | syl113anc 1384 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) → ∃𝑐 ∈ (𝔼‘𝑁)∃𝑑 ∈ (𝔼‘𝑁)(〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝑐, 𝑦〉))) |
| 94 | | opeq1 4873 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐴 → 〈𝑎, 𝑏〉 = 〈𝐴, 𝑏〉) |
| 95 | 94 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → (〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ↔ 〈𝐴, 𝑏〉 = 〈𝐴, 𝐵〉)) |
| 96 | 94 | breq1d 5153 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝐴 → (〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉 ↔ 〈𝐴, 𝑏〉Cgr〈𝑐, 𝑦〉)) |
| 97 | 96 | anbi2d 630 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐴 → ((𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉) ↔ (𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝐴, 𝑏〉Cgr〈𝑐, 𝑦〉))) |
| 98 | 97 | rexbidv 3179 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → (∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉) ↔ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝐴, 𝑏〉Cgr〈𝑐, 𝑦〉))) |
| 99 | 95, 98 | 3anbi13d 1440 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → ((〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)) ↔ (〈𝐴, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝐴, 𝑏〉Cgr〈𝑐, 𝑦〉)))) |
| 100 | 99 | 2rexbidv 3222 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → (∃𝑐 ∈ (𝔼‘𝑁)∃𝑑 ∈ (𝔼‘𝑁)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)) ↔ ∃𝑐 ∈ (𝔼‘𝑁)∃𝑑 ∈ (𝔼‘𝑁)(〈𝐴, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝐴, 𝑏〉Cgr〈𝑐, 𝑦〉)))) |
| 101 | | opeq2 4874 |
. . . . . . . . . 10
⊢ (𝑏 = 𝐵 → 〈𝐴, 𝑏〉 = 〈𝐴, 𝐵〉) |
| 102 | 101 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (𝑏 = 𝐵 → (〈𝐴, 𝑏〉 = 〈𝐴, 𝐵〉 ↔ 〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉)) |
| 103 | 101 | breq1d 5153 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝐵 → (〈𝐴, 𝑏〉Cgr〈𝑐, 𝑦〉 ↔ 〈𝐴, 𝐵〉Cgr〈𝑐, 𝑦〉)) |
| 104 | 103 | anbi2d 630 |
. . . . . . . . . 10
⊢ (𝑏 = 𝐵 → ((𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝐴, 𝑏〉Cgr〈𝑐, 𝑦〉) ↔ (𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝑐, 𝑦〉))) |
| 105 | 104 | rexbidv 3179 |
. . . . . . . . 9
⊢ (𝑏 = 𝐵 → (∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝐴, 𝑏〉Cgr〈𝑐, 𝑦〉) ↔ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝑐, 𝑦〉))) |
| 106 | 102, 105 | 3anbi13d 1440 |
. . . . . . . 8
⊢ (𝑏 = 𝐵 → ((〈𝐴, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝐴, 𝑏〉Cgr〈𝑐, 𝑦〉)) ↔ (〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝑐, 𝑦〉)))) |
| 107 | 106 | 2rexbidv 3222 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → (∃𝑐 ∈ (𝔼‘𝑁)∃𝑑 ∈ (𝔼‘𝑁)(〈𝐴, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝐴, 𝑏〉Cgr〈𝑐, 𝑦〉)) ↔ ∃𝑐 ∈ (𝔼‘𝑁)∃𝑑 ∈ (𝔼‘𝑁)(〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝑐, 𝑦〉)))) |
| 108 | 100, 107 | rspc2ev 3635 |
. . . . . 6
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ ∃𝑐 ∈ (𝔼‘𝑁)∃𝑑 ∈ (𝔼‘𝑁)(〈𝐴, 𝐵〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝑐, 𝑦〉))) → ∃𝑎 ∈ (𝔼‘𝑁)∃𝑏 ∈ (𝔼‘𝑁)∃𝑐 ∈ (𝔼‘𝑁)∃𝑑 ∈ (𝔼‘𝑁)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉))) |
| 109 | 73, 74, 93, 108 | syl3anc 1373 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) → ∃𝑎 ∈ (𝔼‘𝑁)∃𝑏 ∈ (𝔼‘𝑁)∃𝑐 ∈ (𝔼‘𝑁)∃𝑑 ∈ (𝔼‘𝑁)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉))) |
| 110 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (𝔼‘𝑛) = (𝔼‘𝑁)) |
| 111 | 110 | rexeqdv 3327 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑁 → (∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉) ↔ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉))) |
| 112 | 111 | 3anbi3d 1444 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑁 → ((〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)) ↔ (〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)))) |
| 113 | 110, 112 | rexeqbidv 3347 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → (∃𝑑 ∈ (𝔼‘𝑛)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)) ↔ ∃𝑑 ∈ (𝔼‘𝑁)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)))) |
| 114 | 110, 113 | rexeqbidv 3347 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)) ↔ ∃𝑐 ∈ (𝔼‘𝑁)∃𝑑 ∈ (𝔼‘𝑁)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)))) |
| 115 | 110, 114 | rexeqbidv 3347 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)) ↔ ∃𝑏 ∈ (𝔼‘𝑁)∃𝑐 ∈ (𝔼‘𝑁)∃𝑑 ∈ (𝔼‘𝑁)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)))) |
| 116 | 110, 115 | rexeqbidv 3347 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)) ↔ ∃𝑎 ∈ (𝔼‘𝑁)∃𝑏 ∈ (𝔼‘𝑁)∃𝑐 ∈ (𝔼‘𝑁)∃𝑑 ∈ (𝔼‘𝑁)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)))) |
| 117 | 116 | rspcev 3622 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧
∃𝑎 ∈
(𝔼‘𝑁)∃𝑏 ∈ (𝔼‘𝑁)∃𝑐 ∈ (𝔼‘𝑁)∃𝑑 ∈ (𝔼‘𝑁)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉))) → ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉))) |
| 118 | 72, 109, 117 | syl2anc 584 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉)) → ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉))) |
| 119 | 118 | ex 412 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) → ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)))) |
| 120 | 71, 119 | impbid 212 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn 〈𝑐, 𝑑〉 ∧ 〈𝑎, 𝑏〉Cgr〈𝑐, 𝑦〉)) ↔ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
| 121 | 18, 120 | bitrid 283 |
1
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ↔ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |