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

Theorem cfsmolem 8043
Description: Lemma for cfsmo 8044. (Contributed by Mario Carneiro, 28-Feb-2013.)
Hypotheses
Ref Expression
cfsmolem.2  |-  F  =  ( z  e.  _V  |->  ( ( g `  dom  z )  u.  U_ t  e.  dom  z  suc  ( z `  t
) ) )
cfsmolem.3  |-  G  =  (recs ( F )  |`  ( cf `  A
) )
Assertion
Ref Expression
cfsmolem  |-  ( A  e.  On  ->  E. f
( f : ( cf `  A ) --> A  /\  Smo  f  /\  A. z  e.  A  E. w  e.  ( cf `  A ) z 
C_  ( f `  w ) ) )
Distinct variable groups:    f, g,
t, w, z, A   
f, F, t, z   
f, G, w, z
Allowed substitution hints:    F( w, g)    G( t, g)

Proof of Theorem cfsmolem
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cff1 8031 . 2  |-  ( A  e.  On  ->  E. g
( g : ( cf `  A )
-1-1-> A  /\  A. z  e.  A  E. w  e.  ( cf `  A
) z  C_  (
g `  w )
) )
2 cfon 8028 . . . . . . . . . . . 12  |-  ( cf `  A )  e.  On
32oneli 4603 . . . . . . . . . . 11  |-  ( x  e.  ( cf `  A
)  ->  x  e.  On )
433ad2ant3 979 . . . . . . . . . 10  |-  ( ( g : ( cf `  A ) -1-1-> A  /\  A  e.  On  /\  x  e.  ( cf `  A
) )  ->  x  e.  On )
5 eleq1 2426 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  (
x  e.  ( cf `  A )  <->  y  e.  ( cf `  A ) ) )
653anbi3d 1259 . . . . . . . . . . . 12  |-  ( x  =  y  ->  (
( g : ( cf `  A )
-1-1-> A  /\  A  e.  On  /\  x  e.  ( cf `  A
) )  <->  ( g : ( cf `  A
) -1-1-> A  /\  A  e.  On  /\  y  e.  ( cf `  A
) ) ) )
7 fveq2 5632 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  ( G `  x )  =  ( G `  y ) )
87eleq1d 2432 . . . . . . . . . . . 12  |-  ( x  =  y  ->  (
( G `  x
)  e.  A  <->  ( G `  y )  e.  A
) )
96, 8imbi12d 311 . . . . . . . . . . 11  |-  ( x  =  y  ->  (
( ( g : ( cf `  A
) -1-1-> A  /\  A  e.  On  /\  x  e.  ( cf `  A
) )  ->  ( G `  x )  e.  A )  <->  ( (
g : ( cf `  A ) -1-1-> A  /\  A  e.  On  /\  y  e.  ( cf `  A
) )  ->  ( G `  y )  e.  A ) ) )
10 simpl1 959 . . . . . . . . . . . . . . . 16  |-  ( ( ( g : ( cf `  A )
-1-1-> A  /\  A  e.  On  /\  x  e.  ( cf `  A
) )  /\  y  e.  x )  ->  g : ( cf `  A
) -1-1-> A )
11 simpl2 960 . . . . . . . . . . . . . . . 16  |-  ( ( ( g : ( cf `  A )
-1-1-> A  /\  A  e.  On  /\  x  e.  ( cf `  A
) )  /\  y  e.  x )  ->  A  e.  On )
12 ontr1 4541 . . . . . . . . . . . . . . . . . . 19  |-  ( ( cf `  A )  e.  On  ->  (
( y  e.  x  /\  x  e.  ( cf `  A ) )  ->  y  e.  ( cf `  A ) ) )
132, 12ax-mp 8 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  x  /\  x  e.  ( cf `  A ) )  -> 
y  e.  ( cf `  A ) )
1413ancoms 439 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  ( cf `  A )  /\  y  e.  x )  ->  y  e.  ( cf `  A
) )
15143ad2antl3 1120 . . . . . . . . . . . . . . . 16  |-  ( ( ( g : ( cf `  A )
-1-1-> A  /\  A  e.  On  /\  x  e.  ( cf `  A
) )  /\  y  e.  x )  ->  y  e.  ( cf `  A
) )
16 pm2.27 35 . . . . . . . . . . . . . . . 16  |-  ( ( g : ( cf `  A ) -1-1-> A  /\  A  e.  On  /\  y  e.  ( cf `  A
) )  ->  (
( ( g : ( cf `  A
) -1-1-> A  /\  A  e.  On  /\  y  e.  ( cf `  A
) )  ->  ( G `  y )  e.  A )  ->  ( G `  y )  e.  A ) )
1710, 11, 15, 16syl3anc 1183 . . . . . . . . . . . . . . 15  |-  ( ( ( g : ( cf `  A )
-1-1-> A  /\  A  e.  On  /\  x  e.  ( cf `  A
) )  /\  y  e.  x )  ->  (
( ( g : ( cf `  A
) -1-1-> A  /\  A  e.  On  /\  y  e.  ( cf `  A
) )  ->  ( G `  y )  e.  A )  ->  ( G `  y )  e.  A ) )
1817ralimdva 2706 . . . . . . . . . . . . . 14  |-  ( ( g : ( cf `  A ) -1-1-> A  /\  A  e.  On  /\  x  e.  ( cf `  A
) )  ->  ( A. y  e.  x  ( ( g : ( cf `  A
) -1-1-> A  /\  A  e.  On  /\  y  e.  ( cf `  A
) )  ->  ( G `  y )  e.  A )  ->  A. y  e.  x  ( G `  y )  e.  A
) )
19 cfsmolem.3 . . . . . . . . . . . . . . . . . . . . 21  |-  G  =  (recs ( F )  |`  ( cf `  A
) )
2019fveq1i 5633 . . . . . . . . . . . . . . . . . . . 20  |-  ( G `
 x )  =  ( (recs ( F )  |`  ( cf `  A ) ) `  x )
21 fvres 5649 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( cf `  A
)  ->  ( (recs ( F )  |`  ( cf `  A ) ) `
 x )  =  (recs ( F ) `
 x ) )
2220, 21syl5eq 2410 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( cf `  A
)  ->  ( G `  x )  =  (recs ( F ) `  x ) )
23 recsval 6559 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  On  ->  (recs ( F ) `  x
)  =  ( F `
 (recs ( F )  |`  x )
) )
24 recsfnon 6558 . . . . . . . . . . . . . . . . . . . . . . . . 25  |- recs ( F )  Fn  On
25 fnfun 5446 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  (recs ( F )  Fn  On  ->  Fun recs ( F ) )
2624, 25ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  Fun recs ( F )
27 vex 2876 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  x  e. 
_V
28 resfunexg 5857 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( Fun recs ( F )  /\  x  e.  _V )  ->  (recs ( F )  |`  x )  e.  _V )
2926, 27, 28mp2an 653 . . . . . . . . . . . . . . . . . . . . . . 23  |-  (recs ( F )  |`  x
)  e.  _V
30 dmeq 4982 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  =  (recs ( F )  |`  x )  ->  dom  z  =  dom  (recs ( F )  |`  x ) )
3130fveq2d 5636 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  =  (recs ( F )  |`  x )  ->  ( g `  dom  z )  =  ( g `  dom  (recs ( F )  |`  x
) ) )
32 fveq1 5631 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  =  (recs ( F )  |`  x )  ->  ( z `  t
)  =  ( (recs ( F )  |`  x ) `  t
) )
33 suceq 4560 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( z `  t )  =  ( (recs ( F )  |`  x
) `  t )  ->  suc  ( z `  t )  =  suc  ( (recs ( F )  |`  x ) `  t
) )
3432, 33syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  =  (recs ( F )  |`  x )  ->  suc  ( z `  t )  =  suc  ( (recs ( F )  |`  x ) `  t
) )
3530, 34iuneq12d 4031 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  =  (recs ( F )  |`  x )  ->  U_ t  e.  dom  z  suc  ( z `  t )  =  U_ t  e.  dom  (recs ( F )  |`  x
) suc  ( (recs ( F )  |`  x
) `  t )
)
3631, 35uneq12d 3418 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( z  =  (recs ( F )  |`  x )  ->  ( ( g `  dom  z )  u.  U_ t  e.  dom  z  suc  ( z `  t
) )  =  ( ( g `  dom  (recs ( F )  |`  x ) )  u. 
U_ t  e.  dom  (recs ( F )  |`  x ) suc  (
(recs ( F )  |`  x ) `  t
) ) )
37 cfsmolem.2 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F  =  ( z  e.  _V  |->  ( ( g `  dom  z )  u.  U_ t  e.  dom  z  suc  ( z `  t
) ) )
38 fvex 5646 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( g `
 dom  (recs ( F )  |`  x
) )  e.  _V
3929dmex 5044 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  dom  (recs ( F )  |`  x
)  e.  _V
40 fvex 5646 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (recs ( F )  |`  x ) `  t
)  e.  _V
4140sucex 4705 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  suc  (
(recs ( F )  |`  x ) `  t
)  e.  _V
4239, 41iunex 5891 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  U_ t  e.  dom  (recs ( F )  |`  x ) suc  ( (recs ( F )  |`  x ) `  t )  e.  _V
4338, 42unex 4621 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( g `  dom  (recs ( F )  |`  x
) )  u.  U_ t  e.  dom  (recs ( F )  |`  x
) suc  ( (recs ( F )  |`  x
) `  t )
)  e.  _V
4436, 37, 43fvmpt 5709 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (recs ( F )  |`  x )  e.  _V  ->  ( F `  (recs ( F )  |`  x
) )  =  ( ( g `  dom  (recs ( F )  |`  x ) )  u. 
U_ t  e.  dom  (recs ( F )  |`  x ) suc  (
(recs ( F )  |`  x ) `  t
) ) )
4529, 44ax-mp 8 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F `
 (recs ( F )  |`  x )
)  =  ( ( g `  dom  (recs ( F )  |`  x
) )  u.  U_ t  e.  dom  (recs ( F )  |`  x
) suc  ( (recs ( F )  |`  x
) `  t )
)
4623, 45syl6eq 2414 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  On  ->  (recs ( F ) `  x
)  =  ( ( g `  dom  (recs ( F )  |`  x
) )  u.  U_ t  e.  dom  (recs ( F )  |`  x
) suc  ( (recs ( F )  |`  x
) `  t )
) )
47 onss 4685 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  e.  On  ->  x  C_  On )
48 fnssres 5462 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (recs ( F )  Fn  On  /\  x  C_  On )  ->  (recs ( F )  |`  x
)  Fn  x )
4924, 47, 48sylancr 644 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  On  ->  (recs ( F )  |`  x
)  Fn  x )
50 fndm 5448 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (recs ( F )  |`  x )  Fn  x  ->  dom  (recs ( F )  |`  x )  =  x )
51 fveq2 5632 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( dom  (recs ( F )  |`  x )  =  x  ->  ( g `  dom  (recs ( F )  |`  x ) )  =  ( g `  x
) )
52 iuneq1 4020 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( dom  (recs ( F )  |`  x )  =  x  ->  U_ t  e.  dom  (recs ( F )  |`  x ) suc  (
(recs ( F )  |`  x ) `  t
)  =  U_ t  e.  x  suc  ( (recs ( F )  |`  x ) `  t
) )
53 fvres 5649 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  e.  x  ->  (
(recs ( F )  |`  x ) `  t
)  =  (recs ( F ) `  t
) )
54 suceq 4560 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( (recs ( F )  |`  x ) `  t
)  =  (recs ( F ) `  t
)  ->  suc  ( (recs ( F )  |`  x ) `  t
)  =  suc  (recs ( F ) `  t
) )
5553, 54syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( t  e.  x  ->  suc  ( (recs ( F )  |`  x ) `  t
)  =  suc  (recs ( F ) `  t
) )
5655iuneq2i 4025 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  U_ t  e.  x  suc  ( (recs ( F )  |`  x ) `  t
)  =  U_ t  e.  x  suc  (recs ( F ) `  t
)
57 fveq2 5632 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  =  t  ->  (recs ( F ) `  y
)  =  (recs ( F ) `  t
) )
58 suceq 4560 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (recs ( F ) `  y )  =  (recs ( F ) `  t )  ->  suc  (recs ( F ) `  y )  =  suc  (recs ( F ) `  t ) )
5957, 58syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  t  ->  suc  (recs ( F ) `  y )  =  suc  (recs ( F ) `  t ) )
6059cbviunv 4043 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  U_ y  e.  x  suc  (recs ( F ) `  y
)  =  U_ t  e.  x  suc  (recs ( F ) `  t
)
6156, 60eqtr4i 2389 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  U_ t  e.  x  suc  ( (recs ( F )  |`  x ) `  t
)  =  U_ y  e.  x  suc  (recs ( F ) `  y
)
6252, 61syl6eq 2414 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( dom  (recs ( F )  |`  x )  =  x  ->  U_ t  e.  dom  (recs ( F )  |`  x ) suc  (
(recs ( F )  |`  x ) `  t
)  =  U_ y  e.  x  suc  (recs ( F ) `  y
) )
6351, 62uneq12d 3418 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( dom  (recs ( F )  |`  x )  =  x  ->  ( ( g `
 dom  (recs ( F )  |`  x
) )  u.  U_ t  e.  dom  (recs ( F )  |`  x
) suc  ( (recs ( F )  |`  x
) `  t )
)  =  ( ( g `  x )  u.  U_ y  e.  x  suc  (recs ( F ) `  y
) ) )
6449, 50, 633syl 18 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  On  ->  (
( g `  dom  (recs ( F )  |`  x ) )  u. 
U_ t  e.  dom  (recs ( F )  |`  x ) suc  (
(recs ( F )  |`  x ) `  t
) )  =  ( ( g `  x
)  u.  U_ y  e.  x  suc  (recs ( F ) `  y
) ) )
6546, 64eqtrd 2398 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  On  ->  (recs ( F ) `  x
)  =  ( ( g `  x )  u.  U_ y  e.  x  suc  (recs ( F ) `  y
) ) )
663, 65syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( cf `  A
)  ->  (recs ( F ) `  x
)  =  ( ( g `  x )  u.  U_ y  e.  x  suc  (recs ( F ) `  y
) ) )
6722, 66eqtrd 2398 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( cf `  A
)  ->  ( G `  x )  =  ( ( g `  x
)  u.  U_ y  e.  x  suc  (recs ( F ) `  y
) ) )
68673ad2ant2 978 . . . . . . . . . . . . . . . . 17  |-  ( ( ( g : ( cf `  A )
-1-1-> A  /\  A  e.  On )  /\  x  e.  ( cf `  A
)  /\  A. y  e.  x  ( G `  y )  e.  A
)  ->  ( G `  x )  =  ( ( g `  x
)  u.  U_ y  e.  x  suc  (recs ( F ) `  y
) ) )
69 eloni 4505 . . . . . . . . . . . . . . . . . . . 20  |-  ( A  e.  On  ->  Ord  A )
7069adantl 452 . . . . . . . . . . . . . . . . . . 19  |-  ( ( g : ( cf `  A ) -1-1-> A  /\  A  e.  On )  ->  Ord  A )
71703ad2ant1 977 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( g : ( cf `  A )
-1-1-> A  /\  A  e.  On )  /\  x  e.  ( cf `  A
)  /\  A. y  e.  x  ( G `  y )  e.  A
)  ->  Ord  A )
72 f1f 5543 . . . . . . . . . . . . . . . . . . . . 21  |-  ( g : ( cf `  A
) -1-1-> A  ->  g : ( cf `  A
) --> A )
73 ffvelrn 5770 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( g : ( cf `  A ) --> A  /\  x  e.  ( cf `  A ) )  -> 
( g `  x
)  e.  A )
7472, 73sylan 457 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( g : ( cf `  A ) -1-1-> A  /\  x  e.  ( cf `  A ) )  -> 
( g `  x
)  e.  A )
7574adantlr 695 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( g : ( cf `  A )
-1-1-> A  /\  A  e.  On )  /\  x  e.  ( cf `  A
) )  ->  (
g `  x )  e.  A )
76753adant3 976 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( g : ( cf `  A )
-1-1-> A  /\  A  e.  On )  /\  x  e.  ( cf `  A
)  /\  A. y  e.  x  ( G `  y )  e.  A
)  ->  ( g `  x )  e.  A
)
7719fveq1i 5633 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( G `
 y )  =  ( (recs ( F )  |`  ( cf `  A ) ) `  y )
78 fvres 5649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  e.  ( cf `  A
)  ->  ( (recs ( F )  |`  ( cf `  A ) ) `
 y )  =  (recs ( F ) `
 y ) )
7913, 78syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( y  e.  x  /\  x  e.  ( cf `  A ) )  -> 
( (recs ( F )  |`  ( cf `  A ) ) `  y )  =  (recs ( F ) `  y ) )
8077, 79syl5eq 2410 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( y  e.  x  /\  x  e.  ( cf `  A ) )  -> 
( G `  y
)  =  (recs ( F ) `  y
) )
8180adantrl 696 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( y  e.  x  /\  ( A  e.  On  /\  x  e.  ( cf `  A ) ) )  ->  ( G `  y )  =  (recs ( F ) `  y ) )
8281ancoms 439 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( A  e.  On  /\  x  e.  ( cf `  A ) )  /\  y  e.  x )  ->  ( G `  y
)  =  (recs ( F ) `  y
) )
8382eleq1d 2432 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( A  e.  On  /\  x  e.  ( cf `  A ) )  /\  y  e.  x )  ->  ( ( G `  y )  e.  A  <->  (recs ( F ) `  y )  e.  A
) )
84 ordsucss 4712 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( Ord 
A  ->  ( (recs ( F ) `  y
)  e.  A  ->  suc  (recs ( F ) `
 y )  C_  A ) )
8569, 84syl 15 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A  e.  On  ->  (
(recs ( F ) `
 y )  e.  A  ->  suc  (recs ( F ) `  y
)  C_  A )
)
8685ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( A  e.  On  /\  x  e.  ( cf `  A ) )  /\  y  e.  x )  ->  ( (recs ( F ) `  y )  e.  A  ->  suc  (recs ( F ) `  y )  C_  A
) )
8783, 86sylbid 206 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( A  e.  On  /\  x  e.  ( cf `  A ) )  /\  y  e.  x )  ->  ( ( G `  y )  e.  A  ->  suc  (recs ( F ) `  y ) 
C_  A ) )
8887ralimdva 2706 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  On  /\  x  e.  ( cf `  A ) )  -> 
( A. y  e.  x  ( G `  y )  e.  A  ->  A. y  e.  x  suc  (recs ( F ) `
 y )  C_  A ) )
89 iunss 4045 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( U_ y  e.  x  suc  (recs ( F ) `  y )  C_  A  <->  A. y  e.  x  suc  (recs ( F ) `  y )  C_  A
)
9088, 89syl6ibr 218 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  On  /\  x  e.  ( cf `  A ) )  -> 
( A. y  e.  x  ( G `  y )  e.  A  ->  U_ y  e.  x  suc  (recs ( F ) `
 y )  C_  A ) )
91903impia 1149 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  On  /\  x  e.  ( cf `  A )  /\  A. y  e.  x  ( G `  y )  e.  A )  ->  U_ y  e.  x  suc  (recs ( F ) `  y
)  C_  A )
92 onelon 4520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( A  e.  On  /\  (recs ( F ) `  y )  e.  A
)  ->  (recs ( F ) `  y
)  e.  On )
9392ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( A  e.  On  ->  (
(recs ( F ) `
 y )  e.  A  ->  (recs ( F ) `  y
)  e.  On ) )
9493ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( A  e.  On  /\  x  e.  ( cf `  A ) )  /\  y  e.  x )  ->  ( (recs ( F ) `  y )  e.  A  ->  (recs ( F ) `  y
)  e.  On ) )
9583, 94sylbid 206 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( A  e.  On  /\  x  e.  ( cf `  A ) )  /\  y  e.  x )  ->  ( ( G `  y )  e.  A  ->  (recs ( F ) `
 y )  e.  On ) )
96 suceloni 4707 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (recs ( F ) `  y )  e.  On  ->  suc  (recs ( F ) `  y )  e.  On )
9795, 96syl6 29 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( A  e.  On  /\  x  e.  ( cf `  A ) )  /\  y  e.  x )  ->  ( ( G `  y )  e.  A  ->  suc  (recs ( F ) `  y )  e.  On ) )
9897ralimdva 2706 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  On  /\  x  e.  ( cf `  A ) )  -> 
( A. y  e.  x  ( G `  y )  e.  A  ->  A. y  e.  x  suc  (recs ( F ) `
 y )  e.  On ) )
99983impia 1149 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  e.  On  /\  x  e.  ( cf `  A )  /\  A. y  e.  x  ( G `  y )  e.  A )  ->  A. y  e.  x  suc  (recs ( F ) `  y
)  e.  On )
100 fvex 5646 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  (recs ( F ) `  y
)  e.  _V
101100sucex 4705 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  suc  (recs ( F ) `  y
)  e.  _V
10227, 101iunonOLD 6498 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( A. y  e.  x  suc  (recs ( F ) `  y )  e.  On  ->  U_ y  e.  x  suc  (recs ( F ) `
 y )  e.  On )
10399, 102syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  On  /\  x  e.  ( cf `  A )  /\  A. y  e.  x  ( G `  y )  e.  A )  ->  U_ y  e.  x  suc  (recs ( F ) `  y
)  e.  On )
104 simp1 956 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  On  /\  x  e.  ( cf `  A )  /\  A. y  e.  x  ( G `  y )  e.  A )  ->  A  e.  On )
105 onsseleq 4536 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
U_ y  e.  x  suc  (recs ( F ) `
 y )  e.  On  /\  A  e.  On )  ->  ( U_ y  e.  x  suc  (recs ( F ) `
 y )  C_  A 
<->  ( U_ y  e.  x  suc  (recs ( F ) `  y
)  e.  A  \/  U_ y  e.  x  suc  (recs ( F ) `  y )  =  A ) ) )
106103, 104, 105syl2anc 642 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  On  /\  x  e.  ( cf `  A )  /\  A. y  e.  x  ( G `  y )  e.  A )  ->  ( U_ y  e.  x  suc  (recs ( F ) `
 y )  C_  A 
<->  ( U_ y  e.  x  suc  (recs ( F ) `  y
)  e.  A  \/  U_ y  e.  x  suc  (recs ( F ) `  y )  =  A ) ) )
107 idd 21 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  On  /\  x  e.  ( cf `  A )  /\  A. y  e.  x  ( G `  y )  e.  A )  ->  ( U_ y  e.  x  suc  (recs ( F ) `
 y )  e.  A  ->  U_ y  e.  x  suc  (recs ( F ) `  y
)  e.  A ) )
108 simpll 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( x  e.  ( cf `  A )  /\  A. y  e.  x  ( G `  y )  e.  A
)  /\  ( U_ y  e.  x  suc  (recs ( F ) `  y )  =  A  /\  A  e.  On ) )  ->  x  e.  ( cf `  A
) )
109 simprr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( x  e.  ( cf `  A )  /\  A. y  e.  x  ( G `  y )  e.  A
)  /\  ( U_ y  e.  x  suc  (recs ( F ) `  y )  =  A  /\  A  e.  On ) )  ->  A  e.  On )
1103ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( x  e.  ( cf `  A )  /\  A. y  e.  x  ( G `  y )  e.  A
)  /\  ( U_ y  e.  x  suc  (recs ( F ) `  y )  =  A  /\  A  e.  On ) )  ->  x  e.  On )
1113, 49syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  e.  ( cf `  A
)  ->  (recs ( F )  |`  x
)  Fn  x )
112111adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( x  e.  ( cf `  A )  /\  A. y  e.  x  ( G `  y )  e.  A )  ->  (recs ( F )  |`  x
)  Fn  x )
11380ancoms 439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( x  e.  ( cf `  A )  /\  y  e.  x )  ->  ( G `  y )  =  (recs ( F ) `
 y ) )
114 fvres 5649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( y  e.  x  ->  (
(recs ( F )  |`  x ) `  y
)  =  (recs ( F ) `  y
) )
115114adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( x  e.  ( cf `  A )  /\  y  e.  x )  ->  (
(recs ( F )  |`  x ) `  y
)  =  (recs ( F ) `  y
) )
116113, 115eqtr4d 2401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( x  e.  ( cf `  A )  /\  y  e.  x )  ->  ( G `  y )  =  ( (recs ( F )  |`  x
) `  y )
)
117116eleq1d 2432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( x  e.  ( cf `  A )  /\  y  e.  x )  ->  (
( G `  y
)  e.  A  <->  ( (recs ( F )  |`  x
) `  y )  e.  A ) )
118117ralbidva 2644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  e.  ( cf `  A
)  ->  ( A. y  e.  x  ( G `  y )  e.  A  <->  A. y  e.  x  ( (recs ( F )  |`  x ) `  y
)  e.  A ) )
119118biimpa 470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( x  e.  ( cf `  A )  /\  A. y  e.  x  ( G `  y )  e.  A )  ->  A. y  e.  x  ( (recs ( F )  |`  x
) `  y )  e.  A )
120 ffnfv 5796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (recs ( F )  |`  x ) : x --> A  <->  ( (recs ( F )  |`  x
)  Fn  x  /\  A. y  e.  x  ( (recs ( F )  |`  x ) `  y
)  e.  A ) )
121112, 119, 120sylanbrc 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( x  e.  ( cf `  A )  /\  A. y  e.  x  ( G `  y )  e.  A )  ->  (recs ( F )  |`  x
) : x --> A )
122121adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( x  e.  ( cf `  A )  /\  A. y  e.  x  ( G `  y )  e.  A
)  /\  ( U_ y  e.  x  suc  (recs ( F ) `  y )  =  A  /\  A  e.  On ) )  ->  (recs ( F )  |`  x
) : x --> A )
123 eleq2 2427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( U_ y  e.  x  suc  (recs ( F ) `  y )  =  A  ->  ( t  e. 
U_ y  e.  x  suc  (recs ( F ) `
 y )  <->  t  e.  A ) )
124123biimpar 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
U_ y  e.  x  suc  (recs ( F ) `
 y )  =  A  /\  t  e.  A )  ->  t  e.  U_ y  e.  x  suc  (recs ( F ) `
 y ) )
125124adantrl 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
U_ y  e.  x  suc  (recs ( F ) `
 y )  =  A  /\  ( A  e.  On  /\  t  e.  A ) )  -> 
t  e.  U_ y  e.  x  suc  (recs ( F ) `  y
) )
1261253adant1 974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( (recs ( F )  |`  x ) : x --> A  /\  U_ y  e.  x  suc  (recs ( F ) `  y
)  =  A  /\  ( A  e.  On  /\  t  e.  A ) )  ->  t  e.  U_ y  e.  x  suc  (recs ( F ) `  y ) )
127 onelon 4520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( A  e.  On  /\  t  e.  A )  ->  t  e.  On )
128127adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( ( A  e.  On  /\  t  e.  A )  /\  ( (recs ( F )  |`  x
) : x --> A  /\  y  e.  x )
)  ->  t  e.  On )
129114adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( (recs ( F )  |`  x ) : x --> A  /\  y  e.  x )  ->  (
(recs ( F )  |`  x ) `  y
)  =  (recs ( F ) `  y
) )
130 ffvelrn 5770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( (recs ( F )  |`  x ) : x --> A  /\  y  e.  x )  ->  (
(recs ( F )  |`  x ) `  y
)  e.  A )
131129, 130eqeltrrd 2441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( (recs ( F )  |`  x ) : x --> A  /\  y  e.  x )  ->  (recs ( F ) `  y
)  e.  A )
132131, 92sylan2 460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( A  e.  On  /\  ( (recs ( F )  |`  x ) : x --> A  /\  y  e.  x ) )  -> 
(recs ( F ) `
 y )  e.  On )
133132adantlr 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( ( A  e.  On  /\  t  e.  A )  /\  ( (recs ( F )  |`  x
) : x --> A  /\  y  e.  x )
)  ->  (recs ( F ) `  y
)  e.  On )
134 onsssuc 4583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( t  e.  On  /\  (recs ( F ) `  y )  e.  On )  ->  ( t  C_  (recs ( F ) `  y )  <->  t  e.  suc  (recs ( F ) `
 y ) ) )
135128, 133, 134syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( ( A  e.  On  /\  t  e.  A )  /\  ( (recs ( F )  |`  x
) : x --> A  /\  y  e.  x )
)  ->  ( t  C_  (recs ( F ) `
 y )  <->  t  e.  suc  (recs ( F ) `
 y ) ) )
136135anassrs 629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( ( A  e.  On  /\  t  e.  A )  /\  (recs ( F )  |`  x
) : x --> A )  /\  y  e.  x
)  ->  ( t  C_  (recs ( F ) `
 y )  <->  t  e.  suc  (recs ( F ) `
 y ) ) )
137136rexbidva 2645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( A  e.  On  /\  t  e.  A )  /\  (recs ( F )  |`  x ) : x --> A )  ->  ( E. y  e.  x  t  C_  (recs ( F ) `  y )  <->  E. y  e.  x  t  e.  suc  (recs ( F ) `
 y ) ) )
138 eliun 4011 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( t  e.  U_ y  e.  x  suc  (recs ( F ) `  y
)  <->  E. y  e.  x  t  e.  suc  (recs ( F ) `  y
) )
139137, 138syl6bbr 254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( A  e.  On  /\  t  e.  A )  /\  (recs ( F )  |`  x ) : x --> A )  ->  ( E. y  e.  x  t  C_  (recs ( F ) `  y )  <->  t  e.  U_ y  e.  x  suc  (recs ( F ) `  y ) ) )
140139ancoms 439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( (recs ( F )  |`  x ) : x --> A  /\  ( A  e.  On  /\  t  e.  A ) )  -> 
( E. y  e.  x  t  C_  (recs ( F ) `  y
)  <->  t  e.  U_ y  e.  x  suc  (recs ( F ) `  y ) ) )
1411403adant2 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( (recs ( F )  |`  x ) : x --> A  /\  U_ y  e.  x  suc  (recs ( F ) `  y
)  =  A  /\  ( A  e.  On  /\  t  e.  A ) )  ->  ( E. y  e.  x  t  C_  (recs ( F ) `
 y )  <->  t  e.  U_ y  e.  x  suc  (recs ( F ) `  y ) ) )
