MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1otrg Structured version   Visualization version   Unicode version
Theorem f1otrg 24980
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 3040 . . . . . 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 472 . . . . . . . . 9 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> G e. TarskiG )
9 f1otrkg.f . . . . . . . . . . . 12 |- ( ph -> F : B -1-1-onto-> P )
10 f1of 5828 . . . . . . . . . . . 12 |- ( F : B -1-1-onto-> P -> F : B --> P )
119, 10syl 17 . . . . . . . . . . 11 |- ( ph -> F : B --> P )
1211adantr 472 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> F : B --> P )
13 simprl 772 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> x e. B )
1412, 13ffvelrnd 6038 . . . . . . . . 9 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` x ) e. P )
15 simprr 774 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> y e. B )
1612, 15ffvelrnd 6038 . . . . . . . . 9 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` y ) e. P )
174, 5, 6, 8, 14, 16axtgcgrrflx 24589 . . . . . . . 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 472 . . . . . . . . 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 729 . . . . . . . . 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 729 . . . . . . . . 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 24978 . . . . . . . 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 24978 . . . . . . . 8 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( y E x ) = ( ( F ` y ) D ( F ` x ) ) )
2817, 26, 273eqtr4d 2515 . . . . . . 7 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x E y ) = ( y E x ) )
2928ralrimivva 2814 . . . . . 6 |- ( ph -> A. x e. B A. y e. B ( x E y ) = ( y E x ) )
30 f1of1 5827 . . . . . . . . . . 11 |- ( F : B -1-1-onto-> P -> F : B -1-1-> P )
319, 30syl 17 . . . . . . . . . 10 |- ( ph -> F : B -1-1-> P )
32313ad2ant1 1051 . . . . . . . . 9 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> F : B -1-1-> P )
33 simp21 1063 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> x e. B )
34 simp22 1064 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> y e. B )
3533, 34jca 541 . . . . . . . . 9 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( x e. B /\ y e. B ) )
3673ad2ant1 1051 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> G e. TarskiG )
37113ad2ant1 1051 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> F : B --> P )
3837, 33ffvelrnd 6038 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( F ` x ) e. P )
3937, 34ffvelrnd 6038 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( F ` y ) e. P )
40 simp23 1065 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> z e. B )
4137, 40ffvelrnd 6038 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( F ` z ) e. P )
42 simp3 1032 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( x E y ) = ( z E z ) )
4393ad2ant1 1051 . . . . . . . . . . . 12 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> F : B -1-1-onto-> P )
44223ad2antl1 1192 . . . . . . . . . . . 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 1192 . . . . . . . . . . . 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 24978 . . . . . . . . . . 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 24978 . . . . . . . . . . 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 2513 . . . . . . . . . 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 24590 . . . . . . . . 9 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( F ` x ) = ( F ` y ) )
50 f1veqaeq 6179 . . . . . . . . . 10 |- ( ( F : B -1-1-> P /\ ( x e. B /\ y e. B ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
5150imp 436 . . . . . . . . 9 |- ( ( ( F : B -1-1-> P /\ ( x e. B /\ y e. B ) ) /\ ( F ` x ) = ( F ` y ) ) -> x = y )
5232, 35, 49, 51syl21anc 1291 . . . . . . . 8 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> x = y )
53523expia 1233 . . . . . . 7 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x E y ) = ( z E z ) -> x = y ) )
5453ralrimivvva 2815 . . . . . 6 |- ( ph -> A. x e. B A. y e. B A. z e. B ( ( x E y ) = ( z E z ) -> x = y ) )
5529, 54jca 541 . . . . 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 24581 . . . . 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 677 . . . 4 |- ( ph -> H e. TarskiGC )
5893ad2ant1 1051 . . . . . . . . . 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 1031 . . . . . . . . 9 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> ( x e. B /\ y e. B ) )
6173ad2ant1 1051 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> G e. TarskiG )
62143adant3 1050 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> ( F ` x ) e. P )
63163adant3 1050 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> ( F ` y ) e. P )
64 simp3 1032 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> y e. ( x J x ) )
65223ad2antl1 1192 . . . . . . . . . . . 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 1192 . . . . . . . . . . . 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 1050 . . . . . . . . . . . 12 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> x e. B )
68153adant3 1050 . . . . . . . . . . . 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 24979 . . . . . . . . . . 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 215 . . . . . . . . . 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 24593 . . . . . . . . 9 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> ( F ` x ) = ( F ` y ) )
7259, 60, 71, 51syl21anc 1291 . . . . . . . 8 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> x = y )
73723expia 1233 . . . . . . 7 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( y e. ( x J x ) -> x = y ) )
7473ralrimivva 2814 . . . . . 6 |- ( ph -> A. x e. B A. y e. B ( y e. ( x J x ) -> x = y ) )
75 f1ocnv 5840 . . . . . . . . . . . . . 14 |- ( F : B -1-1-onto-> P -> `' F : P -1-1-onto-> B )
76 f1of 5828 . . . . . . . . . . . . . 14 |- ( `' F : P -1-1-onto-> B -> `' F : P --> B )
779, 75, 763syl 18 . . . . . . . . . . . . 13 |- ( ph -> `' F : P --> B )
7877ad5antr 748 . . . . . . . . . . . 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 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 ) ) ) ) -> c e. P )
8078, 79ffvelrnd 6038 . . . . . . . . . . 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 468 . . . . . . . . . . . . 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 2533 . . . . . . . . . . . 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 2533 . . . . . . . . . . . 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 725 . . . . . . . . . . 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 772 . . . . . . . . . . . . . 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 740 . . . . . . . . . . . . . . . 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 740 . . . . . . . . . . . . . . 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 6194 . . . . . . . . . . . . . . . 16 |- ( ( F : B -1-1-onto-> P /\ c e. P ) -> ( F ` ( `' F ` c ) ) = c )
8988eleq1d 2533 . . . . . . . . . . . . . . 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 673 . . . . . . . . . . . . . 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 240 . . . . . . . . . . . . 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 776 . . . . . . . . . . . . . . 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 776 . . . . . . . . . . . . . . . 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 680 . . . . . . . . . . . . . . 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 680 . . . . . . . . . . . . . 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 776 . . . . . . . . . . . . . . 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 776 . . . . . . . . . . . . . . . 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 680 . . . . . . . . . . . . . . 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 680 . . . . . . . . . . . . . 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 1073 . . . . . . . . . . . . . . 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 740 . . . . . . . . . . . . . 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 740 . . . . . . . . . . . . . . 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 740 . . . . . . . . . . . . . 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 24979 . . . . . . . . . . . . 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 240 . . . . . . . . . . . 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 774 . . . . . . . . . . . . . 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 2533 . . . . . . . . . . . . . . 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 673 . . . . . . . . . . . . . 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 240 . . . . . . . . . . . . 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 1074 . . . . . . . . . . . . . . 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 740 . . . . . . . . . . . . . 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 740 . . . . . . . . . . . . . . 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 740 . . . . . . . . . . . . . 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 24979 . . . . . . . . . . . . 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 240 . . . . . . . . . . . 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 541 . . . . . . . . . . 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 3143 . . . . . . . . . 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 740 . . . . . . . . . . 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 740 . . . . . . . . . . . 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 6038 . . . . . . . . . . 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 6038 . . . . . . . . . . 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 1072 . . . . . . . . . . . 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 6038 . . . . . . . . . . 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 6038 . . . . . . . . . . 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 6038 . . . . . . . . . . 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 772 . . . . . . . . . . . 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 24979 . . . . . . . . . . . 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 215 . . . . . . . . . . 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 774 . . . . . . . . . . . 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 24979 . . . . . . . . . . . 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 215 . . . . . . . . . . 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 24594 . . . . . . . . . 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 2918 . . . . . . . . 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 441 . . . . . . . 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 2815 . . . . . . 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 2814 . . . . . 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 748 . . . . . . . . . . . . . . . 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 777 . . . . . . . . . . . . . . . 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 673 . . . . . . . . . . . . . . 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 5739 . . . . . . . . . . . . . . . . . 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 785 . . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . 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 3952 . . . . . . . . . . . . . . . . . 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 729 . . . . . . . . . . . . . . . . 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 772 . . . . . . . . . . . . . . . . 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 6161 . . . . . . . . . . . . . . . . 17 |- ( ( F Fn B /\ s C_ B /\ x e. s ) -> ( F ` x ) e. ( F " s ) )
148141, 145, 146, 147syl3anc 1292 . . . . . . . . . . . . . . . 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 470 . . . . . . . . . . . . . . . . . . 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 3952 . . . . . . . . . . . . . . . . . 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 729 . . . . . . . . . . . . . . . . 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 774 . . . . . . . . . . . . . . . . 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 6161 . . . . . . . . . . . . . . . . 17 |- ( ( F Fn B /\ t C_ B /\ y e. t ) -> ( F ` y ) e. ( F " t ) )
154141, 151, 152, 153syl3anc 1292 . . . . . . . . . . . . . . . 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 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 ) ) -> A. e e. ( F " s ) A. f e. ( F " t ) c e. ( e I f ) )
156 oveq1 6315 . . . . . . . . . . . . . . . . . 18 |- ( e = ( F ` x ) -> ( e I f ) = ( ( F ` x ) I f ) )
157156eleq2d 2534 . . . . . . . . . . . . . . . . 17 |- ( e = ( F ` x ) -> ( c e. ( e I f ) <-> c e. ( ( F ` x ) I f ) ) )
158 oveq2 6316 . . . . . . . . . . . . . . . . . 18 |- ( f = ( F ` y ) -> ( ( F ` x ) I f ) = ( ( F ` x ) I ( F ` y ) ) )
159158eleq2d 2534 . . . . . . . . . . . . . . . . 17 |- ( f = ( F ` y ) -> ( c e. ( ( F ` x ) I f ) <-> c e. ( ( F ` x ) I ( F ` y ) ) ) )
160157, 159rspc2va 3148 . . . . . . . . . . . . . . . 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 1291 . . . . . . . . . . . . . . 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 2549 . . . . . . . . . . . . . 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 746 . . . . . . . . . . . . . . . 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 786 . . . . . . . . . . . . . . . . 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 680 . . . . . . . . . . . . . . . 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 786 . . . . . . . . . . . . . . . . 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 680 . . . . . . . . . . . . . . . 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 772 . . . . . . . . . . . . . . . . 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 3419 . . . . . . . . . . . . . . . 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 774 . . . . . . . . . . . . . . . . 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 3419 . . . . . . . . . . . . . . . 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 746 . . . . . . . . . . . . . . . . 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 770 . . . . . . . . . . . . . . . . 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 6038 . . . . . . . . . . . . . . . 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 24979 . . . . . . . . . . . . . . 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 729 . . . . . . . . . . . . . 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 240 . . . . . . . . . . . . 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 2814 . . . . . . . . . . . 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 733 . . . . . . . . . . 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 746 . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . 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 6038 . . . . . . . . . . . . 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 2537 . . . . . . . . . . . . . . 15 |- ( b = ( `' F ` c ) -> ( b e. ( x J y ) <-> ( `' F ` c ) e. ( x J y ) ) )
1841832ralbidv 2832 . . . . . . . . . . . . . 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 473 . . . . . . . . . . . . 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 3140 . . . . . . . . . . . 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 472 . . . . . . . . . . 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 744 . . . . . . . . . . 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 5185 . . . . . . . . . . . 12 |- ( F " s ) C_ ran F
191 f1ofo 5835 . . . . . . . . . . . . . 14 |- ( F : B -1-1-onto-> P -> F : B -onto-> P )
192 forn 5809 . . . . . . . . . . . . . 14 |- ( F : B -onto-> P -> ran F = P )
1939, 191, 1923syl 18 . . . . . . . . . . . . 13 |- ( ph -> ran F = P )
194193ad3antrrr 744 . . . . . . . . . . . 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 3466 . . . . . . . . . . 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 5185 . . . . . . . . . . . 12 |- ( F " t ) C_ ran F
197196, 194syl5sseq 3466 . . . . . . . . . . 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 744 . . . . . . . . . . . 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 770 . . . . . . . . . . . 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 6038 . . . . . . . . . . 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 748 . . . . . . . . . . . . . . . . . 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 5739 . . . . . . . . . . . . . . . . . 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 740 . . . . . . . . . . . . . . . . 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 770 . . . . . . . . . . . . . . . . 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 6161 . . . . . . . . . . . . . . . . 17 |- ( ( `' F Fn P /\ ( F " s ) C_ P /\ u e. ( F " s ) ) -> ( `' F ` u ) e. ( `' F " ( F " s ) ) )
207203, 204, 205, 206syl3anc 1292 . . . . . . . . . . . . . . . 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 787 . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . 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 3952 . . . . . . . . . . . . . . . . 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 5844 . . . . . . . . . . . . . . . . 17 |- ( ( F : B -1-1-> P /\ s C_ B ) -> ( `' F " ( F " s ) ) = s )
213208, 211, 212syl2anc 673 . . . . . . . . . . . . . . . 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 2551 . . . . . . . . . . . . . . 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 740 . . . . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . . . . 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 6161 . . . . . . . . . . . . . . . . 17 |- ( ( `' F Fn P /\ ( F " t ) C_ P /\ v e. ( F " t ) ) -> ( `' F ` v ) e. ( `' F " ( F " t ) ) )
218203, 215, 216, 217syl3anc 1292 . . . . . . . . . . . . . . . 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 470 . . . . . . . . . . . . . . . . . 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 3952 . . . . . . . . . . . . . . . . 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 5844 . . . . . . . . . . . . . . . . 17 |- ( ( F : B -1-1-> P /\ t C_ B ) -> ( `' F " ( F " t ) ) = t )
222208, 220, 221syl2anc 673 . . . . . . . . . . . . . . . 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 2551 . . . . . . . . . . . . . . 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 777 . . . . . . . . . . . . . . 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 2537 . . . . . . . . . . . . . . . 16 |- ( x = ( `' F ` u ) -> ( x e. ( a J y ) <-> ( `' F ` u ) e. ( a J y ) ) )
226 oveq2 6316 . . . . . . . . . . . . . . . . 17 |- ( y = ( `' F ` v ) -> ( a J y ) = ( a J ( `' F ` v ) ) )
227226eleq2d 2534 . . . . . . . . . . . . . . . 16 |- ( y = ( `' F ` v ) -> ( ( `' F ` u ) e. ( a J y ) <-> ( `' F ` u ) e. ( a J ( `' F ` v ) ) ) )
228225, 227rspc2va 3148 . . . . . . . . . . . . . . 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 1291 . . . . . . . . . . . . . 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 788 . . . . . . . . . . . . . . . 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 680 . . . . . . . . . . . . . . 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 788 . . . . . . . . . . . . . . . 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 680 . . . . . . . . . . . . . . 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 785 . . . . . . . . . . . . . . 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 3419 . . . . . . . . . . . . . . . 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 6201 . . . . . . . . . . . . . . . 16 |- ( ( F : B -1-1-onto-> P /\ v e. P ) -> ( `' F ` v ) e. B )
237201, 235, 236syl2anc 673 . . . . . . . . . . . . . . 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 3419 . . . . . . . . . . . . . . . 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 6201 . . . . . . . . . . . . . . . 16 |- ( ( F : B -1-1-onto-> P /\ u e. P ) -> ( `' F ` u ) e. B )
240201, 238, 239syl2anc 673 . . . . . . . . . . . . . . 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 24979 . . . . . . . . . . . . . 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 215 . . . . . . . . . . . . 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 6194 . . . . . . . . . . . . . 14 |- ( ( F : B -1-1-onto-> P /\ u e. P ) -> ( F ` ( `' F ` u ) ) = u )
244201, 238, 243syl2anc 673 . . . . . . . . . . . . 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 6194 . . . . . . . . . . . . . . 15 |- ( ( F : B -1-1-onto-> P /\ v e. P ) -> ( F ` ( `' F ` v ) ) = v )
246201, 235, 245syl2anc 673 . . . . . . . . . . . . . 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 6324 . . . . . . . . . . . . 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 2563 . . . . . . . . . . . 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 1226 . . . . . . . . . . 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 24596 . . . . . . . . . 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 2918 . . . . . . . . 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 2917 . . . . . . . 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 441 . . . . . . 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 2814 . . . . . 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 1210 . . . . 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 24582 . . . . 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 677 . . . 4 |- ( ph -> H e. TarskiGB )
25857, 257elind 3609 . . 3 |- ( ph -> H e. (TarskiGC i^i TarskiGB ) )
2597ad9antr 756 . . . . . . . . . . . . . . . . 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 756 . . . . . . . . . . . . . . . . . 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 795 . . . . . . . . . . . . . . . . . 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 6038 . . . . . . . . . . . . . . . . 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 793 . . . . . . . . . . . . . . . . . 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 6038 . . . . . . . . . . . . . . . . 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 791 . . . . . . . . . . . . . . . . . 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 6038 . . . . . . . . . . . . . . . . 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