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 30506
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 1240 . 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 30504 . . . . . 6 (𝐺 ∈ TarskiG2D ↔ (𝐺 ∈ V ∧ (∃𝑥𝑃𝑦𝑃𝑧𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑣𝑃 ((((𝑥 𝑢) = (𝑥 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))))
116, 10sylib 208 . . . . 5 (𝜑 → (𝐺 ∈ V ∧ (∃𝑥𝑃𝑦𝑃𝑧𝑃 ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ∧ ∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑣𝑃 ((((𝑥 𝑢) = (𝑥 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))))
1211simprrd 796 . . . 4 (𝜑 → ∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑣𝑃 ((((𝑥 𝑢) = (𝑥 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))
13 axtgupdim2OLD.x . . . . 5 (𝜑𝑋𝑃)
14 axtgupdim2OLD.y . . . . 5 (𝜑𝑌𝑃)
15 axtgupdim2OLD.z . . . . 5 (𝜑𝑍𝑃)
16 oveq1 6622 . . . . . . . . . . 11 (𝑥 = 𝑋 → (𝑥 𝑢) = (𝑋 𝑢))
17 oveq1 6622 . . . . . . . . . . 11 (𝑥 = 𝑋 → (𝑥 𝑣) = (𝑋 𝑣))
1816, 17eqeq12d 2636 . . . . . . . . . 10 (𝑥 = 𝑋 → ((𝑥 𝑢) = (𝑥 𝑣) ↔ (𝑋 𝑢) = (𝑋 𝑣)))
19183anbi1d 1400 . . . . . . . . 9 (𝑥 = 𝑋 → (((𝑥 𝑢) = (𝑥 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ↔ ((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣))))
2019anbi1d 740 . . . . . . . 8 (𝑥 = 𝑋 → ((((𝑥 𝑢) = (𝑥 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) ↔ (((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣)))
21 oveq1 6622 . . . . . . . . . 10 (𝑥 = 𝑋 → (𝑥𝐼𝑦) = (𝑋𝐼𝑦))
2221eleq2d 2684 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑧 ∈ (𝑥𝐼𝑦) ↔ 𝑧 ∈ (𝑋𝐼𝑦)))
23 eleq1 2686 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑥 ∈ (𝑧𝐼𝑦) ↔ 𝑋 ∈ (𝑧𝐼𝑦)))
24 oveq1 6622 . . . . . . . . . 10 (𝑥 = 𝑋 → (𝑥𝐼𝑧) = (𝑋𝐼𝑧))
2524eleq2d 2684 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑋𝐼𝑧)))
2622, 23, 253orbi123d 1395 . . . . . . . 8 (𝑥 = 𝑋 → ((𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ (𝑧 ∈ (𝑋𝐼𝑦) ∨ 𝑋 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑋𝐼𝑧))))
2720, 26imbi12d 334 . . . . . . 7 (𝑥 = 𝑋 → (((((𝑥 𝑢) = (𝑥 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑋𝐼𝑦) ∨ 𝑋 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑋𝐼𝑧)))))
28272ralbidv 2985 . . . . . 6 (𝑥 = 𝑋 → (∀𝑢𝑃𝑣𝑃 ((((𝑥 𝑢) = (𝑥 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑋𝐼𝑦) ∨ 𝑋 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑋𝐼𝑧)))))
29 oveq1 6622 . . . . . . . . . . 11 (𝑦 = 𝑌 → (𝑦 𝑢) = (𝑌 𝑢))
30 oveq1 6622 . . . . . . . . . . 11 (𝑦 = 𝑌 → (𝑦 𝑣) = (𝑌 𝑣))
3129, 30eqeq12d 2636 . . . . . . . . . 10 (𝑦 = 𝑌 → ((𝑦 𝑢) = (𝑦 𝑣) ↔ (𝑌 𝑢) = (𝑌 𝑣)))
32313anbi2d 1401 . . . . . . . . 9 (𝑦 = 𝑌 → (((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ↔ ((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣))))
3332anbi1d 740 . . . . . . . 8 (𝑦 = 𝑌 → ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) ↔ (((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣)))
34 oveq2 6623 . . . . . . . . . 10 (𝑦 = 𝑌 → (𝑋𝐼𝑦) = (𝑋𝐼𝑌))
3534eleq2d 2684 . . . . . . . . 9 (𝑦 = 𝑌 → (𝑧 ∈ (𝑋𝐼𝑦) ↔ 𝑧 ∈ (𝑋𝐼𝑌)))
36 oveq2 6623 . . . . . . . . . 10 (𝑦 = 𝑌 → (𝑧𝐼𝑦) = (𝑧𝐼𝑌))
3736eleq2d 2684 . . . . . . . . 9 (𝑦 = 𝑌 → (𝑋 ∈ (𝑧𝐼𝑦) ↔ 𝑋 ∈ (𝑧𝐼𝑌)))
38 eleq1 2686 . . . . . . . . 9 (𝑦 = 𝑌 → (𝑦 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑧)))
3935, 37, 383orbi123d 1395 . . . . . . . 8 (𝑦 = 𝑌 → ((𝑧 ∈ (𝑋𝐼𝑦) ∨ 𝑋 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑋𝐼𝑧)) ↔ (𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧))))
4033, 39imbi12d 334 . . . . . . 7 (𝑦 = 𝑌 → (((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑋𝐼𝑦) ∨ 𝑋 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑋𝐼𝑧))) ↔ ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧)))))
41402ralbidv 2985 . . . . . 6 (𝑦 = 𝑌 → (∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑋𝐼𝑦) ∨ 𝑋 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑋𝐼𝑧))) ↔ ∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧)))))
42 oveq1 6622 . . . . . . . . . . 11 (𝑧 = 𝑍 → (𝑧 𝑢) = (𝑍 𝑢))
43 oveq1 6622 . . . . . . . . . . 11 (𝑧 = 𝑍 → (𝑧 𝑣) = (𝑍 𝑣))
4442, 43eqeq12d 2636 . . . . . . . . . 10 (𝑧 = 𝑍 → ((𝑧 𝑢) = (𝑧 𝑣) ↔ (𝑍 𝑢) = (𝑍 𝑣)))
45443anbi3d 1402 . . . . . . . . 9 (𝑧 = 𝑍 → (((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ↔ ((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣))))
4645anbi1d 740 . . . . . . . 8 (𝑧 = 𝑍 → ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) ↔ (((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣)))
47 eleq1 2686 . . . . . . . . 9 (𝑧 = 𝑍 → (𝑧 ∈ (𝑋𝐼𝑌) ↔ 𝑍 ∈ (𝑋𝐼𝑌)))
48 oveq1 6622 . . . . . . . . . 10 (𝑧 = 𝑍 → (𝑧𝐼𝑌) = (𝑍𝐼𝑌))
4948eleq2d 2684 . . . . . . . . 9 (𝑧 = 𝑍 → (𝑋 ∈ (𝑧𝐼𝑌) ↔ 𝑋 ∈ (𝑍𝐼𝑌)))
50 oveq2 6623 . . . . . . . . . 10 (𝑧 = 𝑍 → (𝑋𝐼𝑧) = (𝑋𝐼𝑍))
5150eleq2d 2684 . . . . . . . . 9 (𝑧 = 𝑍 → (𝑌 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑍)))
5247, 49, 513orbi123d 1395 . . . . . . . 8 (𝑧 = 𝑍 → ((𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧)) ↔ (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))))
5346, 52imbi12d 334 . . . . . . 7 (𝑧 = 𝑍 → (((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧))) ↔ ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))))
54532ralbidv 2985 . . . . . 6 (𝑧 = 𝑍 → (∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧))) ↔ ∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))))
5528, 41, 54rspc3v 3314 . . . . 5 ((𝑋𝑃𝑌𝑃𝑍𝑃) → (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑣𝑃 ((((𝑥 𝑢) = (𝑥 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) → ∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))))
5613, 14, 15, 55syl3anc 1323 . . . 4 (𝜑 → (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑣𝑃 ((((𝑥 𝑢) = (𝑥 𝑣) ∧ (𝑦 𝑢) = (𝑦 𝑣) ∧ (𝑧 𝑢) = (𝑧 𝑣)) ∧ 𝑢𝑣) → (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) → ∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))))
5712, 56mpd 15 . . 3 (𝜑 → ∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))))
58 axtgupdim2OLD.u . . . 4 (𝜑𝑈𝑃)
59 axtgupdim2OLD.v . . . 4 (𝜑𝑉𝑃)
60 oveq2 6623 . . . . . . . . 9 (𝑢 = 𝑈 → (𝑋 𝑢) = (𝑋 𝑈))
6160eqeq1d 2623 . . . . . . . 8 (𝑢 = 𝑈 → ((𝑋 𝑢) = (𝑋 𝑣) ↔ (𝑋 𝑈) = (𝑋 𝑣)))
62 oveq2 6623 . . . . . . . . 9 (𝑢 = 𝑈 → (𝑌 𝑢) = (𝑌 𝑈))
6362eqeq1d 2623 . . . . . . . 8 (𝑢 = 𝑈 → ((𝑌 𝑢) = (𝑌 𝑣) ↔ (𝑌 𝑈) = (𝑌 𝑣)))
64 oveq2 6623 . . . . . . . . 9 (𝑢 = 𝑈 → (𝑍 𝑢) = (𝑍 𝑈))
6564eqeq1d 2623 . . . . . . . 8 (𝑢 = 𝑈 → ((𝑍 𝑢) = (𝑍 𝑣) ↔ (𝑍 𝑈) = (𝑍 𝑣)))
6661, 63, 653anbi123d 1396 . . . . . . 7 (𝑢 = 𝑈 → (((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ↔ ((𝑋 𝑈) = (𝑋 𝑣) ∧ (𝑌 𝑈) = (𝑌 𝑣) ∧ (𝑍 𝑈) = (𝑍 𝑣))))
67 neeq1 2852 . . . . . . 7 (𝑢 = 𝑈 → (𝑢𝑣𝑈𝑣))
6866, 67anbi12d 746 . . . . . 6 (𝑢 = 𝑈 → ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣) ↔ (((𝑋 𝑈) = (𝑋 𝑣) ∧ (𝑌 𝑈) = (𝑌 𝑣) ∧ (𝑍 𝑈) = (𝑍 𝑣)) ∧ 𝑈𝑣)))
6968imbi1d 331 . . . . 5 (𝑢 = 𝑈 → (((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))) ↔ ((((𝑋 𝑈) = (𝑋 𝑣) ∧ (𝑌 𝑈) = (𝑌 𝑣) ∧ (𝑍 𝑈) = (𝑍 𝑣)) ∧ 𝑈𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))))
70 oveq2 6623 . . . . . . . . 9 (𝑣 = 𝑉 → (𝑋 𝑣) = (𝑋 𝑉))
7170eqeq2d 2631 . . . . . . . 8 (𝑣 = 𝑉 → ((𝑋 𝑈) = (𝑋 𝑣) ↔ (𝑋 𝑈) = (𝑋 𝑉)))
72 oveq2 6623 . . . . . . . . 9 (𝑣 = 𝑉 → (𝑌 𝑣) = (𝑌 𝑉))
7372eqeq2d 2631 . . . . . . . 8 (𝑣 = 𝑉 → ((𝑌 𝑈) = (𝑌 𝑣) ↔ (𝑌 𝑈) = (𝑌 𝑉)))
74 oveq2 6623 . . . . . . . . 9 (𝑣 = 𝑉 → (𝑍 𝑣) = (𝑍 𝑉))
7574eqeq2d 2631 . . . . . . . 8 (𝑣 = 𝑉 → ((𝑍 𝑈) = (𝑍 𝑣) ↔ (𝑍 𝑈) = (𝑍 𝑉)))
7671, 73, 753anbi123d 1396 . . . . . . 7 (𝑣 = 𝑉 → (((𝑋 𝑈) = (𝑋 𝑣) ∧ (𝑌 𝑈) = (𝑌 𝑣) ∧ (𝑍 𝑈) = (𝑍 𝑣)) ↔ ((𝑋 𝑈) = (𝑋 𝑉) ∧ (𝑌 𝑈) = (𝑌 𝑉) ∧ (𝑍 𝑈) = (𝑍 𝑉))))
77 neeq2 2853 . . . . . . 7 (𝑣 = 𝑉 → (𝑈𝑣𝑈𝑉))
7876, 77anbi12d 746 . . . . . 6 (𝑣 = 𝑉 → ((((𝑋 𝑈) = (𝑋 𝑣) ∧ (𝑌 𝑈) = (𝑌 𝑣) ∧ (𝑍 𝑈) = (𝑍 𝑣)) ∧ 𝑈𝑣) ↔ (((𝑋 𝑈) = (𝑋 𝑉) ∧ (𝑌 𝑈) = (𝑌 𝑉) ∧ (𝑍 𝑈) = (𝑍 𝑉)) ∧ 𝑈𝑉)))
7978imbi1d 331 . . . . 5 (𝑣 = 𝑉 → (((((𝑋 𝑈) = (𝑋 𝑣) ∧ (𝑌 𝑈) = (𝑌 𝑣) ∧ (𝑍 𝑈) = (𝑍 𝑣)) ∧ 𝑈𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))) ↔ ((((𝑋 𝑈) = (𝑋 𝑉) ∧ (𝑌 𝑈) = (𝑌 𝑉) ∧ (𝑍 𝑈) = (𝑍 𝑉)) ∧ 𝑈𝑉) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))))
8069, 79rspc2v 3311 . . . 4 ((𝑈𝑃𝑉𝑃) → (∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))) → ((((𝑋 𝑈) = (𝑋 𝑉) ∧ (𝑌 𝑈) = (𝑌 𝑉) ∧ (𝑍 𝑈) = (𝑍 𝑉)) ∧ 𝑈𝑉) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))))
8158, 59, 80syl2anc 692 . . 3 (𝜑 → (∀𝑢𝑃𝑣𝑃 ((((𝑋 𝑢) = (𝑋 𝑣) ∧ (𝑌 𝑢) = (𝑌 𝑣) ∧ (𝑍 𝑢) = (𝑍 𝑣)) ∧ 𝑢𝑣) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))) → ((((𝑋 𝑈) = (𝑋 𝑉) ∧ (𝑌 𝑈) = (𝑌 𝑉) ∧ (𝑍 𝑈) = (𝑍 𝑉)) ∧ 𝑈𝑉) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))))
8257, 81mpd 15 . 2 (𝜑 → ((((𝑋 𝑈) = (𝑋 𝑉) ∧ (𝑌 𝑈) = (𝑌 𝑉) ∧ (𝑍 𝑈) = (𝑍 𝑉)) ∧ 𝑈𝑉) → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))))
834, 5, 82mp2and 714 1 (𝜑 → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  w3o 1035  w3a 1036   = wceq 1480  wcel 1987  wne 2790  wral 2908  wrex 2909  Vcvv 3190  cfv 5857  (class class class)co 6615  Basecbs 15800  distcds 15890  Itvcitv 25269  TarskiG2Dcstrkg2d 30502
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-nul 4759
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-sbc 3423  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-uni 4410  df-br 4624  df-iota 5820  df-fv 5865  df-ov 6618  df-trkg2d 30503
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator