ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  frecsuclem3 Unicode version

Theorem frecsuclem3 6020
Description: Lemma for frecsuc 6021. (Contributed by Jim Kingdon, 15-Aug-2019.)
Hypothesis
Ref Expression
frecsuclem1.h  |-  G  =  ( g  e.  _V  |->  { x  |  ( E. m  e.  om  ( dom  g  =  suc  m  /\  x  e.  ( F `  ( g `
 m ) ) )  \/  ( dom  g  =  (/)  /\  x  e.  A ) ) } )
Assertion
Ref Expression
frecsuclem3  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  (frec ( F ,  A ) `  suc  B )  =  ( F `  (frec ( F ,  A ) `
 B ) ) )
Distinct variable groups:    A, g, m, x, z    B, g, m, x, z    g, F, m, x, z    g, G, m, x, z    g, V, m, x
Allowed substitution hint:    V( z)

Proof of Theorem frecsuclem3
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 eqid 2056 . . . . . . . . . . . . 13  |- recs ( G )  = recs ( G )
2 frecsuclem1.h . . . . . . . . . . . . . 14  |-  G  =  ( g  e.  _V  |->  { x  |  ( E. m  e.  om  ( dom  g  =  suc  m  /\  x  e.  ( F `  ( g `
 m ) ) )  \/  ( dom  g  =  (/)  /\  x  e.  A ) ) } )
32frectfr 6015 . . . . . . . . . . . . 13  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V )  ->  A. y
( Fun  G  /\  ( G `  y )  e.  _V ) )
41, 3tfri1d 5979 . . . . . . . . . . . 12  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V )  -> recs ( G )  Fn  On )
5 fnfun 5023 . . . . . . . . . . . 12  |-  (recs ( G )  Fn  On  ->  Fun recs ( G ) )
64, 5syl 14 . . . . . . . . . . 11  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V )  ->  Fun recs ( G ) )
763adant3 935 . . . . . . . . . 10  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  Fun recs ( G
) )
8 peano2 4345 . . . . . . . . . . 11  |-  ( B  e.  om  ->  suc  B  e.  om )
983ad2ant3 938 . . . . . . . . . 10  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  suc  B  e.  om )
10 resfunexg 5409 . . . . . . . . . 10  |-  ( ( Fun recs ( G )  /\  suc  B  e. 
om )  ->  (recs ( G )  |`  suc  B
)  e.  _V )
117, 9, 10syl2anc 397 . . . . . . . . 9  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  (recs ( G )  |`  suc  B )  e.  _V )
12 simp1 915 . . . . . . . . 9  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  A. z ( F `
 z )  e. 
_V )
13 simp2 916 . . . . . . . . 9  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  A  e.  V
)
1411, 12, 13frecabex 6014 . . . . . . . 8  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  { x  |  ( E. m  e. 
om  ( dom  (recs ( G )  |`  suc  B
)  =  suc  m  /\  x  e.  ( F `  ( (recs ( G )  |`  suc  B
) `  m )
) )  \/  ( dom  (recs ( G )  |`  suc  B )  =  (/)  /\  x  e.  A
) ) }  e.  _V )
15 dmeq 4562 . . . . . . . . . . . . . . . . 17  |-  ( g  =  (recs ( G )  |`  suc  B )  ->  dom  g  =  dom  (recs ( G )  |`  suc  B ) )
1615eqeq1d 2064 . . . . . . . . . . . . . . . 16  |-  ( g  =  (recs ( G )  |`  suc  B )  ->  ( dom  g  =  suc  m  <->  dom  (recs ( G )  |`  suc  B
)  =  suc  m
) )
17 fveq1 5204 . . . . . . . . . . . . . . . . . 18  |-  ( g  =  (recs ( G )  |`  suc  B )  ->  ( g `  m )  =  ( (recs ( G )  |`  suc  B ) `  m ) )
1817fveq2d 5209 . . . . . . . . . . . . . . . . 17  |-  ( g  =  (recs ( G )  |`  suc  B )  ->  ( F `  ( g `  m
) )  =  ( F `  ( (recs ( G )  |`  suc  B ) `  m
) ) )
1918eleq2d 2123 . . . . . . . . . . . . . . . 16  |-  ( g  =  (recs ( G )  |`  suc  B )  ->  ( x  e.  ( F `  (
g `  m )
)  <->  x  e.  ( F `  ( (recs ( G )  |`  suc  B
) `  m )
) ) )
2016, 19anbi12d 450 . . . . . . . . . . . . . . 15  |-  ( g  =  (recs ( G )  |`  suc  B )  ->  ( ( dom  g  =  suc  m  /\  x  e.  ( F `  ( g `  m ) ) )  <-> 
( dom  (recs ( G )  |`  suc  B
)  =  suc  m  /\  x  e.  ( F `  ( (recs ( G )  |`  suc  B
) `  m )
) ) ) )
2120rexbidv 2344 . . . . . . . . . . . . . 14  |-  ( g  =  (recs ( G )  |`  suc  B )  ->  ( E. m  e.  om  ( dom  g  =  suc  m  /\  x  e.  ( F `  (
g `  m )
) )  <->  E. m  e.  om  ( dom  (recs ( G )  |`  suc  B
)  =  suc  m  /\  x  e.  ( F `  ( (recs ( G )  |`  suc  B
) `  m )
) ) ) )
2215eqeq1d 2064 . . . . . . . . . . . . . . 15  |-  ( g  =  (recs ( G )  |`  suc  B )  ->  ( dom  g  =  (/)  <->  dom  (recs ( G )  |`  suc  B )  =  (/) ) )
2322anbi1d 446 . . . . . . . . . . . . . 14  |-  ( g  =  (recs ( G )  |`  suc  B )  ->  ( ( dom  g  =  (/)  /\  x  e.  A )  <->  ( dom  (recs ( G )  |`  suc  B )  =  (/)  /\  x  e.  A ) ) )
2421, 23orbi12d 717 . . . . . . . . . . . . 13  |-  ( g  =  (recs ( G )  |`  suc  B )  ->  ( ( E. m  e.  om  ( dom  g  =  suc  m  /\  x  e.  ( F `  ( g `
 m ) ) )  \/  ( dom  g  =  (/)  /\  x  e.  A ) )  <->  ( E. m  e.  om  ( dom  (recs ( G )  |`  suc  B )  =  suc  m  /\  x  e.  ( F `  (
(recs ( G )  |`  suc  B ) `  m ) ) )  \/  ( dom  (recs ( G )  |`  suc  B
)  =  (/)  /\  x  e.  A ) ) ) )
2524abbidv 2171 . . . . . . . . . . . 12  |-  ( g  =  (recs ( G )  |`  suc  B )  ->  { x  |  ( E. m  e. 
om  ( dom  g  =  suc  m  /\  x  e.  ( F `  (
g `  m )
) )  \/  ( dom  g  =  (/)  /\  x  e.  A ) ) }  =  { x  |  ( E. m  e. 
om  ( dom  (recs ( G )  |`  suc  B
)  =  suc  m  /\  x  e.  ( F `  ( (recs ( G )  |`  suc  B
) `  m )
) )  \/  ( dom  (recs ( G )  |`  suc  B )  =  (/)  /\  x  e.  A
) ) } )
2625, 2fvmptg 5275 . . . . . . . . . . 11  |-  ( ( (recs ( G )  |`  suc  B )  e. 
_V  /\  { x  |  ( E. m  e.  om  ( dom  (recs ( G )  |`  suc  B
)  =  suc  m  /\  x  e.  ( F `  ( (recs ( G )  |`  suc  B
) `  m )
) )  \/  ( dom  (recs ( G )  |`  suc  B )  =  (/)  /\  x  e.  A
) ) }  e.  _V )  ->  ( G `
 (recs ( G )  |`  suc  B ) )  =  { x  |  ( E. m  e.  om  ( dom  (recs ( G )  |`  suc  B
)  =  suc  m  /\  x  e.  ( F `  ( (recs ( G )  |`  suc  B
) `  m )
) )  \/  ( dom  (recs ( G )  |`  suc  B )  =  (/)  /\  x  e.  A
) ) } )
2726ex 112 . . . . . . . . . 10  |-  ( (recs ( G )  |`  suc  B )  e.  _V  ->  ( { x  |  ( E. m  e. 
om  ( dom  (recs ( G )  |`  suc  B
)  =  suc  m  /\  x  e.  ( F `  ( (recs ( G )  |`  suc  B
) `  m )
) )  \/  ( dom  (recs ( G )  |`  suc  B )  =  (/)  /\  x  e.  A
) ) }  e.  _V  ->  ( G `  (recs ( G )  |`  suc  B ) )  =  { x  |  ( E. m  e.  om  ( dom  (recs ( G )  |`  suc  B )  =  suc  m  /\  x  e.  ( F `  ( (recs ( G )  |`  suc  B ) `
 m ) ) )  \/  ( dom  (recs ( G )  |`  suc  B )  =  (/)  /\  x  e.  A
) ) } ) )
2811, 27syl 14 . . . . . . . . 9  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  ( { x  |  ( E. m  e.  om  ( dom  (recs ( G )  |`  suc  B
)  =  suc  m  /\  x  e.  ( F `  ( (recs ( G )  |`  suc  B
) `  m )
) )  \/  ( dom  (recs ( G )  |`  suc  B )  =  (/)  /\  x  e.  A
) ) }  e.  _V  ->  ( G `  (recs ( G )  |`  suc  B ) )  =  { x  |  ( E. m  e.  om  ( dom  (recs ( G )  |`  suc  B )  =  suc  m  /\  x  e.  ( F `  ( (recs ( G )  |`  suc  B ) `
 m ) ) )  \/  ( dom  (recs ( G )  |`  suc  B )  =  (/)  /\  x  e.  A
) ) } ) )
292frecsuclem1 6017 . . . . . . . . . 10  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  (frec ( F ,  A ) `  suc  B )  =  ( G `  (recs ( G )  |`  suc  B
) ) )
3029eqeq1d 2064 . . . . . . . . 9  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  ( (frec ( F ,  A ) `
 suc  B )  =  { x  |  ( E. m  e.  om  ( dom  (recs ( G )  |`  suc  B )  =  suc  m  /\  x  e.  ( F `  ( (recs ( G )  |`  suc  B ) `
 m ) ) )  \/  ( dom  (recs ( G )  |`  suc  B )  =  (/)  /\  x  e.  A
) ) }  <->  ( G `  (recs ( G )  |`  suc  B ) )  =  { x  |  ( E. m  e. 
om  ( dom  (recs ( G )  |`  suc  B
)  =  suc  m  /\  x  e.  ( F `  ( (recs ( G )  |`  suc  B
) `  m )
) )  \/  ( dom  (recs ( G )  |`  suc  B )  =  (/)  /\  x  e.  A
) ) } ) )
3128, 30sylibrd 162 . . . . . . . 8  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  ( { x  |  ( E. m  e.  om  ( dom  (recs ( G )  |`  suc  B
)  =  suc  m  /\  x  e.  ( F `  ( (recs ( G )  |`  suc  B
) `  m )
) )  \/  ( dom  (recs ( G )  |`  suc  B )  =  (/)  /\  x  e.  A
) ) }  e.  _V  ->  (frec ( F ,  A ) `  suc  B )  =  {
x  |  ( E. m  e.  om  ( dom  (recs ( G )  |`  suc  B )  =  suc  m  /\  x  e.  ( F `  (
(recs ( G )  |`  suc  B ) `  m ) ) )  \/  ( dom  (recs ( G )  |`  suc  B
)  =  (/)  /\  x  e.  A ) ) } ) )
3214, 31mpd 13 . . . . . . 7  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  (frec ( F ,  A ) `  suc  B )  =  {
x  |  ( E. m  e.  om  ( dom  (recs ( G )  |`  suc  B )  =  suc  m  /\  x  e.  ( F `  (
(recs ( G )  |`  suc  B ) `  m ) ) )  \/  ( dom  (recs ( G )  |`  suc  B
)  =  (/)  /\  x  e.  A ) ) } )
3332abeq2d 2166 . . . . . 6  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  ( x  e.  (frec ( F ,  A ) `  suc  B )  <->  ( E. m  e.  om  ( dom  (recs ( G )  |`  suc  B
)  =  suc  m  /\  x  e.  ( F `  ( (recs ( G )  |`  suc  B
) `  m )
) )  \/  ( dom  (recs ( G )  |`  suc  B )  =  (/)  /\  x  e.  A
) ) ) )
342frecsuclemdm 6018 . . . . . . . . . . 11  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  dom  (recs ( G )  |`  suc  B
)  =  suc  B
)
35 peano3 4346 . . . . . . . . . . . 12  |-  ( B  e.  om  ->  suc  B  =/=  (/) )
36353ad2ant3 938 . . . . . . . . . . 11  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  suc  B  =/=  (/) )
3734, 36eqnetrd 2244 . . . . . . . . . 10  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  dom  (recs ( G )  |`  suc  B
)  =/=  (/) )
3837neneqd 2241 . . . . . . . . 9  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  -.  dom  (recs ( G )  |`  suc  B
)  =  (/) )
3938intnanrd 852 . . . . . . . 8  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  -.  ( dom  (recs ( G )  |`  suc  B )  =  (/)  /\  x  e.  A ) )
40 biorf 673 . . . . . . . 8  |-  ( -.  ( dom  (recs ( G )  |`  suc  B
)  =  (/)  /\  x  e.  A )  ->  ( E. m  e.  om  ( dom  (recs ( G )  |`  suc  B )  =  suc  m  /\  x  e.  ( F `  ( (recs ( G )  |`  suc  B ) `
 m ) ) )  <->  ( ( dom  (recs ( G )  |`  suc  B )  =  (/)  /\  x  e.  A
)  \/  E. m  e.  om  ( dom  (recs ( G )  |`  suc  B
)  =  suc  m  /\  x  e.  ( F `  ( (recs ( G )  |`  suc  B
) `  m )
) ) ) ) )
4139, 40syl 14 . . . . . . 7  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  ( E. m  e.  om  ( dom  (recs ( G )  |`  suc  B
)  =  suc  m  /\  x  e.  ( F `  ( (recs ( G )  |`  suc  B
) `  m )
) )  <->  ( ( dom  (recs ( G )  |`  suc  B )  =  (/)  /\  x  e.  A
)  \/  E. m  e.  om  ( dom  (recs ( G )  |`  suc  B
)  =  suc  m  /\  x  e.  ( F `  ( (recs ( G )  |`  suc  B
) `  m )
) ) ) ) )
42 orcom 657 . . . . . . 7  |-  ( ( ( dom  (recs ( G )  |`  suc  B
)  =  (/)  /\  x  e.  A )  \/  E. m  e.  om  ( dom  (recs ( G )  |`  suc  B )  =  suc  m  /\  x  e.  ( F `  (
(recs ( G )  |`  suc  B ) `  m ) ) ) )  <->  ( E. m  e.  om  ( dom  (recs ( G )  |`  suc  B
)  =  suc  m  /\  x  e.  ( F `  ( (recs ( G )  |`  suc  B
) `  m )
) )  \/  ( dom  (recs ( G )  |`  suc  B )  =  (/)  /\  x  e.  A
) ) )
4341, 42syl6bb 189 . . . . . 6  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  ( E. m  e.  om  ( dom  (recs ( G )  |`  suc  B
)  =  suc  m  /\  x  e.  ( F `  ( (recs ( G )  |`  suc  B
) `  m )
) )  <->  ( E. m  e.  om  ( dom  (recs ( G )  |`  suc  B )  =  suc  m  /\  x  e.  ( F `  (
(recs ( G )  |`  suc  B ) `  m ) ) )  \/  ( dom  (recs ( G )  |`  suc  B
)  =  (/)  /\  x  e.  A ) ) ) )
4434eqeq1d 2064 . . . . . . . . . 10  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  ( dom  (recs ( G )  |`  suc  B
)  =  suc  m  <->  suc 
B  =  suc  m
) )
45 vex 2577 . . . . . . . . . . . 12  |-  m  e. 
_V
46 suc11g 4308 . . . . . . . . . . . 12  |-  ( ( B  e.  om  /\  m  e.  _V )  ->  ( suc  B  =  suc  m  <->  B  =  m ) )
4745, 46mpan2 409 . . . . . . . . . . 11  |-  ( B  e.  om  ->  ( suc  B  =  suc  m  <->  B  =  m ) )
48473ad2ant3 938 . . . . . . . . . 10  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  ( suc  B  =  suc  m  <->  B  =  m ) )
4944, 48bitrd 181 . . . . . . . . 9  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  ( dom  (recs ( G )  |`  suc  B
)  =  suc  m  <->  B  =  m ) )
50 eqcom 2058 . . . . . . . . 9  |-  ( B  =  m  <->  m  =  B )
5149, 50syl6bb 189 . . . . . . . 8  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  ( dom  (recs ( G )  |`  suc  B
)  =  suc  m  <->  m  =  B ) )
5251anbi1d 446 . . . . . . 7  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  ( ( dom  (recs ( G )  |`  suc  B )  =  suc  m  /\  x  e.  ( F `  (
(recs ( G )  |`  suc  B ) `  m ) ) )  <-> 
( m  =  B  /\  x  e.  ( F `  ( (recs ( G )  |`  suc  B ) `  m
) ) ) ) )
5352rexbidv 2344 . . . . . 6  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  ( E. m  e.  om  ( dom  (recs ( G )  |`  suc  B
)  =  suc  m  /\  x  e.  ( F `  ( (recs ( G )  |`  suc  B
) `  m )
) )  <->  E. m  e.  om  ( m  =  B  /\  x  e.  ( F `  (
(recs ( G )  |`  suc  B ) `  m ) ) ) ) )
5433, 43, 533bitr2d 209 . . . . 5  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  ( x  e.  (frec ( F ,  A ) `  suc  B )  <->  E. m  e.  om  ( m  =  B  /\  x  e.  ( F `  ( (recs ( G )  |`  suc  B
) `  m )
) ) ) )
55 fveq2 5205 . . . . . . . 8  |-  ( m  =  B  ->  (
(recs ( G )  |`  suc  B ) `  m )  =  ( (recs ( G )  |`  suc  B ) `  B ) )
5655fveq2d 5209 . . . . . . 7  |-  ( m  =  B  ->  ( F `  ( (recs ( G )  |`  suc  B
) `  m )
)  =  ( F `
 ( (recs ( G )  |`  suc  B
) `  B )
) )
5756eleq2d 2123 . . . . . 6  |-  ( m  =  B  ->  (
x  e.  ( F `
 ( (recs ( G )  |`  suc  B
) `  m )
)  <->  x  e.  ( F `  ( (recs ( G )  |`  suc  B
) `  B )
) ) )
5857ceqsrexbv 2697 . . . . 5  |-  ( E. m  e.  om  (
m  =  B  /\  x  e.  ( F `  ( (recs ( G )  |`  suc  B ) `
 m ) ) )  <->  ( B  e. 
om  /\  x  e.  ( F `  ( (recs ( G )  |`  suc  B ) `  B
) ) ) )
5954, 58syl6bb 189 . . . 4  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  ( x  e.  (frec ( F ,  A ) `  suc  B )  <->  ( B  e. 
om  /\  x  e.  ( F `  ( (recs ( G )  |`  suc  B ) `  B
) ) ) ) )
60593anibar 1083 . . 3  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  ( x  e.  (frec ( F ,  A ) `  suc  B )  <->  x  e.  ( F `  ( (recs ( G )  |`  suc  B
) `  B )
) ) )
6160eqrdv 2054 . 2  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  (frec ( F ,  A ) `  suc  B )  =  ( F `  ( (recs ( G )  |`  suc  B ) `  B
) ) )
622frecsuclem2 6019 . . 3  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  ( (recs ( G )  |`  suc  B
) `  B )  =  (frec ( F ,  A ) `  B
) )
6362fveq2d 5209 . 2  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  ( F `  ( (recs ( G )  |`  suc  B ) `  B ) )  =  ( F `  (frec ( F ,  A ) `
 B ) ) )
6461, 63eqtrd 2088 1  |-  ( ( A. z ( F `
 z )  e. 
_V  /\  A  e.  V  /\  B  e.  om )  ->  (frec ( F ,  A ) `  suc  B )  =  ( F `  (frec ( F ,  A ) `
 B ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 101    <-> wb 102    \/ wo 639    /\ w3a 896   A.wal 1257    = wceq 1259    e. wcel 1409   {cab 2042    =/= wne 2220   E.wrex 2324   _Vcvv 2574   (/)c0 3251    |-> cmpt 3845   Oncon0 4127   suc csuc 4129   omcom 4340   dom cdm 4372    |` cres 4374   Fun wfun 4923    Fn wfn 4924   ` cfv 4929  recscrecs 5949  freccfrec 6007
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-13 1420  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-coll 3899  ax-sep 3902  ax-nul 3910  ax-pow 3954  ax-pr 3971  ax-un 4197  ax-setind 4289  ax-iinf 4338
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-fal 1265  df-nf 1366  df-sb 1662  df-eu 1919  df-mo 1920  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ne 2221  df-ral 2328  df-rex 2329  df-reu 2330  df-rab 2332  df-v 2576  df-sbc 2787  df-csb 2880  df-dif 2947  df-un 2949  df-in 2951  df-ss 2958  df-nul 3252  df-pw 3388  df-sn 3408  df-pr 3409  df-op 3411  df-uni 3608  df-int 3643  df-iun 3686  df-br 3792  df-opab 3846  df-mpt 3847  df-tr 3882  df-id 4057  df-iord 4130  df-on 4132  df-suc 4135  df-iom 4341  df-xp 4378  df-rel 4379  df-cnv 4380  df-co 4381  df-dm 4382  df-rn 4383  df-res 4384  df-ima 4385  df-iota 4894  df-fun 4931  df-fn 4932  df-f 4933  df-f1 4934  df-fo 4935  df-f1o 4936  df-fv 4937  df-recs 5950  df-frec 6008
This theorem is referenced by:  frecsuc  6021
  Copyright terms: Public domain W3C validator