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

Theorem f1otrge 24302
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 . . 3  |-  ( ph  ->  H  e.  V )
2 elex 3118 . . 3  |-  ( H  e.  V  ->  H  e.  _V )
31, 2syl 16 . 2  |-  ( ph  ->  H  e.  _V )
4 f1otrkg.f . . . . . . . . . 10  |-  ( ph  ->  F : B -1-1-onto-> P )
5 f1ocnv 5834 . . . . . . . . . 10  |-  ( F : B -1-1-onto-> P  ->  `' F : P -1-1-onto-> B )
6 f1of 5822 . . . . . . . . . 10  |-  ( `' F : P -1-1-onto-> B  ->  `' F : P --> B )
74, 5, 63syl 20 . . . . . . . . 9  |-  ( ph  ->  `' F : P --> B )
87ad6antr 735 . . . . . . . 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 : P --> B )
9 simpllr 760 . . . . . . . 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 ) ) )  -> 
c  e.  P )
108, 9ffvelrnd 6033 . . . . . . 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 ) ) )  -> 
( `' F `  c )  e.  B
)
11 simplr 755 . . . . . . . 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 ) ) )  -> 
d  e.  P )
128, 11ffvelrnd 6033 . . . . . . 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 ) ) )  -> 
( `' F `  d )  e.  B
)
13 simpr1 1002 . . . . . . . . 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 `  y
)  e.  ( ( F `  x ) I c ) )
144ad3antrrr 729 . . . . . . . . . . . 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 ) )  ->  F : B -1-1-onto-> P )
1514ad3antrrr 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 ) ) )  ->  F : B -1-1-onto-> P )
16 f1ocnvfv2 6184 . . . . . . . . . . 11  |-  ( ( F : B -1-1-onto-> P  /\  c  e.  P )  ->  ( F `  ( `' F `  c ) )  =  c )
1715, 9, 16syl2anc 661 . . . . . . . . . 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 `  ( `' F `  c ) )  =  c )
1817oveq2d 6312 . . . . . . . . 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 `  x ) I ( F `  ( `' F `  c ) ) )  =  ( ( F `  x
) I c ) )
1913, 18eleqtrrd 2548 . . . . . . . 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 `  y
)  e.  ( ( F `  x ) I ( F `  ( `' F `  c ) ) ) )
20 f1otrkg.p . . . . . . . . 9  |-  P  =  ( Base `  G
)
21 f1otrkg.d . . . . . . . . 9  |-  D  =  ( dist `  G
)
22 f1otrkg.i . . . . . . . . 9  |-  I  =  (Itv `  G )
23 f1otrkg.b . . . . . . . . 9  |-  B  =  ( Base `  H
)
24 f1otrkg.e . . . . . . . . 9  |-  E  =  ( dist `  H
)
25 f1otrkg.j . . . . . . . . 9  |-  J  =  (Itv `  H )
26 simp-4l 767 . . . . . . . . . 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 ) ) )  /\  ( 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 ) ) )
27 simplll 759 . . . . . . . . . . 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 ) )  /\  ( e  e.  B  /\  f  e.  B
) )  ->  ( ph  /\  ( x  e.  B  /\  y  e.  B ) ) )
28 f1otrkg.1 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( e  e.  B  /\  f  e.  B ) )  -> 
( e E f )  =  ( ( F `  e ) D ( F `  f ) ) )
2928adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  B  /\  y  e.  B )
)  /\  ( e  e.  B  /\  f  e.  B ) )  -> 
( e E f )  =  ( ( F `  e ) D ( F `  f ) ) )
3027, 29sylancom 667 . . . . . . . . . 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 ) )  /\  ( e  e.  B  /\  f  e.  B
) )  ->  (
e E f )  =  ( ( F `
 e ) D ( F `  f
) ) )
3126, 30sylancom 667 . . . . . . . . 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 ) ) )  /\  ( e  e.  B  /\  f  e.  B
) )  ->  (
e E f )  =  ( ( F `
 e ) D ( F `  f
) ) )
32 simp-4l 767 . . . . . . . . . 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 ) ) )  /\  ( 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 ) ) )
33 simplll 759 . . . . . . . . . . 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 ) )  /\  ( e  e.  B  /\  f  e.  B  /\  g  e.  B
) )  ->  ( ph  /\  ( x  e.  B  /\  y  e.  B ) ) )
34 f1otrkg.2 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( e  e.  B  /\  f  e.  B  /\  g  e.  B ) )  -> 
( g  e.  ( e J f )  <-> 
( F `  g
)  e.  ( ( F `  e ) I ( F `  f ) ) ) )
3534adantlr 714 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) ) )
3633, 35sylancom 667 . . . . . . . . . 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 ) )  /\  ( e  e.  B  /\  f  e.  B  /\  g  e.  B
) )  ->  (
g  e.  ( e J f )  <->  ( F `  g )  e.  ( ( F `  e
) I ( F `
 f ) ) ) )
3732, 36sylancom 667 . . . . . . . . 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 ) ) )  /\  ( e  e.  B  /\  f  e.  B  /\  g  e.  B
) )  ->  (
g  e.  ( e J f )  <->  ( F `  g )  e.  ( ( F `  e
) I ( F `
 f ) ) ) )
38 simprl 756 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  x  e.  B )
3938ad2antrr 725 . . . . . . . . . 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 ) )  ->  x  e.  B )
4039ad3antrrr 729 . . . . . . . . 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 ) ) )  ->  x  e.  B )
41 simprr 757 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
y  e.  B )
4241ad2antrr 725 . . . . . . . . . 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 ) )  -> 
y  e.  B )
4342ad3antrrr 729 . . . . . . . . 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.  B )
4420, 21, 22, 23, 24, 25, 15, 31, 37, 40, 10, 43f1otrgitv 24300 . . . . . . . 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 ) )  <->  ( F `  y )  e.  ( ( F `  x
) I ( F `
 ( `' F `  c ) ) ) ) )
4519, 44mpbird 232 . . . . . . 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 ) ) )  -> 
y  e.  ( x J ( `' F `  c ) ) )
46 simpr2 1003 . . . . . . . . 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 `  z
)  e.  ( ( F `  x ) I d ) )
47 f1ocnvfv2 6184 . . . . . . . . . . 11  |-  ( ( F : B -1-1-onto-> P  /\  d  e.  P )  ->  ( F `  ( `' F `  d ) )  =  d )
4815, 11, 47syl2anc 661 . . . . . . . . . 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 `  ( `' F `  d ) )  =  d )
4948oveq2d 6312 . . . . . . . . 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 `  x ) I ( F `  ( `' F `  d ) ) )  =  ( ( F `  x
) I d ) )
5046, 49eleqtrrd 2548 . . . . . . . 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 `  z
)  e.  ( ( F `  x ) I ( F `  ( `' F `  d ) ) ) )
51 simplr1 1038 . . . . . . . . . 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 ) )  -> 
z  e.  B )
5251ad3antrrr 729 . . . . . . . . 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.  B )
5320, 21, 22, 23, 24, 25, 15, 31, 37, 40, 12, 52f1otrgitv 24300 . . . . . . . 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 ) ) )  -> 
( z  e.  ( x J ( `' F `  d ) )  <->  ( F `  z )  e.  ( ( F `  x
) I ( F `
 ( `' F `  d ) ) ) ) )
5450, 53mpbird 232 . . . . . . 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 ) ) )  -> 
z  e.  ( x J ( `' F `  d ) ) )
55 simpr3 1004 . . . . . . . . 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 `  v
)  e.  ( c I d ) )
5617, 48oveq12d 6314 . . . . . . . . 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 `  ( `' F `  c ) ) I ( F `
 ( `' F `  d ) ) )  =  ( c I d ) )
5755, 56eleqtrrd 2548 . . . . . . . 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 `  v
)  e.  ( ( F `  ( `' F `  c ) ) I ( F `
 ( `' F `  d ) ) ) )
58 simplr3 1040 . . . . . . . . . 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 ) )  -> 
v  e.  B )
5958ad3antrrr 729 . . . . . . . . 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.  B )
6020, 21, 22, 23, 24, 25, 15, 31, 37, 10, 12, 59f1otrgitv 24300 . . . . . . . 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 ) ) )  -> 
( v  e.  ( ( `' F `  c ) J ( `' F `  d ) )  <->  ( F `  v )  e.  ( ( F `  ( `' F `  c ) ) I ( F `
 ( `' F `  d ) ) ) ) )
6157, 60mpbird 232 . . . . . . 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 ) ) )  -> 
v  e.  ( ( `' F `  c ) J ( `' F `  d ) ) )
62 oveq2 6304 . . . . . . . . . 10  |-  ( a  =  ( `' F `  c )  ->  (
x J a )  =  ( x J ( `' F `  c ) ) )
6362eleq2d 2527 . . . . . . . . 9  |-  ( a  =  ( `' F `  c )  ->  (
y  e.  ( x J a )  <->  y  e.  ( x J ( `' F `  c ) ) ) )
64 oveq1 6303 . . . . . . . . . 10  |-  ( a  =  ( `' F `  c )  ->  (
a J b )  =  ( ( `' F `  c ) J b ) )
6564eleq2d 2527 . . . . . . . . 9  |-  ( a  =  ( `' F `  c )  ->  (
v  e.  ( a J b )  <->  v  e.  ( ( `' F `  c ) J b ) ) )
6663, 653anbi13d 1301 . . . . . . . 8  |-  ( 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 ) ) ) )
67 oveq2 6304 . . . . . . . . . 10  |-  ( b  =  ( `' F `  d )  ->  (
x J b )  =  ( x J ( `' F `  d ) ) )
6867eleq2d 2527 . . . . . . . . 9  |-  ( b  =  ( `' F `  d )  ->  (
z  e.  ( x J b )  <->  z  e.  ( x J ( `' F `  d ) ) ) )
69 oveq2 6304 . . . . . . . . . 10  |-  ( b  =  ( `' F `  d )  ->  (
( `' F `  c ) J b )  =  ( ( `' F `  c ) J ( `' F `  d ) ) )
7069eleq2d 2527 . . . . . . . . 9  |-  ( b  =  ( `' F `  d )  ->  (
v  e.  ( ( `' F `  c ) J b )  <->  v  e.  ( ( `' F `  c ) J ( `' F `  d ) ) ) )
7168, 703anbi23d 1302 . . . . . . . 8  |-  ( 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 ) ) ) ) )
7266, 71rspc2ev 3221 . . . . . . 7  |-  ( ( ( `' 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 ) ) )
7310, 12, 45, 54, 61, 72syl113anc 1240 . . . . . 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
) )  /\  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 ) ) )
74 f1otrge.g . . . . . . . 8  |-  ( ph  ->  G  e. TarskiGE )
7574ad3antrrr 729 . . . . . . 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 ) )  ->  G  e. TarskiGE )
76 f1of 5822 . . . . . . . . . . 11  |-  ( F : B -1-1-onto-> P  ->  F : B
--> P )
774, 76syl 16 . . . . . . . . . 10  |-  ( ph  ->  F : B --> P )
7877adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  ->  F : B --> P )
7978, 38ffvelrnd 6033 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( F `  x
)  e.  P )
8079ad2antrr 725 . . . . . . 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 ) )  -> 
( F `  x
)  e.  P )
8178, 41ffvelrnd 6033 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( F `  y
)  e.  P )
8281ad2antrr 725 . . . . . . 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 ) )  -> 
( F `  y
)  e.  P )
8377ad3antrrr 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 ) )  ->  F : B --> P )
8483, 51ffvelrnd 6033 . . . . . . 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 ) )  -> 
( F `  z
)  e.  P )
85 simplr2 1039 . . . . . . . 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 ) )  ->  u  e.  B )
8683, 85ffvelrnd 6033 . . . . . . 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 ) )  -> 
( F `  u
)  e.  P )
8783, 58ffvelrnd 6033 . . . . . . 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 ) )  -> 
( F `  v
)  e.  P )
88 simpr1 1002 . . . . . . . 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 ) )  ->  u  e.  ( x J v ) )
8920, 21, 22, 23, 24, 25, 14, 30, 36, 39, 58, 85f1otrgitv 24300 . . . . . . . 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 ) )  -> 
( u  e.  ( x J v )  <-> 
( F `  u
)  e.  ( ( F `  x ) I ( F `  v ) ) ) )
9088, 89mpbid 210 . . . . . . 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 ) )  -> 
( F `  u
)  e.  ( ( F `  x ) I ( F `  v ) ) )
91 simpr2 1003 . . . . . . . 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 ) )  ->  u  e.  ( y J z ) )
9220, 21, 22, 23, 24, 25, 14, 30, 36, 42, 51, 85f1otrgitv 24300 . . . . . . . 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 ) )  -> 
( u  e.  ( y J z )  <-> 
( F `  u
)  e.  ( ( F `  y ) I ( F `  z ) ) ) )
9391, 92mpbid 210 . . . . . . 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 ) )  -> 
( F `  u
)  e.  ( ( F `  y ) I ( F `  z ) ) )
9414, 39jca 532 . . . . . . . 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 : B -1-1-onto-> P  /\  x  e.  B
) )
95 simpr3 1004 . . . . . . . 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 ) )  ->  x  =/=  u )
96 dff1o6 6182 . . . . . . . . . . . . 13  |-  ( 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 ) ) )
9796simp3bi 1013 . . . . . . . . . . . 12  |-  ( F : B -1-1-onto-> P  ->  A. x  e.  B  A. u  e.  B  ( ( F `  x )  =  ( F `  u )  ->  x  =  u ) )
9897r19.21bi 2826 . . . . . . . . . . 11  |-  ( ( F : B -1-1-onto-> P  /\  x  e.  B )  ->  A. u  e.  B  ( ( F `  x )  =  ( F `  u )  ->  x  =  u ) )
9998r19.21bi 2826 . . . . . . . . . 10  |-  ( ( ( F : B -1-1-onto-> P  /\  x  e.  B
)  /\  u  e.  B )  ->  (
( F `  x
)  =  ( F `
 u )  ->  x  =  u )
)
10099necon3d 2681 . . . . . . . . 9  |-  ( ( ( F : B -1-1-onto-> P  /\  x  e.  B
)  /\  u  e.  B )  ->  (
x  =/=  u  -> 
( F `  x
)  =/=  ( F `
 u ) ) )
101100imp 429 . . . . . . . 8  |-  ( ( ( ( F : B
-1-1-onto-> P  /\  x  e.  B
)  /\  u  e.  B )  /\  x  =/=  u )  ->  ( F `  x )  =/=  ( F `  u
) )
10294, 85, 95, 101syl21anc 1227 . . . . . . 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 ) )  -> 
( F `  x
)  =/=  ( F `
 u ) )
10320, 21, 22, 75, 80, 82, 84, 86, 87, 90, 93, 102axtgeucl 23996 . . . . . 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. 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 ) ) )
10473, 103r19.29_2a 3001 . . . . 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 ) ) )
105104ex 434 . . . 4  |-  ( ( ( 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 ) ) ) )
106105ralrimivvva 2879 . . 3  |-  ( (
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 ) ) ) )
107106ralrimivva 2878 . 2  |-  ( 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 ) ) ) )
10823, 24, 25istrkge 23980 . 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 ) ) ) ) )
1093, 107, 108sylanbrc 664 1  |-  ( ph  ->  H  e. TarskiGE )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 973    = wceq 1395    e. wcel 1819    =/= wne 2652   A.wral 2807   E.wrex 2808   _Vcvv 3109   `'ccnv 5007   ran crn 5009    Fn wfn 5589   -->wf 5590   -1-1-onto->wf1o 5593   ` cfv 5594  (class class class)co 6296   Basecbs 14644   distcds 14721  TarskiGEcstrkge 23957  Itvcitv 23958
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-opab 4516  df-id 4804  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-ov 6299  df-trkge 23973
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator