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 = ( Base ` G )
istrkg.d 
|- .- = ( dist ` G )
istrkg.i 
|- I = ( Itv ` G )
Assertion istrkg2ld 
|- ( G e. V -> ( G TarskiGDim>= 2 <-> E. x e. P E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) )

Proof

Step Hyp Ref Expression
1 istrkg.p 
 |-  P = ( Base ` G )
2 istrkg.d 
 |-  .- = ( dist ` G )
3 istrkg.i 
 |-  I = ( Itv ` G )
4 2z 
 |-  2 e. ZZ
5 uzid 
 |-  ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
6 4 5 ax-mp 
 |-  2 e. ( ZZ>= ` 2 )
7 1 2 3 istrkgld 
 |-  ( ( G e. V /\ 2 e. ( ZZ>= ` 2 ) ) -> ( G TarskiGDim>= 2 <-> E. f ( f : ( 1 ..^ 2 ) -1-1-> P /\ E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) )
8 6 7 mpan2 
 |-  ( G e. V -> ( G TarskiGDim>= 2 <-> E. f ( f : ( 1 ..^ 2 ) -1-1-> P /\ E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) )
9 r19.41v 
 |-  ( E. x e. P ( E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) /\ f : ( 1 ..^ 2 ) -1-1-> P ) <-> ( E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) /\ f : ( 1 ..^ 2 ) -1-1-> P ) )
10 ancom 
 |-  ( ( E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) /\ f : ( 1 ..^ 2 ) -1-1-> P ) <-> ( f : ( 1 ..^ 2 ) -1-1-> P /\ E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
11 10 rexbii 
 |-  ( E. x e. P ( E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) /\ f : ( 1 ..^ 2 ) -1-1-> P ) <-> E. x e. P ( f : ( 1 ..^ 2 ) -1-1-> P /\ E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
12 ancom 
 |-  ( ( E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) /\ f : ( 1 ..^ 2 ) -1-1-> P ) <-> ( f : ( 1 ..^ 2 ) -1-1-> P /\ E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
13 9 11 12 3bitr3ri 
 |-  ( ( f : ( 1 ..^ 2 ) -1-1-> P /\ E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) <-> E. x e. P ( f : ( 1 ..^ 2 ) -1-1-> P /\ E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
14 13 exbii 
 |-  ( E. f ( f : ( 1 ..^ 2 ) -1-1-> P /\ E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) <-> E. f E. x e. P ( f : ( 1 ..^ 2 ) -1-1-> P /\ E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
15 rexcom4 
 |-  ( E. x e. P E. f ( f : ( 1 ..^ 2 ) -1-1-> P /\ E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) <-> E. f E. x e. P ( f : ( 1 ..^ 2 ) -1-1-> P /\ E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
16 simpr 
 |-  ( ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) -> -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) )
17 16 reximi 
 |-  ( E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) -> E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) )
18 17 reximi 
 |-  ( E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) -> E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) )
19 18 adantl 
 |-  ( ( f : ( 1 ..^ 2 ) -1-1-> P /\ E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) -> E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) )
20 19 exlimiv 
 |-  ( E. f ( f : ( 1 ..^ 2 ) -1-1-> P /\ E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) -> E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) )
21 20 adantl 
 |-  ( ( x e. P /\ E. f ( f : ( 1 ..^ 2 ) -1-1-> P /\ E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) -> E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) )
22 1ex 
 |-  1 e. _V
23 vex 
 |-  x e. _V
24 22 23 f1osn 
 |-  { <. 1 , x >. } : { 1 } -1-1-onto-> { x }
25 f1of1 
 |-  ( { <. 1 , x >. } : { 1 } -1-1-onto-> { x } -> { <. 1 , x >. } : { 1 } -1-1-> { x } )
26 24 25 mp1i 
 |-  ( x e. P -> { <. 1 , x >. } : { 1 } -1-1-> { x } )
27 snssi 
 |-  ( x e. P -> { x } C_ P )
28 f1ss 
 |-  ( ( { <. 1 , x >. } : { 1 } -1-1-> { x } /\ { x } C_ P ) -> { <. 1 , x >. } : { 1 } -1-1-> P )
29 26 27 28 syl2anc 
 |-  ( x e. P -> { <. 1 , x >. } : { 1 } -1-1-> P )
30 fzo12sn 
 |-  ( 1 ..^ 2 ) = { 1 }
31 30 mpteq1i 
 |-  ( j e. ( 1 ..^ 2 ) |-> x ) = ( j e. { 1 } |-> x )
32 fmptsn 
 |-  ( ( 1 e. _V /\ x e. _V ) -> { <. 1 , x >. } = ( j e. { 1 } |-> x ) )
33 22 23 32 mp2an 
 |-  { <. 1 , x >. } = ( j e. { 1 } |-> x )
34 31 33 eqtr4i 
 |-  ( j e. ( 1 ..^ 2 ) |-> x ) = { <. 1 , x >. }
35 34 a1i 
 |-  ( T. -> ( j e. ( 1 ..^ 2 ) |-> x ) = { <. 1 , x >. } )
36 30 a1i 
 |-  ( T. -> ( 1 ..^ 2 ) = { 1 } )
37 eqidd 
 |-  ( T. -> P = P )
38 35 36 37 f1eq123d 
 |-  ( T. -> ( ( j e. ( 1 ..^ 2 ) |-> x ) : ( 1 ..^ 2 ) -1-1-> P <-> { <. 1 , x >. } : { 1 } -1-1-> P ) )
39 38 mptru 
 |-  ( ( j e. ( 1 ..^ 2 ) |-> x ) : ( 1 ..^ 2 ) -1-1-> P <-> { <. 1 , x >. } : { 1 } -1-1-> P )
40 29 39 sylibr 
 |-  ( x e. P -> ( j e. ( 1 ..^ 2 ) |-> x ) : ( 1 ..^ 2 ) -1-1-> P )
41 ral0 
 |-  A. j e. (/) ( ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- x ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- x ) /\ ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- y ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- y ) /\ ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- z ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- z ) )
