MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1otrg Structured version   Unicode version
Theorem f1otrg 23850
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 . . . . . . 7 |- ( ph -> H e. V )
2 elex 3122 . . . . . . 7 |- ( H e. V -> H e. _V )
31, 2syl 16 . . . . . 6 |- ( ph -> H e. _V )
4 f1otrkg.p . . . . . . . . . 10 |- P = ( Base ` G )
5 f1otrkg.d . . . . . . . . . 10 |- D = ( dist ` G )
6 f1otrkg.i . . . . . . . . . 10 |- I = (Itv ` G )
7 f1otrg.g . . . . . . . . . . 11 |- ( ph -> G e. TarskiG )
87adantr 465 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> G e. TarskiG )
9 f1otrkg.f . . . . . . . . . . . . 13 |- ( ph -> F : B -1-1-onto-> P )
10 f1of 5814 . . . . . . . . . . . . 13 |- ( F : B -1-1-onto-> P -> F : B --> P )
119, 10syl 16 . . . . . . . . . . . 12 |- ( ph -> F : B --> P )
1211adantr 465 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> F : B --> P )
13 simprl 755 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> x e. B )
1412, 13ffvelrnd 6020 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` x ) e. P )
15 simprr 756 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> y e. B )
1612, 15ffvelrnd 6020 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` y ) e. P )
174, 5, 6, 8, 14, 16axtgcgrrflx 23587 . . . . . . . . 9 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( F ` x ) D ( F ` y ) ) = ( ( F ` y ) D ( F ` x ) ) )
18 f1otrkg.b . . . . . . . . . 10 |- B = ( Base ` H )
19 f1otrkg.e . . . . . . . . . 10 |- E = ( dist ` H )
20 f1otrkg.j . . . . . . . . . 10 |- J = (Itv ` H )
219adantr 465 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> F : B -1-1-onto-> P )
22 f1otrkg.1 . . . . . . . . . . 11 |- ( ( ph /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
2322adantlr 714 . . . . . . . . . 10 |- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
24 f1otrkg.2 . . . . . . . . . . 11 |- ( ( ph /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )
2524adantlr 714 . . . . . . . . . 10 |- ( ( ( 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 23848 . . . . . . . . 9 |- ( ( 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 23848 . . . . . . . . 9 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( y E x ) = ( ( F ` y ) D ( F ` x ) ) )
2817, 26, 273eqtr4d 2518 . . . . . . . 8 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x E y ) = ( y E x ) )
2928ralrimivva 2885 . . . . . . 7 |- ( ph -> A. x e. B A. y e. B ( x E y ) = ( y E x ) )
30 f1of1 5813 . . . . . . . . . . . 12 |- ( F : B -1-1-onto-> P -> F : B -1-1-> P )
319, 30syl 16 . . . . . . . . . . 11 |- ( ph -> F : B -1-1-> P )
32313ad2ant1 1017 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> F : B -1-1-> P )
33 simp1 996 . . . . . . . . . . . 12 |- ( ( x e. B /\ y e. B /\ z e. B ) -> x e. B )
34333ad2ant2 1018 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> x e. B )
35 simp22 1030 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> y e. B )
3634, 35jca 532 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( x e. B /\ y e. B ) )
3773ad2ant1 1017 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> G e. TarskiG )
38113ad2ant1 1017 . . . . . . . . . . . 12 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> F : B --> P )
39 simp21 1029 . . . . . . . . . . . 12 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> x e. B )
4038, 39ffvelrnd 6020 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( F ` x ) e. P )
4138, 35ffvelrnd 6020 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( F ` y ) e. P )
42 simp23 1031 . . . . . . . . . . . 12 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> z e. B )
4338, 42ffvelrnd 6020 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( F ` z ) e. P )
44 simp3 998 . . . . . . . . . . . 12 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( x E y ) = ( z E z ) )
4593ad2ant1 1017 . . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> F : B -1-1-onto-> P )
46223ad2antl1 1158 . . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
47243ad2antl1 1158 . . . . . . . . . . . . 13 |- ( ( ( 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 ) ) ) )
484, 5, 6, 18, 19, 20, 45, 46, 47, 39, 35f1otrgds 23848 . . . . . . . . . . . 12 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( x E y ) = ( ( F ` x ) D ( F ` y ) ) )
494, 5, 6, 18, 19, 20, 45, 46, 47, 42, 42f1otrgds 23848 . . . . . . . . . . . 12 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( z E z ) = ( ( F ` z ) D ( F ` z ) ) )
5044, 48, 493eqtr3d 2516 . . . . . . . . . . 11 |- ( ( 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 ) ) )
514, 5, 6, 37, 40, 41, 43, 50axtgcgrid 23588 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> ( F ` x ) = ( F ` y ) )
52 f1veqaeq 6154 . . . . . . . . . . 11 |- ( ( F : B -1-1-> P /\ ( x e. B /\ y e. B ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
5352imp 429 . . . . . . . . . 10 |- ( ( ( F : B -1-1-> P /\ ( x e. B /\ y e. B ) ) /\ ( F ` x ) = ( F ` y ) ) -> x = y )
5432, 36, 51, 53syl21anc 1227 . . . . . . . . 9 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( x E y ) = ( z E z ) ) -> x = y )
55543expia 1198 . . . . . . . 8 |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x E y ) = ( z E z ) -> x = y ) )
5655ralrimivvva 2886 . . . . . . 7 |- ( ph -> A. x e. B A. y e. B A. z e. B ( ( x E y ) = ( z E z ) -> x = y ) )
5729, 56jca 532 . . . . . 6 |- ( 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 ) ) )
583, 57jca 532 . . . . 5 |- ( ph -> ( 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 ) ) ) )
5918, 19, 20istrkgc 23579 . . . . 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 ) ) ) )
6058, 59sylibr 212 . . . 4 |- ( ph -> H e. TarskiGC )
61213adant3 1016 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> F : B -1-1-onto-> P )
6261, 30syl 16 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> F : B -1-1-> P )
63133adant3 1016 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> x e. B )
64153adant3 1016 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> y e. B )
6563, 64jca 532 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> ( x e. B /\ y e. B ) )
6683adant3 1016 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> G e. TarskiG )
67143adant3 1016 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> ( F ` x ) e. P )
68163adant3 1016 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> ( F ` y ) e. P )
69 simp3 998 . . . . . . . . . . . 12 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> y e. ( x J x ) )
70233adantl3 1154 . . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
71253adantl3 1154 . . . . . . . . . . . . 13 |- ( ( ( 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 ) ) ) )
724, 5, 6, 18, 19, 20, 61, 70, 71, 63, 63, 64f1otrgitv 23849 . . . . . . . . . . . 12 |- ( ( 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 ) ) ) )
7369, 72mpbid 210 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> ( F ` y ) e. ( ( F ` x ) I ( F ` x ) ) )
744, 5, 6, 66, 67, 68, 73axtgbtwnid 23591 . . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> ( F ` x ) = ( F ` y ) )
7562, 65, 74, 53syl21anc 1227 . . . . . . . . 9 |- ( ( ph /\ ( x e. B /\ y e. B ) /\ y e. ( x J x ) ) -> x = y )
76753expia 1198 . . . . . . . 8 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( y e. ( x J x ) -> x = y ) )
7776ralrimivva 2885 . . . . . . 7 |- ( ph -> A. x e. B A. y e. B ( y e. ( x J x ) -> x = y ) )
78 simprl 755 . . . . . . . . . . . . . . 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 ) ) ) ) -> c e. ( ( F ` u ) I ( F ` y ) ) )
7921ad2antrr 725 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 )
8079ad2antrr 725 . . . . . . . . . . . . . . . 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 ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) -> F : B -1-1-onto-> P )
81 simplr 754 . . . . . . . . . . . . . . . 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 ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) -> c e. P )
82 f1ocnvfv2 6169 . . . . . . . . . . . . . . . . 17 |- ( ( F : B -1-1-onto-> P /\ c e. P ) -> ( F ` ( `' F ` c ) ) = c )
8382eleq1d 2536 . . . . . . . . . . . . . . . 16 |- ( ( 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 ) ) ) )
8480, 81, 83syl2anc 661 . . . . . . . . . . . . . . 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 ` ( `' F ` c ) ) e. ( ( F ` u ) I ( F ` y ) ) <-> c e. ( ( F ` u ) I ( F ` y ) ) ) )
8578, 84mpbird 232 . . . . . . . . . . . . . 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 ) ) )
86 simplll 757 . . . . . . . . . . . . . . . 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 ) ) ) /\ 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 ) ) ) )
87 simpr 461 . . . . . . . . . . . . . . . 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 ) ) ) /\ 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. B /\ f e. B ) )
88 simplll 757 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( 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 ) ) )
89 simpr 461 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( 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. B /\ f e. B ) )
9088, 89, 23syl2anc 661 . . . . . . . . . . . . . . . 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 ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
9186, 87, 90syl2anc 661 . . . . . . . . . . . . . . 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 ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
92 simplll 757 . . . . . . . . . . . . . . . 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 ) ) ) /\ 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 ) ) ) )
93 simpr 461 . . . . . . . . . . . . . . . 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 ) ) ) /\ 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 ) ) -> ( e e. B /\ f e. B /\ g e. B ) )
94 simplll 757 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( 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 ) ) )
95 simpr 461 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( 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 ) ) -> ( e e. B /\ f e. B /\ g e. B ) )
9694, 95, 25syl2anc 661 . . . . . . . . . . . . . . . 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 ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )
9792, 93, 96syl2anc 661 . . . . . . . . . . . . . . 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 ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )
98 simplr2 1039 . . . . . . . . . . . . . . . 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 ) ) ) -> u e. B )
9998ad2antrr 725 . . . . . . . . . . . . . . 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 ) ) ) ) -> u e. B )
10015ad2antrr 725 . . . . . . . . . . . . . . . 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 ) ) ) -> y e. B )
101100ad2antrr 725 . . . . . . . . . . . . . . 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 ) ) ) ) -> y e. B )
102 f1ocnv 5826 . . . . . . . . . . . . . . . . . 18 |- ( F : B -1-1-onto-> P -> `' F : P -1-1-onto-> B )
103 f1of 5814 . . . . . . . . . . . . . . . . . 18 |- ( `' F : P -1-1-onto-> B -> `' F : P --> B )
1049, 102, 1033syl 20 . . . . . . . . . . . . . . . . 17 |- ( ph -> `' F : P --> B )
105104ad5antr 733 . . . . . . . . . . . . . . . 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 ) ) ) /\ c e. P ) /\ ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) ) -> `' F : P --> B )
106105, 81ffvelrnd 6020 . . . . . . . . . . . . . . 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 ` c ) e. B )
1074, 5, 6, 18, 19, 20, 80, 91, 97, 99, 101, 106f1otrgitv 23849 . . . . . . . . . . . . . 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 ` c ) e. ( u J y ) <-> ( F ` ( `' F ` c ) ) e. ( ( F ` u ) I ( F ` y ) ) ) )
10885, 107mpbird 232 . . . . . . . . . . . . 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 ) )
109 simprr 756 . . . . . . . . . . . . . . 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 ) ) ) ) -> c e. ( ( F ` v ) I ( F ` x ) ) )
11082eleq1d 2536 . . . . . . . . . . . . . . . 16 |- ( ( 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 ) ) ) )
11180, 81, 110syl2anc 661 . . . . . . . . . . . . . . 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 ` ( `' F ` c ) ) e. ( ( F ` v ) I ( F ` x ) ) <-> c e. ( ( F ` v ) I ( F ` x ) ) ) )
112109, 111mpbird 232 . . . . . . . . . . . . . 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 ) ) )
113 simplr3 1040 . . . . . . . . . . . . . . . 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 ) ) ) -> v e. B )
114113ad2antrr 725 . . . . . . . . . . . . . . 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 ) ) ) ) -> v e. B )
11513ad2antrr 725 . . . . . . . . . . . . . . . 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 ) ) ) -> x e. B )
116115ad2antrr 725 . . . . . . . . . . . . . . 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 ) ) ) ) -> x e. B )
1174, 5, 6, 18, 19, 20, 80, 91, 97, 114, 116, 106f1otrgitv 23849 . . . . . . . . . . . . . 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 ` c ) e. ( v J x ) <-> ( F ` ( `' F ` c ) ) e. ( ( F ` v ) I ( F ` x ) ) ) )
118112, 117mpbird 232 . . . . . . . . . . . . 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 ) )
119108, 118jca 532 . . . . . . . . . . . 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 ) /\ ( `' F ` c ) e. ( v J x ) ) )
120 simpr 461 . . . . . . . . . . . . . . 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 ) ) ) ) /\ a = ( `' F ` c ) ) -> a = ( `' F ` c ) )
121120eleq1d 2536 . . . . . . . . . . . . . 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 ) ) ) ) /\ a = ( `' F ` c ) ) -> ( a e. ( u J y ) <-> ( `' F ` c ) e. ( u J y ) ) )
122120eleq1d 2536 . . . . . . . . . . . . . 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 ) ) ) ) /\ a = ( `' F ` c ) ) -> ( a e. ( v J x ) <-> ( `' F ` c ) e. ( v J x ) ) )
123121, 122anbi12d 710 . . . . . . . . . . . . 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 e. ( u J y ) /\ a e. ( v J x ) ) <-> ( ( `' F ` c ) e. ( u J y ) /\ ( `' F ` c ) e. ( v J x ) ) ) )
124106, 123rspcedv 3218 . . . . . . . . . . . 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 ) /\ ( `' F ` c ) e. ( v J x ) ) -> E. a e. B ( a e. ( u J y ) /\ a e. ( v J x ) ) ) )
125119, 124mpd 15 . . . . . . . . . . 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 ) ) ) ) -> E. a e. B ( a e. ( u J y ) /\ a e. ( v J x ) ) )
1268ad2antrr 725 . . . . . . . . . . . 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 ) ) ) -> G e. TarskiG )
12712ad2antrr 725 . . . . . . . . . . . . 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 ) ) ) -> F : B --> P )
128127, 115ffvelrnd 6020 . . . . . . . . . . . 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 ` x ) e. P )
129127, 100ffvelrnd 6020 . . . . . . . . . . . 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 ` y ) e. P )
130 simplr1 1038 . . . . . . . . . . . . 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 ) ) ) -> z e. B )
131127, 130ffvelrnd 6020 . . . . . . . . . . . 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 ` z ) e. P )
132127, 98ffvelrnd 6020 . . . . . . . . . . . 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 ` u ) e. P )
133127, 113ffvelrnd 6020 . . . . . . . . . . . 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 ` v ) e. P )
134 simprl 755 . . . . . . . . . . . . 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 ) ) ) -> u e. ( x J z ) )
1354, 5, 6, 18, 19, 20, 79, 90, 96, 115, 130, 98f1otrgitv 23849 . . . . . . . . . . . . 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 ) ) ) -> ( u e. ( x J z ) <-> ( F ` u ) e. ( ( F ` x ) I ( F ` z ) ) ) )
136134, 135mpbid 210 . . . . . . . . . . . 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 ` u ) e. ( ( F ` x ) I ( F ` z ) ) )
137 simprr 756 . . . . . . . . . . . . 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 ) ) ) -> v e. ( y J z ) )
1384, 5, 6, 18, 19, 20, 79, 90, 96, 100, 130, 113f1otrgitv 23849 . . . . . . . . . . . . 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 ) ) ) -> ( v e. ( y J z ) <-> ( F ` v ) e. ( ( F ` y ) I ( F ` z ) ) ) )
139137, 138mpbid 210 . . . . . . . . . . . 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 ` v ) e. ( ( F ` y ) I ( F ` z ) ) )
1404, 5, 6, 126, 128, 129, 131, 132, 133, 136, 139axtgpasch 23592 . . . . . . . . . . 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 ) ) ) -> E. c e. P ( c e. ( ( F ` u ) I ( F ` y ) ) /\ c e. ( ( F ` v ) I ( F ` x ) ) ) )
141125, 140r19.29a 3003 . . . . . . . . . 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. a e. B ( a e. ( u J y ) /\ a e. ( v J x ) ) )
142141ex 434 . . . . . . . . 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 ) ) ) )
143142ralrimivvva 2886 . . . . . . . 8 |- ( ( 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 ) ) ) )
144143ralrimivva 2885 . . . . . . 7 |- ( 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 ) ) ) )
145 nfv 1683 . . . . . . . . . . 11 |- F/ a ( ph /\ ( s e. ~P B /\ t e. ~P B ) )
146 nfre1 2925 . . . . . . . . . . 11 |- F/ a E. a e. B A. x e. s A. y e. t x e. ( a J y )
147145, 146nfan 1875 . . . . . . . . . 10 |- F/ a ( ( 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 ) )
1489ad5antr 733 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( 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 )
149 simpllr 758 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( 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 )
150148, 149, 82syl2anc 661 . . . . . . . . . . . . . . . . 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 ` ( `' F ` c ) ) = c )
151 ffn 5729 . . . . . . . . . . . . . . . . . . . 20 |- ( F : B --> P -> F Fn B )
152148, 10, 1513syl 20 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( 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 )
153 simp-4r 766 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( 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 ) )
154153simpld 459 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( 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 )
155 elpwi 4019 . . . . . . . . . . . . . . . . . . . . 21 |- ( s e. ~P B -> s C_ B )
156154, 155syl 16 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> s C_ B )
157156adantlr 714 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( 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 )
158 simprl 755 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( 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 )
159 fnfvima 6136 . . . . . . . . . . . . . . . . . . 19 |- ( ( F Fn B /\ s C_ B /\ x e. s ) -> ( F ` x ) e. ( F " s ) )
160152, 157, 158, 159syl3anc 1228 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( 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 ) )
161153simprd 463 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( 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 )
162 elpwi 4019 . . . . . . . . . . . . . . . . . . . . 21 |- ( t e. ~P B -> t C_ B )
163161, 162syl 16 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> t C_ B )
164163adantlr 714 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( 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 )
165 simprr 756 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( 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 )
166 fnfvima 6136 . . . . . . . . . . . . . . . . . . 19 |- ( ( F Fn B /\ t C_ B /\ y e. t ) -> ( F ` y ) e. ( F " t ) )
167152, 164, 165, 166syl3anc 1228 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( 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 ) )
168 simplr 754 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( 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 ) )
169 oveq1 6289 . . . . . . . . . . . . . . . . . . . . 21 |- ( e = ( F ` x ) -> ( e I f ) = ( ( F ` x ) I f ) )
170169eleq2d 2537 . . . . . . . . . . . . . . . . . . . 20 |- ( e = ( F ` x ) -> ( c e. ( e I f ) <-> c e. ( ( F ` x ) I f ) ) )
171 oveq2 6290 . . . . . . . . . . . . . . . . . . . . 21 |- ( f = ( F ` y ) -> ( ( F ` x ) I f ) = ( ( F ` x ) I ( F ` y ) ) )
172171eleq2d 2537 . . . . . . . . . . . . . . . . . . . 20 |- ( f = ( F ` y ) -> ( c e. ( ( F ` x ) I f ) <-> c e. ( ( F ` x ) I ( F ` y ) ) ) )
173170, 172rspc2v 3223 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 ) ) ) )
174173imp 429 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( 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 ) ) )
175160, 167, 168, 174syl21anc 1227 . . . . . . . . . . . . . . . . 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 ) ) -> c e. ( ( F ` x ) I ( F ` y ) ) )
176150, 175eqeltrd 2555 . . . . . . . . . . . . . . . 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 ` ( `' F ` c ) ) e. ( ( F ` x ) I ( F ` y ) ) )
1779ad4antr 731 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( 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 )
178 simp-5l 767 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( 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 )
179 simpr 461 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( 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. B /\ f e. B ) )
180178, 179, 22syl2anc 661 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( 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 ) ) )
181 simp-5l 767 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( 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 )
182 simpr 461 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( 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 ) ) -> ( e e. B /\ f e. B /\ g e. B ) )
183181, 182, 24syl2anc 661 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( 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 ) ) ) )
184 simprl 755 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> x e. s )
185156, 184sseldd 3505 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> x e. B )
186 simprr 756 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> y e. t )
187163, 186sseldd 3505 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> y e. B )
188104ad4antr 731 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> `' F : P --> B )
189 simplr 754 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ ( s e. ~P B /\ t e. ~P B ) ) /\ a e. B ) /\ c e. P ) /\ ( x e. s /\ y e. t ) ) -> c e. P )
190188, 189ffvelrnd 6020 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( 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 )
1914, 5, 6, 18, 19, 20, 177, 180, 183, 185, 187, 190f1otrgitv 23849 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( 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 ) ) ) )
192191adantlr 714 . . . . . . . . . . . . . . . 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 ` c ) e. ( x J y ) <-> ( F ` ( `' F ` c ) ) e. ( ( F ` x ) I ( F ` y ) ) ) )
193176, 192mpbird 232 . . . . . . . . . . . . . . 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 ` c ) e. ( x J y ) )
194193ralrimivva 2885 . . . . . . . . . . . . . 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 ) ) -> A. x e. s A. y e. t ( `' F ` c ) e. ( x J y ) )
195194adantllr 718 . . . . . . . . . . . . 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 ) /\ 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 ) )
196104ad4antr 731 . . . . . . . . . . . . . . . 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 ) ) /\ c e. P ) -> `' F : P --> B )
197 simpr 461 . . . . . . . . . . . . . . . 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 ) ) /\ c e. P ) -> c e. P )
198196, 197ffvelrnd 6020 . . . . . . . . . . . . . . 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 ) ) /\ c e. P ) -> ( `' F ` c ) e. B )
199 id 22 . . . . . . . . . . . . . . . . . 18 |- ( b = ( `' F ` c ) -> b = ( `' F ` c ) )
200199eleq1d 2536 . . . . . . . . . . . . . . . . 17 |- ( b = ( `' F ` c ) -> ( b e. ( x J y ) <-> ( `' F ` c ) e. ( x J y ) ) )
2012002ralbidv 2908 . . . . . . . . . . . . . . . 16 |- ( 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 ) ) )
202201adantl 466 . . . . . . . . . . . . . . 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 ) ) /\ 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 ) ) )
203198, 202rspcedv 3218 . . . . . . . . . . . . . 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 ) -> ( 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 ) ) )
204203adantr 465 . . . . . . . . . . . . 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 ) /\ 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 ) ) )
205195, 204mpd 15 . . . . . . . . . . . 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. 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 ) )
2067ad3antrrr 729 . . . . . . . . . . . . 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 ) ) -> G e. TarskiG )
207 imassrn 5346 . . . . . . . . . . . . . 14 |- ( F " s ) C_ ran F
208 f1ofo 5821 . . . . . . . . . . . . . . . . 17 |- ( F : B -1-1-onto-> P -> F : B -onto-> P )
2099, 208syl 16 . . . . . . . . . . . . . . . 16 |- ( ph -> F : B -onto-> P )
210 forn 5796 . . . . . . . . . . . . . . . 16 |- ( F : B -onto-> P -> ran F = P )
211209, 210syl 16 . . . . . . . . . . . . . . 15 |- ( ph -> ran F = P )
212211ad3antrrr 729 . . . . . . . . . . . . . 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 ) ) -> ran F = P )
213207, 212syl5sseq 3552 . . . . . . . . . . . . 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 ) ) -> ( F " s ) C_ P )
214 imassrn 5346 . . . . . . . . . . . . . 14 |- ( F " t ) C_ ran F
215214, 212syl5sseq 3552 . . . . . . . . . . . . 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 ) ) -> ( F " t ) C_ P )
21611ad3antrrr 729 . . . . . . . . . . . . . 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 ) ) -> F : B --> P )
217 simplr 754 . . . . . . . . . . . . . 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 ) ) -> a e. B )
218216, 217ffvelrnd 6020 . . . . . . . . . . . . 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 ) ) -> ( F ` a ) e. P )
2199ad5antr 733 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( 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 )
220 ffn 5729 . . . . . . . . . . . . . . . . . . . 20 |- ( `' F : P --> B -> `' F Fn P )
221219, 102, 103, 2204syl 21 . . . . . . . . . . . . . . . . . . 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 ) ) -> `' F Fn P )
222213ad2antrr 725 . . . . . . . . . . . . . . . . . . 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 ) ) -> ( F " s ) C_ P )
223 simplr 754 . . . . . . . . . . . . . . . . . . 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 ) ) -> u e. ( F " s ) )
224 fnfvima 6136 . . . . . . . . . . . . . . . . . . 19 |- ( ( `' F Fn P /\ ( F " s ) C_ P /\ u e. ( F " s ) ) -> ( `' F ` u ) e. ( `' F " ( F " s ) ) )
225221, 222, 223, 224syl3anc 1228 . . . . . . . . . . . . . . . . . 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 ` u ) e. ( `' F " ( F " s ) ) )
226219, 30syl 16 . . . . . . . . . . . . . . . . . . 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 ) ) -> F : B -1-1-> P )
227 simp-5r 768 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( 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 ) )
228227simpld 459 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( 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 )
229228, 155syl 16 . . . . . . . . . . . . . . . . . . 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 C_ B )
230 f1imacnv 5830 . . . . . . . . . . . . . . . . . . 19 |- ( ( F : B -1-1-> P /\ s C_ B ) -> ( `' F " ( F " s ) ) = s )
231226, 229, 230syl2anc 661 . . . . . . . . . . . . . . . . . 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 " ( F " s ) ) = s )
232225, 231eleqtrd 2557 . . . . . . . . . . . . . . . . 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 ` u ) e. s )
233215ad2antrr 725 . . . . . . . . . . . . . . . . . . 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 ) ) -> ( F " t ) C_ P )
234 simpr 461 . . . . . . . . . . . . . . . . . . 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 ) ) -> v e. ( F " t ) )
235 fnfvima 6136 . . . . . . . . . . . . . . . . . . 19 |- ( ( `' F Fn P /\ ( F " t ) C_ P /\ v e. ( F " t ) ) -> ( `' F ` v ) e. ( `' F " ( F " t ) ) )
236221, 233, 234, 235syl3anc 1228 . . . . . . . . . . . . . . . . . 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 ` v ) e. ( `' F " ( F " t ) ) )
237227simprd 463 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( 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 )
238237, 162syl 16 . . . . . . . . . . . . . . . . . . 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 ) ) -> t C_ B )
239 f1imacnv 5830 . . . . . . . . . . . . . . . . . . 19 |- ( ( F : B -1-1-> P /\ t C_ B ) -> ( `' F " ( F " t ) ) = t )
240226, 238, 239syl2anc 661 . . . . . . . . . . . . . . . . . 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 " ( F " t ) ) = t )
241236, 240eleqtrd 2557 . . . . . . . . . . . . . . . . 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 ` v ) e. t )
242 simpllr 758 . . . . . . . . . . . . . . . . 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 ) ) -> A. x e. s A. y e. t x e. ( a J y ) )
243 eleq1 2539 . . . . . . . . . . . . . . . . . . 19 |- ( x = ( `' F ` u ) -> ( x e. ( a J y ) <-> ( `' F ` u ) e. ( a J y ) ) )
244 oveq2 6290 . . . . . . . . . . . . . . . . . . . 20 |- ( y = ( `' F ` v ) -> ( a J y ) = ( a J ( `' F ` v ) ) )
245244eleq2d 2537 . . . . . . . . . . . . . . . . . . 19 |- ( y = ( `' F ` v ) -> ( ( `' F ` u ) e. ( a J y ) <-> ( `' F ` u ) e. ( a J ( `' F ` v ) ) ) )
246243, 245rspc2v 3223 . . . . . . . . . . . . . . . . . 18 |- ( ( ( `' 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 ) ) ) )
247246imp 429 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( `' 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 ) ) )
248232, 241, 242, 247syl21anc 1227 . . . . . . . . . . . . . . . 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. ( a J ( `' F ` v ) ) )
249 simp-6l 769 . . . . . . . . . . . . . . . . . 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 ) ) /\ ( e e. B /\ f e. B ) ) -> ph )
250 simpr 461 . . . . . . . . . . . . . . . . . 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 ) ) /\ ( e e. B /\ f e. B ) ) -> ( e e. B /\ f e. B ) )
251249, 250, 22syl2anc 661 . . . . . . . . . . . . . . . . 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 ) ) /\ ( e e. B /\ f e. B ) ) -> ( e E f ) = ( ( F ` e ) D ( F ` f ) ) )
252 simp-6l 769 . . . . . . . . . . . . . . . . . 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 ) ) /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ph )
253 simpr 461 . . . . . . . . . . . . . . . . . 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 ) ) /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( e e. B /\ f e. B /\ g e. B ) )
254252, 253, 24syl2anc 661 . . . . . . . . . . . . . . . . 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 ) ) /\ ( e e. B /\ f e. B /\ g e. B ) ) -> ( g e. ( e J f ) <-> ( F ` g ) e. ( ( F ` e ) I ( F ` f ) ) ) )
255217ad2antrr 725 . . . . . . . . . . . . . . . . 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 ) ) -> a e. B )
256233, 234sseldd 3505 . . . . . . . . . . . . . . . . . 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 ) ) -> v e. P )
257 f1ocnvdm 6174 . . . . . . . . . . . . . . . . . 18 |- ( ( F : B -1-1-onto-> P /\ v e. P ) -> ( `' F ` v ) e. B )
258219, 256, 257syl2anc 661 . . . . . . . . . . . . . . . . 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 ` v ) e. B )
259222, 223sseldd 3505 . . . . . . . . . . . . . . . . . 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 ) ) -> u e. P )
260 f1ocnvdm 6174 . . . . . . . . . . . . . . . . . 18 |- ( ( F : B -1-1-onto-> P /\ u e. P ) -> ( `' F ` u ) e. B )
261219, 259, 260syl2anc 661 . . . . . . . . . . . . . . . . 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 ` u ) e. B )
2624, 5, 6, 18, 19, 20, 219, 251, 254, 255, 258, 261f1otrgitv 23849 . . . . . . . . . . . . . . . 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. ( a J ( `' F ` v ) ) <-> ( F ` ( `' F ` u ) ) e. ( ( F ` a ) I ( F ` ( `' F ` v ) ) ) ) )
263248, 262mpbid 210 . . . . . . . . . . . . . . 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 ` ( `' F ` u ) ) e. ( ( F ` a ) I ( F ` ( `' F ` v ) ) ) )
264 f1ocnvfv2 6169 . . . . . . . . . . . . . . . . 17 |- ( ( F : B -1-1-onto-> P /\ u e. P ) -> ( F ` ( `' F ` u ) ) = u )
265219, 259, 264syl2anc 661 . . . . . . . . . . . . . . . 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 ` u ) ) = u )
266 f1ocnvfv2 6169 . . . . . . . . . . . . . . . . . 18 |- ( ( F : B -1-1-onto-> P /\ v e. P ) -> ( F ` ( `' F ` v ) ) = v )
267219, 256, 266syl2anc 661 . . . . . . . . . . . . . . . . 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 ` ( `' F ` v ) ) = v )
268267oveq2d 6298 . . . . . . . . . . . . . . . 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 ` a ) I ( F ` ( `' F ` v ) ) ) = ( ( F ` a ) I v ) )
269265, 268eleq12d 2549 . . . . . . . . . . . . . . 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 ` ( `' F ` u ) ) e. ( ( F ` a ) I ( F ` ( `' F ` v ) ) ) <-> u e. ( ( F ` a ) I v ) ) )
270263, 269mpbid 210 . . . . . . . . . . . . . 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 ) ) -> u e. ( ( F ` a ) I v ) )
2712703impa 1191 . . . . . . . . . . . . 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 ) ) -> u e. ( ( F ` a ) I v ) )
2724, 5, 6, 206, 213, 215, 218, 271axtgcont 23594 . . . . . . . . . . . 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 ) ) -> E. c e. P A. e e. ( F " s ) A. f e. ( F " t ) c e. ( e I f ) )
273205, 272r19.29a 3003 . . . . . . . . . . 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 ) ) -> E. b e. B A. x e. s A. y e. t b e. ( x J y ) )
274273adantllr 718 . . . . . . . . . 10 |- ( ( ( ( ( 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 ) ) /\ 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 ) )
275 simpr 461 . . . . . . . . . 10 |- ( ( ( ph /\ ( s e. ~P B