142126, 141mpbird 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( (recs ( F )  |`  x ) : x --> A  /\  U_ y  e.  x  suc  (recs ( F ) `  y
)  =  A  /\  ( A  e.  On  /\  t  e.  A ) )  ->  E. y  e.  x  t  C_  (recs ( F ) `  y ) )
1431423expa 1152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( (recs ( F )  |`  x ) : x --> A  /\  U_ y  e.  x  suc  (recs ( F ) `  y )  =  A )  /\  ( A  e.  On  /\  t  e.  A ) )  ->  E. y  e.  x  t  C_  (recs ( F ) `  y ) )
144143anassrs 629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( (recs ( F )  |`  x
) : x --> A  /\  U_ y  e.  x  suc  (recs ( F ) `  y )  =  A )  /\  A  e.  On )  /\  t  e.  A )  ->  E. y  e.  x  t  C_  (recs ( F ) `  y ) )
145144ralrimiva 2711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( (recs ( F )  |`  x ) : x --> A  /\  U_ y  e.  x  suc  (recs ( F ) `  y )  =  A )  /\  A  e.  On )  ->  A. t  e.  A  E. y  e.  x  t  C_  (recs ( F ) `  y ) )
146145expl 601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (recs ( F )  |`  x ) : x --> A  ->  ( ( U_ y  e.  x  suc  (recs ( F ) `
 y )  =  A  /\  A  e.  On )  ->  A. t  e.  A  E. y  e.  x  t  C_  (recs ( F ) `  y ) ) )
147121, 146syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( x  e.  ( cf `  A )  /\  A. y  e.  x  ( G `  y )  e.  A )  ->  (
( U_ y  e.  x  suc  (recs ( F ) `
 y )  =  A  /\  A  e.  On )  ->  A. t  e.  A  E. y  e.  x  t  C_  (recs ( F ) `  y ) ) )
148147imp 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( x  e.  ( cf `  A )  /\  A. y  e.  x  ( G `  y )  e.  A
)  /\  ( U_ y  e.  x  suc  (recs ( F ) `  y )  =  A  /\  A  e.  On ) )  ->  A. t  e.  A  E. y  e.  x  t  C_  (recs ( F ) `  y ) )
149 feq1 5480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( f  =  (recs ( F )  |`  x )  ->  ( f : x --> A  <->  (recs ( F )  |`  x ) : x --> A ) )
150 fveq1 5631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( f  =  (recs ( F )  |`  x )  ->  ( f `  y
)  =  ( (recs ( F )  |`  x ) `  y
) )
151150sseq2d 3292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( f  =  (recs ( F )  |`  x )  ->  ( t  C_  (
f `  y )  <->  t 
C_  ( (recs ( F )  |`  x
) `  y )
) )
152151rexbidv 2649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( f  =  (recs ( F )  |`  x )  ->  ( E. y  e.  x  t  C_  (
f `  y )  <->  E. y  e.  x  t 
C_  ( (recs ( F )  |`  x
) `  y )
) )
153114sseq2d 3292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( y  e.  x  ->  (
t  C_  ( (recs ( F )  |`  x
) `  y )  <->  t 
C_  (recs ( F ) `  y ) ) )
154153rexbiia 2661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( E. y  e.  x  t 
C_  ( (recs ( F )  |`  x
) `  y )  <->  E. y  e.  x  t 
C_  (recs ( F ) `  y ) )
155152, 154syl6bb 252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( f  =  (recs ( F )  |`  x )  ->  ( E. y  e.  x  t  C_  (
f `  y )  <->  E. y  e.  x  t 
C_  (recs ( F ) `  y ) ) )
156155ralbidv 2648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( f  =  (recs ( F )  |`  x )  ->  ( A. t  e.  A  E. y  e.  x  t  C_  (
f `  y )  <->  A. t  e.  A  E. y  e.  x  t  C_  (recs ( F ) `
 y ) ) )
157149, 156anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( f  =  (recs ( F )  |`  x )  ->  ( ( f : x --> A  /\  A. t  e.  A  E. y  e.  x  t  C_  ( f `  y
) )  <->  ( (recs ( F )  |`  x
) : x --> A  /\  A. t  e.  A  E. y  e.  x  t  C_  (recs ( F ) `
 y ) ) ) )
15829, 157spcev 2960 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( (recs ( F )  |`  x ) : x --> A  /\  A. t  e.  A  E. y  e.  x  t  C_  (recs ( F ) `  y ) )  ->  E. f ( f : x --> A  /\  A. t  e.  A  E. y  e.  x  t  C_  ( f `  y
) ) )
159122, 148, 158syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( x  e.  ( cf `  A )  /\  A. y  e.  x  ( G `  y )  e.  A
)  /\  ( U_ y  e.  x  suc  (recs ( F ) `  y )  =  A  /\  A  e.  On ) )  ->  E. f
( f : x --> A  /\  A. t  e.  A  E. y  e.  x  t  C_  ( f `  y
) ) )
160 cfflb 8032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( A  e.  On  /\  x  e.  On )  ->  ( E. f ( f : x --> A  /\  A. t  e.  A  E. y  e.  x  t  C_  ( f `  y
) )  ->  ( cf `  A )  C_  x ) )
161160imp 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( A  e.  On  /\  x  e.  On )  /\  E. f ( f : x --> A  /\  A. t  e.  A  E. y  e.  x  t  C_  ( f `  y
) ) )  -> 
( cf `  A
)  C_  x )
162109, 110, 159, 161syl21anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( x  e.  ( cf `  A )  /\  A. y  e.  x  ( G `  y )  e.  A
)  /\  ( U_ y  e.  x  suc  (recs ( F ) `  y )  =  A  /\  A  e.  On ) )  ->  ( cf `  A )  C_  x )
163 ontri1 4529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( cf `  A
)  e.  On  /\  x  e.  On )  ->  ( ( cf `  A
)  C_  x  <->  -.  x  e.  ( cf `  A
) ) )
1642, 3, 163sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  e.  ( cf `  A
)  ->  ( ( cf `  A )  C_  x 
<->  -.  x  e.  ( cf `  A ) ) )
165164ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( x  e.  ( cf `  A )  /\  A. y  e.  x  ( G `  y )  e.  A
)  /\  ( U_ y  e.  x  suc  (recs ( F ) `  y )  =  A  /\  A  e.  On ) )  ->  (
( cf `  A
)  C_  x  <->  -.  x  e.  ( cf `  A
) ) )
166162, 165mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( x  e.  ( cf `  A )  /\  A. y  e.  x  ( G `  y )  e.  A
)  /\  ( U_ y  e.  x  suc  (recs ( F ) `  y )  =  A  /\  A  e.  On ) )  ->  -.  x  e.  ( cf `  A ) )
167108, 166pm2.65i 165 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  -.  (
( x  e.  ( cf `  A )  /\  A. y  e.  x  ( G `  y )  e.  A
)  /\  ( U_ y  e.  x  suc  (recs ( F ) `  y )  =  A  /\  A  e.  On ) )
168167pm2.21i 123 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( x  e.  ( cf `  A )  /\  A. y  e.  x  ( G `  y )  e.  A
)  /\  ( U_ y  e.  x  suc  (recs ( F ) `  y )  =  A  /\  A  e.  On ) )  ->  U_ y  e.  x  suc  (recs ( F ) `  y
)  e.  A )
169168ex 423 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( x  e.  ( cf `  A )  /\  A. y  e.  x  ( G `  y )  e.  A )  ->  (
( U_ y  e.  x  suc  (recs ( F ) `
 y )  =  A  /\  A  e.  On )  ->  U_ y  e.  x  suc  (recs ( F ) `  y
)  e.  A ) )
170169exp3acom23 1377 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  ( cf `  A )  /\  A. y  e.  x  ( G `  y )  e.  A )  ->  ( A  e.  On  ->  (
U_ y  e.  x  suc  (recs ( F ) `
 y )  =  A  ->  U_ y  e.  x  suc  (recs ( F ) `  y
)  e.  A ) ) )
171170com12 27 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( A  e.  On  ->  (
( x  e.  ( cf `  A )  /\  A. y  e.  x  ( G `  y )  e.  A
)  ->  ( U_ y  e.  x  suc  (recs ( F ) `  y )  =  A  ->  U_ y  e.  x  suc  (recs ( F ) `
 y )  e.  A ) ) )
1721713impib 1150 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  On  /\  x  e.  ( cf `  A )  /\  A. y  e.  x  ( G `  y )  e.  A )  ->  ( U_ y  e.  x  suc  (recs ( F ) `
 y )  =  A  ->  U_ y  e.  x  suc  (recs ( F ) `  y
)  e.  A ) )
173107, 172jaod 369 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  On  /\  x  e.  ( cf `  A )  /\  A. y  e.  x  ( G `  y )  e.  A )  ->  (
( U_ y  e.  x  suc  (recs ( F ) `
 y )  e.  A  \/  U_ y  e.  x  suc  (recs ( F ) `  y
)  =  A )  ->  U_ y  e.  x  suc  (recs ( F ) `
 y )  e.  A ) )
174106, 173sylbid 206 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  On  /\  x  e.  ( cf `  A )  /\  A. y  e.  x  ( G `  y )  e.  A )  ->  ( U_ y  e.  x  suc  (recs ( F ) `
 y )  C_  A  ->  U_ y  e.  x  suc  (recs ( F ) `
 y )  e.  A ) )
17591, 174mpd 14 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  On  /\  x  e.  ( cf `  A )  /\  A. y  e.  x  ( G `  y )  e.  A )  ->  U_ y  e.  x  suc  (recs ( F ) `  y
)  e.  A )
1761753adant1l 1175 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( g : ( cf `  A )
-1-1-> A  /\  A  e.  On )  /\  x  e.  ( cf `  A
)  /\  A. y  e.  x  ( G `  y )  e.  A
)  ->  U_ y  e.  x  suc  (recs ( F ) `  y
)  e.  A )
177 ordunel 4721 . . . . . . . . . . . . . . . . . 18  |-  ( ( Ord  A  /\  (
g `  x )  e.  A  /\  U_ y  e.  x  suc  (recs ( F ) `  y
)  e.  A )  ->  ( ( g `
 x )  u. 
U_ y  e.  x  suc  (recs ( F ) `
 y ) )  e.  A )
17871, 76, 176, 177syl3anc 1183 . . . . . . . . . . . . . . . . 17  |-  ( ( ( g : ( cf `  A )
-1-1-> A  /\  A  e.  On )  /\  x  e.  ( cf `  A
)  /\  A. y  e.  x  ( G `  y )  e.  A
)  ->  ( (
g `  x )  u.  U_ y  e.  x  suc  (recs ( F ) `
 y ) )  e.  A )
17968, 178eqeltrd 2440 . . . . . . . . . . . . . . . 16  |-  ( ( ( g : ( cf `  A )
-1-1-> A  /\  A  e.  On )  /\  x  e.  ( cf `  A
)  /\  A. y  e.  x  ( G `  y )  e.  A
)  ->  ( G `  x )  e.  A
)
1801793expia 1154 . . . . . . . . . . . . . . 15  |-  ( ( ( g : ( cf `  A )
-1-1-> A  /\  A  e.  On )  /\  x  e.  ( cf `  A
) )  ->  ( A. y  e.  x  ( G `  y )  e.  A  ->  ( G `  x )  e.  A ) )
1811803impa 1147 . . . . . . . . . . . . . 14  |-  ( ( g : ( cf `  A ) -1-1-> A  /\  A  e.  On  /\  x  e.  ( cf `  A
) )  ->  ( A. y  e.  x  ( G `  y )  e.  A  ->  ( G `  x )  e.  A ) )
18218, 181syld 40 . . . . . . . . . . . . 13  |-  ( ( g : ( cf `  A ) -1-1-> A  /\  A  e.  On  /\  x  e.  ( cf `  A
) )  ->  ( A. y  e.  x  ( ( g : ( cf `  A
) -1-1-> A  /\  A  e.  On  /\  y  e.  ( cf `  A
) )  ->  ( G `  y )  e.  A )  ->  ( G `  x )  e.  A ) )
183182com12 27 . . . . . . . . . . . 12  |-  ( A. y  e.  x  (
( g : ( cf `  A )
-1-1-> A  /\  A  e.  On  /\  y  e.  ( cf `  A
) )  ->  ( G `  y )  e.  A )  ->  (
( g : ( cf `  A )
-1-1-> A  /\  A  e.  On  /\  x  e.  ( cf `  A
) )  ->  ( G `  x )  e.  A ) )
184183a1i 10 . . . . . . . . . . 11  |-  ( x  e.  On  ->  ( A. y  e.  x  ( ( g : ( cf `  A
) -1-1-> A  /\  A  e.  On  /\  y  e.  ( cf `  A
) )  ->  ( G `  y )  e.  A )  ->  (
( g : ( cf `  A )
-1-1-> A  /\  A  e.  On  /\  x  e.  ( cf `  A
) )  ->  ( G `  x )  e.  A ) ) )
1859, 184tfis2 4750 . . . . . . . . . 10  |-  ( x  e.  On  ->  (
( g : ( cf `  A )
-1-1-> A  /\  A  e.  On  /\  x  e.  ( cf `  A
) )  ->  ( G `  x )  e.  A ) )
1864, 185mpcom 32 . . . . . . . . 9  |-  ( ( g : ( cf `  A ) -1-1-> A  /\  A  e.  On  /\  x  e.  ( cf `  A
) )  ->  ( G `  x )  e.  A )
1871863expia 1154 . . . . . . . 8  |-  ( ( g : ( cf `  A ) -1-1-> A  /\  A  e.  On )  ->  ( x  e.  ( cf `  A )  ->  ( G `  x )  e.  A
) )
188187ralrimiv 2710 . . . . . . 7  |-  ( ( g : ( cf `  A ) -1-1-> A  /\  A  e.  On )  ->  A. x  e.  ( cf `  A ) ( G `  x
)  e.  A )
1892onssi 4731 . . . . . . . . 9  |-  ( cf `  A )  C_  On
190 fnssres 5462 . . . . . . . . . 10  |-  ( (recs ( F )  Fn  On  /\  ( cf `  A )  C_  On )  ->  (recs ( F )  |`  ( cf `  A ) )  Fn  ( cf `  A
) )
19119fneq1i 5443 . . . . . . . . . 10  |-  ( G  Fn  ( cf `  A
)  <->  (recs ( F )  |`  ( cf `  A
) )  Fn  ( cf `  A ) )
192190, 191sylibr 203 . . . . . . . . 9  |-  ( (recs ( F )  Fn  On  /\  ( cf `  A )  C_  On )  ->  G  Fn  ( cf `  A ) )
19324, 189, 192mp2an 653 . . . . . . . 8  |-  G  Fn  ( cf `  A )
194 ffnfv 5796 . . . . . . . 8  |-  ( G : ( cf `  A
) --> A  <->  ( G  Fn  ( cf `  A
)  /\  A. x  e.  ( cf `  A
) ( G `  x )  e.  A
) )
195193, 194mpbiran 884 . . . . . . 7  |-  ( G : ( cf `  A
) --> A  <->  A. x  e.  ( cf `  A
) ( G `  x )  e.  A
)
196188, 195sylibr 203 . . . . . 6  |-  ( ( g : ( cf `  A ) -1-1-> A  /\  A  e.  On )  ->  G : ( cf `  A ) --> A )
197196adantlr 695 . . . . 5  |-  ( ( ( g : ( cf `  A )
-1-1-> A  /\  A. z  e.  A  E. w  e.  ( cf `  A
) z  C_  (
g `  w )
)  /\  A  e.  On )  ->  G :
( cf `  A
) --> A )
198 onss 4685 . . . . . . . 8  |-  ( A  e.  On  ->  A  C_  On )
199198adantl 452 . . . . . . 7  |-  ( ( g : ( cf `  A ) -1-1-> A  /\  A  e.  On )  ->  A  C_  On )
2002onordi 4600 . . . . . . . 8  |-  Ord  ( cf `  A )
201100sucid 4574 . . . . . . . . . . . . . . . . . 18  |-  (recs ( F ) `  y
)  e.  suc  (recs ( F ) `  y
)
202 fveq2 5632 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  y  ->  (recs ( F ) `  t
)  =  (recs ( F ) `  y
) )
203 suceq 4560 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (recs ( F ) `  t )  =  (recs ( F ) `  y )  ->  suc  (recs ( F ) `  t )  =  suc  (recs ( F ) `  y ) )
204202, 203syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  y  ->  suc  (recs ( F ) `  t )  =  suc  (recs ( F ) `  y ) )
205204eleq2d 2433 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  y  ->  (
(recs ( F ) `
 y )  e. 
suc  (recs ( F ) `
 t )  <->  (recs ( F ) `  y
)  e.  suc  (recs ( F ) `  y
) ) )
206205rspcev 2969 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  x  /\  (recs ( F ) `  y )  e.  suc  (recs ( F ) `  y ) )  ->  E. t  e.  x  (recs ( F ) `  y )  e.  suc  (recs ( F ) `  t ) )
207201, 206mpan2 652 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  x  ->  E. t  e.  x  (recs ( F ) `  y
)  e.  suc  (recs ( F ) `  t
) )
208 eliun 4011 . . . . . . . . . . . . . . . . 17  |-  ( (recs ( F ) `  y )  e.  U_ t  e.  x  suc  (recs ( F ) `  t )  <->  E. t  e.  x  (recs ( F ) `  y
)  e.  suc  (recs ( F ) `  t
) )
209207, 208sylibr 203 . . . . . . . . . . . . . . . 16  |-  ( y  e.  x  ->  (recs ( F ) `  y
)  e.  U_ t  e.  x  suc  (recs ( F ) `  t
) )
210209, 60syl6eleqr 2457 . . . . . . . . . . . . . . 15  |-  ( y  e.  x  ->  (recs ( F ) `  y
)  e.  U_ y  e.  x  suc  (recs ( F ) `  y
) )
211 elun2 3431 . . . . . . . . . . . . . . 15  |-  ( (recs ( F ) `  y )  e.  U_ y  e.  x  suc  (recs ( F ) `  y )  ->  (recs ( F ) `  y
)  e.  ( ( g `  x )  u.  U_ y  e.  x  suc  (recs ( F ) `  y
) ) )
212210, 211syl 15 . . . . . . . . . . . . . 14  |-  ( y  e.  x  ->  (recs ( F ) `  y
)  e.  ( ( g `  x )  u.  U_ y  e.  x  suc  (recs ( F ) `  y
) ) )
213212adantr 451 . . . . . . . . . . . . 13  |-  ( ( y  e.  x  /\  x  e.  ( cf `  A ) )  -> 
(recs ( F ) `
 y )  e.  ( ( g `  x )  u.  U_ y  e.  x  suc  (recs ( F ) `  y ) ) )
2143adantl 452 . . . . . . . . . . . . . 14  |-  ( ( y  e.  x  /\  x  e.  ( cf `  A ) )  ->  x  e.  On )
215214, 65syl 15 . . . . . . . . . . . . 13  |-  ( ( y  e.  x  /\  x  e.  ( cf `  A ) )  -> 
(recs ( F ) `
 x )  =  ( ( g `  x )  u.  U_ y  e.  x  suc  (recs ( F ) `  y ) ) )
216213, 215eleqtrrd 2443 . . . . . . . . . . . 12  |-  ( ( y  e.  x  /\  x  e.  ( cf `  A ) )  -> 
(recs ( F ) `
 y )  e.  (recs ( F ) `
 x ) )
21722adantl 452 . . . . . . . . . . . . 13  |-  ( ( y  e.  x  /\  x  e.  ( cf `  A ) )  -> 
( G `  x
)  =  (recs ( F ) `  x
) )
21880, 217eleq12d 2434 . . . . . . . . . . . 12  |-  ( ( y  e.  x  /\  x  e.  ( cf `  A ) )  -> 
( ( G `  y )  e.  ( G `  x )  <-> 
(recs ( F ) `
 y )  e.  (recs ( F ) `
 x ) ) )
219216, 218mpbird 223 . . . . . . . . . . 11  |-  ( ( y  e.  x  /\  x  e.  ( cf `  A ) )  -> 
( G `  y
)  e.  ( G `
 x ) )
220219expcom 424 . . . . . . . . . 10  |-  ( x  e.  ( cf `  A
)  ->  ( y  e.  x  ->  ( G `
 y )  e.  ( G `  x
) ) )
221220ralrimiv 2710 . . . . . . . . 9  |-  ( x  e.  ( cf `  A
)  ->  A. y  e.  x  ( G `  y )  e.  ( G `  x ) )
222221rgen 2693 . . . . . . . 8  |-  A. x  e.  ( cf `  A
) A. y  e.  x  ( G `  y )  e.  ( G `  x )
223 issmo2 6508 . . . . . . . . 9  |-  ( G : ( cf `  A
) --> A  ->  (
( A  C_  On  /\ 
Ord  ( cf `  A
)  /\  A. x  e.  ( cf `  A
) A. y  e.  x  ( G `  y )  e.  ( G `  x ) )  ->  Smo  G ) )
224223com12 27 . . . . . . . 8  |-  ( ( A  C_  On  /\  Ord  ( cf `  A )  /\  A. x  e.  ( cf `  A
) A. y  e.  x  ( G `  y )  e.  ( G `  x ) )  ->  ( G : ( cf `  A
) --> A  ->  Smo  G ) )
225200, 222, 224mp3an23 1270 . . . . . . 7  |-  ( A 
C_  On  ->  ( G : ( cf `  A
) --> A  ->  Smo  G ) )
226199, 196, 225sylc 56 . . . . . 6  |-  ( ( g : ( cf `  A ) -1-1-> A  /\  A  e.  On )  ->  Smo  G )
227226adantlr 695 . . . . 5  |-  ( ( ( g : ( cf `  A )
-1-1-> A  /\  A. z  e.  A  E. w  e.  ( cf `  A
) z  C_  (
g `  w )
)  /\  A  e.  On )  ->  Smo  G
)
228 fveq2 5632 . . . . . . . . . . 11  |-  ( x  =  w  ->  (
g `  x )  =  ( g `  w ) )
229 fveq2 5632 . . . . . . . . . . 11  |-  ( x  =  w  ->  ( G `  x )  =  ( G `  w ) )
230228, 229sseq12d 3293 . . . . . . . . . 10  |-  ( x  =  w  ->  (
( g `  x
)  C_  ( G `  x )  <->  ( g `  w )  C_  ( G `  w )
) )
231 ssun1 3426 . . . . . . . . . . 11  |-  ( g `
 x )  C_  ( ( g `  x )  u.  U_ y  e.  x  suc  (recs ( F ) `  y ) )
232231, 67syl5sseqr 3313 . . . . . . . . . 10  |-  ( x  e.  ( cf `  A
)  ->  ( g `  x )  C_  ( G `  x )
)
233230, 232vtoclga 2934 . . . . . . . . 9  |-  ( w  e.  ( cf `  A
)  ->  ( g `  w )  C_  ( G `  w )
)
234 sstr 3273 . . . . . . . . . 10  |-  ( ( z  C_  ( g `  w )  /\  (
g `  w )  C_  ( G `  w
) )  ->  z  C_  ( G `  w
) )
235234expcom 424 . . . . . . . . 9  |-  ( ( g `  w ) 
C_  ( G `  w )  ->  (
z  C_  ( g `  w )  ->  z  C_  ( G `  w
) ) )
236233, 235syl 15 . . . . . . . 8  |-  ( w  e.  ( cf `  A
)  ->  ( z  C_  ( g `  w
)  ->  z  C_  ( G `  w ) ) )
237236reximia 2733 . . . . . . 7  |-  ( E. w  e.  ( cf `  A ) z  C_  ( g `  w
)  ->  E. w  e.  ( cf `  A
) z  C_  ( G `  w )
)
238237ralimi 2703 . . . . . 6  |-  ( A. z  e.  A  E. w  e.  ( cf `  A ) z  C_  ( g `  w
)  ->  A. z  e.  A  E. w  e.  ( cf `  A
) z  C_  ( G `  w )
)
239238ad2antlr 707 . . . . 5  |-  ( ( ( g : ( cf `  A )
-1-1-> A  /\  A. z  e.  A  E. w  e.  ( cf `  A
) z  C_  (
g `  w )
)  /\  A  e.  On )  ->  A. z  e.  A  E. w  e.  ( cf `  A
) z  C_  ( G `  w )
)
240 fnex 5861 . . . . . . 7  |-  ( ( G  Fn  ( cf `  A )  /\  ( cf `  A )  e.  On )  ->  G  e.  _V )
241193, 2, 240mp2an 653 . . . . . 6  |-  G  e. 
_V
242 feq1 5480 . . . . . . 7  |-  ( f  =  G  ->  (
f : ( cf `  A ) --> A  <->  G :
( cf `  A
) --> A ) )
243 smoeq 6509 . . . . . . 7  |-  ( f  =  G  ->  ( Smo  f  <->  Smo  G ) )
244 fveq1 5631 . . . . . . . . . 10  |-  ( f  =  G  ->  (
f `  w )  =  ( G `  w ) )
245244sseq2d 3292 . . . . . . . . 9  |-  ( f  =  G  ->  (
z  C_  ( f `  w )  <->  z  C_  ( G `  w ) ) )
246245rexbidv 2649 . . . . . . . 8  |-  ( f  =  G  ->  ( E. w  e.  ( cf `  A ) z 
C_  ( f `  w )  <->  E. w  e.  ( cf `  A
) z  C_  ( G `  w )
) )
247246ralbidv 2648 . . . . . . 7  |-  ( f  =  G  ->  ( A. z  e.  A  E. w  e.  ( cf `  A ) z 
C_  ( f `  w )  <->  A. z  e.  A  E. w  e.  ( cf `  A
) z  C_  ( G `  w )
) )
248242, 243, 2473anbi123d 1253 . . . . . 6  |-  ( f  =  G  ->  (
( f : ( cf `  A ) --> A  /\  Smo  f  /\  A. z  e.  A  E. w  e.  ( cf `  A ) z 
C_  ( f `  w ) )  <->  ( G : ( cf `  A
) --> A  /\  Smo  G  /\  A. z  e.  A  E. w  e.  ( cf `  A
) z  C_  ( G `  w )
) ) )
249241, 248spcev 2960 . . . . 5  |-  ( ( G : ( cf `  A ) --> A  /\  Smo  G  /\  A. z  e.  A  E. w  e.  ( cf `  A
) z  C_  ( G `  w )
)  ->  E. f
( f : ( cf `  A ) --> A  /\  Smo  f  /\  A. z  e.  A  E. w  e.  ( cf `  A ) z 
C_  ( f `  w ) ) )
250197, 227, 239, 249syl3anc 1183 . . . 4  |-  ( ( ( g : ( cf `  A )
-1-1-> A  /\  A. z  e.  A  E. w  e.  ( cf `  A
) z  C_  (
g `  w )
)  /\  A  e.  On )  ->  E. f
( f : ( cf `  A ) --> A  /\  Smo  f  /\  A. z  e.  A  E. w  e.  ( cf `  A ) z 
C_  ( f `  w ) ) )
251250expcom 424 . . 3  |-  ( A  e.  On  ->  (
( g : ( cf `  A )
-1-1-> A  /\  A. z  e.  A  E. w  e.  ( cf `  A
) z  C_  (
g `  w )
)  ->  E. f
( f : ( cf `  A ) --> A  /\  Smo  f  /\  A. z  e.  A  E. w  e.  ( cf `  A ) z 
C_  ( f `  w ) ) ) )
252251exlimdv 1641 . 2  |-  ( A  e.  On  ->  ( E. g ( g : ( cf `  A
) -1-1-> A  /\  A. z  e.  A  E. w  e.  ( cf `  A
) z  C_  (
g `  w )
)  ->  E. f
( f : ( cf `  A ) --> A  /\  Smo  f  /\  A. z  e.  A  E. w  e.  ( cf `  A ) z 
C_  ( f `  w ) ) ) )
2531, 252mpd 14 1  |-  ( A  e.  On  ->  E. f
( f : ( cf `  A ) --> A  /\  Smo  f  /\  A. z  e.  A  E. w  e.  ( cf `  A ) z 
C_  ( f `  w ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    /\ w3a 935   E.wex 1546    = wceq 1647    e. wcel 1715   A.wral 2628   E.wrex 2629   _Vcvv 2873    u. cun 3236    C_ wss 3238   U_ciun 4007    e. cmpt 4179   Ord word 4494   Oncon0 4495   suc csuc 4497   dom cdm 4792    |` cres 4794   Fun wfun 5352    Fn wfn 5353   -->wf 5354   -1-1->wf1 5355   ` cfv 5358   Smo wsmo 6504  recscrecs 6529   cfccf 7717
This theorem is referenced by:  cfsmo  8044
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-13 1717  ax-14 1719  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-rep 4233  ax-sep 4243  ax-nul 4251  ax-pow 4290  ax-pr 4316  ax-un 4615
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 936  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-eu 2221  df-mo 2222  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-ral 2633  df-rex 2634  df-reu 2635  df-rmo 2636  df-rab 2637  df-v 2875  df-sbc 3078  df-csb 3168  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-pss 3254  df-nul 3544  df-if 3655  df-pw 3716  df-sn 3735  df-pr 3736  df-tp 3737  df-op 3738  df-uni 3930  df-int 3965  df-iun 4009  df-br 4126  df-opab 4180  df-mpt 4181  df-tr 4216  df-eprel 4408  df-id 4412  df-po 4417  df-so 4418  df-fr 4455  df-se 4456  df-we 4457  df-ord 4498  df-on 4499  df-suc 4501  df-xp 4798  df-rel 4799  df-cnv 4800  df-co 4801  df-dm 4802  df-rn 4803  df-res 4804  df-ima 4805  df-iota 5322  df-fun 5360  df-fn 5361  df-f 5362  df-f1 5363  df-fo 5364  df-f1o 5365  df-fv 5366  df-isom 5367  df-ov 5984  df-oprab 5985  df-mpt2 5986  df-1st 6249  df-2nd 6250  df-riota 6446  df-smo 6505  df-recs 6530  df-er 6802  df-map 6917  df-en 7007  df-dom 7008  df-sdom 7009  df-card 7719  df-cf 7721  df-acn 7722
  Copyright terms: Public domain W3C validator