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

Theorem axtgupdim2OLD 31055
Description: Upper dimension axiom for dimension 2, Axiom A9 of [Schwabhauser] p. 13. (Contributed by Thierry Arnoux, 29-May-2019.) (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
istrkg2d.p 𝑃 = (Base‘𝐺)
istrkg2d.d = (dist‘𝐺)
istrkg2d.i 𝐼 = (Itv‘𝐺)
axtgupdim2OLD.x (𝜑𝑋𝑃)
axtgupdim2OLD.y (𝜑𝑌𝑃)
axtgupdim2OLD.z (𝜑𝑍𝑃)
axtgupdim2OLD.u (𝜑𝑈𝑃)
axtgupdim2OLD.v (𝜑𝑉𝑃)
axtgupdim2OLD.0 (𝜑𝑈𝑉)
axtgupdim2OLD.1 (𝜑 → (𝑋 𝑈) = (𝑋 𝑉))
axtgupdim2OLD.2 (𝜑 → (𝑌 𝑈) = (𝑌 𝑉))
axtgupdim2OLD.3 (𝜑 → (𝑍 𝑈) = (𝑍 𝑉))
axtgupdim2OLD.g (𝜑𝐺 ∈ TarskiG2D)
Assertion
Ref Expression
axtgupdim2OLD (𝜑 → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))

