MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1otrg Structured version   Visualization version   Unicode version
Theorem f1otrg 25751
Description: A bijection between bases which conserves distances and intervals conserves also geometries. (Contributed by Thierry Arnoux, 23-Mar-2019.)
Hypotheses
Ref Expression
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
Ref Expression
f1otrg |- ( ph -> H e. TarskiG )
Distinct variable groups:   e, f, g, x, y, z, B   D, e, f, g   e, E, f, g, x, y, z   e, F, f, g, x, y, z   e, I, f, g, x, y   e, J, f, g, x, y, z   P, e, f, g, x, y, z   ph, e, f, g, x, y, z   f, H
Allowed substitution hints:   D( x, y, z)   G( x, y, z, e, f, g)   H( x, y, z, e, g)   I( z)   V( x, y, z, e, f, g)
Proof of Theorem f1otrg
Dummy variables a b c i p s t u v w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1otrg.h . . . . . 6 |- ( ph -> H e. V )
2 elex 3212 . . . . . 6 |- ( H e. V -> H e. _V )
31, 2syl 17 . . . . 5 |- ( ph -> H e. _V )
4 f1otrkg.p . . . . . . . . 9 |- P = ( Base ` G )
5 f1otrkg.d . . . . . . . . 9 |- D = ( dist ` G )
6 f1otrkg.i . . . . . . . . 9 |- I = (Itv ` G )
7 f1otrg.g . . . . . . . . . 10 |- ( ph -> G e. TarskiG )
87adantr 481 . . . . . . . . 9 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> G e. TarskiG )
9 f1otrkg.f . . . . . . . . . . . 12 |- ( ph -> F : B -1-1-onto-> P )
10 f1of 6137 . . . . . . . . . . . 12 |- ( F : B -1-1-onto-> P -> F : B --> P )
119, 10syl 17 . . . . . . . . . . 11 |- ( ph -> F : B --> P )
1211adantr 481 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> F : B --> P )
13 simprl 794 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> x e. B )
1412, 13ffvelrnd 6360 . . . . . . . . 9 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` x ) e. P )
15 simprr 796 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> y e. B )
1612, 15ffvelrnd 6360 . . . . . . . . 9 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` y ) e. P )
174, 5, 6, 8, 14, 16axtgcgrrflx 25361 . . . . . . . 8 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( F ` x ) D ( F ` y ) ) = ( ( F ` y ) D ( F ` x ) ) )
18 f1otrkg.b . . . . . . . . 9 |- B = ( Base ` H )
19 f1otrkg.e . . . . . . . . 9 |- E = ( dist ` H )
20 f1otrkg.j . . . . . . . . 9 |- J = (Itv ` H )
219adantr 481 . . . . . . . . 9 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> F : B -1-1-onto-> P )
22 f1otrkg.1 . . . . . . . . . 10 |- ( ( ph /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
2322adantlr 751 . . . . . . . . 9 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
24 f1otrkg.2 . . . . . . . . . 10 |- ( ( ph /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )
2524adantlr 751 . . . . . . . . 9 |- ( ( ( 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 ) ) ) )
264, 5, 6, 18, 19, 20, 21, 23, 25, 13, 15f1otrgds 25749 . . . . . . . 8 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x E y ) = ( ( F ` x ) D ( F ` y ) ) )
274, 5, 6, 18, 19, 20, 21, 23, 25, 15, 13f1otrgds 25749 . . . . . . . 8 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( y E x ) = ( ( F ` y ) D ( F ` x ) ) )
2817, 26, 273eqtr4d 2666 . . . . . . 7 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x E y ) = ( y E x ) )
2928ralrimivva 2971 . . . . . 6 |- ( ph -> A. x e. B A. y e. B ( x E y ) = ( y E x ) )
30 f1of1 6136 . . . . . . . . . . 11 |- ( F : B -1-1-onto-> P -> F : B -1-1-> P )
319, 30syl 17 . . . . . . . . . 10 |- ( ph -> F : B -1-1-> P )
32313ad2ant1 1082 . . . . . . . . 9 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> F : B -1-1-> P )
33 simp21 1094 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> x e. B )
34 simp22 1095 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> y e. B )
3533, 34jca 554 . . . . . . . . 9 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( x e. B /\ y e. B ) )
3673ad2ant1 1082 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> G e. TarskiG )
37113ad2ant1 1082 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> F : B --> P )
3837, 33ffvelrnd 6360 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( F ` x ) e. P )
3937, 34ffvelrnd 6360 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( F ` y ) e. P )
40 simp23 1096 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> z e. B )
4137, 40ffvelrnd 6360 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( F ` z ) e. P )
42 simp3 1063 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( x E y ) = ( z E z ) )
4393ad2ant1 1082 . . . . . . . . . . . 12 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> F : B -1-1-onto-> P )
44223ad2antl1 1223 . . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
45243ad2antl1 1223 . . . . . . . . . . . 12 |- ( ( ( 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 ) ) ) )
464, 5, 6, 18, 19, 20, 43, 44, 45, 33, 34f1otrgds 25749 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( x E y ) = ( ( F ` x ) D ( F ` y ) ) )
474, 5, 6, 18, 19, 20, 43, 44, 45, 40, 40f1otrgds 25749 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( z E z ) = ( ( F ` z ) D ( F ` z ) ) )
4842, 46, 473eqtr3d 2664 . . . . . . . . . 10 |- ( ( 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 ) ) )
494, 5, 6, 36, 38, 39, 41, 48axtgcgrid 25362 . . . . . . . . 9 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( F ` x ) = ( F ` y ) )
50 f1veqaeq 6514 . . . . . . . . . 10 |- ( ( F : B -1-1-> P /\ ( x e. B /\ y e. B ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
5150imp 445 . . . . . . . . 9 |- ( ( ( F : B -1-1-> P /\ ( x e. B /\ y e. B ) ) /\ ( F ` x ) = ( F ` y ) ) -> x = y )
5232, 35, 49, 51syl21anc 1325 . . . . . . . 8 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> x = y )
53523expia 1267 . . . . . . 7 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x E y ) = ( z E z ) -> x = y ) )
5453ralrimivvva 2972 . . . . . 6 |- ( ph -> A. x e. B A. y e. B A. z e. B ( ( x E y ) = ( z E z ) -> x = y ) )
5529, 54jca 554 . . . . 5 |- ( 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 ) ) )
5618, 19, 20istrkgc 25353 . . . . 5 |- ( 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 ) ) ) )
573, 55, 56sylanbrc 698 . . . 4 |- ( ph -> H e. TarskiGC )
5893ad2ant1 1082 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> F : B -1-1-onto-> P )
5958, 30syl 17 . . . . . . . . 9 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> F : B -1-1-> P )
60 simp2 1062 . . . . . . . . 9 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> ( x e. B /\ y e. B ) )
6173ad2ant1 1082 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> G e. TarskiG )
62143adant3 1081 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> ( F ` x ) e. P )
63163adant3 1081 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> ( F ` y ) e. P )
64 simp3 1063 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> y e. ( x J x ) )
65223ad2antl1 1223 . . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
66243ad2antl1 1223 . . . . . . . . . . . 12 |- ( ( ( 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 ) ) ) )
67133adant3 1081 . . . . . . . . . . . 12 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> x e. B )
68153adant3 1081 . . . . . . . . . . . 12 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> y e. B )
694, 5, 6, 18, 19, 20, 58, 65, 66, 67, 67, 68f1otrgitv 25750 . . . . . . . . . . 11 |- ( ( 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 ) ) ) )
7064, 69mpbid 222 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> ( F ` y ) e. ( ( F ` x ) I ( F ` x ) ) )
714, 5, 6, 61, 62, 63, 70axtgbtwnid 25365 . . . . . . . . 9 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> ( F ` x ) = ( F ` y ) )
7259, 60, 71, 51syl21anc 1325 . . . . . . . 8 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> x = y )
73723expia 1267 . . . . . . 7 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( y e. ( x J x ) -> x = y ) )
7473ralrimivva 2971 . . . . . 6 |- ( ph -> A. x e. B A. y e. B ( y e. ( x J x ) -> x = y ) )
75 f1ocnv 6149 . . . . . . . . . . . . . 14 |- ( F : B -1-1-onto-> P -> `' F : P -1-1-onto-> B )
76 f1of 6137 . . . . . . . . . . . . . 14 |- ( `' F : P -1-1-onto-> B -> `' F : P --> B )
779, 75, 763syl 18 . . . . . . . . . . . . 13 |- ( ph -> `' F : P --> B )
7877ad5antr 770 . . . . . . . . . . . 12 |- ( ( ( ( ( ( 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 792 . . . . . . . . . . . 12 |- ( ( ( ( ( ( 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 )
8078, 79ffvelrnd 6360 . . . . . . . . . . 11 |- ( ( ( ( ( ( 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 477 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( 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 ) )
8281eleq1d 2686 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( 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 ) ) )
8381eleq1d 2686 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( 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 ) ) )
8482, 83anbi12d 747 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( 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 794 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 ) ) )
8621ad2antrr 762 . . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 )
8786ad2antrr 762 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( 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 6533 . . . . . . . . . . . . . . . 16 |- ( ( F : B -1-1-onto-> P /\ c e. P ) -> ( F ` ( `' F ` c ) ) = c )
8988eleq1d 2686 . . . . . . . . . . . . . . 15 |- ( ( 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 ) ) ) )
9087, 79, 89syl2anc 693 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 ) ) ) )
9185, 90mpbird 247 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 simplll 798 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( 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 ) ) -> ( ( ( 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 ) ) ) )
93 simplll 798 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( 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 ) ) -> ( ph /\ ( x e. B /\ y e. B ) ) )
9493, 23sylancom 701 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( 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 ) ) )
9592, 94sylancom 701 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( 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 ) ) )
96 simplll 798 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( 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 ) ) -> ( ( ( 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 ) ) ) )
97 simplll 798 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( 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 ) ) -> ( ph /\ ( x e. B /\ y e. B ) ) )
9897, 25sylancom 701 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( 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 ) ) ) )
9996, 98sylancom 701 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( 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 ) ) ) )
100 simplr2 1104 . . . . . . . . . . . . . . 15 |- ( ( ( ( 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 )
101100ad2antrr 762 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 )
10215ad2antrr 762 . . . . . . . . . . . . . . 15 |- ( ( ( ( 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 )
103102ad2antrr 762 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 )
1044, 5, 6, 18, 19, 20, 87, 95, 99, 101, 103, 80f1otrgitv 25750 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 ) ) ) )
10591, 104mpbird 247 . . . . . . . . . . . 12 |- ( ( ( ( ( ( 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 ) )
106 simprr 796 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 ) ) )
10788eleq1d 2686 . . . . . . . . . . . . . . 15 |- ( ( 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 ) ) ) )
10887, 79, 107syl2anc 693 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 ) ) ) )
109106, 108mpbird 247 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 ) ) )
110 simplr3 1105 . . . . . . . . . . . . . . 15 |- ( ( ( ( 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 )
111110ad2antrr 762 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 )
11213ad2antrr 762 . . . . . . . . . . . . . . 15 |- ( ( ( ( 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 )
113112ad2antrr 762 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 )
1144, 5, 6, 18, 19, 20, 87, 95, 99, 111, 113, 80f1otrgitv 25750 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 ) ) ) )
115109, 114mpbird 247 . . . . . . . . . . . 12 |- ( ( ( ( ( ( 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 ) )
116105, 115jca 554 . . . . . . . . . . 11 |- ( ( ( ( ( ( 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 ) ) )
11780, 84, 116rspcedvd 3317 . . . . . . . . . 10 |- ( ( ( ( ( ( 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 ) ) )
1188ad2antrr 762 . . . . . . . . . . 11 |- ( ( ( ( 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 )
11912ad2antrr 762 . . . . . . . . . . . 12 |- ( ( ( ( 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 )
120119, 112ffvelrnd 6360 . . . . . . . . . . 11 |- ( ( ( ( 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 )
121119, 102ffvelrnd 6360 . . . . . . . . . . 11 |- ( ( ( ( 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 )
122 simplr1 1103 . . . . . . . . . . . 12 |- ( ( ( ( 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 )
123119, 122ffvelrnd 6360 . . . . . . . . . . 11 |- ( ( ( ( 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 )
124119, 100ffvelrnd 6360 . . . . . . . . . . 11 |- ( ( ( ( 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 )
125119, 110ffvelrnd 6360 . . . . . . . . . . 11 |- ( ( ( ( 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 )
126 simprl 794 . . . . . . . . . . . 12 |- ( ( ( ( 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 ) )
1274, 5, 6, 18, 19, 20, 86, 94, 98, 112, 122, 100f1otrgitv 25750 . . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) ) )
128126, 127mpbid 222 . . . . . . . . . . 11 |- ( ( ( ( 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 ) ) )
129 simprr 796 . . . . . . . . . . . 12 |- ( ( ( ( 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 ) )
1304, 5, 6, 18, 19, 20, 86, 94, 98, 102, 122, 110f1otrgitv 25750 . . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) ) )
131129, 130mpbid 222 . . . . . . . . . . 11 |- ( ( ( ( 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 ) ) )
1324, 5, 6, 118, 120, 121, 123, 124, 125, 128, 131axtgpasch 25366 . . . . . . . . . 10 |- ( ( ( ( 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 ) ) ) )
133117, 132r19.29a 3078 . . . . . . . . 9 |- ( ( ( ( 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 ) ) )
134133ex 450 . . . . . . . 8 |- ( ( ( 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 ) ) ) )
135134ralrimivvva 2972 . . . . . . 7 |- ( ( 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 ) ) ) )
136135ralrimivva 2971 . . . . . 6 |- ( 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 ) ) ) )
1379ad5antr 770 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( 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 )
138 simpllr 799 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( 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 )
139137, 138, 88syl2anc 693 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( 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 )
140 ffn 6045 . . . . . . . . . . . . . . . . . 18 |- ( F : B --> P -> F Fn B )
141137, 10, 1403syl 18 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( 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 )
142 simp-4r 807 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( 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 ) )
143142simpld 475 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( 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 )
144143elpwid 4170 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> s C_ B )
145144adantlr 751 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( 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 )
146 simprl 794 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( 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 )
147 fnfvima 6496 . . . . . . . . . . . . . . . . 17 |- ( ( F Fn B /\ s C_ B /\ x e. s ) -> ( F ` x ) e. ( F " s ) )
148141, 145, 146, 147syl3anc 1326 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( 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 ) )
149142simprd 479 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( 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 )
150149elpwid 4170 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> t C_ B )
151150adantlr 751 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( 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 )
152 simprr 796 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( 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 )
153 fnfvima 6496 . . . . . . . . . . . . . . . . 17 |- ( ( F Fn B /\ t C_ B /\ y e. t ) -> ( F ` y ) e. ( F " t ) )
154141, 151, 152, 153syl3anc 1326 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( 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 ) )
155 simplr 792 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( 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 ) )
156 oveq1 6657 . . . . . . . . . . . . . . . . . 18 |- ( e = ( F ` x ) -> ( e I f ) = ( ( F ` x ) I f ) )
157156eleq2d 2687 . . . . . . . . . . . . . . . . 17 |- ( e = ( F ` x ) -> ( c e. ( e I f ) <-> c e. ( ( F ` x ) I f ) ) )
158 oveq2 6658 . . . . . . . . . . . . . . . . . 18 |- ( f = ( F ` y ) -> ( ( F ` x ) I f ) = ( ( F ` x ) I ( F ` y ) ) )
159158eleq2d 2687 . . . . . . . . . . . . . . . . 17 |- ( f = ( F ` y ) -> ( c e. ( ( F ` x ) I f ) <-> c e. ( ( F ` x ) I ( F ` y ) ) ) )
160157, 159rspc2va 3323 . . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 ) ) )
161148, 154, 155, 160syl21anc 1325 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( 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 ) ) )
162139, 161eqeltrd 2701 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 ) ) )
1639ad4antr 768 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( 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 )
164 simp-5l 808 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( 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 )
165164, 22sylancom 701 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( 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 ) ) )
166 simp-5l 808 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( 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 )
167166, 24sylancom 701 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( 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 ) ) ) )
168 simprl 794 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> x e. s )
169144, 168sseldd 3604 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> x e. B )
170 simprr 796 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> y e. t )
171150, 170sseldd 3604 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> y e. B )
17277ad4antr 768 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> `' F : P --> B )
173 simplr 792 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> c e. P )
174172, 173ffvelrnd 6360 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( 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 )
1754, 5, 6, 18, 19, 20, 163, 165, 167, 169, 171, 174f1otrgitv 25750 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( 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 ) ) ) )
176175adantlr 751 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 ) ) ) )
177162, 176mpbird 247 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 ) )
178177ralrimivva 2971 . . . . . . . . . . . 12 |- ( ( ( ( ( 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 ) )
179178adantllr 755 . . . . . . . . . . 11 |- ( ( ( ( ( ( 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 ) )
18077ad4antr 768 . . . . . . . . . . . . . 14 |- ( ( ( ( ( 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 )
181 simpr 477 . . . . . . . . . . . . . 14 |- ( ( ( ( ( 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 )
182180, 181ffvelrnd 6360 . . . . . . . . . . . . 13 |- ( ( ( ( ( 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 )
183 eleq1 2689 . . . . . . . . . . . . . . 15 |- ( b = ( `' F ` c ) -> ( b e. ( x J y ) <-> ( `' F ` c ) e. ( x J y ) ) )
1841832ralbidv 2989 . . . . . . . . . . . . . 14 |- ( 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 ) ) )
185184adantl 482 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 ) ) )
186182, 185rspcedv 3313 . . . . . . . . . . . 12 |- ( ( ( ( ( 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 ) ) )
187186adantr 481 . . . . . . . . . . 11 |- ( ( ( ( ( ( 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 ) ) )
188179, 187mpd 15 . . . . . . . . . 10 |- ( ( ( ( ( ( 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 ) )
1897ad3antrrr 766 . . . . . . . . . . 11 |- ( ( ( ( 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 )
190 imassrn 5477 . . . . . . . . . . . 12 |- ( F " s ) C_ ran F
191 f1ofo 6144 . . . . . . . . . . . . . 14 |- ( F : B -1-1-onto-> P -> F : B -onto-> P )
192 forn 6118 . . . . . . . . . . . . . 14 |- ( F : B -onto-> P -> ran F = P )
1939, 191, 1923syl 18 . . . . . . . . . . . . 13 |- ( ph -> ran F = P )
194193ad3antrrr 766 . . . . . . . . . . . 12 |- ( ( ( ( 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 )
195190, 194syl5sseq 3653 . . . . . . . . . . 11 |- ( ( ( ( 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 )
196 imassrn 5477 . . . . . . . . . . . 12 |- ( F " t ) C_ ran F
197196, 194syl5sseq 3653 . . . . . . . . . . 11 |- ( ( ( ( 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 )
19811ad3antrrr 766 . . . . . . . . . . . 12 |- ( ( ( ( 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 )
199 simplr 792 . . . . . . . . . . . 12 |- ( ( ( ( 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 )
200198, 199ffvelrnd 6360 . . . . . . . . . . 11 |- ( ( ( ( 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 )
2019ad5antr 770 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( 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 )
202 ffn 6045 . . . . . . . . . . . . . . . . . 18 |- ( `' F : P --> B -> `' F Fn P )
203201, 75, 76, 2024syl 19 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( 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 )
204195ad2antrr 762 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( 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 )
205 simplr 792 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( 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 ) )
206 fnfvima 6496 . . . . . . . . . . . . . . . . 17 |- ( ( `' F Fn P /\ ( F " s ) C_ P /\ u e. ( F " s ) ) -> ( `' F ` u ) e. ( `' F " ( F " s ) ) )
207203, 204, 205, 206syl3anc 1326 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( 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 ) ) )
208201, 30syl 17 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( 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 )
209 simp-5r 809 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( 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 ) )
210209simpld 475 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( 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 )
211210elpwid 4170 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( 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 )
212 f1imacnv 6153 . . . . . . . . . . . . . . . . 17 |- ( ( F : B -1-1-> P /\ s C_ B ) -> ( `' F " ( F " s ) ) = s )
213208, 211, 212syl2anc 693 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( 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 )
214207, 213eleqtrd 2703 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( 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 )
215197ad2antrr 762 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( 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 )
216 simpr 477 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( 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 ) )
217 fnfvima 6496 . . . . . . . . . . . . . . . . 17 |- ( ( `' F Fn P /\ ( F " t ) C_ P /\ v e. ( F " t ) ) -> ( `' F ` v ) e. ( `' F " ( F " t ) ) )
218203, 215, 216, 217syl3anc 1326 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( 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 ) ) )
219209simprd 479 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( 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 )
220219elpwid 4170 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( 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 )
221 f1imacnv 6153 . . . . . . . . . . . . . . . . 17 |- ( ( F : B -1-1-> P /\ t C_ B ) -> ( `' F " ( F " t ) ) = t )
222208, 220, 221syl2anc 693 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( 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 )
223218, 222eleqtrd 2703 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( 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 )
224 simpllr 799 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( 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 ) )
225 eleq1 2689 . . . . . . . . . . . . . . . 16 |- ( x = ( `' F ` u ) -> ( x e. ( a J y ) <-> ( `' F ` u ) e. ( a J y ) ) )
226 oveq2 6658 . . . . . . . . . . . . . . . . 17 |- ( y = ( `' F ` v ) -> ( a J y ) = ( a J ( `' F ` v ) ) )
227226eleq2d 2687 . . . . . . . . . . . . . . . 16 |- ( y = ( `' F ` v ) -> ( ( `' F ` u ) e. ( a J y ) <-> ( `' F ` u ) e. ( a J ( `' F ` v ) ) ) )
228225, 227rspc2va 3323 . . . . . . . . . . . . . . 15 |- ( ( ( ( `' 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 ) ) )
229214, 223, 224, 228syl21anc 1325 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 ) ) )
230 simp-6l 810 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( 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 )
231230, 22sylancom 701 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( 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 ) ) )
232 simp-6l 810 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( 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 )
233232, 24sylancom 701 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( 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 ) ) ) )
234 simp-4r 807 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( 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 )
235215, 216sseldd 3604 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( 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 )
236 f1ocnvdm 6540 . . . . . . . . . . . . . . . 16 |- ( ( F : B -1-1-onto-> P /\ v e. P ) -> ( `' F ` v ) e. B )
237201, 235, 236syl2anc 693 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( 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 )
238204, 205sseldd 3604 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( 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 )
239 f1ocnvdm 6540 . . . . . . . . . . . . . . . 16 |- ( ( F : B -1-1-onto-> P /\ u e. P ) -> ( `' F ` u ) e. B )
240201, 238, 239syl2anc 693 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( 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 )
2414, 5, 6, 18, 19, 20, 201, 231, 233, 234, 237, 240f1otrgitv 25750 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 ) ) ) ) )
242229, 241mpbid 222 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 ) ) ) )
243 f1ocnvfv2 6533 . . . . . . . . . . . . . 14 |- ( ( F : B -1-1-onto-> P /\ u e. P ) -> ( F ` ( `' F ` u ) ) = u )
244201, 238, 243syl2anc 693 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 )
245 f1ocnvfv2 6533 . . . . . . . . . . . . . . 15 |- ( ( F : B -1-1-onto-> P /\ v e. P ) -> ( F ` ( `' F ` v ) ) = v )
246201, 235, 245syl2anc 693 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 )
247246oveq2d 6666 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 ) )
248242, 244, 2473eltr3d 2715 . . . . . . . . . . . 12 |- ( ( ( ( ( ( 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 ) )
2492483impa 1259 . . . . . . . . . . 11 |- ( ( ( ( ( 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 ) )
2504, 5, 6, 189, 195, 197, 200, 249axtgcont 25368 . . . . . . . . . 10 |- ( ( ( ( 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 ) )
251188, 250r19.29a 3078 . . . . . . . . 9 |- ( ( ( ( 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 ) )
252251r19.29an 3077 . . . . . . . 8 |- ( ( ( 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 ) )
253252ex 450 . . . . . . 7 |- ( ( 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 ) ) )
254253ralrimivva 2971 . . . . . 6 |- ( 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 ) ) )
25574, 136, 2543jca 1242 . . . . 5 |- ( 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 ) ) ) )
25618, 19, 20istrkgb 25354 . . . . 5 |- ( 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 ) ) ) ) )
2573, 255, 256sylanbrc 698 . . . 4 |- ( ph -> H e. TarskiGB )
25857, 257elind 3798 . . 3 |- ( ph -> H e. (TarskiGC i^i TarskiGB ) )
2597ad9antr 778 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( 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 )
26011ad9antr 778 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 )
261 simp-9r 817 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 )
262260, 261ffvelrnd 6360 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( 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 )
263 simp-8r 815 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 )
264260, 263ffvelrnd 6360 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( 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 )
265 simp-7r 813 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 )
266260, 265ffvelrnd 6360 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( 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 )
267 simp-5r 809 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 )
268260, 267ffvelrnd 6360 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( 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 )
269 simp-4r 807 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 )
270260, 269ffvelrnd 6360 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( 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 )
271 simpllr 799 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 )
272260, 271ffvelrnd 6360 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( 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 )
273 simp-6r 811 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 )
274260, 273ffvelrnd 6360 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( 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 )
275 simplr 792 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 )
276260, 275ffvelrnd 6360 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( 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 )
2779ad9antr 778 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ( ( ( 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 )
278277, 261jca 554 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 ) )
279 simprl1 1106 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 )
280 dff1o6 6531 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( 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 ) ) )
281280simp3bi 1078 . . . . . . . . . . . . . . . . . . . . . 22 |- ( F : B -1-1-onto-> P -> A. x e. B A. y e. B ( ( F ` x ) = ( F ` y ) -> x = y ) )
282281r19.21bi 2932 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( F : B -1-1-onto-> P /\ x e. B ) -> A. y e. B ( ( F ` x ) = ( F ` y ) -> x = y ) )
283282r19.21bi 2932 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( F : B -1-1-onto-> P /\ x e. B ) /\ y e. B ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
284283necon3d 2815 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( F : B -1-1-onto-> P /\ x e. B ) /\ y e. B ) -> ( x =/= y -> ( F ` x ) =/= ( F ` y ) ) )
285284imp 445 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( F : B -1-1-onto-> P /\ x e. B ) /\ y e. B ) /\ x =/= y ) -> ( F ` x ) =/= ( F ` y ) )
286278, 263, 279, 285syl21anc 1325 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( 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 ) )
287 simprl2 1107 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 ) )
28822ex 450 . . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( ( e e. B /\ f e. B ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) ) )
289288ad9antr 778 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( ( ( ( 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 ) ) ) )
290289imp 445 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ( ( ( ( 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 ) ) )
29124ex 450 . . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( ( e e. B /\ f e. B /\ g e. B ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) ) )
292291ad9antr 778 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( ( ( ( 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 ) ) ) ) )
293292imp 445 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ( ( ( ( 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 ) ) ) )
2944, 5, 6, 18, 19, 20, 277, 290, 293, 261, 265, 263f1otrgitv 25750 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 ) ) ) )
295287, 294mpbid 222 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( 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 ) ) )
296 simprl3 1108 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 ) )
2974, 5, 6, 18, 19, 20, 277, 290, 293, 267, 271, 269f1otrgitv 25750 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 ) ) ) )
298296, 297mpbid 222 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( 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 ) ) )
299 simprr 796 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( ( ( ( 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 ) ) ) )
300299simpld 475 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ( ( ( 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 ) ) )
301300simpld 475 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 ) )
3024, 5, 6, 18, 19, 20, 277, 290, 293, 261, 263f1otrgds 25749 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 ) ) )
3034, 5, 6, 18, 19, 20, 277, 290, 293, 267, 269f1otrgds 25749 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 ) ) )
304301, 302, 3033eqtr3d 2664 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( 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 ) ) )
305300simprd 479 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 ) )
3064, 5, 6, 18, 19, 20, 277, 290, 293, 263, 265f1otrgds 25749 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 ) ) )
3074, 5, 6, 18, 19, 20, 277, 290, 293, 269, 271f1otrgds 25749 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 ) ) )
308305, 306, 3073eqtr3d 2664 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( 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 ) ) )
309299simprd 479 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ( ( ( 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 ) ) )
310309simpld 475 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 ) )
3114, 5, 6, 18, 19, 20, 277, 290, 293, 261, 273f1otrgds 25749 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 ) ) )
3124, 5, 6, 18, 19, 20, 277, 290, 293, 267, 275f1otrgds 25749 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 ) ) )
313310, 311, 3123eqtr3d 2664 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( 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 ) ) )
314309simprd 479 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 ) )
3154, 5, 6, 18, 19, 20, 277, 290, 293, 263, 273f1otrgds 25749 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 ) ) )
3164, 5, 6, 18, 19, 20, 277, 290, 293, 269, 275f1otrgds 25749 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( 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 ) ) )
317314, 315, 3163eqtr3d 2664 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( 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 ) ) )
3184, 5, 6, 259, 262, 264, 266, 268, 270, 272, 274, 276, 286, 295, 298, 304, 308, 313, 317axtg5seg 25364 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ( ( 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 ) ) )
3194, 5, 6, 18, 19, 20, 277, 290, 293, 265, 273f1otrgds 25749 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ( ( 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 ) ) )
3204, 5, 6, 18, 19, 20, 277, 290, 293, 271, 275f1otrgds 25749 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ( ( 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 ) ) )
321318, 319, 3203eqtr4d 2666 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( 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 ) )
322321ex 450 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( 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 ) ) )
323322ralrimiva 2966 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( 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 ) ) )
324323ralrimiva 2966 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( 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 ) ) )
325324ralrimiva 2966 . . . . . . . . . . 11 |- ( ( ( ( ( ( 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 ) ) )
326325ralrimiva 2966 . . . . . . . . . 10 |- ( ( ( ( ( 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 ) ) )
327326ralrimiva 2966 . . . . . . . . 9 |- ( ( ( ( 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 ) ) )
328327ralrimiva 2966 . . . . . . . 8 |- ( ( ( 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 ) ) )
329328ralrimiva 2966 . . . . . . 7 |- ( ( 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 ) ) )
330329ralrimiva 2966 . . . . . 6 |- ( 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 ) ) )
331 simp-4l 806 . . . . . . . . . 10 |- ( ( ( ( ( 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 )
332 simplr 792 . . . . . . . . . 10 |- ( ( ( ( ( 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 )
333 simprl 794 . . . . . . . . . . . 12 |- ( ( ( ( ( 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 ) )
334331, 9syl 17 . . . . . . . . . . . . . 14 |- ( ( ( ( ( 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 )
335 f1ocnvfv2 6533 . . . . . . . . . . . . . 14 |- ( ( F : B -1-1-onto-> P /\ w e. P ) -> ( F ` ( `' F ` w ) ) = w )
336334, 332, 335syl2anc 693 . . . . . . . . . . . . 13 |- ( ( ( ( ( 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 )
337336oveq2d 6666 . . . . . . . . . . . 12 |- ( ( ( ( ( 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 ) )
338333, 337eleqtrrd 2704 . . . . . . . . . . 11 |- ( ( ( ( ( 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 ) ) ) )
339331, 22sylan 488 . . . . . . . . . . . 12 |- ( ( ( ( ( ( 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 ) ) )
340331, 24sylan 488 . . . . . . . . . . . 12 |- ( ( ( ( ( ( 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 ) ) ) )
34113ad3antrrr 766 . . . . . . . . . . . 12 |- ( ( ( ( ( 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 )
34277ffvelrnda 6359 . . . . . . . . . . . . 13 |- ( ( ph /\ w e. P ) -> ( `' F ` w ) e. B )
343331, 332, 342syl2anc 693 . . . . . . . . . . . 12 |- ( ( ( ( ( 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 )
34415ad3antrrr 766 . . . . . . . . . . . 12 |- ( ( ( ( ( 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 )
3454, 5, 6, 18, 19, 20, 334, 339, 340, 341, 343, 344f1otrgitv 25750 . . . . . . . . . . 11 |- ( ( ( ( ( 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 ) ) ) ) )
346338, 345mpbird 247 . . . . . . . . . 10 |- ( ( ( ( ( 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 ) ) )
3474, 5, 6, 18, 19, 20, 334, 339, 340, 344, 343f1otrgds 25749 . . . . . . . . . . . 12 |- ( ( ( ( ( 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 ) ) ) )
348336oveq2d 6666 . . . . . . . . . . . 12 |- ( ( ( ( ( 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 ) )
349 simprr 796 . . . . . . . . . . . 12 |- ( ( ( ( ( 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 ) ) )
350347, 348, 3493eqtrd 2660 . . . . . . . . . . 11 |- ( ( ( ( ( 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 ) ) )
351 simprl 794 . . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) -> a e. B )
352351ad2antrr 762 . . . . . . . . . . . 12 |- ( ( ( ( ( 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 )
353 simprr 796 . . . . . . . . . . . . 13 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) -> b e. B )
354353ad2antrr 762 . . . . . . . . . . . 12 |- ( ( ( ( ( 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 )
3554, 5, 6, 18, 19, 20, 334, 339, 340, 352, 354f1otrgds 25749 . . . . . . . . . . 11 |- ( ( ( ( ( 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 ) ) )
356350, 355eqtr4d 2659 . . . . . . . . . 10 |- ( ( ( ( ( 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 ) )
357 oveq2 6658 . . . . . . . . . . . . . . 15 |- ( z = ( `' F ` w ) -> ( x J z ) = ( x J ( `' F ` w ) ) )
358357eleq2d 2687 . . . . . . . . . . . . . 14 |- ( z = ( `' F ` w ) -> ( y e. ( x J z ) <-> y e. ( x J ( `' F ` w ) ) ) )
359 oveq2 6658 . . . . . . . . . . . . . . 15 |- ( z = ( `' F ` w ) -> ( y E z ) = ( y E ( `' F ` w ) ) )
360359eqeq1d 2624 . . . . . . . . . . . . . 14 |- ( z = ( `' F ` w ) -> ( ( y E z ) = ( a E b ) <-> ( y E ( `' F ` w ) ) = ( a E b ) ) )
361358, 360anbi12d 747 . . . . . . . . . . . . 13 |- ( 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 ) ) ) )
362361adantl 482 . . . . . . . . . . . 12 |- ( ( ( 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 ) ) ) )
363342, 362rspcedv 3313 . . . . . . . . . . 11 |- ( ( 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 ) ) ) )
364363imp 445 . . . . . . . . . 10 |- ( ( ( 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 ) ) )
365331, 332, 346, 356, 364syl22anc 1327 . . . . . . . . 9 |- ( ( ( ( ( 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 ) ) )
3668adantr 481 . . . . . . . . . 10 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) -> G e. TarskiG )
36714adantr 481 . . . . . . . . . 10 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) -> ( F ` x ) e. P )
36816adantr 481 . . . . . . . . . 10 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) -> ( F ` y ) e. P )
36912adantr 481 . . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) -> F : B --> P )
370369, 351ffvelrnd 6360 . . . . . . . . . 10 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) -> ( F ` a ) e. P )
371369, 353ffvelrnd 6360 . . . . . . . . . 10 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( a e. B /\ b e. B ) ) -> ( F ` b ) e. P )
3724, 5, 6, 366, 367, 368, 370, 371axtgsegcon 25363 . . . . . . . . 9 |- ( ( ( 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 ) ) ) )
373365, 372r19.29a 3078 . . . . . . . 8 |- ( ( ( 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 ) ) )
374373ralrimivva 2971 . . . . . . 7 |- ( ( 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 ) ) )
375374ralrimivva 2971 . . . . . 6 |- ( 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 ) ) )
3763, 330, 375jca32 558 . . . . 5 |- ( 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 ) ) ) ) )
37718, 19, 20istrkgcb 25355 . . . . 5 |- ( 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 ) ) ) ) )
378376, 377sylibr 224 . . . 4 |- ( ph -> H e. TarskiGCB )
379 f1otrg.l . . . . 5 |- ( 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 ) ) } ) )
38018, 19, 20istrkgl 25357 . . . . 5 |- ( 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 ) ) } ) ) )
3813, 379, 380sylanbrc 698 . . . 4 |- ( 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 ) ) } ) } )
382378, 381elind 3798 . . 3 |- ( 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 ) ) } ) } ) )
383258, 382elind 3798 . 2 |- ( 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 ) ) } ) } ) ) )
384 df-trkg 25352 . 2 |- 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 ) ) } ) } ) )
385383, 384syl6eleqr 2712 1 |- ( ph -> H e. TarskiG )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   \/ w3o 1036   /\ w3a 1037   = wceq 1483   e. wcel 1990   {cab 2608   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   [.wsbc 3435   \ cdif 3571   i^i cin 3573   C_ wss 3574   ~Pcpw 4158   {csn 4177   `'ccnv 5113   ran crn 5115   "cima 5117   Fn wfn 5883   -->wf 5884   -1-1->wf1 5885   -onto->wfo 5886   -1-1-onto->wf1o 5887   ` cfv 5888  (class class class)co 6650   |-> cmpt2 6652   Basecbs 15857   distcds 15950  TarskiGcstrkg 25329  TarskiGCcstrkgc 25330  TarskiGBcstrkgb 25331  TarskiGCBcstrkgcb 25332  Itvcitv 25335  LineGclng 25336
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-trkgc 25347  df-trkgb 25348  df-trkgcb 25349  df-trkg 25352
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator