Metamath Proof Explorer

Theorem f1otrg

Description: A bijection between bases which conserves distances and intervals conserves also geometries. (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 )
f1otrg.g 
|- ( ph -> G e. TarskiG )
f1otrg.l 
|- ( ph -> ( LineG ` H ) = ( x e. B , y e. ( B \ { x } ) |-> { z e. B | ( z e. ( x J y ) \/ x e. ( z J y ) \/ y e. ( x J z ) ) } ) )
Assertion f1otrg 
|- ( ph -> H e. TarskiG )

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 f1otrg.g 
 |-  ( ph -> G e. TarskiG )
12 f1otrg.l 
 |-  ( ph -> ( LineG ` H ) = ( x e. B , y e. ( B \ { x } ) |-> { z e. B | ( z e. ( x J y ) \/ x e. ( z J y ) \/ y e. ( x J z ) ) } ) )
13 10 elexd 
 |-  ( ph -> H e. _V )
14 11 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> G e. TarskiG )
15 f1of 
 |-  ( F : B -1-1-onto-> P -> F : B --> P )
16 7 15 syl 
 |-  ( ph -> F : B --> P )
17 16 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> F : B --> P )
18 simprl 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> x e. B )
19 17 18 ffvelcdmd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` x ) e. P )
20 simprr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> y e. B )
21 17 20 ffvelcdmd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` y ) e. P )
22 1 2 3 14 19 21 axtgcgrrflx 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( F ` x ) D ( F ` y ) ) = ( ( F ` y ) D ( F ` x ) ) )
23 7 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> F : B -1-1-onto-> P )
24 8 adantlr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
25 9 adantlr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )
26 1 2 3 4 5 6 23 24 25 18 20 f1otrgds 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x E y ) = ( ( F ` x ) D ( F ` y ) ) )
27 1 2 3 4 5 6 23 24 25 20 18 f1otrgds 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( y E x ) = ( ( F ` y ) D ( F ` x ) ) )
28 22 26 27 3eqtr4d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x E y ) = ( y E x ) )
29 28 ralrimivva 
 |-  ( ph -> A. x e. B A. y e. B ( x E y ) = ( y E x ) )
30 f1of1 
 |-  ( F : B -1-1-onto-> P -> F : B -1-1-> P )
31 7 30 syl 
 |-  ( ph -> F : B -1-1-> P )
32 31 3ad2ant1 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> F : B -1-1-> P )
33 simp21 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> x e. B )
34 simp22 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> y e. B )
35 33 34 jca 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( x e. B /\ y e. B ) )
36 11 3ad2ant1 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> G e. TarskiG )
37 16 3ad2ant1 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> F : B --> P )
38 37 33 ffvelcdmd 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( F ` x ) e. P )
39 37 34 ffvelcdmd 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( F ` y ) e. P )
40 simp23 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> z e. B )
41 37 40 ffvelcdmd 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( F ` z ) e. P )
42 simp3 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( x E y ) = ( z E z ) )
43 7 3ad2ant1 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> F : B -1-1-onto-> P )
44 8 3ad2antl1 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
45 9 3ad2antl1 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )
46 1 2 3 4 5 6 43 44 45 33 34 f1otrgds 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( x E y ) = ( ( F ` x ) D ( F ` y ) ) )
47 1 2 3 4 5 6 43 44 45 40 40 f1otrgds 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( z E z ) = ( ( F ` z ) D ( F ` z ) ) )
48 42 46 47 3eqtr3d 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( ( F ` x ) D ( F ` y ) ) = ( ( F ` z ) D ( F ` z ) ) )
49 1 2 3 36 38 39 41 48 axtgcgrid 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( F ` x ) = ( F ` y ) )
50 f1veqaeq 
 |-  ( ( F : B -1-1-> P /\ ( x e. B /\ y e. B ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
51 50 imp 
 |-  ( ( ( F : B -1-1-> P /\ ( x e. B /\ y e. B ) ) /\ ( F ` x ) = ( F ` y ) ) -> x = y )
52 32 35 49 51 syl21anc 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> x = y )
53 52 3expia 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x E y ) = ( z E z ) -> x = y ) )
54 53 ralrimivvva 
 |-  ( ph -> A. x e. B A. y e. B A. z e. B ( ( x E y ) = ( z E z ) -> x = y ) )
55 29 54 jca 
 |-  ( ph -> ( A. x e. B A. y e. B ( x E y ) = ( y E x ) /\ A. x e. B A. y e. B A. z e. B ( ( x E y ) = ( z E z ) -> x = y ) ) )
56 4 5 6 istrkgc 
 |-  ( H e. TarskiGC <-> ( H e. _V /\ ( A. x e. B A. y e. B ( x E y ) = ( y E x ) /\ A. x e. B A. y e. B A. z e. B ( ( x E y ) = ( z E z ) -> x = y ) ) ) )
57 13 55 56 sylanbrc 
 |-  ( ph -> H e. TarskiGC )
58 7 3ad2ant1 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> F : B -1-1-onto-> P )
59 58 30 syl 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> F : B -1-1-> P )
60 simp2 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> ( x e. B /\ y e. B ) )
61 11 3ad2ant1 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> G e. TarskiG )
62 19 3adant3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> ( F ` x ) e. P )
63 21 3adant3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> ( F ` y ) e. P )
64 simp3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> y e. ( x J x ) )
65 8 3ad2antl1 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
66 9 3ad2antl1 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )
67 18 3adant3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> x e. B )
68 20 3adant3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> y e. B )
69 1 2 3 4 5 6 58 65 66 67 67 68 f1otrgitv 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> ( y e. ( x J x ) <-> ( F ` y ) e. ( ( F ` x ) I ( F ` x ) ) ) )
70 64 69 mpbid 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> ( F ` y ) e. ( ( F ` x ) I ( F ` x ) ) )
71 1 2 3 61 62 63 70 axtgbtwnid 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> ( F ` x ) = ( F ` y ) )
72 59 60 71 51 syl21anc 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> x = y )
73 72 3expia 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( y e. ( x J x ) -> x = y ) )
74 73 ralrimivva 
 |-  ( ph -> A. x e. B A. y e. B ( y e. ( x J x ) -> x = y ) )
75 f1ocnv 
 |-  ( F : B -1-1-onto-> P -> `' F : P -1-1-onto-> B )
76 f1of 
 |-  ( `' F : P -1-1-onto-> B -> `' F : P --> B )
77 7 75 76 3syl 
 |-  ( ph -> `' F : P --> B )
78 77 ad5antr 
 |-  ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) -> `' F : P --> B )
79 simplr 
 |-  ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) -> c e. P )
80 78 79 ffvelcdmd 
 |-  ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) -> ( `' F ` c ) e. B )
81 simpr 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) /\ a = ( `' F ` c ) ) -> a = ( `' F ` c ) )
82 81 eleq1d 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) /\ a = ( `' F ` c ) ) -> ( a e. ( u J y ) <-> ( `' F ` c ) e. ( u J y ) ) )
83 81 eleq1d 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) /\ a = ( `' F ` c ) ) -> ( a e. ( v J x ) <-> ( `' F ` c ) e. ( v J x ) ) )
84 82 83 anbi12d 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) /\ a = ( `' F ` c ) ) -> ( ( a e. ( u J y ) /\ a e. ( v J x ) ) <-> ( ( `' F ` c ) e. ( u J y ) /\ ( `' F ` c ) e. ( v J x ) ) ) )
85 simprl 
 |-  ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) -> c e. ( ( F ` u ) I ( F ` y ) ) )
86 23 ad2antrr 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) -> F : B -1-1-onto-> P )
87 86 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) -> F : B -1-1-onto-> P )
88 f1ocnvfv2 
 |-  ( ( F : B -1-1-onto-> P /\ c e. P ) -> ( F ` ( `' F ` c ) ) = c )
89 88 eleq1d 
 |-  ( ( F : B -1-1-onto-> P /\ c e. P ) -> ( ( F ` ( `' F ` c ) ) e. ( ( F ` u ) I ( F ` y ) ) <-> c e. ( ( F ` u ) I ( F ` y ) ) ) )
90 87 79 89 syl2anc 
 |-  ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) -> ( ( F ` ( `' F ` c ) ) e. ( ( F ` u ) I ( F ` y ) ) <-> c e. ( ( F ` u ) I ( F ` y ) ) ) )
91 85 90 mpbird 
 |-  ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) -> ( F ` ( `' F ` c ) ) e. ( ( F ` u ) I ( F ` y ) ) )
92 24 ad4ant14 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
93 92 ad4ant14 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
94 25 ad4ant14 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )
95 94 ad4ant14 
 |-  ( ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )
96 simplr2 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) -> u e. B )
97 96 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) -> u e. B )
98 20 ad2antrr 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) -> y e. B )
99 98 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) -> y e. B )
100 1 2 3 4 5 6 87 93 95 97 99 80 f1otrgitv 
 |-  ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) -> ( ( `' F ` c ) e. ( u J y ) <-> ( F ` ( `' F ` c ) ) e. ( ( F ` u ) I ( F ` y ) ) ) )
101 91 100 mpbird 
 |-  ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) -> ( `' F ` c ) e. ( u J y ) )
102 simprr 
 |-  ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) -> c e. ( ( F ` v ) I ( F ` x ) ) )
103 88 eleq1d 
 |-  ( ( F : B -1-1-onto-> P /\ c e. P ) -> ( ( F ` ( `' F ` c ) ) e. ( ( F ` v ) I ( F ` x ) ) <-> c e. ( ( F ` v ) I ( F ` x ) ) ) )
104 87 79 103 syl2anc 
 |-  ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) -> ( ( F ` ( `' F ` c ) ) e. ( ( F ` v ) I ( F ` x ) ) <-> c e. ( ( F ` v ) I ( F ` x ) ) ) )
105 102 104 mpbird 
 |-  ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) -> ( F ` ( `' F ` c ) ) e. ( ( F ` v ) I ( F ` x ) ) )
106 simplr3 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) -> v e. B )
107 106 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) -> v e. B )
108 18 ad2antrr 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) -> x e. B )
109 108 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) -> x e. B )
110 1 2 3 4 5 6 87 93 95 107 109 80 f1otrgitv 
 |-  ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) -> ( ( `' F ` c ) e. ( v J x ) <-> ( F ` ( `' F ` c ) ) e. ( ( F ` v ) I ( F ` x ) ) ) )
111 105 110 mpbird 
 |-  ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) -> ( `' F ` c ) e. ( v J x ) )
112 101 111 jca 
 |-  ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) -> ( ( `' F ` c ) e. ( u J y ) /\ ( `' F ` c ) e. ( v J x ) ) )
113 80 84 112 rspcedvd 
 |-  ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) -> E. a e. B ( a e. ( u J y ) /\ a e. ( v J x ) ) )
114 14 ad2antrr 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) -> G e. TarskiG )
115 17 ad2antrr 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) -> F : B --> P )
116 115 108 ffvelcdmd 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) -> ( F ` x ) e. P )
117 115 98 ffvelcdmd 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) -> ( F ` y ) e. P )
118 simplr1 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) -> z e. B )
119 115 118 ffvelcdmd 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) -> ( F ` z ) e. P )
120 115 96 ffvelcdmd 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) -> ( F ` u ) e. P )
121 115 106 ffvelcdmd 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) -> ( F ` v ) e. P )
122 simprl 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) -> u e. ( x J z ) )
123 1 2 3 4 5 6 86 92 94 108 118 96 f1otrgitv 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) -> ( u e. ( x J z ) <-> ( F ` u ) e. ( ( F ` x ) I ( F ` z ) ) ) )
124 122 123 mpbid 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) -> ( F ` u ) e. ( ( F ` x ) I ( F ` z ) ) )
125 simprr 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) -> v e. ( y J z ) )
126 1 2 3 4 5 6 86 92 94 98 118 106 f1otrgitv 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) -> ( v e. ( y J z ) <-> ( F ` v ) e. ( ( F ` y ) I ( F ` z ) ) ) )
127 125 126 mpbid 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) -> ( F ` v ) e. ( ( F ` y ) I ( F ` z ) ) )
128 1 2 3 114 116 117 119 120 121 124 127 axtgpasch 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) -> E. c e. P ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) )
129 113 128 r19.29a 
 |-  ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) /\ ( u e. ( x J z ) /\ v e. ( y J z ) ) ) -> E. a e. B ( a e. ( u J y ) /\ a e. ( v J x ) ) )
130 129 ex 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( z e. B /\ u e. B /\ v e. B ) ) -> ( ( u e. ( x J z ) /\ v e. ( y J z ) ) -> E. a e. B ( a e. ( u J y ) /\ a e. ( v J x ) ) ) )
131 130 ralrimivvva 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> A. z e. B A. u e. B A. v e. B ( ( u e. ( x J z ) /\ v e. ( y J z ) ) -> E. a e. B ( a e. ( u J y ) /\ a e. ( v J x ) ) ) )
132 131 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 z ) /\ v e. ( y J z ) ) -> E. a e. B ( a e. ( u J y ) /\ a e. ( v J x ) ) ) )
133 7 ad5antr 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ A. e e. ( F " s ) A. f e. ( F " t ) c e. ( e I f ) ) /\ ( x e. s /\ y e. t ) ) -> F : B -1-1-onto-> P )
134 simpllr 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ A. e e. ( F " s ) A. f e. ( F " t ) c e. ( e I f ) ) /\ ( x e. s /\ y e. t ) ) -> c e. P )
135 133 134 88 syl2anc 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ A. e e. ( F " s ) A. f e. ( F " t ) c e. ( e I f ) ) /\ ( x e. s /\ y e. t ) ) -> ( F ` ( `' F ` c ) ) = c )
136 ffn 
 |-  ( F : B --> P -> F Fn B )
137 133 15 136 3syl 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ A. e e. ( F " s ) A. f e. ( F " t ) c e. ( e I f ) ) /\ ( x e. s /\ y e. t ) ) -> F Fn B )
138 simp-4r 
 |-  ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> ( s e. ~P B /\ t e. ~P B ) )
139 138 simpld 
 |-  ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> s e. ~P B )
140 139 elpwid 
 |-  ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> s C_ B )
141 140 adantlr 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ A. e e. ( F " s ) A. f e. ( F " t ) c e. ( e I f ) ) /\ ( x e. s /\ y e. t ) ) -> s C_ B )
142 simprl 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ A. e e. ( F " s ) A. f e. ( F " t ) c e. ( e I f ) ) /\ ( x e. s /\ y e. t ) ) -> x e. s )
143 fnfvima 
 |-  ( ( F Fn B /\ s C_ B /\ x e. s ) -> ( F ` x ) e. ( F " s ) )
144 137 141 142 143 syl3anc 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ A. e e. ( F " s ) A. f e. ( F " t ) c e. ( e I f ) ) /\ ( x e. s /\ y e. t ) ) -> ( F ` x ) e. ( F " s ) )
145 138 simprd 
 |-  ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> t e. ~P B )
146 145 elpwid 
 |-  ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> t C_ B )
147 146 adantlr 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ A. e e. ( F " s ) A. f e. ( F " t ) c e. ( e I f ) ) /\ ( x e. s /\ y e. t ) ) -> t C_ B )
148 simprr 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ A. e e. ( F " s ) A. f e. ( F " t ) c e. ( e I f ) ) /\ ( x e. s /\ y e. t ) ) -> y e. t )
149 fnfvima 
 |-  ( ( F Fn B /\ t C_ B /\ y e. t ) -> ( F ` y ) e. ( F " t ) )
150 137 147 148 149 syl3anc 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ A. e e. ( F " s ) A. f e. ( F " t ) c e. ( e I f ) ) /\ ( x e. s /\ y e. t ) ) -> ( F ` y ) e. ( F " t ) )
151 simplr 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ A. e e. ( F " s ) A. f e. ( F " t ) c e. ( e I f ) ) /\ ( x e. s /\ y e. t ) ) -> A. e e. ( F " s ) A. f e. ( F " t ) c e. ( e I f ) )
152 oveq1 
 |-  ( e = ( F ` x ) -> ( e I f ) = ( ( F ` x ) I f ) )
153 152 eleq2d 
 |-  ( e = ( F ` x ) -> ( c e. ( e I f ) <-> c e. ( ( F ` x ) I f ) ) )
154 oveq2 
 |-  ( f = ( F ` y ) -> ( ( F ` x ) I f ) = ( ( F ` x ) I ( F ` y ) ) )
155 154 eleq2d 
 |-  ( f = ( F ` y ) -> ( c e. ( ( F ` x ) I f ) <-> c e. ( ( F ` x ) I ( F ` y ) ) ) )
156 153 155 rspc2va 
 |-  ( ( ( ( F ` x ) e. ( F " s ) /\ ( F ` y ) e. ( F " t ) ) /\ A. e e. ( F " s ) A. f e. ( F " t ) c e. ( e I f ) ) -> c e. ( ( F ` x ) I ( F ` y ) ) )
157 144 150 151 156 syl21anc 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ A. e e. ( F " s ) A. f e. ( F " t ) c e. ( e I f ) ) /\ ( x e. s /\ y e. t ) ) -> c e. ( ( F ` x ) I ( F ` y ) ) )
158 135 157 eqeltrd 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ A. e e. ( F " s ) A. f e. ( F " t ) c e. ( e I f ) ) /\ ( x e. s /\ y e. t ) ) -> ( F ` ( `' F ` c ) ) e. ( ( F ` x ) I ( F ` y ) ) )
159 7 ad4antr 
 |-  ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> F : B -1-1-onto-> P )
160 simp-5l 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) /\ ( e e. B /\ f e. B ) ) -> ph )
161 160 8 sylancom 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
162 simp-5l 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ph )
163 162 9 sylancom 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )
164 simprl 
 |-  ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> x e. s )
165 140 164 sseldd 
 |-  ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> x e. B )
166 simprr 
 |-  ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> y e. t )
167 146 166 sseldd 
 |-  ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> y e. B )
168 77 ad4antr 
 |-  ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> `' F : P --> B )
169 simplr 
 |-  ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> c e. P )
170 168 169 ffvelcdmd 
 |-  ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> ( `' F ` c ) e. B )
171 1 2 3 4 5 6 159 161 163 165 167 170 f1otrgitv 
 |-  ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> ( ( `' F ` c ) e. ( x J y ) <-> ( F ` ( `' F ` c ) ) e. ( ( F ` x ) I ( F ` y ) ) ) )
172 171 adantlr 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ A. e e. ( F " s ) A. f e. ( F " t ) c e. ( e I f ) ) /\ ( x e. s /\ y e. t ) ) -> ( ( `' F ` c ) e. ( x J y ) <-> ( F ` ( `' F ` c ) ) e. ( ( F ` x ) I ( F ` y ) ) ) )
173 158 172 mpbird 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ A. e e. ( F " s ) A. f e. ( F " t ) c e. ( e I f ) ) /\ ( x e. s /\ y e. t ) ) -> ( `' F ` c ) e. ( x J y ) )
174 173 ralrimivva 
 |-  ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ A. e e. ( F " s ) A. f e. ( F " t ) c e. ( e I f ) ) -> A. x e. s A. y e. t ( `' F ` c ) e. ( x J y ) )
175 174 adantllr 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ c e. P ) /\ A. e e. ( F " s ) A. f e. ( F " t ) c e. ( e I f ) ) -> A. x e. s A. y e. t ( `' F ` c ) e. ( x J y ) )
176 77 ad4antr 
 |-  ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ c e. P ) -> `' F : P --> B )
177 simpr 
 |-  ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ c e. P ) -> c e. P )
178 176 177 ffvelcdmd 
 |-  ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ c e. P ) -> ( `' F ` c ) e. B )
179 eleq1 
 |-  ( b = ( `' F ` c ) -> ( b e. ( x J y ) <-> ( `' F ` c ) e. ( x J y ) ) )
180 179 2ralbidv 
 |-  ( b = ( `' F ` c ) -> ( A. x e. s A. y e. t b e. ( x J y ) <-> A. x e. s A. y e. t ( `' F ` c ) e. ( x J y ) ) )
181 180 adantl 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ c e. P ) /\ b = ( `' F ` c ) ) -> ( A. x e. s A. y e. t b e. ( x J y ) <-> A. x e. s A. y e. t ( `' F ` c ) e. ( x J y ) ) )
182 178 181 rspcedv 
 |-  ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ c e. P ) -> ( A. x e. s A. y e. t ( `' F ` c ) e. ( x J y ) -> E. b e. B A. x e. s A. y e. t b e. ( x J y ) ) )
183 182 adantr 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ c e. P ) /\ A. e e. ( F " s ) A. f e. ( F " t ) c e. ( e I f ) ) -> ( A. x e. s A. y e. t ( `' F ` c ) e. ( x J y ) -> E. b e. B A. x e. s A. y e. t b e. ( x J y ) ) )
184 175 183 mpd 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ c e. P ) /\ A. e e. ( F " s ) A. f e. ( F " t ) c e. ( e I f ) ) -> E. b e. B A. x e. s A. y e. t b e. ( x J y ) )
185 11 ad3antrrr 
 |-  ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) -> G e. TarskiG )
186 imassrn 
 |-  ( F " s ) C_ ran F
187 f1ofo 
 |-  ( F : B -1-1-onto-> P -> F : B -onto-> P )
188 forn 
 |-  ( F : B -onto-> P -> ran F = P )
189 7 187 188 3syl 
 |-  ( ph -> ran F = P )
190 189 ad3antrrr 
 |-  ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) -> ran F = P )
191 186 190 sseqtrid 
 |-  ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) -> ( F " s ) C_ P )
192 imassrn 
 |-  ( F " t ) C_ ran F
193 192 190 sseqtrid 
 |-  ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) -> ( F " t ) C_ P )
194 16 ad3antrrr 
 |-  ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) -> F : B --> P )
195 simplr 
 |-  ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) -> a e. B )
196 194 195 ffvelcdmd 
 |-  ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) -> ( F ` a ) e. P )
197 7 ad5antr 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> F : B -1-1-onto-> P )
198 ffn 
 |-  ( `' F : P --> B -> `' F Fn P )
199 197 75 76 198 4syl 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> `' F Fn P )
200 191 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> ( F " s ) C_ P )
201 simplr 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> u e. ( F " s ) )
202 fnfvima 
 |-  ( ( `' F Fn P /\ ( F " s ) C_ P /\ u e. ( F " s ) ) -> ( `' F ` u ) e. ( `' F " ( F " s ) ) )
203 199 200 201 202 syl3anc 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> ( `' F ` u ) e. ( `' F " ( F " s ) ) )
204 197 30 syl 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> F : B -1-1-> P )
205 simp-5r 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> ( s e. ~P B /\ t e. ~P B ) )
206 205 simpld 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> s e. ~P B )
207 206 elpwid 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> s C_ B )
208 f1imacnv 
 |-  ( ( F : B -1-1-> P /\ s C_ B ) -> ( `' F " ( F " s ) ) = s )
209 204 207 208 syl2anc 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> ( `' F " ( F " s ) ) = s )
210 203 209 eleqtrd 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> ( `' F ` u ) e. s )
211 193 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> ( F " t ) C_ P )
212 simpr 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> v e. ( F " t ) )
213 fnfvima 
 |-  ( ( `' F Fn P /\ ( F " t ) C_ P /\ v e. ( F " t ) ) -> ( `' F ` v ) e. ( `' F " ( F " t ) ) )
214 199 211 212 213 syl3anc 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> ( `' F ` v ) e. ( `' F " ( F " t ) ) )
215 205 simprd 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> t e. ~P B )
216 215 elpwid 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> t C_ B )
217 f1imacnv 
 |-  ( ( F : B -1-1-> P /\ t C_ B ) -> ( `' F " ( F " t ) ) = t )
218 204 216 217 syl2anc 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> ( `' F " ( F " t ) ) = t )
219 214 218 eleqtrd 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> ( `' F ` v ) e. t )
220 simpllr 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> A. x e. s A. y e. t x e. ( a J y ) )
221 eleq1 
 |-  ( x = ( `' F ` u ) -> ( x e. ( a J y ) <-> ( `' F ` u ) e. ( a J y ) ) )
222 oveq2 
 |-  ( y = ( `' F ` v ) -> ( a J y ) = ( a J ( `' F ` v ) ) )
223 222 eleq2d 
 |-  ( y = ( `' F ` v ) -> ( ( `' F ` u ) e. ( a J y ) <-> ( `' F ` u ) e. ( a J ( `' F ` v ) ) ) )
224 221 223 rspc2va 
 |-  ( ( ( ( `' F ` u ) e. s /\ ( `' F ` v ) e. t ) /\ A. x e. s A. y e. t x e. ( a J y ) ) -> ( `' F ` u ) e. ( a J ( `' F ` v ) ) )
225 210 219 220 224 syl21anc 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> ( `' F ` u ) e. ( a J ( `' F ` v ) ) )
226 simp-6l 
 |-  ( ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) /\ ( e e. B /\ f e. B ) ) -> ph )
227 226 8 sylancom 
 |-  ( ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
228 simp-6l 
 |-  ( ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ph )
229 228 9 sylancom 
 |-  ( ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )
230 simp-4r 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> a e. B )
231 211 212 sseldd 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> v e. P )
232 f1ocnvdm 
 |-  ( ( F : B -1-1-onto-> P /\ v e. P ) -> ( `' F ` v ) e. B )
