MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axtgupdim2 Structured version   Visualization version   GIF version

Theorem axtgupdim2 27413
Description: Upper dimension axiom for dimension 2, Axiom A9 of [Schwabhauser] p. 13. Three points 𝑋, 𝑌 and 𝑍 equidistant to two given two points 𝑈 and 𝑉 must be colinear. (Contributed by Thierry Arnoux, 29-May-2019.) (Revised by Thierry Arnoux, 11-Jul-2020.)
Hypotheses
Ref Expression
axtrkge.p 𝑃 = (Base‘𝐺)
axtrkge.d = (dist‘𝐺)
axtrkge.i 𝐼 = (Itv‘𝐺)
axtgupdim2.x (𝜑𝑋𝑃)
axtgupdim2.y (𝜑𝑌𝑃)
axtgupdim2.z (𝜑𝑍𝑃)
axtgupdim2.u (𝜑𝑈𝑃)
axtgupdim2.v (𝜑𝑉𝑃)
axtgupdim2.0 (𝜑𝑈𝑉)
axtgupdim2.1 (𝜑 → (𝑈 𝑋) = (𝑉 𝑋))
axtgupdim2.2 (𝜑 → (𝑈 𝑌) = (𝑉 𝑌))
axtgupdim2.3 (𝜑 → (𝑈 𝑍) = (𝑉 𝑍))
axtgupdim2.w (𝜑𝐺𝑉)
axtgupdim2.g (𝜑 → ¬ 𝐺DimTarskiG≥3)
Assertion
Ref Expression
axtgupdim2 (𝜑 → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))

Proof of Theorem axtgupdim2
Dummy variables 𝑣 𝑢 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 axtgupdim2.1 . . 3 (𝜑 → (𝑈 𝑋) = (𝑉 𝑋))
2 axtgupdim2.2 . . 3 (𝜑 → (𝑈 𝑌) = (𝑉 𝑌))
3 axtgupdim2.3 . . 3 (𝜑 → (𝑈 𝑍) = (𝑉 𝑍))
4 axtgupdim2.0 . . . . . . 7 (𝜑𝑈𝑉)
5 axtgupdim2.g . . . . . . . . . . 11 (𝜑 → ¬ 𝐺DimTarskiG≥3)
6 axtgupdim2.w . . . . . . . . . . . 12 (𝜑𝐺𝑉)
7 axtrkge.p . . . . . . . . . . . . 13 𝑃 = (Base‘𝐺)
8 axtrkge.d . . . . . . . . . . . . 13 = (dist‘𝐺)
9 axtrkge.i . . . . . . . . . . . . 13 𝐼 = (Itv‘𝐺)
107, 8, 9istrkg3ld 27403 . . . . . . . . . . . 12 (𝐺𝑉 → (𝐺DimTarskiG≥3 ↔ ∃𝑢𝑃𝑣𝑃 (𝑢𝑣 ∧ ∃𝑥𝑃𝑦𝑃𝑧𝑃 (((𝑢 𝑥) = (𝑣 𝑥) ∧ (𝑢 𝑦) = (𝑣 𝑦) ∧ (𝑢 𝑧) = (𝑣 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))))
116, 10syl 17 . . . . . . . . . . 11 (𝜑 → (𝐺DimTarskiG≥3 ↔ ∃𝑢𝑃𝑣𝑃 (𝑢𝑣 ∧ ∃𝑥𝑃𝑦𝑃𝑧𝑃 (((𝑢 𝑥) = (𝑣 𝑥) ∧ (𝑢 𝑦) = (𝑣 𝑦) ∧ (𝑢 𝑧) = (𝑣 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))))
125, 11mtbid 323 . . . . . . . . . 10 (𝜑 → ¬ ∃𝑢𝑃𝑣𝑃 (𝑢𝑣 ∧ ∃𝑥𝑃𝑦𝑃𝑧𝑃 (((𝑢 𝑥) = (𝑣 𝑥) ∧ (𝑢 𝑦) = (𝑣 𝑦) ∧ (𝑢 𝑧) = (𝑣 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))))
13 ralnex2 3130 . . . . . . . . . 10 (∀𝑢𝑃𝑣𝑃 ¬ (𝑢𝑣 ∧ ∃𝑥𝑃𝑦𝑃𝑧𝑃 (((𝑢 𝑥) = (𝑣 𝑥) ∧ (𝑢 𝑦) = (𝑣 𝑦) ∧ (𝑢 𝑧) = (𝑣 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) ↔ ¬ ∃𝑢𝑃𝑣𝑃 (𝑢𝑣 ∧ ∃𝑥𝑃𝑦𝑃𝑧𝑃 (((𝑢 𝑥) = (𝑣 𝑥) ∧ (𝑢 𝑦) = (𝑣 𝑦) ∧ (𝑢 𝑧) = (𝑣 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))))
1412, 13sylibr 233 . . . . . . . . 9 (𝜑 → ∀𝑢𝑃𝑣𝑃 ¬ (𝑢𝑣 ∧ ∃𝑥𝑃𝑦𝑃𝑧𝑃 (((𝑢 𝑥) = (𝑣 𝑥) ∧ (𝑢 𝑦) = (𝑣 𝑦) ∧ (𝑢 𝑧) = (𝑣 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))))
15 axtgupdim2.u . . . . . . . . . 10 (𝜑𝑈𝑃)
16 axtgupdim2.v . . . . . . . . . 10 (𝜑𝑉𝑃)
17 neeq1 3006 . . . . . . . . . . . . 13 (𝑢 = 𝑈 → (𝑢𝑣𝑈𝑣))
18 oveq1 7364 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑈 → (𝑢 𝑥) = (𝑈 𝑥))
1918eqeq1d 2738 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑈 → ((𝑢 𝑥) = (𝑣 𝑥) ↔ (𝑈 𝑥) = (𝑣 𝑥)))
20 oveq1 7364 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑈 → (𝑢 𝑦) = (𝑈 𝑦))
2120eqeq1d 2738 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑈 → ((𝑢 𝑦) = (𝑣 𝑦) ↔ (𝑈 𝑦) = (𝑣 𝑦)))
22 oveq1 7364 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑈 → (𝑢 𝑧) = (𝑈 𝑧))
2322eqeq1d 2738 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑈 → ((𝑢 𝑧) = (𝑣 𝑧) ↔ (𝑈 𝑧) = (𝑣 𝑧)))
2419, 21, 233anbi123d 1436 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑈 → (((𝑢 𝑥) = (𝑣 𝑥) ∧ (𝑢 𝑦) = (𝑣 𝑦) ∧ (𝑢 𝑧) = (𝑣 𝑧)) ↔ ((𝑈 𝑥) = (𝑣 𝑥) ∧ (𝑈 𝑦) = (𝑣 𝑦) ∧ (𝑈 𝑧) = (𝑣 𝑧))))
2524anbi1d 630 . . . . . . . . . . . . . . 15 (𝑢 = 𝑈 → ((((𝑢 𝑥) = (𝑣 𝑥) ∧ (𝑢 𝑦) = (𝑣 𝑦) ∧ (𝑢 𝑧) = (𝑣 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ (((𝑈 𝑥) = (𝑣 𝑥) ∧ (𝑈 𝑦) = (𝑣 𝑦) ∧ (𝑈 𝑧) = (𝑣 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))))
2625rexbidv 3175 . . . . . . . . . . . . . 14 (𝑢 = 𝑈 → (∃𝑧𝑃 (((𝑢 𝑥) = (𝑣 𝑥) ∧ (𝑢 𝑦) = (𝑣 𝑦) ∧ (𝑢 𝑧) = (𝑣 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ∃𝑧𝑃 (((𝑈 𝑥) = (𝑣 𝑥) ∧ (𝑈 𝑦) = (𝑣 𝑦) ∧ (𝑈 𝑧) = (𝑣 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))))
27262rexbidv 3213 . . . . . . . . . . . . 13 (𝑢 = 𝑈 → (∃𝑥𝑃𝑦𝑃𝑧𝑃 (((𝑢 𝑥) = (𝑣 𝑥) ∧ (𝑢 𝑦) = (𝑣 𝑦) ∧ (𝑢 𝑧) = (𝑣 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ∃𝑥𝑃𝑦𝑃𝑧𝑃 (((𝑈 𝑥) = (𝑣 𝑥) ∧ (𝑈 𝑦) = (𝑣 𝑦) ∧ (𝑈 𝑧) = (𝑣 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))))
2817, 27anbi12d 631 . . . . . . . . . . . 12 (𝑢 = 𝑈 → ((𝑢𝑣 ∧ ∃𝑥𝑃𝑦𝑃𝑧𝑃 (((𝑢 𝑥) = (𝑣 𝑥) ∧ (𝑢 𝑦) = (𝑣 𝑦) ∧ (𝑢 𝑧) = (𝑣 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) ↔ (𝑈𝑣 ∧ ∃𝑥𝑃𝑦𝑃𝑧𝑃 (((𝑈 𝑥) = (𝑣 𝑥) ∧ (𝑈 𝑦) = (𝑣 𝑦) ∧ (𝑈 𝑧) = (𝑣 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))))
2928notbid 317 . . . . . . . . . . 11 (𝑢 = 𝑈 → (¬ (𝑢𝑣 ∧ ∃𝑥𝑃𝑦𝑃𝑧𝑃 (((𝑢 𝑥) = (𝑣 𝑥) ∧ (𝑢 𝑦) = (𝑣 𝑦) ∧ (𝑢 𝑧) = (𝑣 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) ↔ ¬ (𝑈𝑣 ∧ ∃𝑥𝑃𝑦𝑃𝑧𝑃 (((𝑈 𝑥) = (𝑣 𝑥) ∧ (𝑈 𝑦) = (𝑣 𝑦) ∧ (𝑈 𝑧) = (𝑣 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))))
30 neeq2 3007 . . . . . . . . . . . . 13 (𝑣 = 𝑉 → (𝑈𝑣𝑈𝑉))
31 oveq1 7364 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑉 → (𝑣 𝑥) = (𝑉 𝑥))
3231eqeq2d 2747 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑉 → ((𝑈 𝑥) = (𝑣 𝑥) ↔ (𝑈 𝑥) = (𝑉 𝑥)))
33 oveq1 7364 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑉 → (𝑣 𝑦) = (𝑉 𝑦))
3433eqeq2d 2747 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑉 → ((𝑈 𝑦) = (𝑣 𝑦) ↔ (𝑈 𝑦) = (𝑉 𝑦)))
35 oveq1 7364 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑉 → (𝑣 𝑧) = (𝑉 𝑧))
3635eqeq2d 2747 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑉 → ((𝑈 𝑧) = (𝑣 𝑧) ↔ (𝑈 𝑧) = (𝑉 𝑧)))
3732, 34, 363anbi123d 1436 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑉 → (((𝑈 𝑥) = (𝑣 𝑥) ∧ (𝑈 𝑦) = (𝑣 𝑦) ∧ (𝑈 𝑧) = (𝑣 𝑧)) ↔ ((𝑈 𝑥) = (𝑉 𝑥) ∧ (𝑈 𝑦) = (𝑉 𝑦) ∧ (𝑈 𝑧) = (𝑉 𝑧))))
3837anbi1d 630 . . . . . . . . . . . . . . 15 (𝑣 = 𝑉 → ((((𝑈 𝑥) = (𝑣 𝑥) ∧ (𝑈 𝑦) = (𝑣 𝑦) ∧ (𝑈 𝑧) = (𝑣 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ (((𝑈 𝑥) = (𝑉 𝑥) ∧ (𝑈 𝑦) = (𝑉 𝑦) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))))
3938rexbidv 3175 . . . . . . . . . . . . . 14 (𝑣 = 𝑉 → (∃𝑧𝑃 (((𝑈 𝑥) = (𝑣 𝑥) ∧ (𝑈 𝑦) = (𝑣 𝑦) ∧ (𝑈 𝑧) = (𝑣 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ∃𝑧𝑃 (((𝑈 𝑥) = (𝑉 𝑥) ∧ (𝑈 𝑦) = (𝑉 𝑦) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))))
40392rexbidv 3213 . . . . . . . . . . . . 13 (𝑣 = 𝑉 → (∃𝑥𝑃𝑦𝑃𝑧𝑃 (((𝑈 𝑥) = (𝑣 𝑥) ∧ (𝑈 𝑦) = (𝑣 𝑦) ∧ (𝑈 𝑧) = (𝑣 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ∃𝑥𝑃𝑦𝑃𝑧𝑃 (((𝑈 𝑥) = (𝑉 𝑥) ∧ (𝑈 𝑦) = (𝑉 𝑦) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))))
4130, 40anbi12d 631 . . . . . . . . . . . 12 (𝑣 = 𝑉 → ((𝑈𝑣 ∧ ∃𝑥𝑃𝑦𝑃𝑧𝑃 (((𝑈 𝑥) = (𝑣 𝑥) ∧ (𝑈 𝑦) = (𝑣 𝑦) ∧ (𝑈 𝑧) = (𝑣 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) ↔ (𝑈𝑉 ∧ ∃𝑥𝑃𝑦𝑃𝑧𝑃 (((𝑈 𝑥) = (𝑉 𝑥) ∧ (𝑈 𝑦) = (𝑉 𝑦) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))))
4241notbid 317 . . . . . . . . . . 11 (𝑣 = 𝑉 → (¬ (𝑈𝑣 ∧ ∃𝑥𝑃𝑦𝑃𝑧𝑃 (((𝑈 𝑥) = (𝑣 𝑥) ∧ (𝑈 𝑦) = (𝑣 𝑦) ∧ (𝑈 𝑧) = (𝑣 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) ↔ ¬ (𝑈𝑉 ∧ ∃𝑥𝑃𝑦𝑃𝑧𝑃 (((𝑈 𝑥) = (𝑉 𝑥) ∧ (𝑈 𝑦) = (𝑉 𝑦) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))))
4329, 42rspc2v 3590 . . . . . . . . . 10 ((𝑈𝑃𝑉𝑃) → (∀𝑢𝑃𝑣𝑃 ¬ (𝑢𝑣 ∧ ∃𝑥𝑃𝑦𝑃𝑧𝑃 (((𝑢 𝑥) = (𝑣 𝑥) ∧ (𝑢 𝑦) = (𝑣 𝑦) ∧ (𝑢 𝑧) = (𝑣 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) → ¬ (𝑈𝑉 ∧ ∃𝑥𝑃𝑦𝑃𝑧𝑃 (((𝑈 𝑥) = (𝑉 𝑥) ∧ (𝑈 𝑦) = (𝑉 𝑦) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))))
4415, 16, 43syl2anc 584 . . . . . . . . 9 (𝜑 → (∀𝑢𝑃𝑣𝑃 ¬ (𝑢𝑣 ∧ ∃𝑥𝑃𝑦𝑃𝑧𝑃 (((𝑢 𝑥) = (𝑣 𝑥) ∧ (𝑢 𝑦) = (𝑣 𝑦) ∧ (𝑢 𝑧) = (𝑣 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) → ¬ (𝑈𝑉 ∧ ∃𝑥𝑃𝑦𝑃𝑧𝑃 (((𝑈 𝑥) = (𝑉 𝑥) ∧ (𝑈 𝑦) = (𝑉 𝑦) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))))
4514, 44mpd 15 . . . . . . . 8 (𝜑 → ¬ (𝑈𝑉 ∧ ∃𝑥𝑃𝑦𝑃𝑧𝑃 (((𝑈 𝑥) = (𝑉 𝑥) ∧ (𝑈 𝑦) = (𝑉 𝑦) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))))
46 imnan 400 . . . . . . . 8 ((𝑈𝑉 → ¬ ∃𝑥𝑃𝑦𝑃𝑧𝑃 (((𝑈 𝑥) = (𝑉 𝑥) ∧ (𝑈 𝑦) = (𝑉 𝑦) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))) ↔ ¬ (𝑈𝑉 ∧ ∃𝑥𝑃𝑦𝑃𝑧𝑃 (((𝑈 𝑥) = (𝑉 𝑥) ∧ (𝑈 𝑦) = (𝑉 𝑦) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))))
4745, 46sylibr 233 . . . . . . 7 (𝜑 → (𝑈𝑉 → ¬ ∃𝑥𝑃𝑦𝑃𝑧𝑃 (((𝑈 𝑥) = (𝑉 𝑥) ∧ (𝑈 𝑦) = (𝑉 𝑦) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)))))
484, 47mpd 15 . . . . . 6 (𝜑 → ¬ ∃𝑥𝑃𝑦𝑃𝑧𝑃 (((𝑈 𝑥) = (𝑉 𝑥) ∧ (𝑈 𝑦) = (𝑉 𝑦) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))
49 ralnex3 3131 . . . . . 6 (∀𝑥𝑃𝑦𝑃𝑧𝑃 ¬ (((𝑈 𝑥) = (𝑉 𝑥) ∧ (𝑈 𝑦) = (𝑉 𝑦) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ¬ ∃𝑥𝑃𝑦𝑃𝑧𝑃 (((𝑈 𝑥) = (𝑉 𝑥) ∧ (𝑈 𝑦) = (𝑉 𝑦) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))
5048, 49sylibr 233 . . . . 5 (𝜑 → ∀𝑥𝑃𝑦𝑃𝑧𝑃 ¬ (((𝑈 𝑥) = (𝑉 𝑥) ∧ (𝑈 𝑦) = (𝑉 𝑦) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))))
51 axtgupdim2.x . . . . . 6 (𝜑𝑋𝑃)
52 axtgupdim2.y . . . . . 6 (𝜑𝑌𝑃)
53 axtgupdim2.z . . . . . 6 (𝜑𝑍𝑃)
54 oveq2 7365 . . . . . . . . . . 11 (𝑥 = 𝑋 → (𝑈 𝑥) = (𝑈 𝑋))
55 oveq2 7365 . . . . . . . . . . 11 (𝑥 = 𝑋 → (𝑉 𝑥) = (𝑉 𝑋))
5654, 55eqeq12d 2752 . . . . . . . . . 10 (𝑥 = 𝑋 → ((𝑈 𝑥) = (𝑉 𝑥) ↔ (𝑈 𝑋) = (𝑉 𝑋)))
57563anbi1d 1440 . . . . . . . . 9 (𝑥 = 𝑋 → (((𝑈 𝑥) = (𝑉 𝑥) ∧ (𝑈 𝑦) = (𝑉 𝑦) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ↔ ((𝑈 𝑋) = (𝑉 𝑋) ∧ (𝑈 𝑦) = (𝑉 𝑦) ∧ (𝑈 𝑧) = (𝑉 𝑧))))
58 oveq1 7364 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (𝑥𝐼𝑦) = (𝑋𝐼𝑦))
5958eleq2d 2823 . . . . . . . . . . 11 (𝑥 = 𝑋 → (𝑧 ∈ (𝑥𝐼𝑦) ↔ 𝑧 ∈ (𝑋𝐼𝑦)))
60 eleq1 2825 . . . . . . . . . . 11 (𝑥 = 𝑋 → (𝑥 ∈ (𝑧𝐼𝑦) ↔ 𝑋 ∈ (𝑧𝐼𝑦)))
61 oveq1 7364 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (𝑥𝐼𝑧) = (𝑋𝐼𝑧))
6261eleq2d 2823 . . . . . . . . . . 11 (𝑥 = 𝑋 → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑋𝐼𝑧)))
6359, 60, 623orbi123d 1435 . . . . . . . . . 10 (𝑥 = 𝑋 → ((𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ (𝑧 ∈ (𝑋𝐼𝑦) ∨ 𝑋 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑋𝐼𝑧))))
6463notbid 317 . . . . . . . . 9 (𝑥 = 𝑋 → (¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ ¬ (𝑧 ∈ (𝑋𝐼𝑦) ∨ 𝑋 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑋𝐼𝑧))))
6557, 64anbi12d 631 . . . . . . . 8 (𝑥 = 𝑋 → ((((𝑈 𝑥) = (𝑉 𝑥) ∧ (𝑈 𝑦) = (𝑉 𝑦) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ (((𝑈 𝑋) = (𝑉 𝑋) ∧ (𝑈 𝑦) = (𝑉 𝑦) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ∧ ¬ (𝑧 ∈ (𝑋𝐼𝑦) ∨ 𝑋 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑋𝐼𝑧)))))
6665notbid 317 . . . . . . 7 (𝑥 = 𝑋 → (¬ (((𝑈 𝑥) = (𝑉 𝑥) ∧ (𝑈 𝑦) = (𝑉 𝑦) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) ↔ ¬ (((𝑈 𝑋) = (𝑉 𝑋) ∧ (𝑈 𝑦) = (𝑉 𝑦) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ∧ ¬ (𝑧 ∈ (𝑋𝐼𝑦) ∨ 𝑋 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑋𝐼𝑧)))))
67 oveq2 7365 . . . . . . . . . . 11 (𝑦 = 𝑌 → (𝑈 𝑦) = (𝑈 𝑌))
68 oveq2 7365 . . . . . . . . . . 11 (𝑦 = 𝑌 → (𝑉 𝑦) = (𝑉 𝑌))
6967, 68eqeq12d 2752 . . . . . . . . . 10 (𝑦 = 𝑌 → ((𝑈 𝑦) = (𝑉 𝑦) ↔ (𝑈 𝑌) = (𝑉 𝑌)))
70693anbi2d 1441 . . . . . . . . 9 (𝑦 = 𝑌 → (((𝑈 𝑋) = (𝑉 𝑋) ∧ (𝑈 𝑦) = (𝑉 𝑦) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ↔ ((𝑈 𝑋) = (𝑉 𝑋) ∧ (𝑈 𝑌) = (𝑉 𝑌) ∧ (𝑈 𝑧) = (𝑉 𝑧))))
71 oveq2 7365 . . . . . . . . . . . 12 (𝑦 = 𝑌 → (𝑋𝐼𝑦) = (𝑋𝐼𝑌))
7271eleq2d 2823 . . . . . . . . . . 11 (𝑦 = 𝑌 → (𝑧 ∈ (𝑋𝐼𝑦) ↔ 𝑧 ∈ (𝑋𝐼𝑌)))
73 oveq2 7365 . . . . . . . . . . . 12 (𝑦 = 𝑌 → (𝑧𝐼𝑦) = (𝑧𝐼𝑌))
7473eleq2d 2823 . . . . . . . . . . 11 (𝑦 = 𝑌 → (𝑋 ∈ (𝑧𝐼𝑦) ↔ 𝑋 ∈ (𝑧𝐼𝑌)))
75 eleq1 2825 . . . . . . . . . . 11 (𝑦 = 𝑌 → (𝑦 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑧)))
7672, 74, 753orbi123d 1435 . . . . . . . . . 10 (𝑦 = 𝑌 → ((𝑧 ∈ (𝑋𝐼𝑦) ∨ 𝑋 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑋𝐼𝑧)) ↔ (𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧))))
7776notbid 317 . . . . . . . . 9 (𝑦 = 𝑌 → (¬ (𝑧 ∈ (𝑋𝐼𝑦) ∨ 𝑋 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑋𝐼𝑧)) ↔ ¬ (𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧))))
7870, 77anbi12d 631 . . . . . . . 8 (𝑦 = 𝑌 → ((((𝑈 𝑋) = (𝑉 𝑋) ∧ (𝑈 𝑦) = (𝑉 𝑦) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ∧ ¬ (𝑧 ∈ (𝑋𝐼𝑦) ∨ 𝑋 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑋𝐼𝑧))) ↔ (((𝑈 𝑋) = (𝑉 𝑋) ∧ (𝑈 𝑌) = (𝑉 𝑌) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ∧ ¬ (𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧)))))
7978notbid 317 . . . . . . 7 (𝑦 = 𝑌 → (¬ (((𝑈 𝑋) = (𝑉 𝑋) ∧ (𝑈 𝑦) = (𝑉 𝑦) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ∧ ¬ (𝑧 ∈ (𝑋𝐼𝑦) ∨ 𝑋 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑋𝐼𝑧))) ↔ ¬ (((𝑈 𝑋) = (𝑉 𝑋) ∧ (𝑈 𝑌) = (𝑉 𝑌) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ∧ ¬ (𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧)))))
80 oveq2 7365 . . . . . . . . . . 11 (𝑧 = 𝑍 → (𝑈 𝑧) = (𝑈 𝑍))
81 oveq2 7365 . . . . . . . . . . 11 (𝑧 = 𝑍 → (𝑉 𝑧) = (𝑉 𝑍))
8280, 81eqeq12d 2752 . . . . . . . . . 10 (𝑧 = 𝑍 → ((𝑈 𝑧) = (𝑉 𝑧) ↔ (𝑈 𝑍) = (𝑉 𝑍)))
83823anbi3d 1442 . . . . . . . . 9 (𝑧 = 𝑍 → (((𝑈 𝑋) = (𝑉 𝑋) ∧ (𝑈 𝑌) = (𝑉 𝑌) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ↔ ((𝑈 𝑋) = (𝑉 𝑋) ∧ (𝑈 𝑌) = (𝑉 𝑌) ∧ (𝑈 𝑍) = (𝑉 𝑍))))
84 eleq1 2825 . . . . . . . . . . 11 (𝑧 = 𝑍 → (𝑧 ∈ (𝑋𝐼𝑌) ↔ 𝑍 ∈ (𝑋𝐼𝑌)))
85 oveq1 7364 . . . . . . . . . . . 12 (𝑧 = 𝑍 → (𝑧𝐼𝑌) = (𝑍𝐼𝑌))
8685eleq2d 2823 . . . . . . . . . . 11 (𝑧 = 𝑍 → (𝑋 ∈ (𝑧𝐼𝑌) ↔ 𝑋 ∈ (𝑍𝐼𝑌)))
87 oveq2 7365 . . . . . . . . . . . 12 (𝑧 = 𝑍 → (𝑋𝐼𝑧) = (𝑋𝐼𝑍))
8887eleq2d 2823 . . . . . . . . . . 11 (𝑧 = 𝑍 → (𝑌 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑍)))
8984, 86, 883orbi123d 1435 . . . . . . . . . 10 (𝑧 = 𝑍 → ((𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧)) ↔ (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))))
9089notbid 317 . . . . . . . . 9 (𝑧 = 𝑍 → (¬ (𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧)) ↔ ¬ (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))))
9183, 90anbi12d 631 . . . . . . . 8 (𝑧 = 𝑍 → ((((𝑈 𝑋) = (𝑉 𝑋) ∧ (𝑈 𝑌) = (𝑉 𝑌) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ∧ ¬ (𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧))) ↔ (((𝑈 𝑋) = (𝑉 𝑋) ∧ (𝑈 𝑌) = (𝑉 𝑌) ∧ (𝑈 𝑍) = (𝑉 𝑍)) ∧ ¬ (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))))
9291notbid 317 . . . . . . 7 (𝑧 = 𝑍 → (¬ (((𝑈 𝑋) = (𝑉 𝑋) ∧ (𝑈 𝑌) = (𝑉 𝑌) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ∧ ¬ (𝑧 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑧𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑧))) ↔ ¬ (((𝑈 𝑋) = (𝑉 𝑋) ∧ (𝑈 𝑌) = (𝑉 𝑌) ∧ (𝑈 𝑍) = (𝑉 𝑍)) ∧ ¬ (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))))
9366, 79, 92rspc3v 3593 . . . . . 6 ((𝑋𝑃𝑌𝑃𝑍𝑃) → (∀𝑥𝑃𝑦𝑃𝑧𝑃 ¬ (((𝑈 𝑥) = (𝑉 𝑥) ∧ (𝑈 𝑦) = (𝑉 𝑦) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) → ¬ (((𝑈 𝑋) = (𝑉 𝑋) ∧ (𝑈 𝑌) = (𝑉 𝑌) ∧ (𝑈 𝑍) = (𝑉 𝑍)) ∧ ¬ (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))))
9451, 52, 53, 93syl3anc 1371 . . . . 5 (𝜑 → (∀𝑥𝑃𝑦𝑃𝑧𝑃 ¬ (((𝑈 𝑥) = (𝑉 𝑥) ∧ (𝑈 𝑦) = (𝑉 𝑦) ∧ (𝑈 𝑧) = (𝑉 𝑧)) ∧ ¬ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))) → ¬ (((𝑈 𝑋) = (𝑉 𝑋) ∧ (𝑈 𝑌) = (𝑉 𝑌) ∧ (𝑈 𝑍) = (𝑉 𝑍)) ∧ ¬ (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))))
9550, 94mpd 15 . . . 4 (𝜑 → ¬ (((𝑈 𝑋) = (𝑉 𝑋) ∧ (𝑈 𝑌) = (𝑉 𝑌) ∧ (𝑈 𝑍) = (𝑉 𝑍)) ∧ ¬ (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))))
96 imnan 400 . . . 4 ((((𝑈 𝑋) = (𝑉 𝑋) ∧ (𝑈 𝑌) = (𝑉 𝑌) ∧ (𝑈 𝑍) = (𝑉 𝑍)) → ¬ ¬ (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))) ↔ ¬ (((𝑈 𝑋) = (𝑉 𝑋) ∧ (𝑈 𝑌) = (𝑉 𝑌) ∧ (𝑈 𝑍) = (𝑉 𝑍)) ∧ ¬ (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))))
9795, 96sylibr 233 . . 3 (𝜑 → (((𝑈 𝑋) = (𝑉 𝑋) ∧ (𝑈 𝑌) = (𝑉 𝑌) ∧ (𝑈 𝑍) = (𝑉 𝑍)) → ¬ ¬ (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍))))
981, 2, 3, 97mp3and 1464 . 2 (𝜑 → ¬ ¬ (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))
9998notnotrd 133 1 (𝜑 → (𝑍 ∈ (𝑋𝐼𝑌) ∨ 𝑋 ∈ (𝑍𝐼𝑌) ∨ 𝑌 ∈ (𝑋𝐼𝑍)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3o 1086  w3a 1087   = wceq 1541  wcel 2106  wne 2943  wral 3064  wrex 3073   class class class wbr 5105  cfv 6496  (class class class)co 7357  3c3 12209  Basecbs 17083  distcds 17142  DimTarskiGcstrkgld 27373  Itvcitv 27375
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-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
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-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-2 12216  df-3 12217  df-n0 12414  df-z 12500  df-uz 12764  df-fz 13425  df-fzo 13568  df-trkgld 27394
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator