Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  nofulllem5 Structured version   Visualization version   Unicode version

Theorem nofulllem5 30666
Description: Lemma for nofull (future) . Here, we introduce a new surreal number  X. Eventually, we will show that either  X or a related surreal number has the required properties for the final theorem. We begin by calculating the domain of  X. (Contributed by Scott Fenton, 1-May-2017.)
Hypotheses
Ref Expression
nofulllem5.1  |-  M  = 
|^| { a  e.  On  |  A. x  e.  L  A. y  e.  R  ( x  |`  a )  =/=  ( y  |`  a ) }
nofulllem5.2  |-  S  =  { f  |  E. g  e.  L  E. h  e.  R  E. a  e.  M  (
( g  |`  a
)  =  f  /\  ( h  |`  a )  =  f ) }
nofulllem5.3  |-  X  = 
U. S
Assertion
Ref Expression
nofulllem5  |-  ( ( ( L  C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W
)  /\  A. x  e.  L  A. y  e.  R  x <s y )  ->  dom  X  =  U. M )
Distinct variable groups:    x, L, y, f, g, h, a   
x, R, y, h, f, g, a    x, W, y, f, g, h, a    x, V, y, f, g, h, a    M, a, f, g, h
Allowed substitution hints:    S( x, y, f, g, h, a)    M( x, y)    X( x, y, f, g, h, a)

Proof of Theorem nofulllem5
Dummy variables  b 
j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nofulllem5.3 . . . 4  |-  X  = 
U. S
21dmeqi 5041 . . 3  |-  dom  X  =  dom  U. S
3 dmuni 5050 . . 3  |-  dom  U. S  =  U_ b  e.  S  dom  b
42, 3eqtri 2493 . 2  |-  dom  X  =  U_ b  e.  S  dom  b
5 iunss 4310 . . . . 5  |-  ( U_ b  e.  S  dom  b  C_  U. M  <->  A. b  e.  S  dom  b  C_  U. M )
6 vex 3034 . . . . . . 7  |-  b  e. 
_V
7 eqeq2 2482 . . . . . . . . . 10  |-  ( f  =  b  ->  (
( g  |`  a
)  =  f  <->  ( g  |`  a )  =  b ) )
8 eqeq2 2482 . . . . . . . . . 10  |-  ( f  =  b  ->  (
( h  |`  a
)  =  f  <->  ( h  |`  a )  =  b ) )
97, 8anbi12d 725 . . . . . . . . 9  |-  ( f  =  b  ->  (
( ( g  |`  a )  =  f  /\  ( h  |`  a )  =  f )  <->  ( ( g  |`  a )  =  b  /\  ( h  |`  a )  =  b ) ) )
109rexbidv 2892 . . . . . . . 8  |-  ( f  =  b  ->  ( E. a  e.  M  ( ( g  |`  a )  =  f  /\  ( h  |`  a )  =  f )  <->  E. a  e.  M  ( ( g  |`  a )  =  b  /\  ( h  |`  a )  =  b ) ) )
11102rexbidv 2897 . . . . . . 7  |-  ( f  =  b  ->  ( E. g  e.  L  E. h  e.  R  E. a  e.  M  ( ( g  |`  a )  =  f  /\  ( h  |`  a )  =  f )  <->  E. g  e.  L  E. h  e.  R  E. a  e.  M  ( ( g  |`  a )  =  b  /\  ( h  |`  a )  =  b ) ) )
12 nofulllem5.2 . . . . . . 7  |-  S  =  { f  |  E. g  e.  L  E. h  e.  R  E. a  e.  M  (
( g  |`  a
)  =  f  /\  ( h  |`  a )  =  f ) }
136, 11, 12elab2 3176 . . . . . 6  |-  ( b  e.  S  <->  E. g  e.  L  E. h  e.  R  E. a  e.  M  ( (
g  |`  a )  =  b  /\  ( h  |`  a )  =  b ) )
14 inss1 3643 . . . . . . . . . . . 12  |-  ( a  i^i  dom  g )  C_  a
15 elssuni 4219 . . . . . . . . . . . 12  |-  ( a  e.  M  ->  a  C_ 
U. M )
1614, 15syl5ss 3429 . . . . . . . . . . 11  |-  ( a  e.  M  ->  (
a  i^i  dom  g ) 
C_  U. M )
17 dmres 5131 . . . . . . . . . . . . 13  |-  dom  (
g  |`  a )  =  ( a  i^i  dom  g )
18 dmeq 5040 . . . . . . . . . . . . 13  |-  ( ( g  |`  a )  =  b  ->  dom  (
g  |`  a )  =  dom  b )
1917, 18syl5eqr 2519 . . . . . . . . . . . 12  |-  ( ( g  |`  a )  =  b  ->  ( a  i^i  dom  g )  =  dom  b )
2019sseq1d 3445 . . . . . . . . . . 11  |-  ( ( g  |`  a )  =  b  ->  ( ( a  i^i  dom  g
)  C_  U. M  <->  dom  b  C_  U. M ) )
2116, 20syl5ibcom 228 . . . . . . . . . 10  |-  ( a  e.  M  ->  (
( g  |`  a
)  =  b  ->  dom  b  C_  U. M
) )
2221adantrd 475 . . . . . . . . 9  |-  ( a  e.  M  ->  (
( ( g  |`  a )  =  b  /\  ( h  |`  a )  =  b )  ->  dom  b  C_  U. M ) )
2322rexlimiv 2867 . . . . . . . 8  |-  ( E. a  e.  M  ( ( g  |`  a
)  =  b  /\  ( h  |`  a )  =  b )  ->  dom  b  C_  U. M
)
2423a1i 11 . . . . . . 7  |-  ( ( g  e.  L  /\  h  e.  R )  ->  ( E. a  e.  M  ( ( g  |`  a )  =  b  /\  ( h  |`  a )  =  b )  ->  dom  b  C_  U. M ) )
2524rexlimivv 2876 . . . . . 6  |-  ( E. g  e.  L  E. h  e.  R  E. a  e.  M  (
( g  |`  a
)  =  b  /\  ( h  |`  a )  =  b )  ->  dom  b  C_  U. M
)
2613, 25sylbi 200 . . . . 5  |-  ( b  e.  S  ->  dom  b  C_  U. M )
275, 26mprgbir 2771 . . . 4  |-  U_ b  e.  S  dom  b  C_  U. M
2827a1i 11 . . 3  |-  ( ( ( L  C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W
)  /\  A. x  e.  L  A. y  e.  R  x <s y )  ->  U_ b  e.  S  dom  b  C_  U. M )
29 nofulllem5.1 . . . . . . . . 9  |-  M  = 
|^| { a  e.  On  |  A. x  e.  L  A. y  e.  R  ( x  |`  a )  =/=  ( y  |`  a ) }
3029nofulllem4 30665 . . . . . . . 8  |-  ( ( ( L  C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W
)  /\  A. x  e.  L  A. y  e.  R  x <s y )  ->  M  e.  On )
31 eloni 5440 . . . . . . . 8  |-  ( M  e.  On  ->  Ord  M )
3230, 31syl 17 . . . . . . 7  |-  ( ( ( L  C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W
)  /\  A. x  e.  L  A. y  e.  R  x <s y )  ->  Ord  M )
33 ordsucuniel 6670 . . . . . . 7  |-  ( Ord 
M  ->  ( j  e.  U. M  <->  suc  j  e.  M ) )
3432, 33syl 17 . . . . . 6  |-  ( ( ( L  C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W
)  /\  A. x  e.  L  A. y  e.  R  x <s y )  ->  (
j  e.  U. M  <->  suc  j  e.  M ) )
35 simpr 468 . . . . . . . 8  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  suc  j  e.  M
)  ->  suc  j  e.  M )
36 onss 6636 . . . . . . . . . . . . 13  |-  ( M  e.  On  ->  M  C_  On )
3730, 36syl 17 . . . . . . . . . . . 12  |-  ( ( ( L  C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W
)  /\  A. x  e.  L  A. y  e.  R  x <s y )  ->  M  C_  On )
3837sselda 3418 . . . . . . . . . . 11  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  suc  j  e.  M
)  ->  suc  j  e.  On )
39 ssrab2 3500 . . . . . . . . . . . . . . . . . . 19  |-  { a  e.  On  |  A. x  e.  L  A. y  e.  R  (
x  |`  a )  =/=  ( y  |`  a
) }  C_  On
40 onnmin 6649 . . . . . . . . . . . . . . . . . . 19  |-  ( ( { a  e.  On  |  A. x  e.  L  A. y  e.  R  ( x  |`  a )  =/=  ( y  |`  a ) }  C_  On  /\  suc  j  e. 
{ a  e.  On  |  A. x  e.  L  A. y  e.  R  ( x  |`  a )  =/=  ( y  |`  a ) } )  ->  -.  suc  j  e. 
|^| { a  e.  On  |  A. x  e.  L  A. y  e.  R  ( x  |`  a )  =/=  ( y  |`  a ) } )
4139, 40mpan 684 . . . . . . . . . . . . . . . . . 18  |-  ( suc  j  e.  { a  e.  On  |  A. x  e.  L  A. y  e.  R  (
x  |`  a )  =/=  ( y  |`  a
) }  ->  -.  suc  j  e.  |^| { a  e.  On  |  A. x  e.  L  A. y  e.  R  (
x  |`  a )  =/=  ( y  |`  a
) } )
4241adantl 473 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  suc  j  e.  { a  e.  On  |  A. x  e.  L  A. y  e.  R  (
x  |`  a )  =/=  ( y  |`  a
) } )  ->  -.  suc  j  e.  |^| { a  e.  On  |  A. x  e.  L  A. y  e.  R  ( x  |`  a )  =/=  ( y  |`  a ) } )
4329eleq2i 2541 . . . . . . . . . . . . . . . . 17  |-  ( suc  j  e.  M  <->  suc  j  e. 
|^| { a  e.  On  |  A. x  e.  L  A. y  e.  R  ( x  |`  a )  =/=  ( y  |`  a ) } )
4442, 43sylnibr 312 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  suc  j  e.  { a  e.  On  |  A. x  e.  L  A. y  e.  R  (
x  |`  a )  =/=  ( y  |`  a
) } )  ->  -.  suc  j  e.  M
)
4544ex 441 . . . . . . . . . . . . . . 15  |-  ( ( ( L  C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W
)  /\  A. x  e.  L  A. y  e.  R  x <s y )  ->  ( suc  j  e.  { a  e.  On  |  A. x  e.  L  A. y  e.  R  (
x  |`  a )  =/=  ( y  |`  a
) }  ->  -.  suc  j  e.  M
) )
4645con2d 119 . . . . . . . . . . . . . 14  |-  ( ( ( L  C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W
)  /\  A. x  e.  L  A. y  e.  R  x <s y )  ->  ( suc  j  e.  M  ->  -.  suc  j  e. 
{ a  e.  On  |  A. x  e.  L  A. y  e.  R  ( x  |`  a )  =/=  ( y  |`  a ) } ) )
4746imp 436 . . . . . . . . . . . . 13  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  suc  j  e.  M
)  ->  -.  suc  j  e.  { a  e.  On  |  A. x  e.  L  A. y  e.  R  ( x  |`  a )  =/=  ( y  |`  a ) } )
48 reseq2 5106 . . . . . . . . . . . . . . . . 17  |-  ( a  =  suc  j  -> 
( x  |`  a
)  =  ( x  |`  suc  j ) )
49 reseq2 5106 . . . . . . . . . . . . . . . . 17  |-  ( a  =  suc  j  -> 
( y  |`  a
)  =  ( y  |`  suc  j ) )
5048, 49neeq12d 2704 . . . . . . . . . . . . . . . 16  |-  ( a  =  suc  j  -> 
( ( x  |`  a )  =/=  (
y  |`  a )  <->  ( x  |` 
suc  j )  =/=  ( y  |`  suc  j
) ) )
51502ralbidv 2832 . . . . . . . . . . . . . . 15  |-  ( a  =  suc  j  -> 
( A. x  e.  L  A. y  e.  R  ( x  |`  a )  =/=  (
y  |`  a )  <->  A. x  e.  L  A. y  e.  R  ( x  |` 
suc  j )  =/=  ( y  |`  suc  j
) ) )
52 reseq1 5105 . . . . . . . . . . . . . . . . 17  |-  ( x  =  g  ->  (
x  |`  suc  j )  =  ( g  |`  suc  j ) )
5352neeq1d 2702 . . . . . . . . . . . . . . . 16  |-  ( x  =  g  ->  (
( x  |`  suc  j
)  =/=  ( y  |`  suc  j )  <->  ( g  |` 
suc  j )  =/=  ( y  |`  suc  j
) ) )
54 reseq1 5105 . . . . . . . . . . . . . . . . 17  |-  ( y  =  h  ->  (
y  |`  suc  j )  =  ( h  |`  suc  j ) )
5554neeq2d 2703 . . . . . . . . . . . . . . . 16  |-  ( y  =  h  ->  (
( g  |`  suc  j
)  =/=  ( y  |`  suc  j )  <->  ( g  |` 
suc  j )  =/=  ( h  |`  suc  j
) ) )
5653, 55cbvral2v 3013 . . . . . . . . . . . . . . 15  |-  ( A. x  e.  L  A. y  e.  R  (
x  |`  suc  j )  =/=  ( y  |`  suc  j )  <->  A. g  e.  L  A. h  e.  R  ( g  |` 
suc  j )  =/=  ( h  |`  suc  j
) )
5751, 56syl6bb 269 . . . . . . . . . . . . . 14  |-  ( a  =  suc  j  -> 
( A. x  e.  L  A. y  e.  R  ( x  |`  a )  =/=  (
y  |`  a )  <->  A. g  e.  L  A. h  e.  R  ( g  |` 
suc  j )  =/=  ( h  |`  suc  j
) ) )
5857elrab 3184 . . . . . . . . . . . . 13  |-  ( suc  j  e.  { a  e.  On  |  A. x  e.  L  A. y  e.  R  (
x  |`  a )  =/=  ( y  |`  a
) }  <->  ( suc  j  e.  On  /\  A. g  e.  L  A. h  e.  R  (
g  |`  suc  j )  =/=  ( h  |`  suc  j ) ) )
5947, 58sylnib 311 . . . . . . . . . . . 12  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  suc  j  e.  M
)  ->  -.  ( suc  j  e.  On  /\ 
A. g  e.  L  A. h  e.  R  ( g  |`  suc  j
)  =/=  ( h  |`  suc  j ) ) )
60 imnan 429 . . . . . . . . . . . 12  |-  ( ( suc  j  e.  On  ->  -.  A. g  e.  L  A. h  e.  R  ( g  |`  suc  j )  =/=  (
h  |`  suc  j ) )  <->  -.  ( suc  j  e.  On  /\  A. g  e.  L  A. h  e.  R  (
g  |`  suc  j )  =/=  ( h  |`  suc  j ) ) )
6159, 60sylibr 217 . . . . . . . . . . 11  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  suc  j  e.  M
)  ->  ( suc  j  e.  On  ->  -. 
A. g  e.  L  A. h  e.  R  ( g  |`  suc  j
)  =/=  ( h  |`  suc  j ) ) )
6238, 61mpd 15 . . . . . . . . . 10  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  suc  j  e.  M
)  ->  -.  A. g  e.  L  A. h  e.  R  ( g  |` 
suc  j )  =/=  ( h  |`  suc  j
) )
63 df-ne 2643 . . . . . . . . . . . . . . 15  |-  ( ( g  |`  suc  j )  =/=  ( h  |`  suc  j )  <->  -.  (
g  |`  suc  j )  =  ( h  |`  suc  j ) )
6463con2bii 339 . . . . . . . . . . . . . 14  |-  ( ( g  |`  suc  j )  =  ( h  |`  suc  j )  <->  -.  (
g  |`  suc  j )  =/=  ( h  |`  suc  j ) )
6564rexbii 2881 . . . . . . . . . . . . 13  |-  ( E. h  e.  R  ( g  |`  suc  j )  =  ( h  |`  suc  j )  <->  E. h  e.  R  -.  (
g  |`  suc  j )  =/=  ( h  |`  suc  j ) )
66 rexnal 2836 . . . . . . . . . . . . 13  |-  ( E. h  e.  R  -.  ( g  |`  suc  j
)  =/=  ( h  |`  suc  j )  <->  -.  A. h  e.  R  ( g  |` 
suc  j )  =/=  ( h  |`  suc  j
) )
6765, 66bitri 257 . . . . . . . . . . . 12  |-  ( E. h  e.  R  ( g  |`  suc  j )  =  ( h  |`  suc  j )  <->  -.  A. h  e.  R  ( g  |` 
suc  j )  =/=  ( h  |`  suc  j
) )
6867rexbii 2881 . . . . . . . . . . 11  |-  ( E. g  e.  L  E. h  e.  R  (
g  |`  suc  j )  =  ( h  |`  suc  j )  <->  E. g  e.  L  -.  A. h  e.  R  ( g  |` 
suc  j )  =/=  ( h  |`  suc  j
) )
69 rexnal 2836 . . . . . . . . . . 11  |-  ( E. g  e.  L  -.  A. h  e.  R  ( g  |`  suc  j )  =/=  ( h  |`  suc  j )  <->  -.  A. g  e.  L  A. h  e.  R  ( g  |` 
suc  j )  =/=  ( h  |`  suc  j
) )
7068, 69bitri 257 . . . . . . . . . 10  |-  ( E. g  e.  L  E. h  e.  R  (
g  |`  suc  j )  =  ( h  |`  suc  j )  <->  -.  A. g  e.  L  A. h  e.  R  ( g  |` 
suc  j )  =/=  ( h  |`  suc  j
) )
7162, 70sylibr 217 . . . . . . . . 9  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  suc  j  e.  M
)  ->  E. g  e.  L  E. h  e.  R  ( g  |` 
suc  j )  =  ( h  |`  suc  j
) )
72 simp3 1032 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( L  C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W
)  /\  A. x  e.  L  A. y  e.  R  x <s y )  ->  A. x  e.  L  A. y  e.  R  x <s y )
73 breq1 4398 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  g  ->  (
x <s y  <-> 
g <s y ) )
74 breq2 4399 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  h  ->  (
g <s y  <-> 
g <s h ) )
7573, 74rspc2v 3147 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( g  e.  L  /\  h  e.  R )  ->  ( A. x  e.  L  A. y  e.  R  x <s
y  ->  g <s h ) )
7672, 75mpan9 477 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( g  e.  L  /\  h  e.  R
) )  ->  g
<s h )
7776adantrl 730 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  -> 
g <s h )
78 simp1l 1054 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( L  C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W
)  /\  A. x  e.  L  A. y  e.  R  x <s y )  ->  L  C_  No )
79 simprl 772 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) )  ->  g  e.  L )
80 ssel2 3413 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( L  C_  No  /\  g  e.  L )  ->  g  e.  No )
8178, 79, 80syl2an 485 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  -> 
g  e.  No )
82 sltirr 30630 . . . . . . . . . . . . . . . . . . 19  |-  ( g  e.  No  ->  -.  g <s g )
8381, 82syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  ->  -.  g <s g )
84 breq2 4399 . . . . . . . . . . . . . . . . . . . 20  |-  ( g  =  h  ->  (
g <s g  <-> 
g <s h ) )
8584biimprcd 233 . . . . . . . . . . . . . . . . . . 19  |-  ( g <s h  -> 
( g  =  h  ->  g <s
g ) )
8685con3d 140 . . . . . . . . . . . . . . . . . 18  |-  ( g <s h  -> 
( -.  g <s g  ->  -.  g  =  h )
)
8777, 83, 86sylc 61 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  ->  -.  g  =  h
)
8887adantr 472 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( L 
C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  /\  ( g  |`  suc  j
)  =  ( h  |`  suc  j ) )  ->  -.  g  =  h )
89 ioran 498 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( j  e.  dom  g  \/  j  e.  dom  h )  <->  ( -.  j  e.  dom  g  /\  -.  j  e.  dom  h ) )
90 simp2l 1056 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( L  C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W
)  /\  A. x  e.  L  A. y  e.  R  x <s y )  ->  R  C_  No )
91 simprr 774 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) )  ->  h  e.  R )
92 ssel2 3413 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( R  C_  No  /\  h  e.  R )  ->  h  e.  No )
9390, 91, 92syl2an 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  ->  h  e.  No )
9493adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( L 
C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  /\  -.  j  e.  dom  h )  ->  h  e.  No )
95 nofun 30607 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( h  e.  No  ->  Fun  h )
96 funrel 5606 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( Fun  h  ->  Rel  h )
9794, 95, 963syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( L 
C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  /\  -.  j  e.  dom  h )  ->  Rel  h )
9832adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  ->  Ord  M )
99 simprl 772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  ->  suc  j  e.  M
)
100 ordelon 5454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( Ord  M  /\  suc  j  e.  M )  ->  suc  j  e.  On )
10198, 99, 100syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  ->  suc  j  e.  On )
102 sucelon 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( j  e.  On  <->  suc  j  e.  On )
103101, 102sylibr 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  -> 
j  e.  On )
104 eloni 5440 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( j  e.  On  ->  Ord  j )
105103, 104syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  ->  Ord  j )
106 nodmord 30611 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( h  e.  No  ->  Ord  dom  h )
10793, 106syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  ->  Ord  dom  h )
108 ordtri2or 5525 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( Ord  j  /\  Ord  dom  h )  ->  (
j  e.  dom  h  \/  dom  h  C_  j
) )
109105, 107, 108syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  -> 
( j  e.  dom  h  \/  dom  h  C_  j ) )
110109orcanai 927 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( L 
C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  /\  -.  j  e.  dom  h )  ->  dom  h  C_  j )
111 sssucid 5507 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  j  C_  suc  j
112110, 111syl6ss 3430 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( L 
C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  /\  -.  j  e.  dom  h )  ->  dom  h  C_  suc  j )
113 relssres 5148 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( Rel  h  /\  dom  h  C_  suc  j )  ->  ( h  |`  suc  j )  =  h )
11497, 112, 113syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( L 
C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  /\  -.  j  e.  dom  h )  ->  (
h  |`  suc  j )  =  h )
115114ex 441 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  -> 
( -.  j  e. 
dom  h  ->  (
h  |`  suc  j )  =  h ) )
11681adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( L 
C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  /\  -.  j  e.  dom  g )  ->  g  e.  No )
117 nofun 30607 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( g  e.  No  ->  Fun  g )
118 funrel 5606 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( Fun  g  ->  Rel  g )
119116, 117, 1183syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( L 
C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  /\  -.  j  e.  dom  g )  ->  Rel  g )
120 nodmord 30611 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( g  e.  No  ->  Ord  dom  g )
12181, 120syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  ->  Ord  dom  g )
122 ordtri2or 5525 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( Ord  j  /\  Ord  dom  g )  ->  (
j  e.  dom  g  \/  dom  g  C_  j
) )
123105, 121, 122syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  -> 
( j  e.  dom  g  \/  dom  g  C_  j ) )
124123orcanai 927 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( L 
C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  /\  -.  j  e.  dom  g )  ->  dom  g  C_  j )
125124, 111syl6ss 3430 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( L 
C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  /\  -.  j  e.  dom  g )  ->  dom  g  C_  suc  j )
126 relssres 5148 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( Rel  g  /\  dom  g  C_  suc  j )  ->  ( g  |`  suc  j )  =  g )
127119, 125, 126syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( L 
C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  /\  -.  j  e.  dom  g )  ->  (
g  |`  suc  j )  =  g )
128127ex 441 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  -> 
( -.  j  e. 
dom  g  ->  (
g  |`  suc  j )  =  g ) )
129115, 128anim12d 572 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  -> 
( ( -.  j  e.  dom  h  /\  -.  j  e.  dom  g )  ->  ( ( h  |`  suc  j )  =  h  /\  ( g  |`  suc  j )  =  g ) ) )
130129ancomsd 461 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  -> 
( ( -.  j  e.  dom  g  /\  -.  j  e.  dom  h )  ->  ( ( h  |`  suc  j )  =  h  /\  ( g  |`  suc  j )  =  g ) ) )
131 eqeq12 2484 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( g  |`  suc  j
)  =  g  /\  ( h  |`  suc  j
)  =  h )  ->  ( ( g  |`  suc  j )  =  ( h  |`  suc  j
)  <->  g  =  h ) )
132131biimpd 212 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( g  |`  suc  j
)  =  g  /\  ( h  |`  suc  j
)  =  h )  ->  ( ( g  |`  suc  j )  =  ( h  |`  suc  j
)  ->  g  =  h ) )
133132ancoms 460 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( h  |`  suc  j
)  =  h  /\  ( g  |`  suc  j
)  =  g )  ->  ( ( g  |`  suc  j )  =  ( h  |`  suc  j
)  ->  g  =  h ) )
134130, 133syl6 33 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  -> 
( ( -.  j  e.  dom  g  /\  -.  j  e.  dom  h )  ->  ( ( g  |`  suc  j )  =  ( h  |`  suc  j
)  ->  g  =  h ) ) )
135134com23 80 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  -> 
( ( g  |`  suc  j )  =  ( h  |`  suc  j )  ->  ( ( -.  j  e.  dom  g  /\  -.  j  e.  dom  h )  ->  g  =  h ) ) )
136135imp 436 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( L 
C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  /\  ( g  |`  suc  j
)  =  ( h  |`  suc  j ) )  ->  ( ( -.  j  e.  dom  g  /\  -.  j  e.  dom  h )  ->  g  =  h ) )
13789, 136syl5bi 225 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( L 
C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  /\  ( g  |`  suc  j
)  =  ( h  |`  suc  j ) )  ->  ( -.  (
j  e.  dom  g  \/  j  e.  dom  h )  ->  g  =  h ) )
13888, 137mt3d 130 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( L 
C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  /\  ( g  |`  suc  j
)  =  ( h  |`  suc  j ) )  ->  ( j  e. 
dom  g  \/  j  e.  dom  h ) )
139138ex 441 . . . . . . . . . . . . . 14  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  ( suc  j  e.  M  /\  ( g  e.  L  /\  h  e.  R
) ) )  -> 
( ( g  |`  suc  j )  =  ( h  |`  suc  j )  ->  ( j  e. 
dom  g  \/  j  e.  dom  h ) ) )
140139anassrs 660 . . . . . . . . . . . . 13  |-  ( ( ( ( ( L 
C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  suc  j  e.  M
)  /\  ( g  e.  L  /\  h  e.  R ) )  -> 
( ( g  |`  suc  j )  =  ( h  |`  suc  j )  ->  ( j  e. 
dom  g  \/  j  e.  dom  h ) ) )
141140anassrs 660 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( L  C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  suc  j  e.  M
)  /\  g  e.  L )  /\  h  e.  R )  ->  (
( g  |`  suc  j
)  =  ( h  |`  suc  j )  -> 
( j  e.  dom  g  \/  j  e.  dom  h ) ) )
142141ancld 562 . . . . . . . . . . 11  |-  ( ( ( ( ( ( L  C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  suc  j  e.  M
)  /\  g  e.  L )  /\  h  e.  R )  ->  (
( g  |`  suc  j
)  =  ( h  |`  suc  j )  -> 
( ( g  |`  suc  j )  =  ( h  |`  suc  j )  /\  ( j  e. 
dom  g  \/  j  e.  dom  h ) ) ) )
143142reximdva 2858 . . . . . . . . . 10  |-  ( ( ( ( ( L 
C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  suc  j  e.  M
)  /\  g  e.  L )  ->  ( E. h  e.  R  ( g  |`  suc  j
)  =  ( h  |`  suc  j )  ->  E. h  e.  R  ( ( g  |`  suc  j )  =  ( h  |`  suc  j )  /\  ( j  e. 
dom  g  \/  j  e.  dom  h ) ) ) )
144143reximdva 2858 . . . . . . . . 9  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  suc  j  e.  M
)  ->  ( E. g  e.  L  E. h  e.  R  (
g  |`  suc  j )  =  ( h  |`  suc  j )  ->  E. g  e.  L  E. h  e.  R  ( (
g  |`  suc  j )  =  ( h  |`  suc  j )  /\  (
j  e.  dom  g  \/  j  e.  dom  h ) ) ) )
14571, 144mpd 15 . . . . . . . 8  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  suc  j  e.  M
)  ->  E. g  e.  L  E. h  e.  R  ( (
g  |`  suc  j )  =  ( h  |`  suc  j )  /\  (
j  e.  dom  g  \/  j  e.  dom  h ) ) )
146 reseq2 5106 . . . . . . . . . . . . 13  |-  ( a  =  suc  j  -> 
( g  |`  a
)  =  ( g  |`  suc  j ) )
147 reseq2 5106 . . . . . . . . . . . . 13  |-  ( a  =  suc  j  -> 
( h  |`  a
)  =  ( h  |`  suc  j ) )
148146, 147eqeq12d 2486 . . . . . . . . . . . 12  |-  ( a  =  suc  j  -> 
( ( g  |`  a )  =  ( h  |`  a )  <->  ( g  |`  suc  j )  =  ( h  |`  suc  j ) ) )
149 eleq2 2538 . . . . . . . . . . . 12  |-  ( a  =  suc  j  -> 
( j  e.  a  <-> 
j  e.  suc  j
) )
150148, 1493anbi13d 1367 . . . . . . . . . . 11  |-  ( a  =  suc  j  -> 
( ( ( g  |`  a )  =  ( h  |`  a )  /\  ( j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a )  <->  ( (
g  |`  suc  j )  =  ( h  |`  suc  j )  /\  (
j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  suc  j ) ) )
151 vex 3034 . . . . . . . . . . . . 13  |-  j  e. 
_V
152151sucid 5509 . . . . . . . . . . . 12  |-  j  e. 
suc  j
153 df-3an 1009 . . . . . . . . . . . 12  |-  ( ( ( g  |`  suc  j
)  =  ( h  |`  suc  j )  /\  ( j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  suc  j )  <->  ( (
( g  |`  suc  j
)  =  ( h  |`  suc  j )  /\  ( j  e.  dom  g  \/  j  e.  dom  h ) )  /\  j  e.  suc  j ) )
154152, 153mpbiran2 933 . . . . . . . . . . 11  |-  ( ( ( g  |`  suc  j
)  =  ( h  |`  suc  j )  /\  ( j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  suc  j )  <->  ( (
g  |`  suc  j )  =  ( h  |`  suc  j )  /\  (
j  e.  dom  g  \/  j  e.  dom  h ) ) )
155150, 154syl6bb 269 . . . . . . . . . 10  |-  ( a  =  suc  j  -> 
( ( ( g  |`  a )  =  ( h  |`  a )  /\  ( j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a )  <->  ( (
g  |`  suc  j )  =  ( h  |`  suc  j )  /\  (
j  e.  dom  g  \/  j  e.  dom  h ) ) ) )
1561552rexbidv 2897 . . . . . . . . 9  |-  ( a  =  suc  j  -> 
( E. g  e.  L  E. h  e.  R  ( ( g  |`  a )  =  ( h  |`  a )  /\  ( j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a )  <->  E. g  e.  L  E. h  e.  R  ( (
g  |`  suc  j )  =  ( h  |`  suc  j )  /\  (
j  e.  dom  g  \/  j  e.  dom  h ) ) ) )
157156rspcev 3136 . . . . . . . 8  |-  ( ( suc  j  e.  M  /\  E. g  e.  L  E. h  e.  R  ( ( g  |`  suc  j )  =  ( h  |`  suc  j )  /\  ( j  e. 
dom  g  \/  j  e.  dom  h ) ) )  ->  E. a  e.  M  E. g  e.  L  E. h  e.  R  ( (
g  |`  a )  =  ( h  |`  a
)  /\  ( j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a )
)
15835, 145, 157syl2anc 673 . . . . . . 7  |-  ( ( ( ( L  C_  No  /\  L  e.  V
)  /\  ( R  C_  No  /\  R  e.  W )  /\  A. x  e.  L  A. y  e.  R  x <s y )  /\  suc  j  e.  M
)  ->  E. a  e.  M  E. g  e.  L  E. h  e.  R  ( (
g  |`  a )  =  ( h  |`  a
)  /\  ( j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a )
)
159158ex 441 . . . . . 6  |-  ( ( ( L  C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W
)  /\  A. x  e.  L  A. y  e.  R  x <s y )  ->  ( suc  j  e.  M  ->  E. a  e.  M  E. g  e.  L  E. h  e.  R  ( ( g  |`  a )  =  ( h  |`  a )  /\  ( j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a ) ) )
16034, 159sylbid 223 . . . . 5  |-  ( ( ( L  C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W
)  /\  A. x  e.  L  A. y  e.  R  x <s y )  ->  (
j  e.  U. M  ->  E. a  e.  M  E. g  e.  L  E. h  e.  R  ( ( g  |`  a )  =  ( h  |`  a )  /\  ( j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a ) ) )
161 eliun 4274 . . . . . 6  |-  ( j  e.  U_ b  e.  S  dom  b  <->  E. b  e.  S  j  e.  dom  b )
16212rexeqi 2978 . . . . . 6  |-  ( E. b  e.  S  j  e.  dom  b  <->  E. b  e.  { f  |  E. g  e.  L  E. h  e.  R  E. a  e.  M  (
( g  |`  a
)  =  f  /\  ( h  |`  a )  =  f ) } j  e.  dom  b
)
163 r19.41vv 2930 . . . . . . . . . 10  |-  ( E. h  e.  R  E. a  e.  M  (
( ( g  |`  a )  =  b  /\  ( h  |`  a )  =  b )  /\  j  e. 
dom  b )  <->  ( E. h  e.  R  E. a  e.  M  (
( g  |`  a
)  =  b  /\  ( h  |`  a )  =  b )  /\  j  e.  dom  b ) )
164163rexbii 2881 . . . . . . . . 9  |-  ( E. g  e.  L  E. h  e.  R  E. a  e.  M  (
( ( g  |`  a )  =  b  /\  ( h  |`  a )  =  b )  /\  j  e. 
dom  b )  <->  E. g  e.  L  ( E. h  e.  R  E. a  e.  M  (
( g  |`  a
)  =  b  /\  ( h  |`  a )  =  b )  /\  j  e.  dom  b ) )
165 r19.41v 2928 . . . . . . . . 9  |-  ( E. g  e.  L  ( E. h  e.  R  E. a  e.  M  ( ( g  |`  a )  =  b  /\  ( h  |`  a )  =  b )  /\  j  e. 
dom  b )  <->  ( E. g  e.  L  E. h  e.  R  E. a  e.  M  (
( g  |`  a
)  =  b  /\  ( h  |`  a )  =  b )  /\  j  e.  dom  b ) )
166164, 165bitri 257 . . . . . . . 8  |-  ( E. g  e.  L  E. h  e.  R  E. a  e.  M  (
( ( g  |`  a )  =  b  /\  ( h  |`  a )  =  b )  /\  j  e. 
dom  b )  <->  ( E. g  e.  L  E. h  e.  R  E. a  e.  M  (
( g  |`  a
)  =  b  /\  ( h  |`  a )  =  b )  /\  j  e.  dom  b ) )
167166exbii 1726 . . . . . . 7  |-  ( E. b E. g  e.  L  E. h  e.  R  E. a  e.  M  ( ( ( g  |`  a )  =  b  /\  (
h  |`  a )  =  b )  /\  j  e.  dom  b )  <->  E. b
( E. g  e.  L  E. h  e.  R  E. a  e.  M  ( ( g  |`  a )  =  b  /\  ( h  |`  a )  =  b )  /\  j  e. 
dom  b ) )
168 rexcom 2938 . . . . . . . . 9  |-  ( E. a  e.  M  E. g  e.  L  E. h  e.  R  (
( g  |`  a
)  =  ( h  |`  a )  /\  (
j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a )  <->  E. g  e.  L  E. a  e.  M  E. h  e.  R  ( (
g  |`  a )  =  ( h  |`  a
)  /\  ( j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a )
)
169 rexcom 2938 . . . . . . . . . 10  |-  ( E. a  e.  M  E. h  e.  R  (
( g  |`  a
)  =  ( h  |`  a )  /\  (
j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a )  <->  E. h  e.  R  E. a  e.  M  ( (
g  |`  a )  =  ( h  |`  a
)  /\  ( j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a )
)
170169rexbii 2881 . . . . . . . . 9  |-  ( E. g  e.  L  E. a  e.  M  E. h  e.  R  (
( g  |`  a
)  =  ( h  |`  a )  /\  (
j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a )  <->  E. g  e.  L  E. h  e.  R  E. a  e.  M  ( (
g  |`  a )  =  ( h  |`  a
)  /\  ( j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a )
)
171168, 170bitri 257 . . . . . . . 8  |-  ( E. a  e.  M  E. g  e.  L  E. h  e.  R  (
( g  |`  a
)  =  ( h  |`  a )  /\  (
j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a )  <->  E. g  e.  L  E. h  e.  R  E. a  e.  M  ( (
g  |`  a )  =  ( h  |`  a
)  /\  ( j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a )
)
172 vex 3034 . . . . . . . . . . . . . . . 16  |-  h  e. 
_V
173172resex 5154 . . . . . . . . . . . . . . 15  |-  ( h  |`  a )  e.  _V
174 eqeq2 2482 . . . . . . . . . . . . . . . 16  |-  ( b  =  ( h  |`  a )  ->  (
( g  |`  a
)  =  b  <->  ( g  |`  a )  =  ( h  |`  a )
) )
175 dmeq 5040 . . . . . . . . . . . . . . . . 17  |-  ( b  =  ( h  |`  a )  ->  dom  b  =  dom  ( h  |`  a ) )
176175eleq2d 2534 . . . . . . . . . . . . . . . 16  |-  ( b  =  ( h  |`  a )  ->  (
j  e.  dom  b  <->  j  e.  dom  ( h  |`  a ) ) )
177174, 176anbi12d 725 . . . . . . . . . . . . . . 15  |-  ( b  =  ( h  |`  a )  ->  (
( ( g  |`  a )  =  b  /\  j  e.  dom  b )  <->  ( (
g  |`  a )  =  ( h  |`  a
)  /\  j  e.  dom  ( h  |`  a
) ) ) )
178173, 177ceqsexv 3070 . . . . . . . . . . . . . 14  |-  ( E. b ( b  =  ( h  |`  a
)  /\  ( (
g  |`  a )  =  b  /\  j  e. 
dom  b ) )  <-> 
( ( g  |`  a )  =  ( h  |`  a )  /\  j  e.  dom  ( h  |`  a ) ) )
179 an12 814 . . . . . . . . . . . . . . . 16  |-  ( ( ( h  |`  a
)  =  b  /\  ( ( g  |`  a )  =  b  /\  j  e.  dom  b ) )  <->  ( (
g  |`  a )  =  b  /\  ( ( h  |`  a )  =  b  /\  j  e.  dom  b ) ) )
180 eqcom 2478 . . . . . . . . . . . . . . . . 17  |-  ( b  =  ( h  |`  a )  <->  ( h  |`  a )  =  b )
181180anbi1i 709 . . . . . . . . . . . . . . . 16  |-  ( ( b  =  ( h  |`  a )  /\  (
( g  |`  a
)  =  b  /\  j  e.  dom  b ) )  <->  ( ( h  |`  a )  =  b  /\  ( ( g  |`  a )  =  b  /\  j  e.  dom  b ) ) )
182 anass 661 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( g  |`  a )  =  b  /\  ( h  |`  a )  =  b )  /\  j  e. 
dom  b )  <->  ( (
g  |`  a )  =  b  /\  ( ( h  |`  a )  =  b  /\  j  e.  dom  b ) ) )
183179, 181, 1823bitr4i 285 . . . . . . . . . . . . . . 15  |-  ( ( b  =  ( h  |`  a )  /\  (
( g  |`  a
)  =  b  /\  j  e.  dom  b ) )  <->  ( ( ( g  |`  a )  =  b  /\  (
h  |`  a )  =  b )  /\  j  e.  dom  b ) )
184183exbii 1726 . . . . . . . . . . . . . 14  |-  ( E. b ( b  =  ( h  |`  a
)  /\  ( (
g  |`  a )  =  b  /\  j  e. 
dom  b ) )  <->  E. b ( ( ( g  |`  a )  =  b  /\  (
h  |`  a )  =  b )  /\  j  e.  dom  b ) )
185 dmeq 5040 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( g  |`  a )  =  ( h  |`  a )  ->  dom  ( g  |`  a
)  =  dom  (
h  |`  a ) )
186185eleq2d 2534 . . . . . . . . . . . . . . . . . . 19  |-  ( ( g  |`  a )  =  ( h  |`  a )  ->  (
j  e.  dom  (
g  |`  a )  <->  j  e.  dom  ( h  |`  a
) ) )
187186orbi1d 717 . . . . . . . . . . . . . . . . . 18  |-  ( ( g  |`  a )  =  ( h  |`  a )  ->  (
( j  e.  dom  ( g  |`  a
)  \/  j  e. 
dom  ( h  |`  a ) )  <->  ( j  e.  dom  ( h  |`  a )  \/  j  e.  dom  ( h  |`  a ) ) ) )
188 oridm 523 . . . . . . . . . . . . . . . . . 18  |-  ( ( j  e.  dom  (
h  |`  a )  \/  j  e.  dom  (
h  |`  a ) )  <-> 
j  e.  dom  (
h  |`  a ) )
189187, 188syl6rbb 270 . . . . . . . . . . . . . . . . 17  |-  ( ( g  |`  a )  =  ( h  |`  a )  ->  (
j  e.  dom  (
h  |`  a )  <->  ( j  e.  dom  ( g  |`  a )  \/  j  e.  dom  ( h  |`  a ) ) ) )
190 incom 3616 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  i^i  dom  g )  =  ( dom  g  i^i  a )
19117, 190eqtri 2493 . . . . . . . . . . . . . . . . . . . 20  |-  dom  (
g  |`  a )  =  ( dom  g  i^i  a )
192191elin2 3612 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  dom  ( g  |`  a )  <->  ( j  e.  dom  g  /\  j  e.  a ) )
193 dmres 5131 . . . . . . . . . . . . . . . . . . . . 21  |-  dom  (
h  |`  a )  =  ( a  i^i  dom  h )
194 incom 3616 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  i^i  dom  h )  =  ( dom  h  i^i  a )
195193, 194eqtri 2493 . . . . . . . . . . . . . . . . . . . 20  |-  dom  (
h  |`  a )  =  ( dom  h  i^i  a )
196195elin2 3612 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  dom  ( h  |`  a )  <->  ( j  e.  dom  h  /\  j  e.  a ) )
197192, 196orbi12i 530 . . . . . . . . . . . . . . . . . 18  |-  ( ( j  e.  dom  (
g  |`  a )  \/  j  e.  dom  (
h  |`  a ) )  <-> 
( ( j  e. 
dom  g  /\  j  e.  a )  \/  (
j  e.  dom  h  /\  j  e.  a
) ) )
198 andir 885 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a )  <->  ( (
j  e.  dom  g  /\  j  e.  a
)  \/  ( j  e.  dom  h  /\  j  e.  a )
) )
199197, 198bitr4i 260 . . . . . . . . . . . . . . . . 17  |-  ( ( j  e.  dom  (
g  |`  a )  \/  j  e.  dom  (
h  |`  a ) )  <-> 
( ( j  e. 
dom  g  \/  j  e.  dom  h )  /\  j  e.  a )
)
200189, 199syl6bb 269 . . . . . . . . . . . . . . . 16  |-  ( ( g  |`  a )  =  ( h  |`  a )  ->  (
j  e.  dom  (
h  |`  a )  <->  ( (
j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a ) ) )
201200pm5.32i 649 . . . . . . . . . . . . . . 15  |-  ( ( ( g  |`  a
)  =  ( h  |`  a )  /\  j  e.  dom  ( h  |`  a ) )  <->  ( (
g  |`  a )  =  ( h  |`  a
)  /\  ( (
j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a ) ) )
202 3anass 1011 . . . . . . . . . . . . . . 15  |-  ( ( ( g  |`  a
)  =  ( h  |`  a )  /\  (
j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a )  <->  ( (
g  |`  a )  =  ( h  |`  a
)  /\  ( (
j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a ) ) )
203201, 202bitr4i 260 . . . . . . . . . . . . . 14  |-  ( ( ( g  |`  a
)  =  ( h  |`  a )  /\  j  e.  dom  ( h  |`  a ) )  <->  ( (
g  |`  a )  =  ( h  |`  a
)  /\  ( j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a )
)
204178, 184, 2033bitr3ri 284 . . . . . . . . . . . . 13  |-  ( ( ( g  |`  a
)  =  ( h  |`  a )  /\  (
j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a )  <->  E. b
( ( ( g  |`  a )  =  b  /\  ( h  |`  a )  =  b )  /\  j  e. 
dom  b ) )
205204rexbii 2881 . . . . . . . . . . . 12  |-  ( E. a  e.  M  ( ( g  |`  a
)  =  ( h  |`  a )  /\  (
j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a )  <->  E. a  e.  M  E. b
( ( ( g  |`  a )  =  b  /\  ( h  |`  a )  =  b )  /\  j  e. 
dom  b ) )
206 rexcom4 3053 . . . . . . . . . . . 12  |-  ( E. a  e.  M  E. b ( ( ( g  |`  a )  =  b  /\  (
h  |`  a )  =  b )  /\  j  e.  dom  b )  <->  E. b E. a  e.  M  ( ( ( g  |`  a )  =  b  /\  ( h  |`  a )  =  b )  /\  j  e. 
dom  b ) )
207205, 206bitri 257 . . . . . . . . . . 11  |-  ( E. a  e.  M  ( ( g  |`  a
)  =  ( h  |`  a )  /\  (
j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a )  <->  E. b E. a  e.  M  ( ( ( g  |`  a )  =  b  /\  ( h  |`  a )  =  b )  /\  j  e. 
dom  b ) )
208207rexbii 2881 . . . . . . . . . 10  |-  ( E. h  e.  R  E. a  e.  M  (
( g  |`  a
)  =  ( h  |`  a )  /\  (
j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a )  <->  E. h  e.  R  E. b E. a  e.  M  ( ( ( g  |`  a )  =  b  /\  ( h  |`  a )  =  b )  /\  j  e. 
dom  b ) )
209 rexcom4 3053 . . . . . . . . . 10  |-  ( E. h  e.  R  E. b E. a  e.  M  ( ( ( g  |`  a )  =  b  /\  ( h  |`  a )  =  b )  /\  j  e. 
dom  b )  <->  E. b E. h  e.  R  E. a  e.  M  ( ( ( g  |`  a )  =  b  /\  ( h  |`  a )  =  b )  /\  j  e. 
dom  b ) )
210208, 209bitri 257 . . . . . . . . 9  |-  ( E. h  e.  R  E. a  e.  M  (
( g  |`  a
)  =  ( h  |`  a )  /\  (
j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a )  <->  E. b E. h  e.  R  E. a  e.  M  ( ( ( g  |`  a )  =  b  /\  ( h  |`  a )  =  b )  /\  j  e. 
dom  b ) )
211210rexbii 2881 . . . . . . . 8  |-  ( E. g  e.  L  E. h  e.  R  E. a  e.  M  (
( g  |`  a
)  =  ( h  |`  a )  /\  (
j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a )  <->  E. g  e.  L  E. b E. h  e.  R  E. a  e.  M  ( ( ( g  |`  a )  =  b  /\  ( h  |`  a )  =  b )  /\  j  e. 
dom  b ) )
212 rexcom4 3053 . . . . . . . 8  |-  ( E. g  e.  L  E. b E. h  e.  R  E. a  e.  M  ( ( ( g  |`  a )  =  b  /\  ( h  |`  a )  =  b )  /\  j  e. 
dom  b )  <->  E. b E. g  e.  L  E. h  e.  R  E. a  e.  M  ( ( ( g  |`  a )  =  b  /\  ( h  |`  a )  =  b )  /\  j  e. 
dom  b ) )
213171, 211, 2123bitri 279 . . . . . . 7  |-  ( E. a  e.  M  E. g  e.  L  E. h  e.  R  (
( g  |`  a
)  =  ( h  |`  a )  /\  (
j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a )  <->  E. b E. g  e.  L  E. h  e.  R  E. a  e.  M  ( ( ( g  |`  a )  =  b  /\  ( h  |`  a )  =  b )  /\  j  e. 
dom  b ) )
21411rexab 3189 . . . . . . 7  |-  ( E. b  e.  { f  |  E. g  e.  L  E. h  e.  R  E. a  e.  M  ( ( g  |`  a )  =  f  /\  ( h  |`  a )  =  f ) } j  e. 
dom  b  <->  E. b
( E. g  e.  L  E. h  e.  R  E. a  e.  M  ( ( g  |`  a )  =  b  /\  ( h  |`  a )  =  b )  /\  j  e. 
dom  b ) )
215167, 213, 2143bitr4ri 286 . . . . . 6  |-  ( E. b  e.  { f  |  E. g  e.  L  E. h  e.  R  E. a  e.  M  ( ( g  |`  a )  =  f  /\  ( h  |`  a )  =  f ) } j  e. 
dom  b  <->  E. a  e.  M  E. g  e.  L  E. h  e.  R  ( (
g  |`  a )  =  ( h  |`  a
)  /\  ( j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a )
)
216161, 162, 2153bitri 279 . . . . 5  |-  ( j  e.  U_ b  e.  S  dom  b  <->  E. a  e.  M  E. g  e.  L  E. h  e.  R  ( (
g  |`  a )  =  ( h  |`  a
)  /\  ( j  e.  dom  g  \/  j  e.  dom  h )  /\  j  e.  a )
)
217160, 216syl6ibr 235 . . . 4  |-  ( ( ( L  C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W
)  /\  A. x  e.  L  A. y  e.  R  x <s y )  ->  (
j  e.  U. M  ->  j  e.  U_ b  e.  S  dom  b ) )
218217ssrdv 3424 . . 3  |-  ( ( ( L  C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W
)  /\  A. x  e.  L  A. y  e.  R  x <s y )  ->  U. M  C_ 
U_ b  e.  S  dom  b )
21928, 218eqssd 3435 . 2  |-  ( ( ( L  C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W
)  /\  A. x  e.  L  A. y  e.  R  x <s y )  ->  U_ b  e.  S  dom  b  = 
U. M )
2204, 219syl5eq 2517 1  |-  ( ( ( L  C_  No  /\  L  e.  V )  /\  ( R  C_  No  /\  R  e.  W
)  /\  A. x  e.  L  A. y  e.  R  x <s y )  ->  dom  X  =  U. M )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    \/ wo 375    /\ wa 376    /\ w3a 1007    = wceq 1452   E.wex 1671    e. wcel 1904   {cab 2457    =/= wne 2641   A.wral 2756   E.wrex 2757   {crab 2760    i^i cin 3389    C_ wss 3390   U.cuni 4190   |^|cint 4226   U_ciun 4269   class class class wbr 4395   dom cdm 4839    |` cres 4841   Rel wrel 4844   Ord word 5429   Oncon0 5430   suc csuc 5432   Fun wfun 5583   Nocsur 30598   <scslt 30599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-reu 2763  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-ord 5433  df-on 5434  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-1o 7200  df-2o 7201  df-no 30601  df-slt 30602  df-bday 30603
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator