Metamath Proof Explorer

Theorem istrkg2ld

Description: Property of fulfilling the lower dimension 2 axiom. (Contributed by Thierry Arnoux, 20-Nov-2019)

Ref Expression
Hypotheses istrkg.p ⊢P=BaseG
istrkg.d ⊢-˙=dist⁡G
istrkg.i ⊢I=Itv⁡G
Assertion istrkg2ld ⊢G∈V→GDim𝒢≥2↔∃x∈P∃y∈P∃z∈P¬z∈xIy∨x∈zIy∨y∈xIz

Proof

Step Hyp Ref Expression
1 istrkg.p ⊢P=BaseG
2 istrkg.d ⊢-˙=dist⁡G
3 istrkg.i ⊢I=Itv⁡G
4 2z ⊢2∈ℤ
5 uzid ⊢2∈ℤ→2∈ℤ≥2
6 4 5 ax-mp ⊢2∈ℤ≥2
7 1 2 3 istrkgld ⊢G∈V∧2∈ℤ≥2→GDim𝒢≥2↔∃ff:1..^2⟶1-1P∧∃x∈P∃y∈P∃z∈P∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz
8 6 7 mpan2 ⊢G∈V→GDim𝒢≥2↔∃ff:1..^2⟶1-1P∧∃x∈P∃y∈P∃z∈P∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz
9 r19.41v ⊢∃x∈P∃y∈P∃z∈P∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz∧f:1..^2⟶1-1P↔∃x∈P∃y∈P∃z∈P∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz∧f:1..^2⟶1-1P
10 ancom ⊢∃y∈P∃z∈P∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz∧f:1..^2⟶1-1P↔f:1..^2⟶1-1P∧∃y∈P∃z∈P∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz
11 10 rexbii ⊢∃x∈P∃y∈P∃z∈P∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz∧f:1..^2⟶1-1P↔∃x∈Pf:1..^2⟶1-1P∧∃y∈P∃z∈P∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz
12 ancom ⊢∃x∈P∃y∈P∃z∈P∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz∧f:1..^2⟶1-1P↔f:1..^2⟶1-1P∧∃x∈P∃y∈P∃z∈P∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz
13 9 11 12 3bitr3ri ⊢f:1..^2⟶1-1P∧∃x∈P∃y∈P∃z∈P∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz↔∃x∈Pf:1..^2⟶1-1P∧∃y∈P∃z∈P∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz
14 13 exbii ⊢∃ff:1..^2⟶1-1P∧∃x∈P∃y∈P∃z∈P∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz↔∃f∃x∈Pf:1..^2⟶1-1P∧∃y∈P∃z∈P∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz
15 rexcom4 ⊢∃x∈P∃ff:1..^2⟶1-1P∧∃y∈P∃z∈P∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz↔∃f∃x∈Pf:1..^2⟶1-1P∧∃y∈P∃z∈P∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz
16 simpr ⊢∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz→¬z∈xIy∨x∈zIy∨y∈xIz
17 16 reximi ⊢∃z∈P∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz→∃z∈P¬z∈xIy∨x∈zIy∨y∈xIz
18 17 reximi ⊢∃y∈P∃z∈P∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz→∃y∈P∃z∈P¬z∈xIy∨x∈zIy∨y∈xIz
19 18 adantl ⊢f:1..^2⟶1-1P∧∃y∈P∃z∈P∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz→∃y∈P∃z∈P¬z∈xIy∨x∈zIy∨y∈xIz
20 19 exlimiv ⊢∃ff:1..^2⟶1-1P∧∃y∈P∃z∈P∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz→∃y∈P∃z∈P¬z∈xIy∨x∈zIy∨y∈xIz
21 20 adantl ⊢x∈P∧∃ff:1..^2⟶1-1P∧∃y∈P∃z∈P∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz→∃y∈P∃z∈P¬z∈xIy∨x∈zIy∨y∈xIz
22 1ex ⊢1∈V
23 vex ⊢x∈V
24 22 23 f1osn ⊢1x:1⟶1-1 ontox
25 f1of1 ⊢1x:1⟶1-1 ontox→1x:1⟶1-1x
26 24 25 mp1i ⊢x∈P→1x:1⟶1-1x
27 snssi ⊢x∈P→x⊆P
28 f1ss ⊢1x:1⟶1-1x∧x⊆P→1x:1⟶1-1P
29 26 27 28 syl2anc ⊢x∈P→1x:1⟶1-1P
30 fzo12sn ⊢1..^2=1
31 30 mpteq1i ⊢j∈1..^2⟼x=j∈1⟼x
32 fmptsn ⊢1∈V∧x∈V→1x=j∈1⟼x
33 22 23 32 mp2an ⊢1x=j∈1⟼x
34 31 33 eqtr4i ⊢j∈1..^2⟼x=1x
35 34 a1i ⊢⊤→j∈1..^2⟼x=1x
36 30 a1i ⊢⊤→1..^2=1
37 eqidd ⊢⊤→P=P
38 35 36 37 f1eq123d ⊢⊤→j∈1..^2⟼x:1..^2⟶1-1P↔1x:1⟶1-1P
39 38 mptru ⊢j∈1..^2⟼x:1..^2⟶1-1P↔1x:1⟶1-1P
40 29 39 sylibr ⊢x∈P→j∈1..^2⟼x:1..^2⟶1-1P
41 ral0 ⊢∀j∈∅j∈1..^2⟼x⁡1-˙x=j∈1..^2⟼x⁡j-˙x∧j∈1..^2⟼x⁡1-˙y=j∈1..^2⟼x⁡j-˙y∧j∈1..^2⟼x⁡1-˙z=j∈1..^2⟼x⁡j-˙z
42 fzo0 ⊢2..^2=∅
43 42 raleqi ⊢∀j∈2..^2j∈1..^2⟼x⁡1-˙x=j∈1..^2⟼x⁡j-˙x∧j∈1..^2⟼x⁡1-˙y=j∈1..^2⟼x⁡j-˙y∧j∈1..^2⟼x⁡1-˙z=j∈1..^2⟼x⁡j-˙z↔∀j∈∅j∈1..^2⟼x⁡1-˙x=j∈1..^2⟼x⁡j-˙x∧j∈1..^2⟼x⁡1-˙y=j∈1..^2⟼x⁡j-˙y∧j∈1..^2⟼x⁡1-˙z=j∈1..^2⟼x⁡j-˙z
44 41 43 mpbir ⊢∀j∈2..^2j∈1..^2⟼x⁡1-˙x=j∈1..^2⟼x⁡j-˙x∧j∈1..^2⟼x⁡1-˙y=j∈1..^2⟼x⁡j-˙y∧j∈1..^2⟼x⁡1-˙z=j∈1..^2⟼x⁡j-˙z
45 44 jctl ⊢¬z∈xIy∨x∈zIy∨y∈xIz→∀j∈2..^2j∈1..^2⟼x⁡1-˙x=j∈1..^2⟼x⁡j-˙x∧j∈1..^2⟼x⁡1-˙y=j∈1..^2⟼x⁡j-˙y∧j∈1..^2⟼x⁡1-˙z=j∈1..^2⟼x⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz
46 45 reximi ⊢∃z∈P¬z∈xIy∨x∈zIy∨y∈xIz→∃z∈P∀j∈2..^2j∈1..^2⟼x⁡1-˙x=j∈1..^2⟼x⁡j-˙x∧j∈1..^2⟼x⁡1-˙y=j∈1..^2⟼x⁡j-˙y∧j∈1..^2⟼x⁡1-˙z=j∈1..^2⟼x⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz
47 46 reximi ⊢∃y∈P∃z∈P¬z∈xIy∨x∈zIy∨y∈xIz→∃y∈P∃z∈P∀j∈2..^2j∈1..^2⟼x⁡1-˙x=j∈1..^2⟼x⁡j-˙x∧j∈1..^2⟼x⁡1-˙y=j∈1..^2⟼x⁡j-˙y∧j∈1..^2⟼x⁡1-˙z=j∈1..^2⟼x⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz
48 ovex ⊢1..^2∈V
49 48 mptex ⊢j∈1..^2⟼x∈V
50 f1eq1 ⊢f=j∈1..^2⟼x→f:1..^2⟶1-1P↔j∈1..^2⟼x:1..^2⟶1-1P
51 nfmpt1 ⊢Ⅎ_jj∈1..^2⟼x
52 51 nfeq2 ⊢Ⅎjf=j∈1..^2⟼x
53 nfv ⊢Ⅎjy∈P∧z∈P
54 52 53 nfan ⊢Ⅎjf=j∈1..^2⟼x∧y∈P∧z∈P
55 simpll ⊢f=j∈1..^2⟼x∧y∈P∧z∈P∧j∈2..^2→f=j∈1..^2⟼x
56 55 fveq1d ⊢f=j∈1..^2⟼x∧y∈P∧z∈P∧j∈2..^2→f⁡1=j∈1..^2⟼x⁡1
57 56 oveq1d ⊢f=j∈1..^2⟼x∧y∈P∧z∈P∧j∈2..^2→f⁡1-˙x=j∈1..^2⟼x⁡1-˙x
58 55 fveq1d ⊢f=j∈1..^2⟼x∧y∈P∧z∈P∧j∈2..^2→f⁡j=j∈1..^2⟼x⁡j
59 58 oveq1d ⊢f=j∈1..^2⟼x∧y∈P∧z∈P∧j∈2..^2→f⁡j-˙x=j∈1..^2⟼x⁡j-˙x
60 57 59 eqeq12d ⊢f=j∈1..^2⟼x∧y∈P∧z∈P∧j∈2..^2→f⁡1-˙x=f⁡j-˙x↔j∈1..^2⟼x⁡1-˙x=j∈1..^2⟼x⁡j-˙x
61 56 oveq1d ⊢f=j∈1..^2⟼x∧y∈P∧z∈P∧j∈2..^2→f⁡1-˙y=j∈1..^2⟼x⁡1-˙y
62 58 oveq1d ⊢f=j∈1..^2⟼x∧y∈P∧z∈P∧j∈2..^2→f⁡j-˙y=j∈1..^2⟼x⁡j-˙y
63 61 62 eqeq12d ⊢f=j∈1..^2⟼x∧y∈P∧z∈P∧j∈2..^2→f⁡1-˙y=f⁡j-˙y↔j∈1..^2⟼x⁡1-˙y=j∈1..^2⟼x⁡j-˙y
64 56 oveq1d ⊢f=j∈1..^2⟼x∧y∈P∧z∈P∧j∈2..^2→f⁡1-˙z=j∈1..^2⟼x⁡1-˙z
65 58 oveq1d ⊢f=j∈1..^2⟼x∧y∈P∧z∈P∧j∈2..^2→f⁡j-˙z=j∈1..^2⟼x⁡j-˙z
66 64 65 eqeq12d ⊢f=j∈1..^2⟼x∧y∈P∧z∈P∧j∈2..^2→f⁡1-˙z=f⁡j-˙z↔j∈1..^2⟼x⁡1-˙z=j∈1..^2⟼x⁡j-˙z
67 60 63 66 3anbi123d ⊢f=j∈1..^2⟼x∧y∈P∧z∈P∧j∈2..^2→f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z↔j∈1..^2⟼x⁡1-˙x=j∈1..^2⟼x⁡j-˙x∧j∈1..^2⟼x⁡1-˙y=j∈1..^2⟼x⁡j-˙y∧j∈1..^2⟼x⁡1-˙z=j∈1..^2⟼x⁡j-˙z
68 54 67 ralbida ⊢f=j∈1..^2⟼x∧y∈P∧z∈P→∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z↔∀j∈2..^2j∈1..^2⟼x⁡1-˙x=j∈1..^2⟼x⁡j-˙x∧j∈1..^2⟼x⁡1-˙y=j∈1..^2⟼x⁡j-˙y∧j∈1..^2⟼x⁡1-˙z=j∈1..^2⟼x⁡j-˙z
69 68 anbi1d ⊢f=j∈1..^2⟼x∧y∈P∧z∈P→∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz↔∀j∈2..^2j∈1..^2⟼x⁡1-˙x=j∈1..^2⟼x⁡j-˙x∧j∈1..^2⟼x⁡1-˙y=j∈1..^2⟼x⁡j-˙y∧j∈1..^2⟼x⁡1-˙z=j∈1..^2⟼x⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz
70 69 2rexbidva ⊢f=j∈1..^2⟼x→∃y∈P∃z∈P∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz↔∃y∈P∃z∈P∀j∈2..^2j∈1..^2⟼x⁡1-˙x=j∈1..^2⟼x⁡j-˙x∧j∈1..^2⟼x⁡1-˙y=j∈1..^2⟼x⁡j-˙y∧j∈1..^2⟼x⁡1-˙z=j∈1..^2⟼x⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz
71 50 70 anbi12d ⊢f=j∈1..^2⟼x→f:1..^2⟶1-1P∧∃y∈P∃z∈P∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz↔j∈1..^2⟼x:1..^2⟶1-1P∧∃y∈P∃z∈P∀j∈2..^2j∈1..^2⟼x⁡1-˙x=j∈1..^2⟼x⁡j-˙x∧j∈1..^2⟼x⁡1-˙y=j∈1..^2⟼x⁡j-˙y∧j∈1..^2⟼x⁡1-˙z=j∈1..^2⟼x⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz
72 49 71 spcev ⊢j∈1..^2⟼x:1..^2⟶1-1P∧∃y∈P∃z∈P∀j∈2..^2j∈1..^2⟼x⁡1-˙x=j∈1..^2⟼x⁡j-˙x∧j∈1..^2⟼x⁡1-˙y=j∈1..^2⟼x⁡j-˙y∧j∈1..^2⟼x⁡1-˙z=j∈1..^2⟼x⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz→∃ff:1..^2⟶1-1P∧∃y∈P∃z∈P∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz
73 40 47 72 syl2an ⊢x∈P∧∃y∈P∃z∈P¬z∈xIy∨x∈zIy∨y∈xIz→∃ff:1..^2⟶1-1P∧∃y∈P∃z∈P∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz
74 21 73 impbida ⊢x∈P→∃ff:1..^2⟶1-1P∧∃y∈P∃z∈P∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz↔∃y∈P∃z∈P¬z∈xIy∨x∈zIy∨y∈xIz
75 74 rexbiia ⊢∃x∈P∃ff:1..^2⟶1-1P∧∃y∈P∃z∈P∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz↔∃x∈P∃y∈P∃z∈P¬z∈xIy∨x∈zIy∨y∈xIz
76 14 15 75 3bitr2i ⊢∃ff:1..^2⟶1-1P∧∃x∈P∃y∈P∃z∈P∀j∈2..^2f⁡1-˙x=f⁡j-˙x∧f⁡1-˙y=f⁡j-˙y∧f⁡1-˙z=f⁡j-˙z∧¬z∈xIy∨x∈zIy∨y∈xIz↔∃x∈P∃y∈P∃z∈P¬z∈xIy∨x∈zIy∨y∈xIz
77 8 76 bitrdi ⊢G∈V→GDim𝒢≥2↔∃x∈P∃y∈P∃z∈P¬z∈xIy∨x∈zIy∨y∈xIz