Metamath Proof Explorer

Theorem f1otrge

Description: A bijection between bases which conserves distances and intervals conserves also the property of being a Euclidean geometry. (Contributed by Thierry Arnoux, 23-Mar-2019)

Ref Expression
Hypotheses f1otrkg.p 
|- P = ( Base ` G )
f1otrkg.d 
|- D = ( dist ` G )
f1otrkg.i 
|- I = ( Itv ` G )
f1otrkg.b 
|- B = ( Base ` H )
f1otrkg.e 
|- E = ( dist ` H )
f1otrkg.j 
|- J = ( Itv ` H )
f1otrkg.f 
|- ( ph -> F : B -1-1-onto-> P )
f1otrkg.1 
|- ( ( ph /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
f1otrkg.2 
|- ( ( ph /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )
f1otrg.h 
|- ( ph -> H e. V )
f1otrge.g 
|- ( ph -> G e. TarskiGE )
Assertion f1otrge 
|- ( ph -> H e. TarskiGE )

Proof

Step Hyp Ref Expression
1 f1otrkg.p 
 |-  P = ( Base ` G )
2 f1otrkg.d 
 |-  D = ( dist ` G )
3 f1otrkg.i 
 |-  I = ( Itv ` G )
4 f1otrkg.b 
 |-  B = ( Base ` H )
5 f1otrkg.e 
 |-  E = ( dist ` H )
6 f1otrkg.j 
 |-  J = ( Itv ` H )
7 f1otrkg.f 
 |-  ( ph -> F : B -1-1-onto-> P )
8 f1otrkg.1 
 |-  ( ( ph /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
9 f1otrkg.2 
 |-  ( ( ph /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )
10 f1otrg.h 
 |-  ( ph -> H e. V )
11 f1otrge.g 
 |-  ( ph -> G e. TarskiGE )
12 10 elexd 
 |-  ( ph -> H e. _V )
13 f1ocnv 
 |-  ( F : B -1-1-onto-> P -> `' F : P -1-1-onto-> B )
14 f1of 
 |-  ( `' F : P -1-1-onto-> B -> `' F : P --> B )
15 7 13 14 3syl 
 |-  ( ph -> `' F : P --> B )
16 15 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> `' F : P --> B )
17 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> c e. P )
18 16 17 ffvelcdmd 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( `' F ` c ) e. B )
19 simplr 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> d e. P )
20 16 19 ffvelcdmd 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( `' F ` d ) e. B )
21 simpr1 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( F ` y ) e. ( ( F ` x ) I c ) )
22 7 ad3antrrr 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> F : B -1-1-onto-> P )
23 22 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> F : B -1-1-onto-> P )
24 f1ocnvfv2 
 |-  ( ( F : B -1-1-onto-> P /\ c e. P ) -> ( F ` ( `' F ` c ) ) = c )
25 23 17 24 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( F ` ( `' F ` c ) ) = c )
26 25 oveq2d 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( ( F ` x ) I ( F ` ( `' F ` c ) ) ) = ( ( F ` x ) I c ) )
27 21 26 eleqtrrd 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( F ` y ) e. ( ( F ` x ) I ( F ` ( `' F ` c ) ) ) )
28 8 ad5ant15 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
29 28 ad5ant15 
 |-  ( ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
30 9 ad5ant15 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )
31 30 ad5ant15 
 |-  ( ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )
32 simprl 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> x e. B )
33 32 ad2antrr 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> x e. B )
34 33 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> x e. B )
35 simprr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> y e. B )
36 35 ad2antrr 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> y e. B )
37 36 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> y e. B )
38 1 2 3 4 5 6 23 29 31 34 18 37 f1otrgitv 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( y e. ( x J ( `' F ` c ) ) <-> ( F ` y ) e. ( ( F ` x ) I ( F ` ( `' F ` c ) ) ) ) )
39 27 38 mpbird 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> y e. ( x J ( `' F ` c ) ) )
40 simpr2 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( F ` z ) e. ( ( F ` x ) I d ) )
41 f1ocnvfv2 
 |-  ( ( F : B -1-1-onto-> P /\ d e. P ) -> ( F ` ( `' F ` d ) ) = d )
42 23 19 41 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( F ` ( `' F ` d ) ) = d )
43 42 oveq2d 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( ( F ` x ) I ( F ` ( `' F ` d ) ) ) = ( ( F ` x ) I d ) )
44 40 43 eleqtrrd 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( F ` z ) e. ( ( F ` x ) I ( F ` ( `' F ` d ) ) ) )
45 simplr1 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> z e. B )
46 45 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> z e. B )
47 1 2 3 4 5 6 23 29 31 34 20 46 f1otrgitv 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( z e. ( x J ( `' F ` d ) ) <-> ( F ` z ) e. ( ( F ` x ) I ( F ` ( `' F ` d ) ) ) ) )
48 44 47 mpbird 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> z e. ( x J ( `' F ` d ) ) )
49 simpr3 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( F ` v ) e. ( c I d ) )
50 25 42 oveq12d 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( ( F ` ( `' F ` c ) ) I ( F ` ( `' F ` d ) ) ) = ( c I d ) )
51 49 50 eleqtrrd 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( F ` v ) e. ( ( F ` ( `' F ` c ) ) I ( F ` ( `' F ` d ) ) ) )
52 simplr3 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> v e. B )
53 52 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> v e. B )
54 1 2 3 4 5 6 23 29 31 18 20 53 f1otrgitv 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> ( v e. ( ( `' F ` c ) J ( `' F ` d ) ) <-> ( F ` v ) e. ( ( F ` ( `' F ` c ) ) I ( F ` ( `' F ` d ) ) ) ) )
55 51 54 mpbird 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> v e. ( ( `' F ` c ) J ( `' F ` d ) ) )
56 oveq2 
 |-  ( a = ( `' F ` c ) -> ( x J a ) = ( x J ( `' F ` c ) ) )
57 56 eleq2d 
 |-  ( a = ( `' F ` c ) -> ( y e. ( x J a ) <-> y e. ( x J ( `' F ` c ) ) ) )
58 oveq1 
 |-  ( a = ( `' F ` c ) -> ( a J b ) = ( ( `' F ` c ) J b ) )
59 58 eleq2d 
 |-  ( a = ( `' F ` c ) -> ( v e. ( a J b ) <-> v e. ( ( `' F ` c ) J b ) ) )
60 57 59 3anbi13d 
 |-  ( a = ( `' F ` c ) -> ( ( y e. ( x J a ) /\ z e. ( x J b ) /\ v e. ( a J b ) ) <-> ( y e. ( x J ( `' F ` c ) ) /\ z e. ( x J b ) /\ v e. ( ( `' F ` c ) J b ) ) ) )
61 oveq2 
 |-  ( b = ( `' F ` d ) -> ( x J b ) = ( x J ( `' F ` d ) ) )
62 61 eleq2d 
 |-  ( b = ( `' F ` d ) -> ( z e. ( x J b ) <-> z e. ( x J ( `' F ` d ) ) ) )
63 oveq2 
 |-  ( b = ( `' F ` d ) -> ( ( `' F ` c ) J b ) = ( ( `' F ` c ) J ( `' F ` d ) ) )
64 63 eleq2d 
 |-  ( b = ( `' F ` d ) -> ( v e. ( ( `' F ` c ) J b ) <-> v e. ( ( `' F ` c ) J ( `' F ` d ) ) ) )
65 62 64 3anbi23d 
 |-  ( b = ( `' F ` d ) -> ( ( y e. ( x J ( `' F ` c ) ) /\ z e. ( x J b ) /\ v e. ( ( `' F ` c ) J b ) ) <-> ( y e. ( x J ( `' F ` c ) ) /\ z e. ( x J ( `' F ` d ) ) /\ v e. ( ( `' F ` c ) J ( `' F ` d ) ) ) ) )
66 60 65 rspc2ev 
 |-  ( ( ( `' F ` c ) e. B /\ ( `' F ` d ) e. B /\ ( y e. ( x J ( `' F ` c ) ) /\ z e. ( x J ( `' F ` d ) ) /\ v e. ( ( `' F ` c ) J ( `' F ` d ) ) ) ) -> E. a e. B E. b e. B ( y e. ( x J a ) /\ z e. ( x J b ) /\ v e. ( a J b ) ) )
67 18 20 39 48 55 66 syl113anc 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) /\ c e. P ) /\ d e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) ) -> E. a e. B E. b e. B ( y e. ( x J a ) /\ z e. ( x J b ) /\ v e. ( a J b ) ) )
68 11 ad3antrrr 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> G e. TarskiGE )
69 f1of 
 |-  ( F : B -1-1-onto-> P -> F : B --> P )
70 7 69 syl 
 |-  ( ph -> F : B --> P )
71 70 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> F : B --> P )
72 71 32 ffvelcdmd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` x ) e. P )
73 72 ad2antrr 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> ( F ` x ) e. P )
74 71 35 ffvelcdmd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` y ) e. P )
75 74 ad2antrr 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> ( F ` y ) e. P )
76 70 ad3antrrr 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> F : B --> P )
77 76 45 ffvelcdmd 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> ( F ` z ) e. P )
78 simplr2 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> u e. B )
79 76 78 ffvelcdmd 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> ( F ` u ) e. P )
80 76 52 ffvelcdmd 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> ( F ` v ) e. P )
81 simpr1 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> u e. ( x J v ) )
82 1 2 3 4 5 6 22 28 30 33 52 78 f1otrgitv 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> ( u e. ( x J v ) <-> ( F ` u ) e. ( ( F ` x ) I ( F ` v ) ) ) )
83 81 82 mpbid 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> ( F ` u ) e. ( ( F ` x ) I ( F ` v ) ) )
84 simpr2 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> u e. ( y J z ) )
85 1 2 3 4 5 6 22 28 30 36 45 78 f1otrgitv 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> ( u e. ( y J z ) <-> ( F ` u ) e. ( ( F ` y ) I ( F ` z ) ) ) )
86 84 85 mpbid 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> ( F ` u ) e. ( ( F ` y ) I ( F ` z ) ) )
87 simpr3 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> x =/= u )
88 dff1o6 
 |-  ( F : B -1-1-onto-> P <-> ( F Fn B /\ ran F = P /\ A. x e. B A. u e. B ( ( F ` x ) = ( F ` u ) -> x = u ) ) )
89 88 simp3bi 
 |-  ( F : B -1-1-onto-> P -> A. x e. B A. u e. B ( ( F ` x ) = ( F ` u ) -> x = u ) )
90 89 r19.21bi 
 |-  ( ( F : B -1-1-onto-> P /\ x e. B ) -> A. u e. B ( ( F ` x ) = ( F ` u ) -> x = u ) )
91 90 r19.21bi 
 |-  ( ( ( F : B -1-1-onto-> P /\ x e. B ) /\ u e. B ) -> ( ( F ` x ) = ( F ` u ) -> x = u ) )
92 91 necon3d 
 |-  ( ( ( F : B -1-1-onto-> P /\ x e. B ) /\ u e. B ) -> ( x =/= u -> ( F ` x ) =/= ( F ` u ) ) )
93 92 imp 
 |-  ( ( ( ( F : B -1-1-onto-> P /\ x e. B ) /\ u e. B ) /\ x =/= u ) -> ( F ` x ) =/= ( F ` u ) )
94 22 33 78 87 93 syl1111anc 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> ( F ` x ) =/= ( F ` u ) )
95 1 2 3 68 73 75 77 79 80 83 86 94 axtgeucl 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> E. c e. P E. d e. P ( ( F ` y ) e. ( ( F ` x ) I c ) /\ ( F ` z ) e. ( ( F ` x ) I d ) /\ ( F ` v ) e. ( c I d ) ) )
96 67 95 r19.29vva 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) ) -> E. a e. B E. b e. B ( y e. ( x J a ) /\ z e. ( x J b ) /\ v e. ( a J b ) ) )
97 96 ex 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) -> ( ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) -> E. a e. B E. b e. B ( y e. ( x J a ) /\ z e. ( x J b ) /\ v e. ( a J b ) ) ) )
98 97 ralrimivvva 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> A. z e. B A. u e. B A. v e. B ( ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) -> E. a e. B E. b e. B ( y e. ( x J a ) /\ z e. ( x J b ) /\ v e. ( a J b ) ) ) )
99 98 ralrimivva 
 |-  ( ph -> A. x e. B A. y e. B A. z e. B A. u e. B A. v e. B ( ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) -> E. a e. B E. b e. B ( y e. ( x J a ) /\ z e. ( x J b ) /\ v e. ( a J b ) ) ) )
100 4 5 6 istrkge 
 |-  ( H e. TarskiGE <-> ( H e. _V /\ A. x e. B A. y e. B A. z e. B A. u e. B A. v e. B ( ( u e. ( x J v ) /\ u e. ( y J z ) /\ x =/= u ) -> E. a e. B E. b e. B ( y e. ( x J a ) /\ z e. ( x J b ) /\ v e. ( a J b ) ) ) ) )
101 12 99 100 sylanbrc 
 |-  ( ph -> H e. TarskiGE )