Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  axtgupdim2ALTV Structured version   Visualization version   GIF version

Theorem axtgupdim2ALTV 33281
Description: Alternate version of axtgupdim2 27413. (Contributed by Thierry Arnoux, 29-May-2019.) (New usage is discouraged.)
Hypotheses
Ref Expression
istrkg2d.p 𝑃 = (Base‘𝐺)
istrkg2d.d = (dist‘𝐺)
istrkg2d.i 𝐼 = (Itv‘𝐺)
axtgupdim2ALTV.x (𝜑𝑋𝑃)
axtgupdim2ALTV.y (𝜑𝑌𝑃)
axtgupdim2ALTV.z (𝜑𝑍𝑃)
axtgupdim2ALTV.u (𝜑𝑈𝑃)
axtgupdim2ALTV.v (𝜑𝑉𝑃)
axtgupdim2ALTV.0 (𝜑𝑈𝑉)
axtgupdim2ALTV.1 (𝜑 → (𝑋 𝑈) = (𝑋 𝑉))
axtgupdim2ALTV.2 (𝜑 → (𝑌 𝑈) = (𝑌 𝑉))
axtgupdim2ALTV.3 (𝜑 → (𝑍 𝑈) = (𝑍 𝑉))
axtgupdim2ALTV.g (𝜑𝐺 ∈ TarskiG2D)
Assertion
Ref Expression
axtgupdim2ALTV (𝜑 → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))

Proof of Theorem axtgupdim2ALTV
Dummy variables 𝑢 𝑣 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 axtgupdim2ALTV.1 . . 3 (𝜑 → (𝑋 𝑈) = (𝑋 𝑉))
2 axtgupdim2ALTV.2 . . 3 (𝜑 → (𝑌 𝑈) = (𝑌 𝑉))
3 axtgupdim2ALTV.3 . . 3 (𝜑 → (𝑍 𝑈) = (𝑍 𝑉))
41, 2, 33jca 1128 . 2 (𝜑 → ((𝑋 𝑈) = (𝑋 𝑉) ∧ (𝑌 𝑈) = (𝑌 𝑉) ∧ (𝑍 𝑈) = (𝑍 𝑉)))
5 axtgupdim2ALTV.0 . 2 (𝜑𝑈𝑉)
6 axtgupdim2ALTV.g . . . . . 6 (𝜑𝐺 ∈ TarskiG2D)
7 istrkg2d.p . . . . . . 7 𝑃 = (Base‘𝐺)
8 istrkg2d.d . . . . . . 7 = (dist‘𝐺)
9 istrkg2d.i . . . . . . 7 𝐼 = (Itv‘𝐺)
107, 8, 9istrkg2d 33279 . . . . . 6 (𝐺 ∈ TarskiG2D ↔ (𝐺 ∈ V ∧ (∃𝑥𝑃𝑦𝑃𝑧𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑣𝑃 ((((𝑥 𝑢) = (𝑥 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))))
116, 10sylib 217 . . . . 5 (𝜑 → (𝐺 ∈ V ∧ (∃𝑥𝑃𝑦𝑃𝑧𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑣𝑃 ((((𝑥 𝑢) = (𝑥 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))))
1211simprrd 772 . . . 4 (𝜑 → ∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑣𝑃 ((((𝑥 𝑢) = (𝑥 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))
13 axtgupdim2ALTV.x . . . . 5 (𝜑𝑋𝑃)
14 axtgupdim2ALTV.y . . . . 5 (𝜑𝑌𝑃)
15 axtgupdim2ALTV.z . . . . 5 (𝜑𝑍𝑃)
16 oveq1 7364 . . . . . . . . . . 11 (𝑥 = 𝑋 → (𝑥 𝑢) = (𝑋 𝑢))
17 oveq1 7364 . . . . . . . . . . 11 (𝑥 = 𝑋 → (𝑥 𝑣) = (𝑋 𝑣))
1816, 17eqeq12d 2752 . . . . . . . . . 10 (𝑥 = 𝑋 → ((𝑥 𝑢) = (𝑥 𝑣) ↔ (𝑋 𝑢) = (𝑋 𝑣)))
19183anbi1d 1440 . . . . . . . . 9 (𝑥 = 𝑋 → (((𝑥 𝑢) = (𝑥 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ↔ ((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣))))
2019anbi1d 630 . . . . . . . 8 (𝑥 = 𝑋 → ((((𝑥 𝑢) = (𝑥 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) ↔ (((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣)))
21 oveq1 7364 . . . . . . . . . 10 (𝑥 = 𝑋 → (𝑥𝐼𝑦) = (𝑋𝐼𝑦))
2221eleq2d 2823 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑧 ∈ (𝑥𝐼𝑦) ↔ 𝑧 ∈ (𝑋𝐼𝑦)))
23 eleq1 2825 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑥 ∈ (𝑧𝐼𝑦) ↔ 𝑋 ∈ (𝑧𝐼𝑦)))
24 oveq1 7364 . . . . . . . . . 10 (𝑥 = 𝑋 → (𝑥𝐼𝑧) = (𝑋𝐼𝑧))
2524eleq2d 2823 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑋𝐼𝑧)))
2622, 23, 253orbi123d 1435 . . . . . . . 8 (𝑥 = 𝑋 → ((𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ (𝑧 ∈ (𝑋𝐼𝑦) ∨ 𝑋 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑋𝐼𝑧))))
2720, 26imbi12d 344 . . . . . . 7 (𝑥 = 𝑋 → (((((𝑥 𝑢) = (𝑥 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑋𝐼𝑦) ∨ 𝑋 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑋𝐼𝑧)))))
28272ralbidv 3212 . . . . . 6 (𝑥 = 𝑋 → (∀𝑢𝑃𝑣𝑃 ((((𝑥 𝑢) = (𝑥 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑋𝐼𝑦) ∨ 𝑋 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑋𝐼𝑧)))))
29 oveq1 7364 . . . . . . . . . . 11 (𝑦 = 𝑌 → (𝑦 𝑢) = (𝑌 𝑢))
30 oveq1 7364 . . . . . . . . . . 11 (𝑦 = 𝑌 → (𝑦 𝑣) = (𝑌 𝑣))
3129, 30eqeq12d 2752 . . . . . . . . . 10 (𝑦 = 𝑌 → ((𝑦 𝑢) = (𝑦 𝑣) ↔ (𝑌 𝑢) = (𝑌 𝑣)))
32313anbi2d 1441 . . . . . . . . 9 (𝑦 = 𝑌 → (((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ↔ ((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣))))
3332anbi1d 630 . . . . . . . 8 (𝑦 = 𝑌 → ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) ↔ (((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣)))
34 oveq2 7365 . . . . . . . . . 10 (𝑦 = 𝑌 → (𝑋𝐼𝑦) = (𝑋𝐼𝑌))
3534eleq2d 2823 . . . . . . . . 9 (𝑦 = 𝑌 → (𝑧 ∈ (𝑋𝐼𝑦) ↔ 𝑧 ∈ (𝑋𝐼𝑌)))
36 oveq2 7365 . . . . . . . . . 10 (𝑦 = 𝑌 → (𝑧𝐼𝑦) = (𝑧𝐼𝑌))
3736eleq2d 2823 . . . . . . . . 9 (𝑦 = 𝑌 → (𝑋 ∈ (𝑧𝐼𝑦) ↔ 𝑋 ∈ (𝑧𝐼𝑌)))
38 eleq1 2825 . . . . . . . . 9 (𝑦 = 𝑌 → (𝑦 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑧)))
3935, 37, 383orbi123d 1435 . . . . . . . 8 (𝑦 = 𝑌 → ((𝑧 ∈ (𝑋𝐼𝑦) ∨ 𝑋 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑋𝐼𝑧)) ↔ (𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧))))
4033, 39imbi12d 344 . . . . . . 7 (𝑦 = 𝑌 → (((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑋𝐼𝑦) ∨ 𝑋 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑋𝐼𝑧))) ↔ ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧)))))
41402ralbidv 3212 . . . . . 6 (𝑦 = 𝑌 → (∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑋𝐼𝑦) ∨ 𝑋 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑋𝐼𝑧))) ↔ ∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧)))))
42 oveq1 7364 . . . . . . . . . . 11 (𝑧 = 𝑍 → (𝑧 𝑢) = (𝑍 𝑢))
43 oveq1 7364 . . . . . . . . . . 11 (𝑧 = 𝑍 → (𝑧 𝑣) = (𝑍 𝑣))
4442, 43eqeq12d 2752 . . . . . . . . . 10 (𝑧 = 𝑍 → ((𝑧 𝑢) = (𝑧 𝑣) ↔ (𝑍 𝑢) = (𝑍 𝑣)))
45443anbi3d 1442 . . . . . . . . 9 (𝑧 = 𝑍 → (((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ↔ ((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣))))
4645anbi1d 630 . . . . . . . 8 (𝑧 = 𝑍 → ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) ↔ (((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣)))
47 eleq1 2825 . . . . . . . . 9 (𝑧 = 𝑍 → (𝑧 ∈ (𝑋𝐼𝑌) ↔ 𝑍 ∈ (𝑋𝐼𝑌)))
48 oveq1 7364 . . . . . . . . . 10 (𝑧 = 𝑍 → (𝑧𝐼𝑌) = (𝑍𝐼𝑌))
4948eleq2d 2823 . . . . . . . . 9 (𝑧 = 𝑍 → (𝑋 ∈ (𝑧𝐼𝑌) ↔ 𝑋 ∈ (𝑍𝐼𝑌)))
50 oveq2 7365 . . . . . . . . . 10 (𝑧 = 𝑍 → (𝑋𝐼𝑧) = (𝑋𝐼𝑍))
5150eleq2d 2823 . . . . . . . . 9 (𝑧 = 𝑍 → (𝑌 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑍)))
5247, 49, 513orbi123d 1435 . . . . . . . 8 (𝑧 = 𝑍 → ((𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧)) ↔ (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))))
5346, 52imbi12d 344 . . . . . . 7 (𝑧 = 𝑍 → (((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧))) ↔ ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))))
54532ralbidv 3212 . . . . . 6 (𝑧 = 𝑍 → (∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧))) ↔ ∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))))
5528, 41, 54rspc3v 3593 . . . . 5 ((𝑋𝑃𝑌𝑃𝑍𝑃) → (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑣𝑃 ((((𝑥 𝑢) = (𝑥 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) → ∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))))
5613, 14, 15, 55syl3anc 1371 . . . 4 (𝜑 → (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑣𝑃 ((((𝑥 𝑢) = (𝑥 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) → ∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))))
5712, 56mpd 15 . . 3 (𝜑 → ∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))))
58 axtgupdim2ALTV.u . . . 4 (𝜑𝑈𝑃)
59 axtgupdim2ALTV.v . . . 4 (𝜑𝑉𝑃)
60 oveq2 7365 . . . . . . . . 9 (𝑢 = 𝑈 → (𝑋 𝑢) = (𝑋 𝑈))
6160eqeq1d 2738 . . . . . . . 8 (𝑢 = 𝑈 → ((𝑋 𝑢) = (𝑋 𝑣) ↔ (𝑋 𝑈) = (𝑋 𝑣)))
62 oveq2 7365 . . . . . . . . 9 (𝑢 = 𝑈 → (𝑌 𝑢) = (𝑌 𝑈))
6362eqeq1d 2738 . . . . . . . 8 (𝑢 = 𝑈 → ((𝑌 𝑢) = (𝑌 𝑣) ↔ (𝑌 𝑈) = (𝑌 𝑣)))
64 oveq2 7365 . . . . . . . . 9 (𝑢 = 𝑈 → (𝑍 𝑢) = (𝑍 𝑈))
6564eqeq1d 2738 . . . . . . . 8 (𝑢 = 𝑈 → ((𝑍 𝑢) = (𝑍 𝑣) ↔ (𝑍 𝑈) = (𝑍 𝑣)))
6661, 63, 653anbi123d 1436 . . . . . . 7 (𝑢 = 𝑈 → (((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ↔ ((𝑋 𝑈) = (𝑋 𝑣) ∧ (𝑌 𝑈) = (𝑌 𝑣) ∧ (𝑍 𝑈) = (𝑍 𝑣))))
67 neeq1 3006 . . . . . . 7 (𝑢 = 𝑈 → (𝑢𝑣𝑈𝑣))
6866, 67anbi12d 631 . . . . . 6 (𝑢 = 𝑈 → ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣) ↔ (((𝑋 𝑈) = (𝑋 𝑣) ∧ (𝑌 𝑈) = (𝑌 𝑣) ∧ (𝑍 𝑈) = (𝑍 𝑣)) ∧ 𝑈𝑣)))
6968imbi1d 341 . . . . 5 (𝑢 = 𝑈 → (((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))) ↔ ((((𝑋 𝑈) = (𝑋 𝑣) ∧ (𝑌 𝑈) = (𝑌 𝑣) ∧ (𝑍 𝑈) = (𝑍 𝑣)) ∧ 𝑈𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))))
70 oveq2 7365 . . . . . . . . 9 (𝑣 = 𝑉 → (𝑋 𝑣) = (𝑋 𝑉))
7170eqeq2d 2747 . . . . . . . 8 (𝑣 = 𝑉 → ((𝑋 𝑈) = (𝑋 𝑣) ↔ (𝑋 𝑈) = (𝑋 𝑉)))
72 oveq2 7365 . . . . . . . . 9 (𝑣 = 𝑉 → (𝑌 𝑣) = (𝑌 𝑉))
7372eqeq2d 2747 . . . . . . . 8 (𝑣 = 𝑉 → ((𝑌 𝑈) = (𝑌 𝑣) ↔ (𝑌 𝑈) = (𝑌 𝑉)))
74 oveq2 7365 . . . . . . . . 9 (𝑣 = 𝑉 → (𝑍 𝑣) = (𝑍 𝑉))
7574eqeq2d 2747 . . . . . . . 8 (𝑣 = 𝑉 → ((𝑍 𝑈) = (𝑍 𝑣) ↔ (𝑍 𝑈) = (𝑍 𝑉)))
7671, 73, 753anbi123d 1436 . . . . . . 7 (𝑣 = 𝑉 → (((𝑋 𝑈) = (𝑋 𝑣) ∧ (𝑌 𝑈) = (𝑌 𝑣) ∧ (𝑍 𝑈) = (𝑍 𝑣)) ↔ ((𝑋 𝑈) = (𝑋 𝑉) ∧ (𝑌 𝑈) = (𝑌 𝑉) ∧ (𝑍 𝑈) = (𝑍 𝑉))))
77 neeq2 3007 . . . . . . 7 (𝑣 = 𝑉 → (𝑈𝑣𝑈𝑉))
7876, 77anbi12d 631 . . . . . 6 (𝑣 = 𝑉 → ((((𝑋 𝑈) = (𝑋 𝑣) ∧ (𝑌 𝑈) = (𝑌 𝑣) ∧ (𝑍 𝑈) = (𝑍 𝑣)) ∧ 𝑈𝑣) ↔ (((𝑋 𝑈) = (𝑋 𝑉) ∧ (𝑌 𝑈) = (𝑌 𝑉) ∧ (𝑍 𝑈) = (𝑍 𝑉)) ∧ 𝑈𝑉)))
7978imbi1d 341 . . . . 5 (𝑣 = 𝑉 → (((((𝑋 𝑈) = (𝑋 𝑣) ∧ (𝑌 𝑈) = (𝑌 𝑣) ∧ (𝑍 𝑈) = (𝑍 𝑣)) ∧ 𝑈𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))) ↔ ((((𝑋 𝑈) = (𝑋 𝑉) ∧ (𝑌 𝑈) = (𝑌 𝑉) ∧ (𝑍 𝑈) = (𝑍 𝑉)) ∧ 𝑈𝑉) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))))
8069, 79rspc2v 3590 . . . 4 ((𝑈𝑃𝑉𝑃) → (∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))) → ((((𝑋 𝑈) = (𝑋 𝑉) ∧ (𝑌 𝑈) = (𝑌 𝑉) ∧ (𝑍 𝑈) = (𝑍 𝑉)) ∧ 𝑈𝑉) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))))
8158, 59, 80syl2anc 584 . . 3 (𝜑 → (∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))) → ((((𝑋 𝑈) = (𝑋 𝑉) ∧ (𝑌 𝑈) = (𝑌 𝑉) ∧ (𝑍 𝑈) = (𝑍 𝑉)) ∧ 𝑈𝑉) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))))
8257, 81mpd 15 . 2 (𝜑 → ((((𝑋 𝑈) = (𝑋 𝑉) ∧ (𝑌 𝑈) = (𝑌 𝑉) ∧ (𝑍 𝑈) = (𝑍 𝑉)) ∧ 𝑈𝑉) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))))
834, 5, 82mp2and 697 1 (𝜑 → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  w3o 1086  w3a 1087   = wceq 1541  wcel 2106  wne 2943  wral 3064  wrex 3073  Vcvv 3445  cfv 6496  (class class class)co 7357  Basecbs 17083  distcds 17142  Itvcitv 27375  TarskiG2Dcstrkg2d 33277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-nul 5263
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-iota 6448  df-fv 6504  df-ov 7360  df-trkg2d 33278
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator