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

Theorem f1otrge 23253
Description: A bijection between bases which conserves distances and intervals conserves also the property of being a Euclidean geometry. (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 )
f1otrge.g  |-  ( ph  ->  G  e. TarskiGE )
Assertion
Ref Expression
f1otrge  |-  ( ph  ->  H  e. TarskiGE )
Distinct variable groups:    e, f,
g, B    D, e,
f, g    e, E, f, g    e, F, f, g    e, I, f, g    e, J, f, g    P, e, f, g    ph, e, f, g    f, H
Allowed substitution hints:    G( e, f, g)    H( e, g)    V( e, f, g)

Proof of Theorem f1otrge
Dummy variables  a 
b  c  d  u  v  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1otrg.h . . . 4  |-  ( ph  ->  H  e.  V )
2 elex 3077 . . . 4  |-  ( H  e.  V  ->  H  e.  _V )
31, 2syl 16 . . 3  |-  ( ph  ->  H  e.  _V )
4 f1otrkg.f . . . . . . . . . . 11  |-  ( ph  ->  F : B -1-1-onto-> P )
5 f1ocnv 5751 . . . . . . . . . . 11  |-  ( F : B -1-1-onto-> P  ->  `' F : P -1-1-onto-> B )
6 f1of 5739 . . . . . . . . . . 11  |-  ( `' F : P -1-1-onto-> B  ->  `' F : P --> B )
74, 5, 63syl 20 . . . . . . . . . 10  |-  ( ph  ->  `' F : P --> B )
87ad6antr 735 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  ->  `' F : P --> B )
9 simpllr 758 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  -> 
c  e.  P )
108, 9ffvelrnd 5943 . . . . . . . 8  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  -> 
( `' F `  c )  e.  B
)
11 simplr 754 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  -> 
d  e.  P )
128, 11ffvelrnd 5943 . . . . . . . 8  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  -> 
( `' F `  d )  e.  B
)
13 simpr1 994 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  -> 
( F `  y
)  e.  ( ( F `  x ) I c ) )
144adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  F : B -1-1-onto-> P )
1514ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  ->  F : B -1-1-onto-> P )
1615ad3antrrr 729 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  ->  F : B -1-1-onto-> P )
17 f1ocnvfv2 6083 . . . . . . . . . . . . 13  |-  ( ( F : B -1-1-onto-> P  /\  c  e.  P )  ->  ( F `  ( `' F `  c ) )  =  c )
1816, 9, 17syl2anc 661 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  -> 
( F `  ( `' F `  c ) )  =  c )
1918oveq2d 6206 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  -> 
( ( F `  x ) I ( F `  ( `' F `  c ) ) )  =  ( ( F `  x
) I c ) )
2013, 19eleqtrrd 2542 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  -> 
( F `  y
)  e.  ( ( F `  x ) I ( F `  ( `' F `  c ) ) ) )
21 f1otrkg.p . . . . . . . . . . 11  |-  P  =  ( Base `  G
)
22 f1otrkg.d . . . . . . . . . . 11  |-  D  =  ( dist `  G
)
23 f1otrkg.i . . . . . . . . . . 11  |-  I  =  (Itv `  G )
24 f1otrkg.b . . . . . . . . . . 11  |-  B  =  ( Base `  H
)
25 f1otrkg.e . . . . . . . . . . 11  |-  E  =  ( dist `  H
)
26 f1otrkg.j . . . . . . . . . . 11  |-  J  =  (Itv `  H )
27 simp-4l 765 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  /\  c  e.  P )  /\  d  e.  P
)  /\  ( ( F `  y )  e.  ( ( F `  x ) I c )  /\  ( F `
 z )  e.  ( ( F `  x ) I d )  /\  ( F `
 v )  e.  ( c I d ) ) )  /\  ( 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 v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) ) )
28 simpr 461 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  /\  c  e.  P )  /\  d  e.  P
)  /\  ( ( F `  y )  e.  ( ( F `  x ) I c )  /\  ( F `
 z )  e.  ( ( F `  x ) I d )  /\  ( F `
 v )  e.  ( c I d ) ) )  /\  ( e  e.  B  /\  f  e.  B
) )  ->  (
e  e.  B  /\  f  e.  B )
)
29 simplll 757 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  /\  ( e  e.  B  /\  f  e.  B
) )  ->  ( ph  /\  ( x  e.  B  /\  y  e.  B ) ) )
30 simpr 461 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  /\  ( e  e.  B  /\  f  e.  B
) )  ->  (
e  e.  B  /\  f  e.  B )
)
31 f1otrkg.1 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( e  e.  B  /\  f  e.  B ) )  -> 
( e E f )  =  ( ( F `  e ) D ( F `  f ) ) )
3231adantlr 714 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( e  e.  B  /\  f  e.  B ) )  -> 
( e E f )  =  ( ( F `  e ) D ( F `  f ) ) )
3329, 30, 32syl2anc 661 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  /\  ( e  e.  B  /\  f  e.  B
) )  ->  (
e E f )  =  ( ( F `
 e ) D ( F `  f
) ) )
3427, 28, 33syl2anc 661 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  /\  c  e.  P )  /\  d  e.  P
)  /\  ( ( F `  y )  e.  ( ( F `  x ) I c )  /\  ( F `
 z )  e.  ( ( F `  x ) I d )  /\  ( F `
 v )  e.  ( c I d ) ) )  /\  ( e  e.  B  /\  f  e.  B
) )  ->  (
e E f )  =  ( ( F `
 e ) D ( F `  f
) ) )
35 simp-4l 765 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  /\  c  e.  P )  /\  d  e.  P
)  /\  ( ( F `  y )  e.  ( ( F `  x ) I c )  /\  ( F `
 z )  e.  ( ( F `  x ) I d )  /\  ( F `
 v )  e.  ( c I d ) ) )  /\  ( 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 v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) ) )
36 simpr 461 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  /\  c  e.  P )  /\  d  e.  P
)  /\  ( ( F `  y )  e.  ( ( F `  x ) I c )  /\  ( F `
 z )  e.  ( ( F `  x ) I d )  /\  ( F `
 v )  e.  ( c I d ) ) )  /\  ( e  e.  B  /\  f  e.  B  /\  g  e.  B
) )  ->  (
e  e.  B  /\  f  e.  B  /\  g  e.  B )
)
37 simplll 757 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  /\  ( e  e.  B  /\  f  e.  B  /\  g  e.  B
) )  ->  ( ph  /\  ( x  e.  B  /\  y  e.  B ) ) )
38 simpr 461 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  /\  ( e  e.  B  /\  f  e.  B  /\  g  e.  B
) )  ->  (
e  e.  B  /\  f  e.  B  /\  g  e.  B )
)
39 f1otrkg.2 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( e  e.  B  /\  f  e.  B  /\  g  e.  B ) )  -> 
( g  e.  ( e J f )  <-> 
( F `  g
)  e.  ( ( F `  e ) I ( F `  f ) ) ) )
4039adantlr 714 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) ) ) )
4137, 38, 40syl2anc 661 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  /\  ( e  e.  B  /\  f  e.  B  /\  g  e.  B
) )  ->  (
g  e.  ( e J f )  <->  ( F `  g )  e.  ( ( F `  e
) I ( F `
 f ) ) ) )
4235, 36, 41syl2anc 661 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  /\  c  e.  P )  /\  d  e.  P
)  /\  ( ( F `  y )  e.  ( ( F `  x ) I c )  /\  ( F `
 z )  e.  ( ( F `  x ) I d )  /\  ( F `
 v )  e.  ( c I d ) ) )  /\  ( e  e.  B  /\  f  e.  B  /\  g  e.  B
) )  ->  (
g  e.  ( e J f )  <->  ( F `  g )  e.  ( ( F `  e
) I ( F `
 f ) ) ) )
43 simprl 755 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  x  e.  B )
4443ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  ->  x  e.  B )
4544ad3antrrr 729 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  ->  x  e.  B )
46 simprr 756 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
y  e.  B )
4746ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  -> 
y  e.  B )
4847ad3antrrr 729 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  -> 
y  e.  B )
4921, 22, 23, 24, 25, 26, 16, 34, 42, 45, 10, 48f1otrgitv 23251 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  -> 
( y  e.  ( x J ( `' F `  c ) )  <->  ( F `  y )  e.  ( ( F `  x
) I ( F `
 ( `' F `  c ) ) ) ) )
5020, 49mpbird 232 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  -> 
y  e.  ( x J ( `' F `  c ) ) )
51 simpr2 995 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  -> 
( F `  z
)  e.  ( ( F `  x ) I d ) )
52 f1ocnvfv2 6083 . . . . . . . . . . . . 13  |-  ( ( F : B -1-1-onto-> P  /\  d  e.  P )  ->  ( F `  ( `' F `  d ) )  =  d )
5316, 11, 52syl2anc 661 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  -> 
( F `  ( `' F `  d ) )  =  d )
5453oveq2d 6206 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  -> 
( ( F `  x ) I ( F `  ( `' F `  d ) ) )  =  ( ( F `  x
) I d ) )
5551, 54eleqtrrd 2542 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  -> 
( F `  z
)  e.  ( ( F `  x ) I ( F `  ( `' F `  d ) ) ) )
56 simplr1 1030 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  -> 
z  e.  B )
5756ad3antrrr 729 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  -> 
z  e.  B )
5821, 22, 23, 24, 25, 26, 16, 34, 42, 45, 12, 57f1otrgitv 23251 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  -> 
( z  e.  ( x J ( `' F `  d ) )  <->  ( F `  z )  e.  ( ( F `  x
) I ( F `
 ( `' F `  d ) ) ) ) )
5955, 58mpbird 232 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  -> 
z  e.  ( x J ( `' F `  d ) ) )
60 simpr3 996 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  -> 
( F `  v
)  e.  ( c I d ) )
6118, 53oveq12d 6208 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  -> 
( ( F `  ( `' F `  c ) ) I ( F `
 ( `' F `  d ) ) )  =  ( c I d ) )
6260, 61eleqtrrd 2542 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  -> 
( F `  v
)  e.  ( ( F `  ( `' F `  c ) ) I ( F `
 ( `' F `  d ) ) ) )
63 simplr3 1032 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  -> 
v  e.  B )
6463ad3antrrr 729 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  -> 
v  e.  B )
6521, 22, 23, 24, 25, 26, 16, 34, 42, 10, 12, 64f1otrgitv 23251 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  -> 
( v  e.  ( ( `' F `  c ) J ( `' F `  d ) )  <->  ( F `  v )  e.  ( ( F `  ( `' F `  c ) ) I ( F `
 ( `' F `  d ) ) ) ) )
6662, 65mpbird 232 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  -> 
v  e.  ( ( `' F `  c ) J ( `' F `  d ) ) )
6750, 59, 663jca 1168 . . . . . . . 8  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  -> 
( y  e.  ( x J ( `' F `  c ) )  /\  z  e.  ( x J ( `' F `  d ) )  /\  v  e.  ( ( `' F `  c ) J ( `' F `  d ) ) ) )
68 oveq2 6198 . . . . . . . . . . 11  |-  ( a  =  ( `' F `  c )  ->  (
x J a )  =  ( x J ( `' F `  c ) ) )
6968eleq2d 2521 . . . . . . . . . 10  |-  ( a  =  ( `' F `  c )  ->  (
y  e.  ( x J a )  <->  y  e.  ( x J ( `' F `  c ) ) ) )
70 oveq1 6197 . . . . . . . . . . 11  |-  ( a  =  ( `' F `  c )  ->  (
a J b )  =  ( ( `' F `  c ) J b ) )
7170eleq2d 2521 . . . . . . . . . 10  |-  ( a  =  ( `' F `  c )  ->  (
v  e.  ( a J b )  <->  v  e.  ( ( `' F `  c ) J b ) ) )
7269, 713anbi13d 1292 . . . . . . . . 9  |-  ( a  =  ( `' F `  c )  ->  (
( y  e.  ( x J a )  /\  z  e.  ( x J b )  /\  v  e.  ( a J b ) )  <->  ( y  e.  ( x J ( `' F `  c ) )  /\  z  e.  ( x J b )  /\  v  e.  ( ( `' F `  c ) J b ) ) ) )
73 oveq2 6198 . . . . . . . . . . 11  |-  ( b  =  ( `' F `  d )  ->  (
x J b )  =  ( x J ( `' F `  d ) ) )
7473eleq2d 2521 . . . . . . . . . 10  |-  ( b  =  ( `' F `  d )  ->  (
z  e.  ( x J b )  <->  z  e.  ( x J ( `' F `  d ) ) ) )
75 oveq2 6198 . . . . . . . . . . 11  |-  ( b  =  ( `' F `  d )  ->  (
( `' F `  c ) J b )  =  ( ( `' F `  c ) J ( `' F `  d ) ) )
7675eleq2d 2521 . . . . . . . . . 10  |-  ( b  =  ( `' F `  d )  ->  (
v  e.  ( ( `' F `  c ) J b )  <->  v  e.  ( ( `' F `  c ) J ( `' F `  d ) ) ) )
7774, 763anbi23d 1293 . . . . . . . . 9  |-  ( b  =  ( `' F `  d )  ->  (
( y  e.  ( x J ( `' F `  c ) )  /\  z  e.  ( x J b )  /\  v  e.  ( ( `' F `  c ) J b ) )  <->  ( y  e.  ( x J ( `' F `  c ) )  /\  z  e.  ( x J ( `' F `  d ) )  /\  v  e.  ( ( `' F `  c ) J ( `' F `  d ) ) ) ) )
7872, 77rspc2ev 3178 . . . . . . . 8  |-  ( ( ( `' F `  c )  e.  B  /\  ( `' F `  d )  e.  B  /\  ( y  e.  ( x J ( `' F `  c ) )  /\  z  e.  ( x J ( `' F `  d ) )  /\  v  e.  ( ( `' F `  c ) J ( `' F `  d ) ) ) )  ->  E. a  e.  B  E. b  e.  B  ( y  e.  ( x J a )  /\  z  e.  ( x J b )  /\  v  e.  ( a J b ) ) )
7910, 12, 67, 78syl3anc 1219 . . . . . . 7  |-  ( ( ( ( ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  /\  ( u  e.  (
x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
) )  /\  c  e.  P )  /\  d  e.  P )  /\  (
( F `  y
)  e.  ( ( F `  x ) I c )  /\  ( F `  z )  e.  ( ( F `
 x ) I d )  /\  ( F `  v )  e.  ( c I d ) ) )  ->  E. a  e.  B  E. b  e.  B  ( y  e.  ( x J a )  /\  z  e.  ( x J b )  /\  v  e.  ( a J b ) ) )
80 f1otrge.g . . . . . . . . 9  |-  ( ph  ->  G  e. TarskiGE )
8180ad3antrrr 729 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  ->  G  e. TarskiGE )
82 f1of 5739 . . . . . . . . . . . 12  |-  ( F : B -1-1-onto-> P  ->  F : B
--> P )
834, 82syl 16 . . . . . . . . . . 11  |-  ( ph  ->  F : B --> P )
8483adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  F : B --> P )
8584, 43ffvelrnd 5943 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( F `  x
)  e.  P )
8685ad2antrr 725 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  -> 
( F `  x
)  e.  P )
8784, 46ffvelrnd 5943 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( F `  y
)  e.  P )
8887ad2antrr 725 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  -> 
( F `  y
)  e.  P )
8984ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  ->  F : B --> P )
9089, 56ffvelrnd 5943 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  -> 
( F `  z
)  e.  P )
91 simplr2 1031 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  ->  u  e.  B )
9289, 91ffvelrnd 5943 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  -> 
( F `  u
)  e.  P )
9389, 63ffvelrnd 5943 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  -> 
( F `  v
)  e.  P )
94 simpr1 994 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  ->  u  e.  ( x J v ) )
9521, 22, 23, 24, 25, 26, 15, 33, 41, 44, 63, 91f1otrgitv 23251 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  -> 
( u  e.  ( x J v )  <-> 
( F `  u
)  e.  ( ( F `  x ) I ( F `  v ) ) ) )
9694, 95mpbid 210 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  -> 
( F `  u
)  e.  ( ( F `  x ) I ( F `  v ) ) )
97 simpr2 995 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  ->  u  e.  ( y J z ) )
9821, 22, 23, 24, 25, 26, 15, 33, 41, 47, 56, 91f1otrgitv 23251 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  -> 
( u  e.  ( y J z )  <-> 
( F `  u
)  e.  ( ( F `  y ) I ( F `  z ) ) ) )
9997, 98mpbid 210 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  -> 
( F `  u
)  e.  ( ( F `  y ) I ( F `  z ) ) )
10015, 44jca 532 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  -> 
( F : B -1-1-onto-> P  /\  x  e.  B
) )
101 simpr3 996 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  ->  x  =/=  u )
102 dff1o6 6081 . . . . . . . . . . . . . 14  |-  ( F : B -1-1-onto-> P  <->  ( F  Fn  B  /\  ran  F  =  P  /\  A. x  e.  B  A. u  e.  B  ( ( F `  x )  =  ( F `  u )  ->  x  =  u ) ) )
103102simp3bi 1005 . . . . . . . . . . . . 13  |-  ( F : B -1-1-onto-> P  ->  A. x  e.  B  A. u  e.  B  ( ( F `  x )  =  ( F `  u )  ->  x  =  u ) )
104103r19.21bi 2910 . . . . . . . . . . . 12  |-  ( ( F : B -1-1-onto-> P  /\  x  e.  B )  ->  A. u  e.  B  ( ( F `  x )  =  ( F `  u )  ->  x  =  u ) )
105104r19.21bi 2910 . . . . . . . . . . 11  |-  ( ( ( F : B -1-1-onto-> P  /\  x  e.  B
)  /\  u  e.  B )  ->  (
( F `  x
)  =  ( F `
 u )  ->  x  =  u )
)
106105necon3d 2672 . . . . . . . . . 10  |-  ( ( ( F : B -1-1-onto-> P  /\  x  e.  B
)  /\  u  e.  B )  ->  (
x  =/=  u  -> 
( F `  x
)  =/=  ( F `
 u ) ) )
107106imp 429 . . . . . . . . 9  |-  ( ( ( ( F : B
-1-1-onto-> P  /\  x  e.  B
)  /\  u  e.  B )  /\  x  =/=  u )  ->  ( F `  x )  =/=  ( F `  u
) )
108100, 91, 101, 107syl21anc 1218 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  -> 
( F `  x
)  =/=  ( F `
 u ) )
10921, 22, 23, 81, 86, 88, 90, 92, 93, 96, 99, 108axtgeucl 23050 . . . . . . 7  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  ->  E. c  e.  P  E. d  e.  P  ( ( F `  y )  e.  ( ( F `  x
) I c )  /\  ( F `  z )  e.  ( ( F `  x
) I d )  /\  ( F `  v )  e.  ( c I d ) ) )
11079, 109r19.29_2a 2960 . . . . . 6  |-  ( ( ( ( ph  /\  ( x  e.  B  /\  y  e.  B
) )  /\  (
z  e.  B  /\  u  e.  B  /\  v  e.  B )
)  /\  ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u ) )  ->  E. a  e.  B  E. b  e.  B  ( y  e.  ( x J a )  /\  z  e.  ( x J b )  /\  v  e.  ( a J b ) ) )
111110ex 434 . . . . 5  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( z  e.  B  /\  u  e.  B  /\  v  e.  B ) )  -> 
( ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u )  ->  E. a  e.  B  E. b  e.  B  ( y  e.  ( x J a )  /\  z  e.  ( x J b )  /\  v  e.  ( a J b ) ) ) )
112111ralrimivvva 2905 . . . 4  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  A. z  e.  B  A. u  e.  B  A. v  e.  B  ( ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u )  ->  E. a  e.  B  E. b  e.  B  ( y  e.  ( x J a )  /\  z  e.  ( x J b )  /\  v  e.  ( a J b ) ) ) )
113112ralrimivva 2904 . . 3  |-  ( 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 v )  /\  u  e.  ( y J z )  /\  x  =/=  u )  ->  E. a  e.  B  E. b  e.  B  ( y  e.  ( x J a )  /\  z  e.  ( x J b )  /\  v  e.  ( a J b ) ) ) )
1143, 113jca 532 . 2  |-  ( ph  ->  ( H  e.  _V  /\ 
A. x  e.  B  A. y  e.  B  A. z  e.  B  A. u  e.  B  A. v  e.  B  ( ( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u )  ->  E. a  e.  B  E. b  e.  B  ( y  e.  ( x J a )  /\  z  e.  ( x J b )  /\  v  e.  ( a J b ) ) ) ) )
11524, 25, 26istrkge 23034 . 2  |-  ( H  e. TarskiGE  <->  ( H  e.  _V  /\  A. x  e.  B  A. y  e.  B  A. z  e.  B  A. u  e.  B  A. v  e.  B  (
( u  e.  ( x J v )  /\  u  e.  ( y J z )  /\  x  =/=  u
)  ->  E. a  e.  B  E. b  e.  B  ( y  e.  ( x J a )  /\  z  e.  ( x J b )  /\  v  e.  ( a J b ) ) ) ) )
116114, 115sylibr 212 1  |-  ( ph  ->  H  e. TarskiGE )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965    = wceq 1370    e. wcel 1758    =/= wne 2644   A.wral 2795   E.wrex 2796   _Vcvv 3068   `'ccnv 4937   ran crn 4939    Fn wfn 5511   -->wf 5512   -1-1-onto->wf1o 5515   ` cfv 5516  (class class class)co 6190   Basecbs 14276   distcds 14349  TarskiGEcstrkge 23011  Itvcitv 23012
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-sbc 3285  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-opab 4449  df-id 4734  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-rn 4949  df-res 4950  df-ima 4951  df-iota 5479  df-fun 5518  df-fn 5519  df-f 5520  df-f1 5521  df-fo 5522  df-f1o 5523  df-fv 5524  df-ov 6193  df-trkge 23027
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator