MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1otrg Structured version   Unicode version

Theorem f1otrg 23122
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 2986 . . . . . . 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 5646 . . . . . . . . . . . . 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 5849 . . . . . . . . . 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 5849 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( F `  y
)  e.  P )
174, 5, 6, 8, 14, 16axtgcgrrflx 22928 . . . . . . . . 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 23120 . . . . . . . . 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 23120 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( y E x )  =  ( ( F `  y ) D ( F `  x ) ) )
2817, 26, 273eqtr4d 2485 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( x E y )  =  ( y E x ) )
2928ralrimivva 2813 . . . . . . 7  |-  ( ph  ->  A. x  e.  B  A. y  e.  B  ( x E y )  =  ( y E x ) )
30 f1of1 5645 . . . . . . . . . . . 12  |-  ( F : B -1-1-onto-> P  ->  F : B -1-1-> P )
319, 30syl 16 . . . . . . . . . . 11  |-  ( ph  ->  F : B -1-1-> P
)
32313ad2ant1 1009 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  ->  F : B -1-1-> P )
33 simp1 988 . . . . . . . . . . . 12  |-  ( ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  ->  x  e.  B )
34333ad2ant2 1010 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  ->  x  e.  B )
35 simp22 1022 . . . . . . . . . . 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 1009 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  ->  G  e. TarskiG )
38113ad2ant1 1009 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  ->  F : B --> P )
39 simp21 1021 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  ->  x  e.  B )
4038, 39ffvelrnd 5849 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  -> 
( F `  x
)  e.  P )
4138, 35ffvelrnd 5849 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  -> 
( F `  y
)  e.  P )
42 simp23 1023 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  -> 
z  e.  B )
4338, 42ffvelrnd 5849 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  -> 
( F `  z
)  e.  P )
44 simp3 990 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  -> 
( x E y )  =  ( z E z ) )
4593ad2ant1 1009 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  ->  F : B -1-1-onto-> P )
46223ad2antl1 1150 . . . . . . . . . . . . 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 1150 . . . . . . . . . . . . 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 23120 . . . . . . . . . . . 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 23120 . . . . . . . . . . . 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 2483 . . . . . . . . . . 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 22929 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  -> 
( F `  x
)  =  ( F `
 y ) )
52 f1veqaeq 5977 . . . . . . . . . . 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 1217 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  ->  x  =  y )
55543expia 1189 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B ) )  -> 
( ( x E y )  =  ( z E z )  ->  x  =  y ) )
5655ralrimivvva 2814 . . . . . . 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 22922 . . . . 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 1008 . . . . . . . . . . 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 1008 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B )  /\  y  e.  ( x J x ) )  ->  x  e.  B )
64153adant3 1008 . . . . . . . . . . 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 1008 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B )  /\  y  e.  ( x J x ) )  ->  G  e. TarskiG )
67143adant3 1008 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B )  /\  y  e.  ( x J x ) )  ->  ( F `  x )  e.  P )
68163adant3 1008 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B )  /\  y  e.  ( x J x ) )  ->  ( F `  y )  e.  P )
69 simp3 990 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B )  /\  y  e.  ( x J x ) )  ->  y  e.  ( x J x ) )
70233adantl3 1146 . . . . . . . . . . . . 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 1146 . . . . . . . . . . . . 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 23121 . . . . . . . . . . . 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 22932 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B )  /\  y  e.  ( x J x ) )  ->  ( F `  x )  =  ( F `  y ) )
7562, 65, 74, 53syl21anc 1217 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B )  /\  y  e.  ( x J x ) )  ->  x  =  y )
76753expia 1189 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( y  e.  ( x J x )  ->  x  =  y ) )
7776ralrimivva 2813 . . . . . . 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 5989 . . . . . . . . . . . . . . . . 17  |-  ( ( F : B -1-1-onto-> P  /\  c  e.  P )  ->  ( F `  ( `' F `  c ) )  =  c )
8382eleq1d 2509 . . . . . . . . . . . . . . . 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 1031 . . . . . . . . . . . . . . . 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 5658 . . . . . . . . . . . . . . . . . 18  |-  ( F : B -1-1-onto-> P  ->  `' F : P -1-1-onto-> B )
103 f1of 5646 . . . . . . . . . . . . . . . . . 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 5849 . . . . . . . . . . . . . . 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 23121 . . . . . . . . . . . . . 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 2509 . . . . . . . . . . . . . . . 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 1032 . . . . . . . . . . . . . . . 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 23121 . . . . . . . . . . . . . 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 2509 . . . . . . . . . . . . . 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 2509 . . . . . . . . . . . . . 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 3082 . . . . . . . . . . . 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 5849 . . . . . . . . . . . 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 5849 . . . . . . . . . . . 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 1030 . . . . . . . . . . . . 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 5849 . . . . . . . . . . . 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 5849 . . . . . . . . . . . 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 5849 . . . . . . . . . . . 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 23121 . . . . . . . . . . . . 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 23121 . . . . . . . . . . . . 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 22933 . . . . . . . . . . 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 2867 . . . . . . . . . 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 2814 . . . . . . . 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 2813 . . . . . . 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 1673 . . . . . . . . . . 11  |-  F/ a ( ph  /\  (
s  e.  ~P B  /\  t  e.  ~P B ) )
146 nfre1 2777 . . . . . . . . . . 11  |-  F/ a E. a  e.  B  A. x  e.  s  A. y  e.  t  x  e.  ( a J y )
147145, 146nfan 1861 . . . . . . . . . 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 5564 . . . . . . . . . . . . . . . . . . . 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 3874 . . . . . . . . . . . . . . . . . . . . 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 5960 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F  Fn  B  /\  s  C_  B  /\  x  e.  s )  ->  ( F `  x )  e.  ( F " s
) )
160152, 157, 158, 159syl3anc 1218 . . . . . . . . . . . . . . . . . 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 3874 . . . . . . . . . . . . . . . . . . . . 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 5960 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F  Fn  B  /\  t  C_  B  /\  y  e.  t )  ->  ( F `  y )  e.  ( F " t
) )
167152, 164, 165, 166syl3anc 1218 . . . . . . . . . . . . . . . . . 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 6103 . . . . . . . . . . . . . . . . . . . . 21  |-  ( e  =  ( F `  x )  ->  (
e I f )  =  ( ( F `
 x ) I f ) )
170169eleq2d 2510 . . . . . . . . . . . . . . . . . . . 20  |-  ( e  =  ( F `  x )  ->  (
c  e.  ( e I f )  <->  c  e.  ( ( F `  x ) I f ) ) )
171 oveq2 6104 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f  =  ( F `  y )  ->  (
( F `  x
) I f )  =  ( ( F `
 x ) I ( F `  y
) ) )
172171eleq2d 2510 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  =  ( F `  y )  ->  (
c  e.  ( ( F `  x ) I f )  <->  c  e.  ( ( F `  x ) I ( F `  y ) ) ) )
173170, 172rspc2v 3084 . . . . . . . . . . . . . . . . . . 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 1217 . . . . . . . . . . . . . . . . 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 2517 . . . . . . . . . . . . . . . 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 3362 . . . . . . . . . . . . . . . . . 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 3362 . . . . . . . . . . . . . . . . . 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 5849 . . . . . . . . . . . . . . . . . 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 23121 . . . . . . . . . . . . . . . . 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 2813 . . . . . . . . . . . . . 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 5849 . . . . . . . . . . . . . . 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 2509 . . . . . . . . . . . . . . . . 17  |-  ( b  =  ( `' F `  c )  ->  (
b  e.  ( x J y )  <->  ( `' F `  c )  e.  ( x J y ) ) )
2012002ralbidv 2762 . . . . . . . . . . . . . . . 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 3082 . . . . . . . . . . . . . 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 5185 . . . . . . . . . . . . . 14  |-  ( F
" s )  C_  ran  F
208 f1ofo 5653 . . . . . . . . . . . . . . . . 17  |-  ( F : B -1-1-onto-> P  ->  F : B -onto-> P )
2099, 208syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  F : B -onto-> P
)
210 forn 5628 . . . . . . . . . . . . . . . 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 3409 . . . . . . . . . . . . 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 5185 . . . . . . . . . . . . . 14  |-  ( F
" t )  C_  ran  F
215214, 212syl5sseq 3409 . . . . . . . . . . . . 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 5849 . . . . . . . . . . . . 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 5564 . . . . . . . . . . . . . . . . . . . 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 5960 . . . . . . . . . . . . . . . . . . 19  |-  ( ( `' F  Fn  P  /\  ( F " s
)  C_  P  /\  u  e.  ( F " s ) )  -> 
( `' F `  u )  e.  ( `' F " ( F
" s ) ) )
225221, 222, 223, 224syl3anc 1218 . . . . . . . . . . . . . . . . . 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 5662 . . . . . . . . . . . . . . . . . . 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 2519 . . . . . . . . . . . . . . . . 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 5960 . . . . . . . . . . . . . . . . . . 19  |-  ( ( `' F  Fn  P  /\  ( F " t
)  C_  P  /\  v  e.  ( F " t ) )  -> 
( `' F `  v )  e.  ( `' F " ( F
" t ) ) )
236221, 233, 234, 235syl3anc 1218 . . . . . . . . . . . . . . . . . 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 5662 . . . . . . . . . . . . . . . . . . 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 2519 . . . . . . . . . . . . . . . . 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 2503 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  ( `' F `  u )  ->  (
x  e.  ( a J y )  <->  ( `' F `  u )  e.  ( a J y ) ) )
244 oveq2 6104 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  ( `' F `  v )  ->  (
a J y )  =  ( a J ( `' F `  v ) ) )
245244eleq2d 2510 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  ( `' F `  v )  ->  (
( `' F `  u )  e.  ( a J y )  <-> 
( `' F `  u )  e.  ( a J ( `' F `  v ) ) ) )
246243, 245rspc2v 3084 . . . . . . . . . . . . . . . . . 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 1217 . . . . . . . . . . . . . . . 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 3362 . . . . . . . . . . . . . . . . . 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 5994 . . . . . . . . . . . . . . . . . 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 3362 . . . . . . . . . . . . . . . . . 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 5994 . . . . . . . . . . . . . . . . . 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 23121 . . . . . . . . . . . . . . . 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 5989 . . . . . . . . . . . . . . . . 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 5989 . . . . . . . . . . . . . . . . . 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 6112 . . . . . . . . . . . . . . . 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 2511 . . . . . . . . . . . . . . 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 1182 . . . . . . . . . . . . 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 22935 . . . . . . . . . . . 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 2867 . . . . . . . . . . 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.