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

Theorem f1otrg 24152
Description: A bijection between bases which conserves distances and intervals conserves also geometries. (Contributed by Thierry Arnoux, 23-Mar-2019.)
Hypotheses
Ref Expression
f1otrkg.p  |-  P  =  ( Base `  G
)
f1otrkg.d  |-  D  =  ( dist `  G
)
f1otrkg.i  |-  I  =  (Itv `  G )
f1otrkg.b  |-  B  =  ( Base `  H
)
f1otrkg.e  |-  E  =  ( dist `  H
)
f1otrkg.j  |-  J  =  (Itv `  H )
f1otrkg.f  |-  ( ph  ->  F : B -1-1-onto-> P )
f1otrkg.1  |-  ( (
ph  /\  ( e  e.  B  /\  f  e.  B ) )  -> 
( e E f )  =  ( ( F `  e ) D ( F `  f ) ) )
f1otrkg.2  |-  ( (
ph  /\  ( e  e.  B  /\  f  e.  B  /\  g  e.  B ) )  -> 
( g  e.  ( e J f )  <-> 
( F `  g
)  e.  ( ( F `  e ) I ( F `  f ) ) ) )
f1otrg.h  |-  ( ph  ->  H  e.  V )
f1otrg.g  |-  ( ph  ->  G  e. TarskiG )
f1otrg.l  |-  ( ph  ->  (LineG `  H )  =  ( x  e.  B ,  y  e.  ( B  \  {
x } )  |->  { z  e.  B  | 
( z  e.  ( x J y )  \/  x  e.  ( z J y )  \/  y  e.  ( x J z ) ) } ) )
Assertion
Ref Expression
f1otrg  |-  ( ph  ->  H  e. TarskiG )
Distinct variable groups:    e, f,
g, x, y, z, B    D, e, f, g   
e, E, f, g, x, y, z    e, F, f, g, x, y, z    e, I, f, g, x, y    e, J, f, g, x, y, z    P, e, f, g, x, y, z    ph, e,
f, g, x, y, z    f, H
Allowed substitution hints:    D( x, y, z)    G( x, y, z, e, f, g)    H( x, y, z, e, g)    I( z)    V( x, y, z, e, f, g)

Proof of Theorem f1otrg
Dummy variables  a 
b  c  i  p  s  t  u  v  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1otrg.h . . . . . 6  |-  ( ph  ->  H  e.  V )
2 elex 3104 . . . . . 6  |-  ( H  e.  V  ->  H  e.  _V )
31, 2syl 16 . . . . 5  |-  ( ph  ->  H  e.  _V )
4 f1otrkg.p . . . . . . . . 9  |-  P  =  ( Base `  G
)
5 f1otrkg.d . . . . . . . . 9  |-  D  =  ( dist `  G
)
6 f1otrkg.i . . . . . . . . 9  |-  I  =  (Itv `  G )
7 f1otrg.g . . . . . . . . . 10  |-  ( ph  ->  G  e. TarskiG )
87adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  G  e. TarskiG )
9 f1otrkg.f . . . . . . . . . . . 12  |-  ( ph  ->  F : B -1-1-onto-> P )
10 f1of 5806 . . . . . . . . . . . 12  |-  ( F : B -1-1-onto-> P  ->  F : B
--> P )
119, 10syl 16 . . . . . . . . . . 11  |-  ( ph  ->  F : B --> P )
1211adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  F : B --> P )
13 simprl 756 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  x  e.  B )
1412, 13ffvelrnd 6017 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( F `  x
)  e.  P )
15 simprr 757 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
y  e.  B )
1612, 15ffvelrnd 6017 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( F `  y
)  e.  P )
174, 5, 6, 8, 14, 16axtgcgrrflx 23837 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( ( F `  x ) D ( F `  y ) )  =  ( ( F `  y ) D ( F `  x ) ) )
18 f1otrkg.b . . . . . . . . 9  |-  B  =  ( Base `  H
)
19 f1otrkg.e . . . . . . . . 9  |-  E  =  ( dist `  H
)
20 f1otrkg.j . . . . . . . . 9  |-  J  =  (Itv `  H )
219adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  F : B -1-1-onto-> P )
22 f1otrkg.1 . . . . . . . . . 10  |-  ( (
ph  /\  ( e  e.  B  /\  f  e.  B ) )  -> 
( e E f )  =  ( ( F `  e ) D ( F `  f ) ) )
2322adantlr 714 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( e  e.  B  /\  f  e.  B ) )  -> 
( e E f )  =  ( ( F `  e ) D ( F `  f ) ) )
24 f1otrkg.2 . . . . . . . . . 10  |-  ( (
ph  /\  ( e  e.  B  /\  f  e.  B  /\  g  e.  B ) )  -> 
( g  e.  ( e J f )  <-> 
( F `  g
)  e.  ( ( F `  e ) I ( F `  f ) ) ) )
2524adantlr 714 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( e  e.  B  /\  f  e.  B  /\  g  e.  B ) )  -> 
( g  e.  ( e J f )  <-> 
( F `  g
)  e.  ( ( F `  e ) I ( F `  f ) ) ) )
264, 5, 6, 18, 19, 20, 21, 23, 25, 13, 15f1otrgds 24150 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( x E y )  =  ( ( F `  x ) D ( F `  y ) ) )
274, 5, 6, 18, 19, 20, 21, 23, 25, 15, 13f1otrgds 24150 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( y E x )  =  ( ( F `  y ) D ( F `  x ) ) )
2817, 26, 273eqtr4d 2494 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( x E y )  =  ( y E x ) )
2928ralrimivva 2864 . . . . . 6  |-  ( ph  ->  A. x  e.  B  A. y  e.  B  ( x E y )  =  ( y E x ) )
30 f1of1 5805 . . . . . . . . . . 11  |-  ( F : B -1-1-onto-> P  ->  F : B -1-1-> P )
319, 30syl 16 . . . . . . . . . 10  |-  ( ph  ->  F : B -1-1-> P
)
32313ad2ant1 1018 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  ->  F : B -1-1-> P )
33 simp21 1030 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  ->  x  e.  B )
34 simp22 1031 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  -> 
y  e.  B )
3533, 34jca 532 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  -> 
( x  e.  B  /\  y  e.  B
) )
3673ad2ant1 1018 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  ->  G  e. TarskiG )
37113ad2ant1 1018 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  ->  F : B --> P )
3837, 33ffvelrnd 6017 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  -> 
( F `  x
)  e.  P )
3937, 34ffvelrnd 6017 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  -> 
( F `  y
)  e.  P )
40 simp23 1032 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  -> 
z  e.  B )
4137, 40ffvelrnd 6017 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  -> 
( F `  z
)  e.  P )
42 simp3 999 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  -> 
( x E y )  =  ( z E z ) )
4393ad2ant1 1018 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  ->  F : B -1-1-onto-> P )
44223ad2antl1 1159 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  ( x E y )  =  ( z E z ) )  /\  ( e  e.  B  /\  f  e.  B ) )  -> 
( e E f )  =  ( ( F `  e ) D ( F `  f ) ) )
45243ad2antl1 1159 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  ( x E y )  =  ( z E z ) )  /\  ( e  e.  B  /\  f  e.  B  /\  g  e.  B ) )  -> 
( g  e.  ( e J f )  <-> 
( F `  g
)  e.  ( ( F `  e ) I ( F `  f ) ) ) )
464, 5, 6, 18, 19, 20, 43, 44, 45, 33, 34f1otrgds 24150 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  -> 
( x E y )  =  ( ( F `  x ) D ( F `  y ) ) )
474, 5, 6, 18, 19, 20, 43, 44, 45, 40, 40f1otrgds 24150 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  -> 
( z E z )  =  ( ( F `  z ) D ( F `  z ) ) )
4842, 46, 473eqtr3d 2492 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  -> 
( ( F `  x ) D ( F `  y ) )  =  ( ( F `  z ) D ( F `  z ) ) )
494, 5, 6, 36, 38, 39, 41, 48axtgcgrid 23838 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  -> 
( F `  x
)  =  ( F `
 y ) )
50 f1veqaeq 6153 . . . . . . . . . 10  |-  ( ( F : B -1-1-> P  /\  ( x  e.  B  /\  y  e.  B
) )  ->  (
( F `  x
)  =  ( F `
 y )  ->  x  =  y )
)
5150imp 429 . . . . . . . . 9  |-  ( ( ( F : B -1-1-> P  /\  ( x  e.  B  /\  y  e.  B ) )  /\  ( F `  x )  =  ( F `  y ) )  ->  x  =  y )
5232, 35, 49, 51syl21anc 1228 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B )  /\  (
x E y )  =  ( z E z ) )  ->  x  =  y )
53523expia 1199 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B ) )  -> 
( ( x E y )  =  ( z E z )  ->  x  =  y ) )
5453ralrimivvva 2865 . . . . . 6  |-  ( ph  ->  A. x  e.  B  A. y  e.  B  A. z  e.  B  ( ( x E y )  =  ( z E z )  ->  x  =  y ) )
5529, 54jca 532 . . . . 5  |-  ( ph  ->  ( A. x  e.  B  A. y  e.  B  ( x E y )  =  ( y E x )  /\  A. x  e.  B  A. y  e.  B  A. z  e.  B  ( ( x E y )  =  ( z E z )  ->  x  =  y ) ) )
5618, 19, 20istrkgc 23829 . . . . 5  |-  ( H  e. TarskiGC  <->  ( H  e.  _V  /\  ( A. x  e.  B  A. y  e.  B  ( x E y )  =  ( y E x )  /\  A. x  e.  B  A. y  e.  B  A. z  e.  B  (
( x E y )  =  ( z E z )  ->  x  =  y )
) ) )
573, 55, 56sylanbrc 664 . . . 4  |-  ( ph  ->  H  e. TarskiGC )
5893ad2ant1 1018 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B )  /\  y  e.  ( x J x ) )  ->  F : B -1-1-onto-> P )
5958, 30syl 16 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B )  /\  y  e.  ( x J x ) )  ->  F : B -1-1-> P )
60 simp2 998 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B )  /\  y  e.  ( x J x ) )  ->  (
x  e.  B  /\  y  e.  B )
)
6173ad2ant1 1018 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B )  /\  y  e.  ( x J x ) )  ->  G  e. TarskiG )
62143adant3 1017 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B )  /\  y  e.  ( x J x ) )  ->  ( F `  x )  e.  P )
63163adant3 1017 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B )  /\  y  e.  ( x J x ) )  ->  ( F `  y )  e.  P )
64 simp3 999 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B )  /\  y  e.  ( x J x ) )  ->  y  e.  ( x J x ) )
65223ad2antl1 1159 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )  /\  y  e.  (
x J x ) )  /\  ( e  e.  B  /\  f  e.  B ) )  -> 
( e E f )  =  ( ( F `  e ) D ( F `  f ) ) )
66243ad2antl1 1159 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )  /\  y  e.  (
x J x ) )  /\  ( e  e.  B  /\  f  e.  B  /\  g  e.  B ) )  -> 
( g  e.  ( e J f )  <-> 
( F `  g
)  e.  ( ( F `  e ) I ( F `  f ) ) ) )
67133adant3 1017 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B )  /\  y  e.  ( x J x ) )  ->  x  e.  B )
68153adant3 1017 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B )  /\  y  e.  ( x J x ) )  ->  y  e.  B )
694, 5, 6, 18, 19, 20, 58, 65, 66, 67, 67, 68f1otrgitv 24151 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B )  /\  y  e.  ( x J x ) )  ->  (
y  e.  ( x J x )  <->  ( F `  y )  e.  ( ( F `  x
) I ( F `
 x ) ) ) )
7064, 69mpbid 210 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B )  /\  y  e.  ( x J x ) )  ->  ( F `  y )  e.  ( ( F `  x ) I ( F `  x ) ) )
714, 5, 6, 61, 62, 63, 70axtgbtwnid 23841 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B )  /\  y  e.  ( x J x ) )  ->  ( F `  x )  =  ( F `  y ) )
7259, 60, 71, 51syl21anc 1228 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B )  /\  y  e.  ( x J x ) )  ->  x  =  y )
73723expia 1199 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( y  e.  ( x J x )  ->  x  =  y ) )
7473ralrimivva 2864 . . . . . 6  |-  ( ph  ->  A. x  e.  B  A. y  e.  B  ( y  e.  ( x J x )  ->  x  =  y ) )
75 f1ocnv 5818 . . . . . . . . . . . . . 14  |-  ( F : B -1-1-onto-> P  ->  `' F : P -1-1-onto-> B )
76 f1of 5806 . . . . . . . . . . . . . 14  |-  ( `' F : P -1-1-onto-> B  ->  `' F : P --> B )
779, 75, 763syl 20 . . . . . . . . . . . . 13  |-  ( ph  ->  `' F : P --> B )
7877ad5antr 733 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B
) )  /\  (
u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  /\  c  e.  P )  /\  (
c  e.  ( ( F `  u ) I ( F `  y ) )  /\  c  e.  ( ( F `  v )
I ( F `  x ) ) ) )  ->  `' F : P --> B )
79 simplr 755 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B
) )  /\  (
u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  /\  c  e.  P )  /\  (
c  e.  ( ( F `  u ) I ( F `  y ) )  /\  c  e.  ( ( F `  v )
I ( F `  x ) ) ) )  ->  c  e.  P )
8078, 79ffvelrnd 6017 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B
) )  /\  (
u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  /\  c  e.  P )  /\  (
c  e.  ( ( F `  u ) I ( F `  y ) )  /\  c  e.  ( ( F `  v )
I ( F `  x ) ) ) )  ->  ( `' F `  c )  e.  B )
81 simpr 461 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J z )  /\  v  e.  ( y J z ) ) )  /\  c  e.  P )  /\  (
c  e.  ( ( F `  u ) I ( F `  y ) )  /\  c  e.  ( ( F `  v )
I ( F `  x ) ) ) )  /\  a  =  ( `' F `  c ) )  -> 
a  =  ( `' F `  c ) )
8281eleq1d 2512 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J z )  /\  v  e.  ( y J z ) ) )  /\  c  e.  P )  /\  (
c  e.  ( ( F `  u ) I ( F `  y ) )  /\  c  e.  ( ( F `  v )
I ( F `  x ) ) ) )  /\  a  =  ( `' F `  c ) )  -> 
( a  e.  ( u J y )  <-> 
( `' F `  c )  e.  ( u J y ) ) )
8381eleq1d 2512 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J z )  /\  v  e.  ( y J z ) ) )  /\  c  e.  P )  /\  (
c  e.  ( ( F `  u ) I ( F `  y ) )  /\  c  e.  ( ( F `  v )
I ( F `  x ) ) ) )  /\  a  =  ( `' F `  c ) )  -> 
( a  e.  ( v J x )  <-> 
( `' F `  c )  e.  ( v J x ) ) )
8482, 83anbi12d 710 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J z )  /\  v  e.  ( y J z ) ) )  /\  c  e.  P )  /\  (
c  e.  ( ( F `  u ) I ( F `  y ) )  /\  c  e.  ( ( F `  v )
I ( F `  x ) ) ) )  /\  a  =  ( `' F `  c ) )  -> 
( ( a  e.  ( u J y )  /\  a  e.  ( v J x ) )  <->  ( ( `' F `  c )  e.  ( u J y )  /\  ( `' F `  c )  e.  ( v J x ) ) ) )
85 simprl 756 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B
) )  /\  (
u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  /\  c  e.  P )  /\  (
c  e.  ( ( F `  u ) I ( F `  y ) )  /\  c  e.  ( ( F `  v )
I ( F `  x ) ) ) )  ->  c  e.  ( ( F `  u ) I ( F `  y ) ) )
8621ad2antrr 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 ) ) )  ->  F : B -1-1-onto-> P )
8786ad2antrr 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 ) ) ) )  ->  F : B
-1-1-onto-> P )
88 f1ocnvfv2 6168 . . . . . . . . . . . . . . . 16  |-  ( ( F : B -1-1-onto-> P  /\  c  e.  P )  ->  ( F `  ( `' F `  c ) )  =  c )
8988eleq1d 2512 . . . . . . . . . . . . . . 15  |-  ( ( F : B -1-1-onto-> P  /\  c  e.  P )  ->  ( ( F `  ( `' F `  c ) )  e.  ( ( F `  u ) I ( F `  y ) )  <->  c  e.  ( ( F `  u ) I ( F `  y ) ) ) )
9087, 79, 89syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B
) )  /\  (
u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  /\  c  e.  P )  /\  (
c  e.  ( ( F `  u ) I ( F `  y ) )  /\  c  e.  ( ( F `  v )
I ( F `  x ) ) ) )  ->  ( ( F `  ( `' F `  c )
)  e.  ( ( F `  u ) I ( F `  y ) )  <->  c  e.  ( ( F `  u ) I ( F `  y ) ) ) )
9185, 90mpbird 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 `  ( `' F `  c ) )  e.  ( ( F `  u ) I ( F `  y ) ) )
92 simplll 759 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J z )  /\  v  e.  ( y J z ) ) )  /\  c  e.  P )  /\  (
c  e.  ( ( F `  u ) I ( F `  y ) )  /\  c  e.  ( ( F `  v )
I ( F `  x ) ) ) )  /\  ( e  e.  B  /\  f  e.  B ) )  -> 
( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J z )  /\  v  e.  ( y J z ) ) ) )
93 simplll 759 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  /\  ( e  e.  B  /\  f  e.  B
) )  ->  ( ph  /\  ( x  e.  B  /\  y  e.  B ) ) )
9493, 23sylancom 667 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  /\  ( e  e.  B  /\  f  e.  B
) )  ->  (
e E f )  =  ( ( F `
 e ) D ( F `  f
) ) )
9592, 94sylancom 667 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J z )  /\  v  e.  ( y J z ) ) )  /\  c  e.  P )  /\  (
c  e.  ( ( F `  u ) I ( F `  y ) )  /\  c  e.  ( ( F `  v )
I ( F `  x ) ) ) )  /\  ( e  e.  B  /\  f  e.  B ) )  -> 
( e E f )  =  ( ( F `  e ) D ( F `  f ) ) )
96 simplll 759 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J z )  /\  v  e.  ( y J z ) ) )  /\  c  e.  P )  /\  (
c  e.  ( ( F `  u ) I ( F `  y ) )  /\  c  e.  ( ( F `  v )
I ( F `  x ) ) ) )  /\  ( e  e.  B  /\  f  e.  B  /\  g  e.  B ) )  -> 
( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J z )  /\  v  e.  ( y J z ) ) ) )
97 simplll 759 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  /\  ( e  e.  B  /\  f  e.  B  /\  g  e.  B
) )  ->  ( ph  /\  ( x  e.  B  /\  y  e.  B ) ) )
9897, 25sylancom 667 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  /\  ( e  e.  B  /\  f  e.  B  /\  g  e.  B
) )  ->  (
g  e.  ( e J f )  <->  ( F `  g )  e.  ( ( F `  e
) I ( F `
 f ) ) ) )
9996, 98sylancom 667 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J z )  /\  v  e.  ( y J z ) ) )  /\  c  e.  P )  /\  (
c  e.  ( ( F `  u ) I ( F `  y ) )  /\  c  e.  ( ( F `  v )
I ( F `  x ) ) ) )  /\  ( e  e.  B  /\  f  e.  B  /\  g  e.  B ) )  -> 
( g  e.  ( e J f )  <-> 
( F `  g
)  e.  ( ( F `  e ) I ( F `  f ) ) ) )
100 simplr2 1040 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  ->  u  e.  B )
101100ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B
) )  /\  (
u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  /\  c  e.  P )  /\  (
c  e.  ( ( F `  u ) I ( F `  y ) )  /\  c  e.  ( ( F `  v )
I ( F `  x ) ) ) )  ->  u  e.  B )
10215ad2antrr 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 ) ) )  -> 
y  e.  B )
103102ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B
) )  /\  (
u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  /\  c  e.  P )  /\  (
c  e.  ( ( F `  u ) I ( F `  y ) )  /\  c  e.  ( ( F `  v )
I ( F `  x ) ) ) )  ->  y  e.  B )
1044, 5, 6, 18, 19, 20, 87, 95, 99, 101, 103, 80f1otrgitv 24151 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B
) )  /\  (
u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  /\  c  e.  P )  /\  (
c  e.  ( ( F `  u ) I ( F `  y ) )  /\  c  e.  ( ( F `  v )
I ( F `  x ) ) ) )  ->  ( ( `' F `  c )  e.  ( u J y )  <->  ( F `  ( `' F `  c ) )  e.  ( ( F `  u ) I ( F `  y ) ) ) )
10591, 104mpbird 232 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B
) )  /\  (
u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  /\  c  e.  P )  /\  (
c  e.  ( ( F `  u ) I ( F `  y ) )  /\  c  e.  ( ( F `  v )
I ( F `  x ) ) ) )  ->  ( `' F `  c )  e.  ( u J y ) )
106 simprr 757 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B
) )  /\  (
u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  /\  c  e.  P )  /\  (
c  e.  ( ( F `  u ) I ( F `  y ) )  /\  c  e.  ( ( F `  v )
I ( F `  x ) ) ) )  ->  c  e.  ( ( F `  v ) I ( F `  x ) ) )
10788eleq1d 2512 . . . . . . . . . . . . . . 15  |-  ( ( F : B -1-1-onto-> P  /\  c  e.  P )  ->  ( ( F `  ( `' F `  c ) )  e.  ( ( F `  v ) I ( F `  x ) )  <->  c  e.  ( ( F `  v ) I ( F `  x ) ) ) )
10887, 79, 107syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B
) )  /\  (
u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  /\  c  e.  P )  /\  (
c  e.  ( ( F `  u ) I ( F `  y ) )  /\  c  e.  ( ( F `  v )
I ( F `  x ) ) ) )  ->  ( ( F `  ( `' F `  c )
)  e.  ( ( F `  v ) I ( F `  x ) )  <->  c  e.  ( ( F `  v ) I ( F `  x ) ) ) )
109106, 108mpbird 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 `  ( `' F `  c ) )  e.  ( ( F `  v ) I ( F `  x ) ) )
110 simplr3 1041 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  -> 
v  e.  B )
111110ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B
) )  /\  (
u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  /\  c  e.  P )  /\  (
c  e.  ( ( F `  u ) I ( F `  y ) )  /\  c  e.  ( ( F `  v )
I ( F `  x ) ) ) )  ->  v  e.  B )
11213ad2antrr 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 ) ) )  ->  x  e.  B )
113112ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B
) )  /\  (
u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  /\  c  e.  P )  /\  (
c  e.  ( ( F `  u ) I ( F `  y ) )  /\  c  e.  ( ( F `  v )
I ( F `  x ) ) ) )  ->  x  e.  B )
1144, 5, 6, 18, 19, 20, 87, 95, 99, 111, 113, 80f1otrgitv 24151 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B
) )  /\  (
u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  /\  c  e.  P )  /\  (
c  e.  ( ( F `  u ) I ( F `  y ) )  /\  c  e.  ( ( F `  v )
I ( F `  x ) ) ) )  ->  ( ( `' F `  c )  e.  ( v J x )  <->  ( F `  ( `' F `  c ) )  e.  ( ( F `  v ) I ( F `  x ) ) ) )
115109, 114mpbird 232 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B
) )  /\  (
u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  /\  c  e.  P )  /\  (
c  e.  ( ( F `  u ) I ( F `  y ) )  /\  c  e.  ( ( F `  v )
I ( F `  x ) ) ) )  ->  ( `' F `  c )  e.  ( v J x ) )
116105, 115jca 532 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B
) )  /\  (
u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  /\  c  e.  P )  /\  (
c  e.  ( ( F `  u ) I ( F `  y ) )  /\  c  e.  ( ( F `  v )
I ( F `  x ) ) ) )  ->  ( ( `' F `  c )  e.  ( u J y )  /\  ( `' F `  c )  e.  ( v J x ) ) )
11780, 84, 116rspcedvd 3201 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B
) )  /\  (
u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  /\  c  e.  P )  /\  (
c  e.  ( ( F `  u ) I ( F `  y ) )  /\  c  e.  ( ( F `  v )
I ( F `  x ) ) ) )  ->  E. a  e.  B  ( a  e.  ( u J y )  /\  a  e.  ( v J x ) ) )
1188ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  ->  G  e. TarskiG )
11912ad2antrr 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 ) ) )  ->  F : B --> P )
120119, 112ffvelrnd 6017 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  -> 
( F `  x
)  e.  P )
121119, 102ffvelrnd 6017 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  -> 
( F `  y
)  e.  P )
122 simplr1 1039 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  -> 
z  e.  B )
123119, 122ffvelrnd 6017 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  -> 
( F `  z
)  e.  P )
124119, 100ffvelrnd 6017 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  -> 
( F `  u
)  e.  P )
125119, 110ffvelrnd 6017 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  -> 
( F `  v
)  e.  P )
126 simprl 756 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  ->  u  e.  ( x J z ) )
1274, 5, 6, 18, 19, 20, 86, 94, 98, 112, 122, 100f1otrgitv 24151 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  -> 
( u  e.  ( x J z )  <-> 
( F `  u
)  e.  ( ( F `  x ) I ( F `  z ) ) ) )
128126, 127mpbid 210 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  -> 
( F `  u
)  e.  ( ( F `  x ) I ( F `  z ) ) )
129 simprr 757 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  -> 
v  e.  ( y J z ) )
1304, 5, 6, 18, 19, 20, 86, 94, 98, 102, 122, 110f1otrgitv 24151 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  -> 
( v  e.  ( y J z )  <-> 
( F `  v
)  e.  ( ( F `  y ) I ( F `  z ) ) ) )
131129, 130mpbid 210 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  -> 
( F `  v
)  e.  ( ( F `  y ) I ( F `  z ) ) )
1324, 5, 6, 118, 120, 121, 123, 124, 125, 128, 131axtgpasch 23842 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  ->  E. c  e.  P  ( c  e.  ( ( F `  u
) I ( F `
 y ) )  /\  c  e.  ( ( F `  v
) I ( F `
 x ) ) ) )
133117, 132r19.29a 2985 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J z )  /\  v  e.  ( y J z ) ) )  ->  E. a  e.  B  ( a  e.  ( u J y )  /\  a  e.  ( v J x ) ) )
134133ex 434 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  -> 
( ( u  e.  ( x J z )  /\  v  e.  ( y J z ) )  ->  E. a  e.  B  ( a  e.  ( u J y )  /\  a  e.  ( v J x ) ) ) )
135134ralrimivvva 2865 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  A. z  e.  B  A. u  e.  B  A. v  e.  B  ( ( u  e.  ( x J z )  /\  v  e.  ( y J z ) )  ->  E. a  e.  B  ( a  e.  ( u J y )  /\  a  e.  ( v J x ) ) ) )
136135ralrimivva 2864 . . . . . 6  |-  ( ph  ->  A. x  e.  B  A. y  e.  B  A. z  e.  B  A. u  e.  B  A. v  e.  B  ( ( u  e.  ( x J z )  /\  v  e.  ( y J z ) )  ->  E. a  e.  B  ( a  e.  ( u J y )  /\  a  e.  ( v J x ) ) ) )
1379ad5antr 733 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  c  e.  P )  /\  A. e  e.  ( F " s ) A. f  e.  ( F " t
) c  e.  ( e I f ) )  /\  ( x  e.  s  /\  y  e.  t ) )  ->  F : B -1-1-onto-> P )
138 simpllr 760 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  c  e.  P )  /\  A. e  e.  ( F " s ) A. f  e.  ( F " t
) c  e.  ( e I f ) )  /\  ( x  e.  s  /\  y  e.  t ) )  -> 
c  e.  P )
139137, 138, 88syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  c  e.  P )  /\  A. e  e.  ( F " s ) A. f  e.  ( F " t
) c  e.  ( e I f ) )  /\  ( x  e.  s  /\  y  e.  t ) )  -> 
( F `  ( `' F `  c ) )  =  c )
140 ffn 5721 . . . . . . . . . . . . . . . . . 18  |-  ( F : B --> P  ->  F  Fn  B )
141137, 10, 1403syl 20 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  c  e.  P )  /\  A. e  e.  ( F " s ) A. f  e.  ( F " t
) c  e.  ( e I f ) )  /\  ( x  e.  s  /\  y  e.  t ) )  ->  F  Fn  B )
142 simp-4r 768 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  c  e.  P
)  /\  ( x  e.  s  /\  y  e.  t ) )  -> 
( s  e.  ~P B  /\  t  e.  ~P B ) )
143142simpld 459 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  c  e.  P
)  /\  ( x  e.  s  /\  y  e.  t ) )  -> 
s  e.  ~P B
)
144143elpwid 4007 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  c  e.  P
)  /\  ( x  e.  s  /\  y  e.  t ) )  -> 
s  C_  B )
145144adantlr 714 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  c  e.  P )  /\  A. e  e.  ( F " s ) A. f  e.  ( F " t
) c  e.  ( e I f ) )  /\  ( x  e.  s  /\  y  e.  t ) )  -> 
s  C_  B )
146 simprl 756 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  c  e.  P )  /\  A. e  e.  ( F " s ) A. f  e.  ( F " t
) c  e.  ( e I f ) )  /\  ( x  e.  s  /\  y  e.  t ) )  ->  x  e.  s )
147 fnfvima 6135 . . . . . . . . . . . . . . . . 17  |-  ( ( F  Fn  B  /\  s  C_  B  /\  x  e.  s )  ->  ( F `  x )  e.  ( F " s
) )
148141, 145, 146, 147syl3anc 1229 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  c  e.  P )  /\  A. e  e.  ( F " s ) A. f  e.  ( F " t
) c  e.  ( e I f ) )  /\  ( x  e.  s  /\  y  e.  t ) )  -> 
( F `  x
)  e.  ( F
" s ) )
149142simprd 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  c  e.  P
)  /\  ( x  e.  s  /\  y  e.  t ) )  -> 
t  e.  ~P B
)
150149elpwid 4007 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  c  e.  P
)  /\  ( x  e.  s  /\  y  e.  t ) )  -> 
t  C_  B )
151150adantlr 714 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  c  e.  P )  /\  A. e  e.  ( F " s ) A. f  e.  ( F " t
) c  e.  ( e I f ) )  /\  ( x  e.  s  /\  y  e.  t ) )  -> 
t  C_  B )
152 simprr 757 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  c  e.  P )  /\  A. e  e.  ( F " s ) A. f  e.  ( F " t
) c  e.  ( e I f ) )  /\  ( x  e.  s  /\  y  e.  t ) )  -> 
y  e.  t )
153 fnfvima 6135 . . . . . . . . . . . . . . . . 17  |-  ( ( F  Fn  B  /\  t  C_  B  /\  y  e.  t )  ->  ( F `  y )  e.  ( F " t
) )
154141, 151, 152, 153syl3anc 1229 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  c  e.  P )  /\  A. e  e.  ( F " s ) A. f  e.  ( F " t
) c  e.  ( e I f ) )  /\  ( x  e.  s  /\  y  e.  t ) )  -> 
( F `  y
)  e.  ( F
" t ) )
155 simplr 755 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  c  e.  P )  /\  A. e  e.  ( F " s ) A. f  e.  ( F " t
) c  e.  ( e I f ) )  /\  ( x  e.  s  /\  y  e.  t ) )  ->  A. e  e.  ( F " s ) A. f  e.  ( F " t ) c  e.  ( e I f ) )
156 oveq1 6288 . . . . . . . . . . . . . . . . . 18  |-  ( e  =  ( F `  x )  ->  (
e I f )  =  ( ( F `
 x ) I f ) )