Proof of Theorem axtgupdim2OLD
Dummy variables 𝑢 𝑣 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 axtgupdim2OLD.1 . . 3 (𝜑 → (𝑋 𝑈) = (𝑋 𝑉))
2 axtgupdim2OLD.2 . . 3 (𝜑 → (𝑌 𝑈) = (𝑌 𝑉))
3 axtgupdim2OLD.3 . . 3 (𝜑 → (𝑍 𝑈) = (𝑍 𝑉))
41, 2, 33jca 1123 . 2 (𝜑 → ((𝑋 𝑈) = (𝑋 𝑉) ∧ (𝑌 𝑈) = (𝑌 𝑉) ∧ (𝑍 𝑈) = (𝑍 𝑉)))
5 axtgupdim2OLD.0 . 2 (𝜑𝑈𝑉)
6 axtgupdim2OLD.g . . . . . 6 (𝜑𝐺 ∈ TarskiG2D)
7 istrkg2d.p . . . . . . 7 𝑃 = (Base‘𝐺)
8 istrkg2d.d . . . . . . 7 = (dist‘𝐺)
9 istrkg2d.i . . . . . . 7 𝐼 = (Itv‘𝐺)
107, 8, 9istrkg2d 31053 . . . . . 6 (𝐺 ∈ TarskiG2D ↔ (𝐺 ∈ V ∧ (∃𝑥𝑃𝑦𝑃𝑧𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑣𝑃 ((((𝑥 𝑢) = (𝑥 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))))
116, 10sylib 208 . . . . 5 (𝜑 → (𝐺 ∈ V ∧ (∃𝑥𝑃𝑦𝑃𝑧𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑣𝑃 ((((𝑥 𝑢) = (𝑥 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))))
1211simprrd 814 . . . 4 (𝜑 → ∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑣𝑃 ((((𝑥 𝑢) = (𝑥 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))
13 axtgupdim2OLD.x . . . . 5 (𝜑𝑋𝑃)
14 axtgupdim2OLD.y . . . . 5 (𝜑𝑌𝑃)
15 axtgupdim2OLD.z . . . . 5 (𝜑𝑍𝑃)
16 oveq1 6820 . . . . . . . . . . 11 (𝑥 = 𝑋 → (𝑥 𝑢) = (𝑋 𝑢))
17 oveq1 6820 . . . . . . . . . . 11 (𝑥 = 𝑋 → (𝑥 𝑣) = (𝑋 𝑣))
1816, 17eqeq12d 2775 . . . . . . . . . 10 (𝑥 = 𝑋 → ((𝑥 𝑢) = (𝑥 𝑣) ↔ (𝑋 𝑢) = (𝑋 𝑣)))
19183anbi1d 1552 . . . . . . . . 9 (𝑥 = 𝑋 → (((𝑥 𝑢) = (𝑥 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ↔ ((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣))))
2019anbi1d 743 . . . . . . . 8 (𝑥 = 𝑋 → ((((𝑥 𝑢) = (𝑥 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) ↔ (((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣)))
21 oveq1 6820 . . . . . . . . . 10 (𝑥 = 𝑋 → (𝑥𝐼𝑦) = (𝑋𝐼𝑦))
2221eleq2d 2825 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑧 ∈ (𝑥𝐼𝑦) ↔ 𝑧 ∈ (𝑋𝐼𝑦)))
23 eleq1 2827 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑥 ∈ (𝑧𝐼𝑦) ↔ 𝑋 ∈ (𝑧𝐼𝑦)))
24 oveq1 6820 . . . . . . . . . 10 (𝑥 = 𝑋 → (𝑥𝐼𝑧) = (𝑋𝐼𝑧))
2524eleq2d 2825 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑋𝐼𝑧)))
2622, 23, 253orbi123d 1547 . . . . . . . 8 (𝑥 = 𝑋 → ((𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ (𝑧 ∈ (𝑋𝐼𝑦) ∨ 𝑋 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑋𝐼𝑧))))
2720, 26imbi12d 333 . . . . . . 7 (𝑥 = 𝑋 → (((((𝑥 𝑢) = (𝑥 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑋𝐼𝑦) ∨ 𝑋 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑋𝐼𝑧)))))
28272ralbidv 3127 . . . . . 6 (𝑥 = 𝑋 → (∀𝑢𝑃𝑣𝑃 ((((𝑥 𝑢) = (𝑥 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑋𝐼𝑦) ∨ 𝑋 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑋𝐼𝑧)))))
29 oveq1 6820 . . . . . . . . . . 11 (𝑦 = 𝑌 → (𝑦 𝑢) = (𝑌 𝑢))
30 oveq1 6820 . . . . . . . . . . 11 (𝑦 = 𝑌 → (𝑦 𝑣) = (𝑌 𝑣))
3129, 30eqeq12d 2775 . . . . . . . . . 10 (𝑦 = 𝑌 → ((𝑦 𝑢) = (𝑦 𝑣) ↔ (𝑌 𝑢) = (𝑌 𝑣)))
32313anbi2d 1553 . . . . . . . . 9 (𝑦 = 𝑌 → (((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ↔ ((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣))))
3332anbi1d 743 . . . . . . . 8 (𝑦 = 𝑌 → ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) ↔ (((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣)))
34 oveq2 6821 . . . . . . . . . 10 (𝑦 = 𝑌 → (𝑋𝐼𝑦) = (𝑋𝐼𝑌))
3534eleq2d 2825 . . . . . . . . 9 (𝑦 = 𝑌 → (𝑧 ∈ (𝑋𝐼𝑦) ↔ 𝑧 ∈ (𝑋𝐼𝑌)))
36 oveq2 6821 . . . . . . . . . 10 (𝑦 = 𝑌 → (𝑧𝐼𝑦) = (𝑧𝐼𝑌))
3736eleq2d 2825 . . . . . . . . 9 (𝑦 = 𝑌 → (𝑋 ∈ (𝑧𝐼𝑦) ↔ 𝑋 ∈ (𝑧𝐼𝑌)))
38 eleq1 2827 . . . . . . . . 9 (𝑦 = 𝑌 → (𝑦 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑧)))
3935, 37, 383orbi123d 1547 . . . . . . . 8 (𝑦 = 𝑌 → ((𝑧 ∈ (𝑋𝐼𝑦) ∨ 𝑋 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑋𝐼𝑧)) ↔ (𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧))))
4033, 39imbi12d 333 . . . . . . 7 (𝑦 = 𝑌 → (((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑋𝐼𝑦) ∨ 𝑋 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑋𝐼𝑧))) ↔ ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧)))))
41402ralbidv 3127 . . . . . 6 (𝑦 = 𝑌 → (∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑋𝐼𝑦) ∨ 𝑋 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑋𝐼𝑧))) ↔ ∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧)))))
42 oveq1 6820 . . . . . . . . . . 11 (𝑧 = 𝑍 → (𝑧 𝑢) = (𝑍 𝑢))
43 oveq1 6820 . . . . . . . . . . 11 (𝑧 = 𝑍 → (𝑧 𝑣) = (𝑍 𝑣))
4442, 43eqeq12d 2775 . . . . . . . . . 10 (𝑧 = 𝑍 → ((𝑧 𝑢) = (𝑧 𝑣) ↔ (𝑍 𝑢) = (𝑍 𝑣)))
45443anbi3d 1554 . . . . . . . . 9 (𝑧 = 𝑍 → (((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ↔ ((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣))))
4645anbi1d 743 . . . . . . . 8 (𝑧 = 𝑍 → ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) ↔ (((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣)))
47 eleq1 2827 . . . . . . . . 9 (𝑧 = 𝑍 → (𝑧 ∈ (𝑋𝐼𝑌) ↔ 𝑍 ∈ (𝑋𝐼𝑌)))
48 oveq1 6820 . . . . . . . . . 10 (𝑧 = 𝑍 → (𝑧𝐼𝑌) = (𝑍𝐼𝑌))
4948eleq2d 2825 . . . . . . . . 9 (𝑧 = 𝑍 → (𝑋 ∈ (𝑧𝐼𝑌) ↔ 𝑋 ∈ (𝑍𝐼𝑌)))
50 oveq2 6821 . . . . . . . . . 10 (𝑧 = 𝑍 → (𝑋𝐼𝑧) = (𝑋𝐼𝑍))
5150eleq2d 2825 . . . . . . . . 9 (𝑧 = 𝑍 → (𝑌 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑍)))
5247, 49, 513orbi123d 1547 . . . . . . . 8 (𝑧 = 𝑍 → ((𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧)) ↔ (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))))
5346, 52imbi12d 333 . . . . . . 7 (𝑧 = 𝑍 → (((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧))) ↔ ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))))
54532ralbidv 3127 . . . . . 6 (𝑧 = 𝑍 → (∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧))) ↔ ∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))))
5528, 41, 54rspc3v 3464 . . . . 5 ((𝑋𝑃𝑌𝑃𝑍𝑃) → (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑣𝑃 ((((𝑥 𝑢) = (𝑥 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) → ∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))))
5613, 14, 15, 55syl3anc 1477 . . . 4 (𝜑 → (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑣𝑃 ((((𝑥 𝑢) = (𝑥 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) → ∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))))
5712, 56mpd 15 . . 3 (𝜑 → ∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))))
58 axtgupdim2OLD.u . . . 4 (𝜑𝑈𝑃)
59 axtgupdim2OLD.v . . . 4 (𝜑𝑉𝑃)
60 oveq2 6821 . . . . . . . . 9 (𝑢 = 𝑈 → (𝑋 𝑢) = (𝑋 𝑈))
6160eqeq1d 2762 . . . . . . . 8 (𝑢 = 𝑈 → ((𝑋 𝑢) = (𝑋 𝑣) ↔ (𝑋 𝑈) = (𝑋 𝑣)))
62 oveq2 6821 . . . . . . . . 9 (𝑢 = 𝑈 → (𝑌 𝑢) = (𝑌 𝑈))
6362eqeq1d 2762 . . . . . . . 8 (𝑢 = 𝑈 → ((𝑌 𝑢) = (𝑌 𝑣) ↔ (𝑌 𝑈) = (𝑌 𝑣)))
64 oveq2 6821 . . . . . . . . 9 (𝑢 = 𝑈 → (𝑍 𝑢) = (𝑍 𝑈))
6564eqeq1d 2762 . . . . . . . 8 (𝑢 = 𝑈 → ((𝑍 𝑢) = (𝑍 𝑣) ↔ (𝑍 𝑈) = (𝑍 𝑣)))
6661, 63, 653anbi123d 1548 . . . . . . 7 (𝑢 = 𝑈 → (((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ↔ ((𝑋 𝑈) = (𝑋 𝑣) ∧ (𝑌 𝑈) = (𝑌 𝑣) ∧ (𝑍 𝑈) = (𝑍 𝑣))))
67 neeq1 2994 . . . . . . 7 (𝑢 = 𝑈 → (𝑢𝑣𝑈𝑣))
6866, 67anbi12d 749 . . . . . 6 (𝑢 = 𝑈 → ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣) ↔ (((𝑋 𝑈) = (𝑋 𝑣) ∧ (𝑌 𝑈) = (𝑌 𝑣) ∧ (𝑍 𝑈) = (𝑍 𝑣)) ∧ 𝑈𝑣)))
6968imbi1d 330 . . . . 5 (𝑢 = 𝑈 → (((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))) ↔ ((((𝑋 𝑈) = (𝑋 𝑣) ∧ (𝑌 𝑈) = (𝑌 𝑣) ∧ (𝑍 𝑈) = (𝑍 𝑣)) ∧ 𝑈𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))))
70 oveq2 6821 . . . . . . . . 9 (𝑣 = 𝑉 → (𝑋 𝑣) = (𝑋 𝑉))
7170eqeq2d 2770 . . . . . . . 8 (𝑣 = 𝑉 → ((𝑋 𝑈) = (𝑋 𝑣) ↔ (𝑋 𝑈) = (𝑋 𝑉)))
72 oveq2 6821 . . . . . . . . 9 (𝑣 = 𝑉 → (𝑌 𝑣) = (𝑌 𝑉))
7372eqeq2d 2770 . . . . . . . 8 (𝑣 = 𝑉 → ((𝑌 𝑈) = (𝑌 𝑣) ↔ (𝑌 𝑈) = (𝑌 𝑉)))
74 oveq2 6821 . . . . . . . . 9 (𝑣 = 𝑉 → (𝑍 𝑣) = (𝑍 𝑉))
7574eqeq2d 2770 . . . . . . . 8 (𝑣 = 𝑉 → ((𝑍 𝑈) = (𝑍 𝑣) ↔ (𝑍 𝑈) = (𝑍 𝑉)))
7671, 73, 753anbi123d 1548 . . . . . . 7 (𝑣 = 𝑉 → (((𝑋 𝑈) = (𝑋 𝑣) ∧ (𝑌 𝑈) = (𝑌 𝑣) ∧ (𝑍 𝑈) = (𝑍 𝑣)) ↔ ((𝑋 𝑈) = (𝑋 𝑉) ∧ (𝑌 𝑈) = (𝑌 𝑉) ∧ (𝑍 𝑈) = (𝑍 𝑉))))
77 neeq2 2995 . . . . . . 7 (𝑣 = 𝑉 → (𝑈𝑣𝑈𝑉))
7876, 77anbi12d 749 . . . . . 6 (𝑣 = 𝑉 → ((((𝑋 𝑈) = (𝑋 𝑣) ∧ (𝑌 𝑈) = (𝑌 𝑣) ∧ (𝑍 𝑈) = (𝑍 𝑣)) ∧ 𝑈𝑣) ↔ (((𝑋 𝑈) = (𝑋 𝑉) ∧ (𝑌 𝑈) = (𝑌 𝑉) ∧ (𝑍 𝑈) = (𝑍 𝑉)) ∧ 𝑈𝑉)))
7978imbi1d 330 . . . . 5 (𝑣 = 𝑉 → (((((𝑋 𝑈) = (𝑋 𝑣) ∧ (𝑌 𝑈) = (𝑌 𝑣) ∧ (𝑍 𝑈) = (𝑍 𝑣)) ∧ 𝑈𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))) ↔ ((((𝑋 𝑈) = (𝑋 𝑉) ∧ (𝑌 𝑈) = (𝑌 𝑉) ∧ (𝑍 𝑈) = (𝑍 𝑉)) ∧ 𝑈𝑉) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))))
8069, 79rspc2v 3461 . . . 4 ((𝑈𝑃𝑉𝑃) → (∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))) → ((((𝑋 𝑈) = (𝑋 𝑉) ∧ (𝑌 𝑈) = (𝑌 𝑉) ∧ (𝑍 𝑈) = (𝑍 𝑉)) ∧ 𝑈𝑉) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))))
8158, 59, 80syl2anc 696 . . 3 (𝜑 → (∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))) → ((((𝑋 𝑈) = (𝑋 𝑉) ∧ (𝑌 𝑈) = (𝑌 𝑉) ∧ (𝑍 𝑈) = (𝑍 𝑉)) ∧ 𝑈𝑉) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))))
8257, 81mpd 15 . 2 (𝜑 → ((((𝑋 𝑈) = (𝑋 𝑉) ∧ (𝑌 𝑈) = (𝑌 𝑉) ∧ (𝑍 𝑈) = (𝑍 𝑉)) ∧ 𝑈𝑉) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))))
834, 5, 82mp2and 717 1 (𝜑 → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383  w3o 1071  w3a 1072   = wceq 1632  wcel 2139  wne 2932  wral 3050  wrex 3051  Vcvv 3340  cfv 6049  (class class class)co 6813  Basecbs 16059  distcds 16152  Itvcitv 25534  TarskiG2Dcstrkg2d 31051
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-nul 4941
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-ov 6816  df-trkg2d 31052
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator