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

Theorem dfrecs2 30722
Description: A quantifier-free definition of recs. (Contributed by Scott Fenton, 17-Jul-2020.)
Assertion
Ref Expression
dfrecs2  |- recs ( F )  =  U. (
( Funs  i^i  ( `'Domain " On ) ) 
\  dom  ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  (FullFun F  o. Restrict ) ) ) )

Proof of Theorem dfrecs2
Dummy variables  f  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfrecs3 7102 . 2  |- recs ( F )  =  U. {
f  |  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) ) ) }
2 elin 3649 . . . . . . . . 9  |-  ( f  e.  ( Funs  i^i  ( `'Domain " On ) )  <-> 
( f  e.  Funs  /\  f  e.  ( `'Domain " On ) ) )
3 vex 3083 . . . . . . . . . . 11  |-  f  e. 
_V
43elfuns 30687 . . . . . . . . . 10  |-  ( f  e.  Funs  <->  Fun  f )
5 vex 3083 . . . . . . . . . . . . . 14  |-  x  e. 
_V
65, 3brcnv 5036 . . . . . . . . . . . . 13  |-  ( x `'Domain f  <->  fDomain x )
73, 5brdomain 30705 . . . . . . . . . . . . 13  |-  ( fDomain
x  <->  x  =  dom  f )
86, 7bitri 252 . . . . . . . . . . . 12  |-  ( x `'Domain f  <->  x  =  dom  f )
98rexbii 2924 . . . . . . . . . . 11  |-  ( E. x  e.  On  x `'Domain f  <->  E. x  e.  On  x  =  dom  f )
103elima 5192 . . . . . . . . . . 11  |-  ( f  e.  ( `'Domain " On ) 
<->  E. x  e.  On  x `'Domain f )
11 risset 2950 . . . . . . . . . . 11  |-  ( dom  f  e.  On  <->  E. x  e.  On  x  =  dom  f )
129, 10, 113bitr4i 280 . . . . . . . . . 10  |-  ( f  e.  ( `'Domain " On ) 
<->  dom  f  e.  On )
134, 12anbi12i 701 . . . . . . . . 9  |-  ( ( f  e.  Funs  /\  f  e.  ( `'Domain " On ) )  <->  ( Fun  f  /\  dom  f  e.  On ) )
142, 13bitri 252 . . . . . . . 8  |-  ( f  e.  ( Funs  i^i  ( `'Domain " On ) )  <-> 
( Fun  f  /\  dom  f  e.  On ) )
153eldm 5051 . . . . . . . . . . 11  |-  ( f  e.  dom  ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  (FullFun F  o. Restrict ) ) )  <->  E. y 
f ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  (FullFun F  o. Restrict ) ) ) y )
16 brdif 4474 . . . . . . . . . . . . 13  |-  ( f ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  (FullFun F  o. Restrict ) ) ) y  <->  ( f
( `'  _E  o. Domain ) y  /\  -.  f Fix ( `'Apply  o.  (FullFun F  o. Restrict ) ) y ) )
17 vex 3083 . . . . . . . . . . . . . . . 16  |-  y  e. 
_V
183, 17brco 5024 . . . . . . . . . . . . . . 15  |-  ( f ( `'  _E  o. Domain ) y  <->  E. x ( fDomain
x  /\  x `'  _E  y ) )
197anbi1i 699 . . . . . . . . . . . . . . . . 17  |-  ( ( fDomain x  /\  x `'  _E  y )  <->  ( x  =  dom  f  /\  x `'  _E  y ) )
2019exbii 1712 . . . . . . . . . . . . . . . 16  |-  ( E. x ( fDomain x  /\  x `'  _E  y
)  <->  E. x ( x  =  dom  f  /\  x `'  _E  y
) )
213dmex 6740 . . . . . . . . . . . . . . . . 17  |-  dom  f  e.  _V
22 breq1 4426 . . . . . . . . . . . . . . . . 17  |-  ( x  =  dom  f  -> 
( x `'  _E  y 
<->  dom  f `'  _E  y ) )
2321, 22ceqsexv 3118 . . . . . . . . . . . . . . . 16  |-  ( E. x ( x  =  dom  f  /\  x `'  _E  y )  <->  dom  f `'  _E  y )
2420, 23bitri 252 . . . . . . . . . . . . . . 15  |-  ( E. x ( fDomain x  /\  x `'  _E  y
)  <->  dom  f `'  _E  y )
2521, 17brcnv 5036 . . . . . . . . . . . . . . . 16  |-  ( dom  f `'  _E  y  <->  y  _E  dom  f )
2621epelc 4766 . . . . . . . . . . . . . . . 16  |-  ( y  _E  dom  f  <->  y  e.  dom  f )
2725, 26bitri 252 . . . . . . . . . . . . . . 15  |-  ( dom  f `'  _E  y  <->  y  e.  dom  f )
2818, 24, 273bitri 274 . . . . . . . . . . . . . 14  |-  ( f ( `'  _E  o. Domain ) y  <->  y  e.  dom  f )
29 df-br 4424 . . . . . . . . . . . . . . . 16  |-  ( f Fix ( `'Apply  o.  (FullFun F  o. Restrict ) ) y  <->  <. f ,  y >.  e.  Fix ( `'Apply  o.  (FullFun F  o. Restrict ) ) )
30 opex 4685 . . . . . . . . . . . . . . . . 17  |-  <. f ,  y >.  e.  _V
3130elfix 30675 . . . . . . . . . . . . . . . 16  |-  ( <.
f ,  y >.  e.  Fix ( `'Apply  o.  (FullFun F  o. Restrict ) )  <->  <. f ,  y >. ( `'Apply  o.  (FullFun F  o. Restrict ) ) <.
f ,  y >.
)
3230, 30brco 5024 . . . . . . . . . . . . . . . . 17  |-  ( <.
f ,  y >.
( `'Apply  o.  (FullFun F  o. Restrict ) ) <.
f ,  y >.  <->  E. x ( <. f ,  y >. (FullFun F  o. Restrict ) x  /\  x `'Apply <. f ,  y
>. ) )
33 ancom 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
<. f ,  y >.
(FullFun F  o. Restrict ) x  /\  x `'Apply <. f ,  y >. )  <->  ( x `'Apply <. f ,  y >.  /\  <. f ,  y >. (FullFun F  o. Restrict ) x ) )
345, 30brcnv 5036 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x `'Apply <. f ,  y
>. 
<-> 
<. f ,  y >.Apply x )
353, 17, 5brapply 30710 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( <.
f ,  y >.Apply x 
<->  x  =  ( f `
 y ) )
3634, 35bitri 252 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x `'Apply <. f ,  y
>. 
<->  x  =  ( f `
 y ) )
3736anbi1i 699 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x `'Apply <. f ,  y >.  /\  <. f ,  y >. (FullFun F  o. Restrict ) x )  <-> 
( x  =  ( f `  y )  /\  <. f ,  y
>. (FullFun F  o. Restrict ) x ) )
3833, 37bitri 252 . . . . . . . . . . . . . . . . . . 19  |-  ( (
<. f ,  y >.
(FullFun F  o. Restrict ) x  /\  x `'Apply <. f ,  y >. )  <->  ( x  =  ( f `
 y )  /\  <.
f ,  y >.
(FullFun F  o. Restrict ) x ) )
3938exbii 1712 . . . . . . . . . . . . . . . . . 18  |-  ( E. x ( <. f ,  y >. (FullFun F  o. Restrict ) x  /\  x `'Apply <. f ,  y
>. )  <->  E. x ( x  =  ( f `  y )  /\  <. f ,  y >. (FullFun F  o. Restrict ) x ) )
40 fvex 5891 . . . . . . . . . . . . . . . . . . 19  |-  ( f `
 y )  e. 
_V
41 breq2 4427 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  ( f `  y )  ->  ( <. f ,  y >.
(FullFun F  o. Restrict ) x  <->  <. f ,  y >.
(FullFun F  o. Restrict ) ( f `  y ) ) )
4240, 41ceqsexv 3118 . . . . . . . . . . . . . . . . . 18  |-  ( E. x ( x  =  ( f `  y
)  /\  <. f ,  y >. (FullFun F  o. Restrict ) x )  <->  <. f ,  y
>. (FullFun F  o. Restrict ) ( f `  y ) )
4339, 42bitri 252 . . . . . . . . . . . . . . . . 17  |-  ( E. x ( <. f ,  y >. (FullFun F  o. Restrict ) x  /\  x `'Apply <. f ,  y
>. )  <->  <. f ,  y
>. (FullFun F  o. Restrict ) ( f `  y ) )
4430, 40brco 5024 . . . . . . . . . . . . . . . . . 18  |-  ( <.
f ,  y >.
(FullFun F  o. Restrict ) ( f `  y )  <->  E. x ( <. f ,  y >.Restrict x  /\  xFullFun F ( f `  y ) ) )
453, 17, 5brrestrict 30721 . . . . . . . . . . . . . . . . . . . . 21  |-  ( <.
f ,  y >.Restrict x  <-> 
x  =  ( f  |`  y ) )
4645anbi1i 699 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
<. f ,  y >.Restrict x  /\  xFullFun F ( f `  y ) )  <->  ( x  =  ( f  |`  y
)  /\  xFullFun F ( f `  y ) ) )
4746exbii 1712 . . . . . . . . . . . . . . . . . . 19  |-  ( E. x ( <. f ,  y >.Restrict x  /\  xFullFun F ( f `  y ) )  <->  E. x
( x  =  ( f  |`  y )  /\  xFullFun F ( f `
 y ) ) )
483resex 5167 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  |`  y )  e.  _V
49 breq1 4426 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  ( f  |`  y )  ->  (
xFullFun F ( f `  y )  <->  ( f  |`  y )FullFun F ( f `  y ) ) )
5048, 49ceqsexv 3118 . . . . . . . . . . . . . . . . . . 19  |-  ( E. x ( x  =  ( f  |`  y
)  /\  xFullFun F ( f `  y ) )  <->  ( f  |`  y )FullFun F ( f `
 y ) )
5147, 50bitri 252 . . . . . . . . . . . . . . . . . 18  |-  ( E. x ( <. f ,  y >.Restrict x  /\  xFullFun F ( f `  y ) )  <->  ( f  |`  y )FullFun F ( f `  y ) )
5248, 40brfullfun 30720 . . . . . . . . . . . . . . . . . 18  |-  ( ( f  |`  y )FullFun F ( f `  y
)  <->  ( f `  y )  =  ( F `  ( f  |`  y ) ) )
5344, 51, 523bitri 274 . . . . . . . . . . . . . . . . 17  |-  ( <.
f ,  y >.
(FullFun F  o. Restrict ) ( f `  y )  <-> 
( f `  y
)  =  ( F `
 ( f  |`  y ) ) )
5432, 43, 533bitri 274 . . . . . . . . . . . . . . . 16  |-  ( <.
f ,  y >.
( `'Apply  o.  (FullFun F  o. Restrict ) ) <.
f ,  y >.  <->  ( f `  y )  =  ( F `  ( f  |`  y
) ) )
5529, 31, 543bitri 274 . . . . . . . . . . . . . . 15  |-  ( f Fix ( `'Apply  o.  (FullFun F  o. Restrict ) ) y  <-> 
( f `  y
)  =  ( F `
 ( f  |`  y ) ) )
5655notbii 297 . . . . . . . . . . . . . 14  |-  ( -.  f Fix ( `'Apply 
o.  (FullFun F  o. Restrict ) ) y  <->  -.  ( f `  y )  =  ( F `  ( f  |`  y ) ) )
5728, 56anbi12i 701 . . . . . . . . . . . . 13  |-  ( ( f ( `'  _E  o. Domain ) y  /\  -.  f Fix ( `'Apply  o.  (FullFun F  o. Restrict ) ) y )  <->  ( y  e. 
dom  f  /\  -.  ( f `  y
)  =  ( F `
 ( f  |`  y ) ) ) )
5816, 57bitri 252 . . . . . . . . . . . 12  |-  ( f ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  (FullFun F  o. Restrict ) ) ) y  <->  ( y  e.  dom  f  /\  -.  ( f `  y
)  =  ( F `
 ( f  |`  y ) ) ) )
5958exbii 1712 . . . . . . . . . . 11  |-  ( E. y  f ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  (FullFun F  o. Restrict ) ) ) y  <->  E. y
( y  e.  dom  f  /\  -.  ( f `
 y )  =  ( F `  (
f  |`  y ) ) ) )
6015, 59bitri 252 . . . . . . . . . 10  |-  ( f  e.  dom  ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  (FullFun F  o. Restrict ) ) )  <->  E. y
( y  e.  dom  f  /\  -.  ( f `
 y )  =  ( F `  (
f  |`  y ) ) ) )
61 df-rex 2777 . . . . . . . . . 10  |-  ( E. y  e.  dom  f  -.  ( f `  y
)  =  ( F `
 ( f  |`  y ) )  <->  E. y
( y  e.  dom  f  /\  -.  ( f `
 y )  =  ( F `  (
f  |`  y ) ) ) )
62 rexnal 2870 . . . . . . . . . 10  |-  ( E. y  e.  dom  f  -.  ( f `  y
)  =  ( F `
 ( f  |`  y ) )  <->  -.  A. y  e.  dom  f ( f `
 y )  =  ( F `  (
f  |`  y ) ) )
6360, 61, 623bitr2ri 277 . . . . . . . . 9  |-  ( -. 
A. y  e.  dom  f ( f `  y )  =  ( F `  ( f  |`  y ) )  <->  f  e.  dom  ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  (FullFun F  o. Restrict ) ) ) )
6463con1bii 332 . . . . . . . 8  |-  ( -.  f  e.  dom  (
( `'  _E  o. Domain ) 
\  Fix ( `'Apply  o.  (FullFun F  o. Restrict ) ) )  <->  A. y  e.  dom  f ( f `  y )  =  ( F `  ( f  |`  y ) ) )
6514, 64anbi12i 701 . . . . . . 7  |-  ( ( f  e.  ( Funs 
i^i  ( `'Domain " On ) )  /\  -.  f  e.  dom  ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  (FullFun F  o. Restrict ) ) ) )  <->  ( ( Fun  f  /\  dom  f  e.  On )  /\  A. y  e.  dom  f ( f `  y )  =  ( F `  ( f  |`  y
) ) ) )
66 anass 653 . . . . . . 7  |-  ( ( ( Fun  f  /\  dom  f  e.  On )  /\  A. y  e. 
dom  f ( f `
 y )  =  ( F `  (
f  |`  y ) ) )  <->  ( Fun  f  /\  ( dom  f  e.  On  /\  A. y  e.  dom  f ( f `
 y )  =  ( F `  (
f  |`  y ) ) ) ) )
6765, 66bitri 252 . . . . . 6  |-  ( ( f  e.  ( Funs 
i^i  ( `'Domain " On ) )  /\  -.  f  e.  dom  ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  (FullFun F  o. Restrict ) ) ) )  <->  ( Fun  f  /\  ( dom  f  e.  On  /\  A. y  e.  dom  f ( f `
 y )  =  ( F `  (
f  |`  y ) ) ) ) )
68 eleq1 2495 . . . . . . . . 9  |-  ( x  =  dom  f  -> 
( x  e.  On  <->  dom  f  e.  On ) )
69 raleq 3022 . . . . . . . . 9  |-  ( x  =  dom  f  -> 
( A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) )  <->  A. y  e.  dom  f ( f `
 y )  =  ( F `  (
f  |`  y ) ) ) )
7068, 69anbi12d 715 . . . . . . . 8  |-  ( x  =  dom  f  -> 
( ( x  e.  On  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) ) )  <-> 
( dom  f  e.  On  /\  A. y  e. 
dom  f ( f `
 y )  =  ( F `  (
f  |`  y ) ) ) ) )
7170anbi2d 708 . . . . . . 7  |-  ( x  =  dom  f  -> 
( ( Fun  f  /\  ( x  e.  On  /\ 
A. y  e.  x  ( f `  y
)  =  ( F `
 ( f  |`  y ) ) ) )  <->  ( Fun  f  /\  ( dom  f  e.  On  /\  A. y  e.  dom  f ( f `
 y )  =  ( F `  (
f  |`  y ) ) ) ) ) )
7221, 71ceqsexv 3118 . . . . . 6  |-  ( E. x ( x  =  dom  f  /\  ( Fun  f  /\  (
x  e.  On  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y
) ) ) ) )  <->  ( Fun  f  /\  ( dom  f  e.  On  /\  A. y  e.  dom  f ( f `
 y )  =  ( F `  (
f  |`  y ) ) ) ) )
73 df-fn 5604 . . . . . . . . . 10  |-  ( f  Fn  x  <->  ( Fun  f  /\  dom  f  =  x ) )
74 eqcom 2431 . . . . . . . . . . 11  |-  ( dom  f  =  x  <->  x  =  dom  f )
7574anbi2i 698 . . . . . . . . . 10  |-  ( ( Fun  f  /\  dom  f  =  x )  <->  ( Fun  f  /\  x  =  dom  f ) )
76 ancom 451 . . . . . . . . . 10  |-  ( ( Fun  f  /\  x  =  dom  f )  <->  ( x  =  dom  f  /\  Fun  f ) )
7773, 75, 763bitri 274 . . . . . . . . 9  |-  ( f  Fn  x  <->  ( x  =  dom  f  /\  Fun  f ) )
7877anbi1i 699 . . . . . . . 8  |-  ( ( f  Fn  x  /\  ( x  e.  On  /\ 
A. y  e.  x  ( f `  y
)  =  ( F `
 ( f  |`  y ) ) ) )  <->  ( ( x  =  dom  f  /\  Fun  f )  /\  (
x  e.  On  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y
) ) ) ) )
79 an12 804 . . . . . . . 8  |-  ( ( f  Fn  x  /\  ( x  e.  On  /\ 
A. y  e.  x  ( f `  y
)  =  ( F `
 ( f  |`  y ) ) ) )  <->  ( x  e.  On  /\  ( f  Fn  x  /\  A. y  e.  x  (
f `  y )  =  ( F `  ( f  |`  y
) ) ) ) )
80 anass 653 . . . . . . . 8  |-  ( ( ( x  =  dom  f  /\  Fun  f )  /\  ( x  e.  On  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) ) ) )  <->  ( x  =  dom  f  /\  ( Fun  f  /\  (
x  e.  On  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y
) ) ) ) ) )
8178, 79, 803bitr3ri 279 . . . . . . 7  |-  ( ( x  =  dom  f  /\  ( Fun  f  /\  ( x  e.  On  /\ 
A. y  e.  x  ( f `  y
)  =  ( F `
 ( f  |`  y ) ) ) ) )  <->  ( x  e.  On  /\  ( f  Fn  x  /\  A. y  e.  x  (
f `  y )  =  ( F `  ( f  |`  y
) ) ) ) )
8281exbii 1712 . . . . . 6  |-  ( E. x ( x  =  dom  f  /\  ( Fun  f  /\  (
x  e.  On  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y
) ) ) ) )  <->  E. x ( x  e.  On  /\  (
f  Fn  x  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y
) ) ) ) )
8367, 72, 823bitr2i 276 . . . . 5  |-  ( ( f  e.  ( Funs 
i^i  ( `'Domain " On ) )  /\  -.  f  e.  dom  ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  (FullFun F  o. Restrict ) ) ) )  <->  E. x
( x  e.  On  /\  ( f  Fn  x  /\  A. y  e.  x  ( f `  y
)  =  ( F `
 ( f  |`  y ) ) ) ) )
84 eldif 3446 . . . . 5  |-  ( f  e.  ( ( Funs 
i^i  ( `'Domain " On ) )  \  dom  ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  (FullFun F  o. Restrict ) ) ) )  <->  ( f  e.  ( Funs  i^i  ( `'Domain " On ) )  /\  -.  f  e. 
dom  ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  (FullFun F  o. Restrict ) ) ) ) )
85 df-rex 2777 . . . . 5  |-  ( E. x  e.  On  (
f  Fn  x  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y
) ) )  <->  E. x
( x  e.  On  /\  ( f  Fn  x  /\  A. y  e.  x  ( f `  y
)  =  ( F `
 ( f  |`  y ) ) ) ) )
8683, 84, 853bitr4i 280 . . . 4  |-  ( f  e.  ( ( Funs 
i^i  ( `'Domain " On ) )  \  dom  ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  (FullFun F  o. Restrict ) ) ) )  <->  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y ) ) ) )
8786abbi2i 2550 . . 3  |-  ( (
Funs  i^i  ( `'Domain " On ) )  \  dom  ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  (FullFun F  o. Restrict ) ) ) )  =  { f  |  E. x  e.  On  (
f  Fn  x  /\  A. y  e.  x  ( f `  y )  =  ( F `  ( f  |`  y
) ) ) }
8887unieqi 4228 . 2  |-  U. (
( Funs  i^i  ( `'Domain " On ) ) 
\  dom  ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  (FullFun F  o. Restrict ) ) ) )  = 
U. { f  |  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y
)  =  ( F `
 ( f  |`  y ) ) ) }
891, 88eqtr4i 2454 1  |- recs ( F )  =  U. (
( Funs  i^i  ( `'Domain " On ) ) 
\  dom  ( ( `'  _E  o. Domain )  \  Fix ( `'Apply  o.  (FullFun F  o. Restrict ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    /\ wa 370    = wceq 1437   E.wex 1657    e. wcel 1872   {cab 2407   A.wral 2771   E.wrex 2772    \ cdif 3433    i^i cin 3435   <.cop 4004   U.cuni 4219   class class class wbr 4423    _E cep 4762   `'ccnv 4852   dom cdm 4853    |` cres 4855   "cima 4856    o. ccom 4857   Oncon0 5442   Fun wfun 5595    Fn wfn 5596   ` cfv 5601  recscrecs 7100   Fixcfix 30606   Funscfuns 30608  Domaincdomain 30614  Applycapply 30616  FullFuncfullfn 30621  Restrictcrestrict 30622
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-symdif 3693  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-fo 5607  df-fv 5609  df-1st 6807  df-2nd 6808  df-wrecs 7039  df-recs 7101  df-txp 30625  df-pprod 30626  df-bigcup 30629  df-fix 30630  df-funs 30632  df-singleton 30633  df-singles 30634  df-image 30635  df-cart 30636  df-img 30637  df-domain 30638  df-range 30639  df-cap 30641  df-restrict 30642  df-apply 30644  df-funpart 30645  df-fullfun 30646
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator