Step | Hyp | Ref
| Expression |
1 | | axtgeucl.6 |
. 2
⊢ (𝜑 → 𝑈 ∈ (𝑋𝐼𝑉)) |
2 | | axtgeucl.7 |
. 2
⊢ (𝜑 → 𝑈 ∈ (𝑌𝐼𝑍)) |
3 | | axtgeucl.8 |
. 2
⊢ (𝜑 → 𝑋 ≠ 𝑈) |
4 | | axtgeucl.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈
TarskiGE) |
5 | | axtrkge.p |
. . . . . . 7
⊢ 𝑃 = (Base‘𝐺) |
6 | | axtrkge.d |
. . . . . . 7
⊢ − =
(dist‘𝐺) |
7 | | axtrkge.i |
. . . . . . 7
⊢ 𝐼 = (Itv‘𝐺) |
8 | 5, 6, 7 | istrkge 26814 |
. . . . . 6
⊢ (𝐺 ∈ TarskiGE
↔ (𝐺 ∈ V ∧
∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))) |
9 | 4, 8 | sylib 217 |
. . . . 5
⊢ (𝜑 → (𝐺 ∈ V ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))) |
10 | 9 | simprd 496 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))) |
11 | | axtgeucl.1 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝑃) |
12 | | axtgeucl.2 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝑃) |
13 | | axtgeucl.3 |
. . . . 5
⊢ (𝜑 → 𝑍 ∈ 𝑃) |
14 | | oveq1 7276 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → (𝑥𝐼𝑣) = (𝑋𝐼𝑣)) |
15 | 14 | eleq2d 2826 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝑢 ∈ (𝑥𝐼𝑣) ↔ 𝑢 ∈ (𝑋𝐼𝑣))) |
16 | | neeq1 3008 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝑥 ≠ 𝑢 ↔ 𝑋 ≠ 𝑢)) |
17 | 15, 16 | 3anbi13d 1437 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) ↔ (𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑋 ≠ 𝑢))) |
18 | | oveq1 7276 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (𝑥𝐼𝑎) = (𝑋𝐼𝑎)) |
19 | 18 | eleq2d 2826 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → (𝑦 ∈ (𝑥𝐼𝑎) ↔ 𝑦 ∈ (𝑋𝐼𝑎))) |
20 | | oveq1 7276 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (𝑥𝐼𝑏) = (𝑋𝐼𝑏)) |
21 | 20 | eleq2d 2826 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → (𝑧 ∈ (𝑥𝐼𝑏) ↔ 𝑧 ∈ (𝑋𝐼𝑏))) |
22 | 19, 21 | 3anbi12d 1436 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → ((𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ (𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))) |
23 | 22 | 2rexbidv 3231 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))) |
24 | 17, 23 | imbi12d 345 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))) |
25 | 24 | 2ralbidv 3125 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))) |
26 | | oveq1 7276 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑌 → (𝑦𝐼𝑧) = (𝑌𝐼𝑧)) |
27 | 26 | eleq2d 2826 |
. . . . . . . . 9
⊢ (𝑦 = 𝑌 → (𝑢 ∈ (𝑦𝐼𝑧) ↔ 𝑢 ∈ (𝑌𝐼𝑧))) |
28 | 27 | 3anbi2d 1440 |
. . . . . . . 8
⊢ (𝑦 = 𝑌 → ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑋 ≠ 𝑢) ↔ (𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑧) ∧ 𝑋 ≠ 𝑢))) |
29 | | eleq1 2828 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑌 → (𝑦 ∈ (𝑋𝐼𝑎) ↔ 𝑌 ∈ (𝑋𝐼𝑎))) |
30 | 29 | 3anbi1d 1439 |
. . . . . . . . 9
⊢ (𝑦 = 𝑌 → ((𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))) |
31 | 30 | 2rexbidv 3231 |
. . . . . . . 8
⊢ (𝑦 = 𝑌 → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))) |
32 | 28, 31 | imbi12d 345 |
. . . . . . 7
⊢ (𝑦 = 𝑌 → (((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))) |
33 | 32 | 2ralbidv 3125 |
. . . . . 6
⊢ (𝑦 = 𝑌 → (∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))) |
34 | | oveq2 7277 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑍 → (𝑌𝐼𝑧) = (𝑌𝐼𝑍)) |
35 | 34 | eleq2d 2826 |
. . . . . . . . 9
⊢ (𝑧 = 𝑍 → (𝑢 ∈ (𝑌𝐼𝑧) ↔ 𝑢 ∈ (𝑌𝐼𝑍))) |
36 | 35 | 3anbi2d 1440 |
. . . . . . . 8
⊢ (𝑧 = 𝑍 → ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑧) ∧ 𝑋 ≠ 𝑢) ↔ (𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢))) |
37 | | eleq1 2828 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑍 → (𝑧 ∈ (𝑋𝐼𝑏) ↔ 𝑍 ∈ (𝑋𝐼𝑏))) |
38 | 37 | 3anbi2d 1440 |
. . . . . . . . 9
⊢ (𝑧 = 𝑍 → ((𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))) |
39 | 38 | 2rexbidv 3231 |
. . . . . . . 8
⊢ (𝑧 = 𝑍 → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))) |
40 | 36, 39 | imbi12d 345 |
. . . . . . 7
⊢ (𝑧 = 𝑍 → (((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))) |
41 | 40 | 2ralbidv 3125 |
. . . . . 6
⊢ (𝑧 = 𝑍 → (∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑧) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑧 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))) |
42 | 25, 33, 41 | rspc3v 3574 |
. . . . 5
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) → ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))) |
43 | 11, 12, 13, 42 | syl3anc 1370 |
. . . 4
⊢ (𝜑 → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑥𝐼𝑣) ∧ 𝑢 ∈ (𝑦𝐼𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑎) ∧ 𝑧 ∈ (𝑥𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) → ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))) |
44 | 10, 43 | mpd 15 |
. . 3
⊢ (𝜑 → ∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)))) |
45 | | axtgeucl.4 |
. . . 4
⊢ (𝜑 → 𝑈 ∈ 𝑃) |
46 | | axtgeucl.5 |
. . . 4
⊢ (𝜑 → 𝑉 ∈ 𝑃) |
47 | | eleq1 2828 |
. . . . . . 7
⊢ (𝑢 = 𝑈 → (𝑢 ∈ (𝑋𝐼𝑣) ↔ 𝑈 ∈ (𝑋𝐼𝑣))) |
48 | | eleq1 2828 |
. . . . . . 7
⊢ (𝑢 = 𝑈 → (𝑢 ∈ (𝑌𝐼𝑍) ↔ 𝑈 ∈ (𝑌𝐼𝑍))) |
49 | | neeq2 3009 |
. . . . . . 7
⊢ (𝑢 = 𝑈 → (𝑋 ≠ 𝑢 ↔ 𝑋 ≠ 𝑈)) |
50 | 47, 48, 49 | 3anbi123d 1435 |
. . . . . 6
⊢ (𝑢 = 𝑈 → ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) ↔ (𝑈 ∈ (𝑋𝐼𝑣) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈))) |
51 | 50 | imbi1d 342 |
. . . . 5
⊢ (𝑢 = 𝑈 → (((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ((𝑈 ∈ (𝑋𝐼𝑣) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))))) |
52 | | oveq2 7277 |
. . . . . . . 8
⊢ (𝑣 = 𝑉 → (𝑋𝐼𝑣) = (𝑋𝐼𝑉)) |
53 | 52 | eleq2d 2826 |
. . . . . . 7
⊢ (𝑣 = 𝑉 → (𝑈 ∈ (𝑋𝐼𝑣) ↔ 𝑈 ∈ (𝑋𝐼𝑉))) |
54 | 53 | 3anbi1d 1439 |
. . . . . 6
⊢ (𝑣 = 𝑉 → ((𝑈 ∈ (𝑋𝐼𝑣) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈) ↔ (𝑈 ∈ (𝑋𝐼𝑉) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈))) |
55 | | eleq1 2828 |
. . . . . . . 8
⊢ (𝑣 = 𝑉 → (𝑣 ∈ (𝑎𝐼𝑏) ↔ 𝑉 ∈ (𝑎𝐼𝑏))) |
56 | 55 | 3anbi3d 1441 |
. . . . . . 7
⊢ (𝑣 = 𝑉 → ((𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏)))) |
57 | 56 | 2rexbidv 3231 |
. . . . . 6
⊢ (𝑣 = 𝑉 → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏)) ↔ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏)))) |
58 | 54, 57 | imbi12d 345 |
. . . . 5
⊢ (𝑣 = 𝑉 → (((𝑈 ∈ (𝑋𝐼𝑣) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) ↔ ((𝑈 ∈ (𝑋𝐼𝑉) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏))))) |
59 | 51, 58 | rspc2v 3571 |
. . . 4
⊢ ((𝑈 ∈ 𝑃 ∧ 𝑉 ∈ 𝑃) → (∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) → ((𝑈 ∈ (𝑋𝐼𝑉) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏))))) |
60 | 45, 46, 59 | syl2anc 584 |
. . 3
⊢ (𝜑 → (∀𝑢 ∈ 𝑃 ∀𝑣 ∈ 𝑃 ((𝑢 ∈ (𝑋𝐼𝑣) ∧ 𝑢 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑢) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑣 ∈ (𝑎𝐼𝑏))) → ((𝑈 ∈ (𝑋𝐼𝑉) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏))))) |
61 | 44, 60 | mpd 15 |
. 2
⊢ (𝜑 → ((𝑈 ∈ (𝑋𝐼𝑉) ∧ 𝑈 ∈ (𝑌𝐼𝑍) ∧ 𝑋 ≠ 𝑈) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏)))) |
62 | 1, 2, 3, 61 | mp3and 1463 |
1
⊢ (𝜑 → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑎) ∧ 𝑍 ∈ (𝑋𝐼𝑏) ∧ 𝑉 ∈ (𝑎𝐼𝑏))) |