233 197 231 232 syl2anc 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> ( `' F ` v ) e. B )
234 200 201 sseldd 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> u e. P )
235 f1ocnvdm 
 |-  ( ( F : B -1-1-onto-> P /\ u e. P ) -> ( `' F ` u ) e. B )
236 197 234 235 syl2anc 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> ( `' F ` u ) e. B )
237 1 2 3 4 5 6 197 227 229 230 233 236 f1otrgitv 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> ( ( `' F ` u ) e. ( a J ( `' F ` v ) ) <-> ( F ` ( `' F ` u ) ) e. ( ( F ` a ) I ( F ` ( `' F ` v ) ) ) ) )
238 225 237 mpbid 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> ( F ` ( `' F ` u ) ) e. ( ( F ` a ) I ( F ` ( `' F ` v ) ) ) )
239 f1ocnvfv2 
 |-  ( ( F : B -1-1-onto-> P /\ u e. P ) -> ( F ` ( `' F ` u ) ) = u )
240 197 234 239 syl2anc 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> ( F ` ( `' F ` u ) ) = u )
241 f1ocnvfv2 
 |-  ( ( F : B -1-1-onto-> P /\ v e. P ) -> ( F ` ( `' F ` v ) ) = v )
242 197 231 241 syl2anc 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> ( F ` ( `' F ` v ) ) = v )
243 242 oveq2d 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> ( ( F ` a ) I ( F ` ( `' F ` v ) ) ) = ( ( F ` a ) I v ) )
244 238 240 243 3eltr3d 
 |-  ( ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) ) /\ v e. ( F " t ) ) -> u e. ( ( F ` a ) I v ) )
245 244 3impa 
 |-  ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) /\ u e. ( F " s ) /\ v e. ( F " t ) ) -> u e. ( ( F ` a ) I v ) )
246 1 2 3 185 191 193 196 245 axtgcont 
 |-  ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) -> E. c e. P A. e e. ( F " s ) A. f e. ( F " t ) c e. ( e I f ) )
247 184 246 r19.29a 
 |-  ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ A. x e. s A. y e. t x e. ( a J y ) ) -> E. b e. B A. x e. s A. y e. t b e. ( x J y ) )
248 247 rexlimdva2 
 |-  ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( E. a e. B A. x e. s A. y e. t x e. ( a J y ) -> E. b e. B A. x e. s A. y e. t b e. ( x J y ) ) )
249 248 ralrimivva 
 |-  ( ph -> A. s e. ~P B A. t e. ~P B ( E. a e. B A. x e. s A. y e. t x e. ( a J y ) -> E. b e. B A. x e. s A. y e. t b e. ( x J y ) ) )
250 74 132 249 3jca 
 |-  ( ph -> ( A. x e. B A. y e. B ( y e. ( x J x ) -> x = y ) /\ A. x e. B A. y e. B A. z e. B A. u e. B A. v e. B ( ( u e. ( x J z ) /\ v e. ( y J z ) ) -> E. a e. B ( a e. ( u J y ) /\ a e. ( v J x ) ) ) /\ A. s e. ~P B A. t e. ~P B ( E. a e. B A. x e. s A. y e. t x e. ( a J y ) -> E. b e. B A. x e. s A. y e. t b e. ( x J y ) ) ) )
251 4 5 6 istrkgb 
 |-  ( H e. TarskiGB <-> ( H e. _V /\ ( A. x e. B A. y e. B ( y e. ( x J x ) -> x = y ) /\ A. x e. B A. y e. B A. z e. B A. u e. B A. v e. B ( ( u e. ( x J z ) /\ v e. ( y J z ) ) -> E. a e. B ( a e. ( u J y ) /\ a e. ( v J x ) ) ) /\ A. s e. ~P B A. t e. ~P B ( E. a e. B A. x e. s A. y e. t x e. ( a J y ) -> E. b e. B A. x e. s A. y e. t b e. ( x J y ) ) ) ) )
252 13 250 251 sylanbrc 
 |-  ( ph -> H e. TarskiGB )
253 57 252 elind 
 |-  ( ph -> H e. ( TarskiGC i^i TarskiGB ) )
254 11 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> G e. TarskiG )
255 16 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> F : B --> P )
256 simp-9r 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> x e. B )
257 255 256 ffvelcdmd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( F ` x ) e. P )
258 simp-8r 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> y e. B )
259 255 258 ffvelcdmd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( F ` y ) e. P )
260 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> z e. B )
261 255 260 ffvelcdmd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( F ` z ) e. P )
262 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> a e. B )
263 255 262 ffvelcdmd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( F ` a ) e. P )
264 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> b e. B )
265 255 264 ffvelcdmd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( F ` b ) e. P )
266 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> c e. B )
267 255 266 ffvelcdmd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( F ` c ) e. P )
268 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> u e. B )
269 255 268 ffvelcdmd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( F ` u ) e. P )
270 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> v e. B )
271 255 270 ffvelcdmd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( F ` v ) e. P )
272 7 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> F : B -1-1-onto-> P )
273 272 256 jca 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( F : B -1-1-onto-> P /\ x e. B ) )
274 simprl1 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> x =/= y )
275 dff1o6 
 |-  ( F : B -1-1-onto-> P <-> ( F Fn B /\ ran F = P /\ A. x e. B A. y e. B ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
276 275 simp3bi 
 |-  ( F : B -1-1-onto-> P -> A. x e. B A. y e. B ( ( F ` x ) = ( F ` y ) -> x = y ) )
277 276 r19.21bi 
 |-  ( ( F : B -1-1-onto-> P /\ x e. B ) -> A. y e. B ( ( F ` x ) = ( F ` y ) -> x = y ) )
278 277 r19.21bi 
 |-  ( ( ( F : B -1-1-onto-> P /\ x e. B ) /\ y e. B ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
279 278 necon3d 
 |-  ( ( ( F : B -1-1-onto-> P /\ x e. B ) /\ y e. B ) -> ( x =/= y -> ( F ` x ) =/= ( F ` y ) ) )
280 279 imp 
 |-  ( ( ( ( F : B -1-1-onto-> P /\ x e. B ) /\ y e. B ) /\ x =/= y ) -> ( F ` x ) =/= ( F ` y ) )
281 273 258 274 280 syl21anc 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( F ` x ) =/= ( F ` y ) )
282 simprl2 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> y e. ( x J z ) )
283 8 ex 
 |-  ( ph -> ( ( e e. B /\ f e. B ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) ) )
284 283 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( ( e e. B /\ f e. B ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) ) )
285 284 imp 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
286 9 ex 
 |-  ( ph -> ( ( e e. B /\ f e. B /\ g e. B ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) ) )
287 286 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( ( e e. B /\ f e. B /\ g e. B ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) ) )
288 287 imp 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )
289 1 2 3 4 5 6 272 285 288 256 260 258 f1otrgitv 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( y e. ( x J z ) <-> ( F ` y ) e. ( ( F ` x ) I ( F ` z ) ) ) )
290 282 289 mpbid 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( F ` y ) e. ( ( F ` x ) I ( F ` z ) ) )
291 simprl3 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> b e. ( a J c ) )
292 1 2 3 4 5 6 272 285 288 262 266 264 f1otrgitv 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( b e. ( a J c ) <-> ( F ` b ) e. ( ( F ` a ) I ( F ` c ) ) ) )
293 291 292 mpbid 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( F ` b ) e. ( ( F ` a ) I ( F ` c ) ) )
294 simprr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) )
295 294 simpld 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) )
296 295 simpld 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( x E y ) = ( a E b ) )
297 1 2 3 4 5 6 272 285 288 256 258 f1otrgds 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( x E y ) = ( ( F ` x ) D ( F ` y ) ) )
298 1 2 3 4 5 6 272 285 288 262 264 f1otrgds 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( a E b ) = ( ( F ` a ) D ( F ` b ) ) )
299 296 297 298 3eqtr3d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( ( F ` x ) D ( F ` y ) ) = ( ( F ` a ) D ( F ` b ) ) )
300 295 simprd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( y E z ) = ( b E c ) )
301 1 2 3 4 5 6 272 285 288 258 260 f1otrgds 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( y E z ) = ( ( F ` y ) D ( F ` z ) ) )
302 1 2 3 4 5 6 272 285 288 264 266 f1otrgds 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( b E c ) = ( ( F ` b ) D ( F ` c ) ) )
303 300 301 302 3eqtr3d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( ( F ` y ) D ( F ` z ) ) = ( ( F ` b ) D ( F ` c ) ) )
304 294 simprd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) )
305 304 simpld 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( x E u ) = ( a E v ) )
306 1 2 3 4 5 6 272 285 288 256 268 f1otrgds 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( x E u ) = ( ( F ` x ) D ( F ` u ) ) )
307 1 2 3 4 5 6 272 285 288 262 270 f1otrgds 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( a E v ) = ( ( F ` a ) D ( F ` v ) ) )
308 305 306 307 3eqtr3d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( ( F ` x ) D ( F ` u ) ) = ( ( F ` a ) D ( F ` v ) ) )
309 304 simprd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( y E u ) = ( b E v ) )
310 1 2 3 4 5 6 272 285 288 258 268 f1otrgds 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( y E u ) = ( ( F ` y ) D ( F ` u ) ) )
311 1 2 3 4 5 6 272 285 288 264 270 f1otrgds 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( b E v ) = ( ( F ` b ) D ( F ` v ) ) )
312 309 310 311 3eqtr3d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( ( F ` y ) D ( F ` u ) ) = ( ( F ` b ) D ( F ` v ) ) )
313 1 2 3 254 257 259 261 263 265 267 269 271 281 290 293 299 303 308 312 axtg5seg 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( ( F ` z ) D ( F ` u ) ) = ( ( F ` c ) D ( F ` v ) ) )
314 1 2 3 4 5 6 272 285 288 260 268 f1otrgds 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( z E u ) = ( ( F ` z ) D ( F ` u ) ) )
315 1 2 3 4 5 6 272 285 288 266 270 f1otrgds 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( c E v ) = ( ( F ` c ) D ( F ` v ) ) )
316 313 314 315 3eqtr4d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) /\ ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) ) -> ( z E u ) = ( c E v ) )
317 316 ex 
 |-  ( ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) /\ v e. B ) -> ( ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) -> ( z E u ) = ( c E v ) ) )
318 317 ralrimiva 
 |-  ( ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) /\ c e. B ) -> A. v e. B ( ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) -> ( z E u ) = ( c E v ) ) )
319 318 ralrimiva 
 |-  ( ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) /\ b e. B ) -> A. c e. B A. v e. B ( ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) -> ( z E u ) = ( c E v ) ) )
320 319 ralrimiva 
 |-  ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) /\ a e. B ) -> A. b e. B A. c e. B A. v e. B ( ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) -> ( z E u ) = ( c E v ) ) )
321 320 ralrimiva 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) /\ u e. B ) -> A. a e. B A. b e. B A. c e. B A. v e. B ( ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) -> ( z E u ) = ( c E v ) ) )
322 321 ralrimiva 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ z e. B ) -> A. u e. B A. a e. B A. b e. B A. c e. B A. v e. B ( ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) -> ( z E u ) = ( c E v ) ) )
323 322 ralrimiva 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> A. z e. B A. u e. B A. a e. B A. b e. B A. c e. B A. v e. B ( ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) -> ( z E u ) = ( c E v ) ) )
324 323 ralrimiva 
 |-  ( ( ph /\ x e. B ) -> A. y e. B A. z e. B A. u e. B A. a e. B A. b e. B A. c e. B A. v e. B ( ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) -> ( z E u ) = ( c E v ) ) )
325 324 ralrimiva 
 |-  ( ph -> A. x e. B A. y e. B A. z e. B A. u e. B A. a e. B A. b e. B A. c e. B A. v e. B ( ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) -> ( z E u ) = ( c E v ) ) )
326 simp-4l 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) /\ w e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I w ) /\ ( ( F ` y ) D w ) = ( ( F ` a ) D ( F ` b ) ) ) ) -> ph )
327 simplr 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) /\ w e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I w ) /\ ( ( F ` y ) D w ) = ( ( F ` a ) D ( F ` b ) ) ) ) -> w e. P )
328 simprl 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) /\ w e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I w ) /\ ( ( F ` y ) D w ) = ( ( F ` a ) D ( F ` b ) ) ) ) -> ( F ` y ) e. ( ( F ` x ) I w ) )
329 326 7 syl 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) /\ w e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I w ) /\ ( ( F ` y ) D w ) = ( ( F ` a ) D ( F ` b ) ) ) ) -> F : B -1-1-onto-> P )
330 f1ocnvfv2 
 |-  ( ( F : B -1-1-onto-> P /\ w e. P ) -> ( F ` ( `' F ` w ) ) = w )
331 329 327 330 syl2anc 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) /\ w e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I w ) /\ ( ( F ` y ) D w ) = ( ( F ` a ) D ( F ` b ) ) ) ) -> ( F ` ( `' F ` w ) ) = w )
332 331 oveq2d 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) /\ w e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I w ) /\ ( ( F ` y ) D w ) = ( ( F ` a ) D ( F ` b ) ) ) ) -> ( ( F ` x ) I ( F ` ( `' F ` w ) ) ) = ( ( F ` x ) I w ) )
333 328 332 eleqtrrd 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) /\ w e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I w ) /\ ( ( F ` y ) D w ) = ( ( F ` a ) D ( F ` b ) ) ) ) -> ( F ` y ) e. ( ( F ` x ) I ( F ` ( `' F ` w ) ) ) )
334 326 8 sylan 
 |-  ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) /\ w e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I w ) /\ ( ( F ` y ) D w ) = ( ( F ` a ) D ( F ` b ) ) ) ) /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
335 326 9 sylan 
 |-  ( ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) /\ w e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I w ) /\ ( ( F ` y ) D w ) = ( ( F ` a ) D ( F ` b ) ) ) ) /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )
336 18 ad3antrrr 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) /\ w e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I w ) /\ ( ( F ` y ) D w ) = ( ( F ` a ) D ( F ` b ) ) ) ) -> x e. B )
337 77 ffvelcdmda 
 |-  ( ( ph /\ w e. P ) -> ( `' F ` w ) e. B )
338 326 327 337 syl2anc 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) /\ w e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I w ) /\ ( ( F ` y ) D w ) = ( ( F ` a ) D ( F ` b ) ) ) ) -> ( `' F ` w ) e. B )
339 20 ad3antrrr 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) /\ w e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I w ) /\ ( ( F ` y ) D w ) = ( ( F ` a ) D ( F ` b ) ) ) ) -> y e. B )
340 1 2 3 4 5 6 329 334 335 336 338 339 f1otrgitv 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) /\ w e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I w ) /\ ( ( F ` y ) D w ) = ( ( F ` a ) D ( F ` b ) ) ) ) -> ( y e. ( x J ( `' F ` w ) ) <-> ( F ` y ) e. ( ( F ` x ) I ( F ` ( `' F ` w ) ) ) ) )
341 333 340 mpbird 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) /\ w e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I w ) /\ ( ( F ` y ) D w ) = ( ( F ` a ) D ( F ` b ) ) ) ) -> y e. ( x J ( `' F ` w ) ) )
342 1 2 3 4 5 6 329 334 335 339 338 f1otrgds 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) /\ w e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I w ) /\ ( ( F ` y ) D w ) = ( ( F ` a ) D ( F ` b ) ) ) ) -> ( y E ( `' F ` w ) ) = ( ( F ` y ) D ( F ` ( `' F ` w ) ) ) )
343 331 oveq2d 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) /\ w e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I w ) /\ ( ( F ` y ) D w ) = ( ( F ` a ) D ( F ` b ) ) ) ) -> ( ( F ` y ) D ( F ` ( `' F ` w ) ) ) = ( ( F ` y ) D w ) )
344 simprr 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) /\ w e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I w ) /\ ( ( F ` y ) D w ) = ( ( F ` a ) D ( F ` b ) ) ) ) -> ( ( F ` y ) D w ) = ( ( F ` a ) D ( F ` b ) ) )
345 342 343 344 3eqtrd 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) /\ w e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I w ) /\ ( ( F ` y ) D w ) = ( ( F ` a ) D ( F ` b ) ) ) ) -> ( y E ( `' F ` w ) ) = ( ( F ` a ) D ( F ` b ) ) )
346 simprl 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) -> a e. B )
347 346 ad2antrr 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) /\ w e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I w ) /\ ( ( F ` y ) D w ) = ( ( F ` a ) D ( F ` b ) ) ) ) -> a e. B )
348 simprr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) -> b e. B )
349 348 ad2antrr 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) /\ w e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I w ) /\ ( ( F ` y ) D w ) = ( ( F ` a ) D ( F ` b ) ) ) ) -> b e. B )
350 1 2 3 4 5 6 329 334 335 347 349 f1otrgds 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) /\ w e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I w ) /\ ( ( F ` y ) D w ) = ( ( F ` a ) D ( F ` b ) ) ) ) -> ( a E b ) = ( ( F ` a ) D ( F ` b ) ) )
351 345 350 eqtr4d 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) /\ w e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I w ) /\ ( ( F ` y ) D w ) = ( ( F ` a ) D ( F ` b ) ) ) ) -> ( y E ( `' F ` w ) ) = ( a E b ) )
352 oveq2 
 |-  ( z = ( `' F ` w ) -> ( x J z ) = ( x J ( `' F ` w ) ) )
353 352 eleq2d 
 |-  ( z = ( `' F ` w ) -> ( y e. ( x J z ) <-> y e. ( x J ( `' F ` w ) ) ) )
354 oveq2 
 |-  ( z = ( `' F ` w ) -> ( y E z ) = ( y E ( `' F ` w ) ) )
355 354 eqeq1d 
 |-  ( z = ( `' F ` w ) -> ( ( y E z ) = ( a E b ) <-> ( y E ( `' F ` w ) ) = ( a E b ) ) )
356 353 355 anbi12d 
 |-  ( z = ( `' F ` w ) -> ( ( y e. ( x J z ) /\ ( y E z ) = ( a E b ) ) <-> ( y e. ( x J ( `' F ` w ) ) /\ ( y E ( `' F ` w ) ) = ( a E b ) ) ) )
357 356 adantl 
 |-  ( ( ( ph /\ w e. P ) /\ z = ( `' F ` w ) ) -> ( ( y e. ( x J z ) /\ ( y E z ) = ( a E b ) ) <-> ( y e. ( x J ( `' F ` w ) ) /\ ( y E ( `' F ` w ) ) = ( a E b ) ) ) )
358 337 357 rspcedv 
 |-  ( ( ph /\ w e. P ) -> ( ( y e. ( x J ( `' F ` w ) ) /\ ( y E ( `' F ` w ) ) = ( a E b ) ) -> E. z e. B ( y e. ( x J z ) /\ ( y E z ) = ( a E b ) ) ) )
359 358 imp 
 |-  ( ( ( ph /\ w e. P ) /\ ( y e. ( x J ( `' F ` w ) ) /\ ( y E ( `' F ` w ) ) = ( a E b ) ) ) -> E. z e. B ( y e. ( x J z ) /\ ( y E z ) = ( a E b ) ) )
360 326 327 341 351 359 syl22anc 
 |-  ( ( ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) /\ w e. P ) /\ ( ( F ` y ) e. ( ( F ` x ) I w ) /\ ( ( F ` y ) D w ) = ( ( F ` a ) D ( F ` b ) ) ) ) -> E. z e. B ( y e. ( x J z ) /\ ( y E z ) = ( a E b ) ) )
361 14 adantr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) -> G e. TarskiG )
362 19 adantr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) -> ( F ` x ) e. P )
363 21 adantr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) -> ( F ` y ) e. P )
364 17 adantr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) -> F : B --> P )
365 364 346 ffvelcdmd 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) -> ( F ` a ) e. P )
366 364 348 ffvelcdmd 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) -> ( F ` b ) e. P )
367 1 2 3 361 362 363 365 366 axtgsegcon 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) -> E. w e. P ( ( F ` y ) e. ( ( F ` x ) I w ) /\ ( ( F ` y ) D w ) = ( ( F ` a ) D ( F ` b ) ) ) )
368 360 367 r19.29a 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) -> E. z e. B ( y e. ( x J z ) /\ ( y E z ) = ( a E b ) ) )
369 368 ralrimivva 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> A. a e. B A. b e. B E. z e. B ( y e. ( x J z ) /\ ( y E z ) = ( a E b ) ) )
370 369 ralrimivva 
 |-  ( ph -> A. x e. B A. y e. B A. a e. B A. b e. B E. z e. B ( y e. ( x J z ) /\ ( y E z ) = ( a E b ) ) )
371 13 325 370 jca32 
 |-  ( ph -> ( H e. _V /\ ( A. x e. B A. y e. B A. z e. B A. u e. B A. a e. B A. b e. B A. c e. B A. v e. B ( ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) -> ( z E u ) = ( c E v ) ) /\ A. x e. B A. y e. B A. a e. B A. b e. B E. z e. B ( y e. ( x J z ) /\ ( y E z ) = ( a E b ) ) ) ) )
372 4 5 6 istrkgcb 
 |-  ( H e. TarskiGCB <-> ( H e. _V /\ ( A. x e. B A. y e. B A. z e. B A. u e. B A. a e. B A. b e. B A. c e. B A. v e. B ( ( ( x =/= y /\ y e. ( x J z ) /\ b e. ( a J c ) ) /\ ( ( ( x E y ) = ( a E b ) /\ ( y E z ) = ( b E c ) ) /\ ( ( x E u ) = ( a E v ) /\ ( y E u ) = ( b E v ) ) ) ) -> ( z E u ) = ( c E v ) ) /\ A. x e. B A. y e. B A. a e. B A. b e. B E. z e. B ( y e. ( x J z ) /\ ( y E z ) = ( a E b ) ) ) ) )
373 371 372 sylibr 
 |-  ( ph -> H e. TarskiGCB )
374 4 5 6 istrkgl 
 |-  ( H e. { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } <-> ( H e. _V /\ ( LineG ` H ) = ( x e. B , y e. ( B \ { x } ) |-> { z e. B | ( z e. ( x J y ) \/ x e. ( z J y ) \/ y e. ( x J z ) ) } ) ) )
375 13 12 374 sylanbrc 
 |-  ( ph -> H e. { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } )
376 373 375 elind 
 |-  ( ph -> H e. ( TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } ) )
377 253 376 elind 
 |-  ( ph -> H e. ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } ) ) )
378 df-trkg 
 |-  TarskiG = ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } ) )
379 377 378 eleqtrrdi 
 |-  ( ph -> H e. TarskiG )