157156eleq2d 2513 . . . . . . . . . . . . . . . . 17  |-  ( e  =  ( F `  x )  ->  (
c  e.  ( e I f )  <->  c  e.  ( ( F `  x ) I f ) ) )
158 oveq2 6289 . . . . . . . . . . . . . . . . . 18  |-  ( f  =  ( F `  y )  ->  (
( F `  x
) I f )  =  ( ( F `
 x ) I ( F `  y
) ) )
159158eleq2d 2513 . . . . . . . . . . . . . . . . 17  |-  ( f  =  ( F `  y )  ->  (
c  e.  ( ( F `  x ) I f )  <->  c  e.  ( ( F `  x ) I ( F `  y ) ) ) )
160157, 159rspc2va 3206 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( F `  x )  e.  ( F " s )  /\  ( F `  y )  e.  ( F " t ) )  /\  A. e  e.  ( F " s
) A. f  e.  ( F " t
) c  e.  ( e I f ) )  ->  c  e.  ( ( F `  x ) I ( F `  y ) ) )
161148, 154, 155, 160syl21anc 1228 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  c  e.  P )  /\  A. e  e.  ( F " s ) A. f  e.  ( F " t
) c  e.  ( e I f ) )  /\  ( x  e.  s  /\  y  e.  t ) )  -> 
c  e.  ( ( F `  x ) I ( F `  y ) ) )
162139, 161eqeltrd 2531 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  c  e.  P )  /\  A. e  e.  ( F " s ) A. f  e.  ( F " t
) c  e.  ( e I f ) )  /\  ( x  e.  s  /\  y  e.  t ) )  -> 
( F `  ( `' F `  c ) )  e.  ( ( F `  x ) I ( F `  y ) ) )
1639ad4antr 731 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  c  e.  P
)  /\  ( x  e.  s  /\  y  e.  t ) )  ->  F : B -1-1-onto-> P )
164 simp-5l 769 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  c  e.  P )  /\  (
x  e.  s  /\  y  e.  t )
)  /\  ( e  e.  B  /\  f  e.  B ) )  ->  ph )
165164, 22sylancom 667 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  c  e.  P )  /\  (
x  e.  s  /\  y  e.  t )
)  /\  ( e  e.  B  /\  f  e.  B ) )  -> 
( e E f )  =  ( ( F `  e ) D ( F `  f ) ) )
166 simp-5l 769 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  c  e.  P )  /\  (
x  e.  s  /\  y  e.  t )
)  /\  ( e  e.  B  /\  f  e.  B  /\  g  e.  B ) )  ->  ph )
167166, 24sylancom 667 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  c  e.  P )  /\  (
x  e.  s  /\  y  e.  t )
)  /\  ( e  e.  B  /\  f  e.  B  /\  g  e.  B ) )  -> 
( g  e.  ( e J f )  <-> 
( F `  g
)  e.  ( ( F `  e ) I ( F `  f ) ) ) )
168 simprl 756 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  c  e.  P
)  /\  ( x  e.  s  /\  y  e.  t ) )  ->  x  e.  s )
169144, 168sseldd 3490 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  c  e.  P
)  /\  ( x  e.  s  /\  y  e.  t ) )  ->  x  e.  B )
170 simprr 757 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  c  e.  P
)  /\  ( x  e.  s  /\  y  e.  t ) )  -> 
y  e.  t )
171150, 170sseldd 3490 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  c  e.  P
)  /\  ( x  e.  s  /\  y  e.  t ) )  -> 
y  e.  B )
17277ad4antr 731 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  c  e.  P
)  /\  ( x  e.  s  /\  y  e.  t ) )  ->  `' F : P --> B )
173 simplr 755 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  c  e.  P
)  /\  ( x  e.  s  /\  y  e.  t ) )  -> 
c  e.  P )
174172, 173ffvelrnd 6017 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  c  e.  P
)  /\  ( x  e.  s  /\  y  e.  t ) )  -> 
( `' F `  c )  e.  B
)
1754, 5, 6, 18, 19, 20, 163, 165, 167, 169, 171, 174f1otrgitv 24151 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  c  e.  P
)  /\  ( x  e.  s  /\  y  e.  t ) )  -> 
( ( `' F `  c )  e.  ( x J y )  <-> 
( F `  ( `' F `  c ) )  e.  ( ( F `  x ) I ( F `  y ) ) ) )
176175adantlr 714 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  c  e.  P )  /\  A. e  e.  ( F " s ) A. f  e.  ( F " t
) c  e.  ( e I f ) )  /\  ( x  e.  s  /\  y  e.  t ) )  -> 
( ( `' F `  c )  e.  ( x J y )  <-> 
( F `  ( `' F `  c ) )  e.  ( ( F `  x ) I ( F `  y ) ) ) )
177162, 176mpbird 232 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  c  e.  P )  /\  A. e  e.  ( F " s ) A. f  e.  ( F " t
) c  e.  ( e I f ) )  /\  ( x  e.  s  /\  y  e.  t ) )  -> 
( `' F `  c )  e.  ( x J y ) )
178177ralrimivva 2864 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  c  e.  P
)  /\  A. e  e.  ( F " s
) A. f  e.  ( F " t
) c  e.  ( e I f ) )  ->  A. x  e.  s  A. y  e.  t  ( `' F `  c )  e.  ( x J y ) )
179178adantllr 718 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  c  e.  P )  /\  A. e  e.  ( F " s ) A. f  e.  ( F " t
) c  e.  ( e I f ) )  ->  A. x  e.  s  A. y  e.  t  ( `' F `  c )  e.  ( x J y ) )
18077ad4antr 731 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  A. x  e.  s 
A. y  e.  t  x  e.  ( a J y ) )  /\  c  e.  P
)  ->  `' F : P --> B )
181 simpr 461 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  A. x  e.  s 
A. y  e.  t  x  e.  ( a J y ) )  /\  c  e.  P
)  ->  c  e.  P )
182180, 181ffvelrnd 6017 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  A. x  e.  s 
A. y  e.  t  x  e.  ( a J y ) )  /\  c  e.  P
)  ->  ( `' F `  c )  e.  B )
183 eleq1 2515 . . . . . . . . . . . . . . 15  |-  ( b  =  ( `' F `  c )  ->  (
b  e.  ( x J y )  <->  ( `' F `  c )  e.  ( x J y ) ) )
1841832ralbidv 2887 . . . . . . . . . . . . . 14  |-  ( b  =  ( `' F `  c )  ->  ( A. x  e.  s  A. y  e.  t 
b  e.  ( x J y )  <->  A. x  e.  s  A. y  e.  t  ( `' F `  c )  e.  ( x J y ) ) )
185184adantl 466 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  c  e.  P )  /\  b  =  ( `' F `  c ) )  -> 
( A. x  e.  s  A. y  e.  t  b  e.  ( x J y )  <->  A. x  e.  s  A. y  e.  t 
( `' F `  c )  e.  ( x J y ) ) )
186182, 185rspcedv 3200 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  A. x  e.  s 
A. y  e.  t  x  e.  ( a J y ) )  /\  c  e.  P
)  ->  ( A. x  e.  s  A. y  e.  t  ( `' F `  c )  e.  ( x J y )  ->  E. b  e.  B  A. x  e.  s  A. y  e.  t  b  e.  ( x J y ) ) )
187186adantr 465 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  c  e.  P )  /\  A. e  e.  ( F " s ) A. f  e.  ( F " t
) c  e.  ( e I f ) )  ->  ( A. x  e.  s  A. y  e.  t  ( `' F `  c )  e.  ( x J y )  ->  E. b  e.  B  A. x  e.  s  A. y  e.  t  b  e.  ( x J y ) ) )
188179, 187mpd 15 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  c  e.  P )  /\  A. e  e.  ( F " s ) A. f  e.  ( F " t
) c  e.  ( e I f ) )  ->  E. b  e.  B  A. x  e.  s  A. y  e.  t  b  e.  ( x J y ) )
1897ad3antrrr 729 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  A. x  e.  s 
A. y  e.  t  x  e.  ( a J y ) )  ->  G  e. TarskiG )
190 imassrn 5338 . . . . . . . . . . . 12  |-  ( F
" s )  C_  ran  F
191 f1ofo 5813 . . . . . . . . . . . . . 14  |-  ( F : B -1-1-onto-> P  ->  F : B -onto-> P )
192 forn 5788 . . . . . . . . . . . . . 14  |-  ( F : B -onto-> P  ->  ran  F  =  P )
1939, 191, 1923syl 20 . . . . . . . . . . . . 13  |-  ( ph  ->  ran  F  =  P )
194193ad3antrrr 729 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  A. x  e.  s 
A. y  e.  t  x  e.  ( a J y ) )  ->  ran  F  =  P )
195190, 194syl5sseq 3537 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  A. x  e.  s 
A. y  e.  t  x  e.  ( a J y ) )  ->  ( F "
s )  C_  P
)
196 imassrn 5338 . . . . . . . . . . . 12  |-  ( F
" t )  C_  ran  F
197196, 194syl5sseq 3537 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  A. x  e.  s 
A. y  e.  t  x  e.  ( a J y ) )  ->  ( F "
t )  C_  P
)
19811ad3antrrr 729 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  A. x  e.  s 
A. y  e.  t  x  e.  ( a J y ) )  ->  F : B --> P )
199 simplr 755 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  A. x  e.  s 
A. y  e.  t  x  e.  ( a J y ) )  ->  a  e.  B
)
200198, 199ffvelrnd 6017 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  A. x  e.  s 
A. y  e.  t  x  e.  ( a J y ) )  ->  ( F `  a )  e.  P
)
2019ad5antr 733 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s
) )  /\  v  e.  ( F " t
) )  ->  F : B -1-1-onto-> P )
202 ffn 5721 . . . . . . . . . . . . . . . . . 18  |-  ( `' F : P --> B  ->  `' F  Fn  P
)
203201, 75, 76, 2024syl 21 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s
) )  /\  v  e.  ( F " t
) )  ->  `' F  Fn  P )
204195ad2antrr 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
) )  ->  ( F " s )  C_  P )
205 simplr 755 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s
) )  /\  v  e.  ( F " t
) )  ->  u  e.  ( F " s
) )
206 fnfvima 6135 . . . . . . . . . . . . . . . . 17  |-  ( ( `' F  Fn  P  /\  ( F " s
)  C_  P  /\  u  e.  ( F " s ) )  -> 
( `' F `  u )  e.  ( `' F " ( F
" s ) ) )
207203, 204, 205, 206syl3anc 1229 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s
) )  /\  v  e.  ( F " t
) )  ->  ( `' F `  u )  e.  ( `' F " ( F " s
) ) )
208201, 30syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s
) )  /\  v  e.  ( F " t
) )  ->  F : B -1-1-> P )
209 simp-5r 770 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s
) )  /\  v  e.  ( F " t
) )  ->  (
s  e.  ~P B  /\  t  e.  ~P B ) )
210209simpld 459 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s
) )  /\  v  e.  ( F " t
) )  ->  s  e.  ~P B )
211210elpwid 4007 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s
) )  /\  v  e.  ( F " t
) )  ->  s  C_  B )
212 f1imacnv 5822 . . . . . . . . . . . . . . . . 17  |-  ( ( F : B -1-1-> P  /\  s  C_  B )  ->  ( `' F " ( F " s
) )  =  s )
213208, 211, 212syl2anc 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
" s ) )  =  s )
214207, 213eleqtrd 2533 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s
) )  /\  v  e.  ( F " t
) )  ->  ( `' F `  u )  e.  s )
215197ad2antrr 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
) )  ->  ( F " t )  C_  P )
216 simpr 461 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s
) )  /\  v  e.  ( F " t
) )  ->  v  e.  ( F " t
) )
217 fnfvima 6135 . . . . . . . . . . . . . . . . 17  |-  ( ( `' F  Fn  P  /\  ( F " t
)  C_  P  /\  v  e.  ( F " t ) )  -> 
( `' F `  v )  e.  ( `' F " ( F
" t ) ) )
218203, 215, 216, 217syl3anc 1229 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s
) )  /\  v  e.  ( F " t
) )  ->  ( `' F `  v )  e.  ( `' F " ( F " t
) ) )
219209simprd 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s
) )  /\  v  e.  ( F " t
) )  ->  t  e.  ~P B )
220219elpwid 4007 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s
) )  /\  v  e.  ( F " t
) )  ->  t  C_  B )
221 f1imacnv 5822 . . . . . . . . . . . . . . . . 17  |-  ( ( F : B -1-1-> P  /\  t  C_  B )  ->  ( `' F " ( F " t
) )  =  t )
222208, 220, 221syl2anc 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
" t ) )  =  t )
223218, 222eleqtrd 2533 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s
) )  /\  v  e.  ( F " t
) )  ->  ( `' F `  v )  e.  t )
224 simpllr 760 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s
) )  /\  v  e.  ( F " t
) )  ->  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )
225 eleq1 2515 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( `' F `  u )  ->  (
x  e.  ( a J y )  <->  ( `' F `  u )  e.  ( a J y ) ) )
226 oveq2 6289 . . . . . . . . . . . . . . . . 17  |-  ( y  =  ( `' F `  v )  ->  (
a J y )  =  ( a J ( `' F `  v ) ) )
227226eleq2d 2513 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( `' F `  v )  ->  (
( `' F `  u )  e.  ( a J y )  <-> 
( `' F `  u )  e.  ( a J ( `' F `  v ) ) ) )
228225, 227rspc2va 3206 . . . . . . . . . . . . . . 15  |-  ( ( ( ( `' F `  u )  e.  s  /\  ( `' F `  v )  e.  t )  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  ->  ( `' F `  u )  e.  ( a J ( `' F `  v ) ) )
229214, 223, 224, 228syl21anc 1228 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s
) )  /\  v  e.  ( F " t
) )  ->  ( `' F `  u )  e.  ( a J ( `' F `  v ) ) )
230 simp-6l 771 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  (
s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  A. x  e.  s 
A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s ) )  /\  v  e.  ( F " t
) )  /\  (
e  e.  B  /\  f  e.  B )
)  ->  ph )
231230, 22sylancom 667 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  (
s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  A. x  e.  s 
A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s ) )  /\  v  e.  ( F " t
) )  /\  (
e  e.  B  /\  f  e.  B )
)  ->  ( e E f )  =  ( ( F `  e ) D ( F `  f ) ) )
232 simp-6l 771 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  (
s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  A. x  e.  s 
A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s ) )  /\  v  e.  ( F " t
) )  /\  (
e  e.  B  /\  f  e.  B  /\  g  e.  B )
)  ->  ph )
233232, 24sylancom 667 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  (
s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  A. x  e.  s 
A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s ) )  /\  v  e.  ( F " t
) )  /\  (
e  e.  B  /\  f  e.  B  /\  g  e.  B )
)  ->  ( g  e.  ( e J f )  <->  ( F `  g )  e.  ( ( F `  e
) I ( F `
 f ) ) ) )
234 simp-4r 768 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s
) )  /\  v  e.  ( F " t
) )  ->  a  e.  B )
235215, 216sseldd 3490 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s
) )  /\  v  e.  ( F " t
) )  ->  v  e.  P )
236 f1ocnvdm 6173 . . . . . . . . . . . . . . . 16  |-  ( ( F : B -1-1-onto-> P  /\  v  e.  P )  ->  ( `' F `  v )  e.  B
)
237201, 235, 236syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s
) )  /\  v  e.  ( F " t
) )  ->  ( `' F `  v )  e.  B )
238204, 205sseldd 3490 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s
) )  /\  v  e.  ( F " t
) )  ->  u  e.  P )
239 f1ocnvdm 6173 . . . . . . . . . . . . . . . 16  |-  ( ( F : B -1-1-onto-> P  /\  u  e.  P )  ->  ( `' F `  u )  e.  B
)
240201, 238, 239syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s
) )  /\  v  e.  ( F " t
) )  ->  ( `' F `  u )  e.  B )
2414, 5, 6, 18, 19, 20, 201, 231, 233, 234, 237, 240f1otrgitv 24151 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s
) )  /\  v  e.  ( F " t
) )  ->  (
( `' F `  u )  e.  ( a J ( `' F `  v ) )  <->  ( F `  ( `' F `  u ) )  e.  ( ( F `  a ) I ( F `  ( `' F `  v ) ) ) ) )
242229, 241mpbid 210 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s
) )  /\  v  e.  ( F " t
) )  ->  ( F `  ( `' F `  u )
)  e.  ( ( F `  a ) I ( F `  ( `' F `  v ) ) ) )
243 f1ocnvfv2 6168 . . . . . . . . . . . . . 14  |-  ( ( F : B -1-1-onto-> P  /\  u  e.  P )  ->  ( F `  ( `' F `  u ) )  =  u )
244201, 238, 243syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s
) )  /\  v  e.  ( F " t
) )  ->  ( F `  ( `' F `  u )
)  =  u )
245 f1ocnvfv2 6168 . . . . . . . . . . . . . . 15  |-  ( ( F : B -1-1-onto-> P  /\  v  e.  P )  ->  ( F `  ( `' F `  v ) )  =  v )
246201, 235, 245syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s
) )  /\  v  e.  ( F " t
) )  ->  ( F `  ( `' F `  v )
)  =  v )
247246oveq2d 6297 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s
) )  /\  v  e.  ( F " t
) )  ->  (
( F `  a
) I ( F `
 ( `' F `  v ) ) )  =  ( ( F `
 a ) I v ) )
248242, 244, 2473eltr3d 2545 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B
)  /\  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s
) )  /\  v  e.  ( F " t
) )  ->  u  e.  ( ( F `  a ) I v ) )
2492483impa 1192 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  A. x  e.  s 
A. y  e.  t  x  e.  ( a J y ) )  /\  u  e.  ( F " s )  /\  v  e.  ( F " t ) )  ->  u  e.  ( ( F `  a ) I v ) )
2504, 5, 6, 189, 195, 197, 200, 249axtgcont 23844 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  A. x  e.  s 
A. y  e.  t  x  e.  ( a J y ) )  ->  E. c  e.  P  A. e  e.  ( F " s ) A. f  e.  ( F " t ) c  e.  ( e I f ) )
251188, 250r19.29a 2985 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  /\  a  e.  B )  /\  A. x  e.  s 
A. y  e.  t  x  e.  ( a J y ) )  ->  E. b  e.  B  A. x  e.  s  A. y  e.  t 
b  e.  ( x J y ) )
252251r19.29an 2984 . . . . . . . 8  |-  ( ( ( ph  /\  (
s  e.  ~P B  /\  t  e.  ~P B ) )  /\  E. a  e.  B  A. x  e.  s  A. y  e.  t  x  e.  ( a J y ) )  ->  E. b  e.  B  A. x  e.  s  A. y  e.  t  b  e.  ( x J y ) )
253252ex 434 . . . . . . 7  |-  ( (
ph  /\  ( s  e.  ~P B  /\  t  e.  ~P B ) )  ->  ( E. a  e.  B  A. x  e.  s  A. y  e.  t  x  e.  ( a J y )  ->  E. b  e.  B  A. x  e.  s  A. y  e.  t  b  e.  ( x J y ) ) )
254253ralrimivva 2864 . . . . . 6  |-  ( ph  ->  A. s  e.  ~P  B A. t  e.  ~P  B ( E. a  e.  B  A. x  e.  s  A. y  e.  t  x  e.  ( a J y )  ->  E. b  e.  B  A. x  e.  s  A. y  e.  t  b  e.  ( x J y ) ) )
25574, 136, 2543jca 1177 . . . . 5  |-  ( ph  ->  ( A. x  e.  B  A. y  e.  B  ( y  e.  ( x J x )  ->  x  =  y )  /\  A. x  e.  B  A. y  e.  B  A. z  e.  B  A. u  e.  B  A. v  e.  B  (
( u  e.  ( x J z )  /\  v  e.  ( y J z ) )  ->  E. a  e.  B  ( a  e.  ( u J y )  /\  a  e.  ( v J x ) ) )  /\  A. s  e.  ~P  B A. t  e.  ~P  B ( E. a  e.  B  A. x  e.  s  A. y  e.  t  x  e.  ( a J y )  ->  E. b  e.  B  A. x  e.  s  A. y  e.  t  b  e.  ( x J y ) ) ) )
25618, 19, 20istrkgb 23830 . . . . 5  |-  ( H  e. TarskiGB  <->  ( H  e.  _V  /\  ( A. x  e.  B  A. y  e.  B  ( y  e.  ( x J x )  ->  x  =  y )  /\  A. x  e.  B  A. y  e.  B  A. z  e.  B  A. u  e.  B  A. v  e.  B  ( (
u  e.  ( x J z )  /\  v  e.  ( y J z ) )  ->  E. a  e.  B  ( a  e.  ( u J y )  /\  a  e.  ( v J x ) ) )  /\  A. s  e.  ~P  B A. t  e.  ~P  B ( E. a  e.  B  A. x  e.  s  A. y  e.  t  x  e.  ( a J y )  ->  E. b  e.  B  A. x  e.  s  A. y  e.  t  b  e.  ( x J y ) ) ) ) )
2573, 255, 256sylanbrc 664 . . . 4  |-  ( ph  ->  H  e. TarskiGB )
25857, 257elind 3673 . . 3  |-  ( ph  ->  H  e.  (TarskiGC  i^i TarskiGB ) )
2597ad9antr 741 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ( (
ph  /\  x  e.  B )  /\  y  e.  B )  /\  z  e.  B )  /\  u  e.  B )  /\  a  e.  B )  /\  b  e.  B )  /\  c  e.  B )  /\  v  e.  B )  /\  (
( x  =/=  y  /\  y  e.  (
x J z )  /\  b  e.  ( a J c ) )  /\  ( ( ( x E y )  =  ( a E b )  /\  ( y E z )  =  ( b E c ) )  /\  ( ( x E u )  =  ( a E v )  /\  ( y E u )  =  ( b E v ) ) ) ) )  ->  G  e. TarskiG )
26011ad9antr 741 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ( (
ph  /\  x  e.  B )  /\  y  e.  B )  /\  z  e.  B )  /\  u  e.  B )  /\  a  e.  B )  /\  b  e.  B )  /\  c  e.  B )  /\  v  e.  B )  /\  (
( x  =/=  y  /\  y  e.  (
x J z )  /\  b  e.  ( a J c ) )  /\  ( ( ( x E y )  =  ( a E b )  /\  ( y E z )  =  ( b E c ) )  /\  ( ( x E u )  =  ( a E v )  /\  ( y E u )  =  ( b E v ) ) ) ) )  ->  F : B
--> P )
261 simp-9r 778 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ( (
ph  /\  x  e.  B )  /\  y  e.  B )  /\  z  e.  B )  /\  u  e.  B )  /\  a  e.  B )  /\  b  e.  B )  /\  c  e.  B )  /\  v  e.  B )  /\  (
( x  =/=  y  /\  y  e.  (
x J z )  /\  b  e.  ( a J c ) )  /\  ( ( ( x E y )  =  ( a E b )  /\  ( y E z )  =  ( b E c ) )  /\  ( ( x E u )  =  ( a E v )  /\  ( y E u )  =  ( b E v ) ) ) ) )  ->  x  e.  B )
262260, 261ffvelrnd 6017 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ( (
ph  /\  x  e.  B )  /\  y  e.  B )  /\  z  e.  B )  /\  u  e.  B )  /\  a  e.  B )  /\  b  e.  B )  /\  c  e.  B )  /\  v  e.  B )  /\  (
( x  =/=  y  /\  y  e.  (
x J z )  /\  b  e.  ( a J c ) )  /\  ( ( ( x E y )  =  ( a E b )  /\  ( y E z )  =  ( b E c ) )  /\  ( ( x E u )  =  ( a E v )  /\  ( y E u )  =  ( b E v ) ) ) ) )  ->  ( F `  x )  e.  P
)
263 simp-8r 776 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ( (
ph  /\  x  e.  B )  /\  y  e.  B )  /\  z  e.  B )  /\  u  e.  B )  /\  a  e.  B )  /\  b  e.  B )  /\  c  e.  B )  /\  v  e.  B )  /\  (
( x  =/=  y  /\  y  e.  (
x J z )  /\  b  e.  ( a J c ) )  /\  ( ( ( x E y )  =  ( a E b )  /\  ( y E z )  =  ( b E c ) )  /\  ( ( x E u )  =  ( a E v )  /\  ( y E u )  =  ( b E v ) ) ) ) )  ->  y  e.  B )
264260, 263ffvelrnd 6017 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ( (
ph  /\  x  e.  B )  /\  y  e.  B )  /\  z  e.  B )  /\  u  e.  B )  /\  a  e.  B )  /\  b  e.  B )  /\  c  e.  B )  /\  v  e.  B )  /\  (
( x  =/=  y  /\  y  e.  (
x J z )  /\  b  e.  ( a J c ) )  /\  ( ( ( x E y )  =  ( a E b )  /\  ( y E z )  =  ( b E c ) )  /\  ( ( x E u )  =  ( a E v )  /\  ( y E u )  =  ( b E v ) ) ) ) )  ->  ( F `  y )  e.  P
)
265 simp-7r 774 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ( (
ph  /\  x  e.  B )  /\  y  e.  B )  /\  z  e.  B )  /\  u  e.  B )  /\  a  e.  B )  /\  b  e.  B )  /\  c  e.  B )  /\  v  e.  B )  /\  (
( x  =/=  y  /\  y  e.  (
x J z )  /\  b  e.  ( a J c ) )  /\  ( ( ( x E y )  =  ( a E b )  /\  ( y E z )  =  ( b E c ) )  /\  ( ( x E u )  =  ( a E v )  /\  ( y E u )  =  ( b E v ) ) ) ) )  ->  z  e.  B )
266260, 265ffvelrnd 6017 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ( (
ph  /\  x  e.  B )  /\  y  e.  B )  /\  z  e.  B )  /\  u  e.  B )  /\  a  e.  B )  /\  b  e.  B )  /\  c  e.  B )  /\  v  e.  B )  /\  (
( x  =/=  y  /\