42 fzo0 
 |-  ( 2 ..^ 2 ) = (/)
43 42 raleqi 
 |-  ( A. j e. ( 2 ..^ 2 ) ( ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- x ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- x ) /\ ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- y ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- y ) /\ ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- z ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- z ) ) <-> A. j e. (/) ( ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- x ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- x ) /\ ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- y ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- y ) /\ ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- z ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- z ) ) )
44 41 43 mpbir 
 |-  A. j e. ( 2 ..^ 2 ) ( ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- x ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- x ) /\ ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- y ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- y ) /\ ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- z ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- z ) )
45 44 jctl 
 |-  ( -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) -> ( A. j e. ( 2 ..^ 2 ) ( ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- x ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- x ) /\ ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- y ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- y ) /\ ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- z ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) )
46 45 reximi 
 |-  ( E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) -> E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- x ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- x ) /\ ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- y ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- y ) /\ ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- z ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) )
47 46 reximi 
 |-  ( E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) -> E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- x ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- x ) /\ ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- y ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- y ) /\ ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- z ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) )
48 ovex 
 |-  ( 1 ..^ 2 ) e. _V
49 48 mptex 
 |-  ( j e. ( 1 ..^ 2 ) |-> x ) e. _V
50 f1eq1 
 |-  ( f = ( j e. ( 1 ..^ 2 ) |-> x ) -> ( f : ( 1 ..^ 2 ) -1-1-> P <-> ( j e. ( 1 ..^ 2 ) |-> x ) : ( 1 ..^ 2 ) -1-1-> P ) )
51 nfmpt1 
 |-  F/_ j ( j e. ( 1 ..^ 2 ) |-> x )
52 51 nfeq2 
 |-  F/ j f = ( j e. ( 1 ..^ 2 ) |-> x )
53 nfv 
 |-  F/ j ( y e. P /\ z e. P )
54 52 53 nfan 
 |-  F/ j ( f = ( j e. ( 1 ..^ 2 ) |-> x ) /\ ( y e. P /\ z e. P ) )
55 simpll 
 |-  ( ( ( f = ( j e. ( 1 ..^ 2 ) |-> x ) /\ ( y e. P /\ z e. P ) ) /\ j e. ( 2 ..^ 2 ) ) -> f = ( j e. ( 1 ..^ 2 ) |-> x ) )
56 55 fveq1d 
 |-  ( ( ( f = ( j e. ( 1 ..^ 2 ) |-> x ) /\ ( y e. P /\ z e. P ) ) /\ j e. ( 2 ..^ 2 ) ) -> ( f ` 1 ) = ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) )
57 56 oveq1d 
 |-  ( ( ( f = ( j e. ( 1 ..^ 2 ) |-> x ) /\ ( y e. P /\ z e. P ) ) /\ j e. ( 2 ..^ 2 ) ) -> ( ( f ` 1 ) .- x ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- x ) )
58 55 fveq1d 
 |-  ( ( ( f = ( j e. ( 1 ..^ 2 ) |-> x ) /\ ( y e. P /\ z e. P ) ) /\ j e. ( 2 ..^ 2 ) ) -> ( f ` j ) = ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) )
59 58 oveq1d 
 |-  ( ( ( f = ( j e. ( 1 ..^ 2 ) |-> x ) /\ ( y e. P /\ z e. P ) ) /\ j e. ( 2 ..^ 2 ) ) -> ( ( f ` j ) .- x ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- x ) )
60 57 59 eqeq12d 
 |-  ( ( ( f = ( j e. ( 1 ..^ 2 ) |-> x ) /\ ( y e. P /\ z e. P ) ) /\ j e. ( 2 ..^ 2 ) ) -> ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) <-> ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- x ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- x ) ) )
61 56 oveq1d 
 |-  ( ( ( f = ( j e. ( 1 ..^ 2 ) |-> x ) /\ ( y e. P /\ z e. P ) ) /\ j e. ( 2 ..^ 2 ) ) -> ( ( f ` 1 ) .- y ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- y ) )
62 58 oveq1d 
 |-  ( ( ( f = ( j e. ( 1 ..^ 2 ) |-> x ) /\ ( y e. P /\ z e. P ) ) /\ j e. ( 2 ..^ 2 ) ) -> ( ( f ` j ) .- y ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- y ) )
63 61 62 eqeq12d 
 |-  ( ( ( f = ( j e. ( 1 ..^ 2 ) |-> x ) /\ ( y e. P /\ z e. P ) ) /\ j e. ( 2 ..^ 2 ) ) -> ( ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) <-> ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- y ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- y ) ) )
64 56 oveq1d 
 |-  ( ( ( f = ( j e. ( 1 ..^ 2 ) |-> x ) /\ ( y e. P /\ z e. P ) ) /\ j e. ( 2 ..^ 2 ) ) -> ( ( f ` 1 ) .- z ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- z ) )
65 58 oveq1d 
 |-  ( ( ( f = ( j e. ( 1 ..^ 2 ) |-> x ) /\ ( y e. P /\ z e. P ) ) /\ j e. ( 2 ..^ 2 ) ) -> ( ( f ` j ) .- z ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- z ) )
66 64 65 eqeq12d 
 |-  ( ( ( f = ( j e. ( 1 ..^ 2 ) |-> x ) /\ ( y e. P /\ z e. P ) ) /\ j e. ( 2 ..^ 2 ) ) -> ( ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) <-> ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- z ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- z ) ) )
67 60 63 66 3anbi123d 
 |-  ( ( ( f = ( j e. ( 1 ..^ 2 ) |-> x ) /\ ( y e. P /\ z e. P ) ) /\ j e. ( 2 ..^ 2 ) ) -> ( ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) <-> ( ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- x ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- x ) /\ ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- y ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- y ) /\ ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- z ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- z ) ) ) )
68 54 67 ralbida 
 |-  ( ( f = ( j e. ( 1 ..^ 2 ) |-> x ) /\ ( y e. P /\ z e. P ) ) -> ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) <-> A. j e. ( 2 ..^ 2 ) ( ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- x ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- x ) /\ ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- y ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- y ) /\ ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- z ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- z ) ) ) )
69 68 anbi1d 
 |-  ( ( f = ( j e. ( 1 ..^ 2 ) |-> x ) /\ ( y e. P /\ z e. P ) ) -> ( ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) <-> ( A. j e. ( 2 ..^ 2 ) ( ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- x ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- x ) /\ ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- y ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- y ) /\ ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- z ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
70 69 2rexbidva 
 |-  ( f = ( j e. ( 1 ..^ 2 ) |-> x ) -> ( E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) <-> E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- x ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- x ) /\ ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- y ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- y ) /\ ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- z ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
71 50 70 anbi12d 
 |-  ( f = ( j e. ( 1 ..^ 2 ) |-> x ) -> ( ( f : ( 1 ..^ 2 ) -1-1-> P /\ E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) <-> ( ( j e. ( 1 ..^ 2 ) |-> x ) : ( 1 ..^ 2 ) -1-1-> P /\ E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- x ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- x ) /\ ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- y ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- y ) /\ ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- z ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) )
72 49 71 spcev 
 |-  ( ( ( j e. ( 1 ..^ 2 ) |-> x ) : ( 1 ..^ 2 ) -1-1-> P /\ E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- x ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- x ) /\ ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- y ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- y ) /\ ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` 1 ) .- z ) = ( ( ( j e. ( 1 ..^ 2 ) |-> x ) ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) -> E. f ( f : ( 1 ..^ 2 ) -1-1-> P /\ E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
73 40 47 72 syl2an 
 |-  ( ( x e. P /\ E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) -> E. f ( f : ( 1 ..^ 2 ) -1-1-> P /\ E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) )
74 21 73 impbida 
 |-  ( x e. P -> ( E. f ( f : ( 1 ..^ 2 ) -1-1-> P /\ E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) <-> E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) )
75 74 rexbiia 
 |-  ( E. x e. P E. f ( f : ( 1 ..^ 2 ) -1-1-> P /\ E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) <-> E. x e. P E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) )
76 14 15 75 3bitr2i 
 |-  ( E. f ( f : ( 1 ..^ 2 ) -1-1-> P /\ E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ 2 ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) <-> E. x e. P E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) )
77 8 76 bitrdi 
 |-  ( G e. V -> ( G TarskiGDim>= 2 <-> E. x e. P E. y e. P E. z e. P -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) )