Metamath Proof Explorer

Theorem dfrecs2

Description: A quantifier-free definition of recs . (Contributed by Scott Fenton, 17-Jul-2020)

Ref Expression
Assertion dfrecs2 
|- recs ( F ) = U. ( ( Funs i^i ( `' Domain " On ) ) \ dom ( ( `' _E o. Domain ) \ Fix ( `' Apply o. ( FullFun F o. Restrict ) ) ) )

Proof

Step Hyp Ref Expression
1 dfrecs3 
 |-  recs ( F ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
2 elin 
 |-  ( f e. ( Funs i^i ( `' Domain " On ) ) <-> ( f e. Funs /\ f e. ( `' Domain " On ) ) )
3 vex 
 |-  f e. _V
4 3 elfuns 
 |-  ( f e. Funs <-> Fun f )
5 vex 
 |-  x e. _V
6 5 3 brcnv 
 |-  ( x `' Domain f <-> f Domain x )
7 3 5 brdomain 
 |-  ( f Domain x <-> x = dom f )
8 6 7 bitri 
 |-  ( x `' Domain f <-> x = dom f )
9 8 rexbii 
 |-  ( E. x e. On x `' Domain f <-> E. x e. On x = dom f )
10 3 elima 
 |-  ( f e. ( `' Domain " On ) <-> E. x e. On x `' Domain f )
11 risset 
 |-  ( dom f e. On <-> E. x e. On x = dom f )
12 9 10 11 3bitr4i 
 |-  ( f e. ( `' Domain " On ) <-> dom f e. On )
13 4 12 anbi12i 
 |-  ( ( f e. Funs /\ f e. ( `' Domain " On ) ) <-> ( Fun f /\ dom f e. On ) )
14 2 13 bitri 
 |-  ( f e. ( Funs i^i ( `' Domain " On ) ) <-> ( Fun f /\ dom f e. On ) )
15 3 eldm 
 |-  ( 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 
 |-  ( 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 
 |-  y e. _V
18 3 17 brco 
 |-  ( f ( `' _E o. Domain ) y <-> E. x ( f Domain x /\ x `' _E y ) )
19 7 anbi1i 
 |-  ( ( f Domain x /\ x `' _E y ) <-> ( x = dom f /\ x `' _E y ) )
20 19 exbii 
 |-  ( E. x ( f Domain x /\ x `' _E y ) <-> E. x ( x = dom f /\ x `' _E y ) )
21 3 dmex 
 |-  dom f e. _V
22 breq1 
 |-  ( x = dom f -> ( x `' _E y <-> dom f `' _E y ) )
23 21 22 ceqsexv 
 |-  ( E. x ( x = dom f /\ x `' _E y ) <-> dom f `' _E y )
24 20 23 bitri 
 |-  ( E. x ( f Domain x /\ x `' _E y ) <-> dom f `' _E y )
25 21 17 brcnv 
 |-  ( dom f `' _E y <-> y _E dom f )
26 21 epeli 
 |-  ( y _E dom f <-> y e. dom f )
27 25 26 bitri 
 |-  ( dom f `' _E y <-> y e. dom f )
28 18 24 27 3bitri 
 |-  ( f ( `' _E o. Domain ) y <-> y e. dom f )
29 df-br 
 |-  ( f Fix ( `' Apply o. ( FullFun F o. Restrict ) ) y <-> <. f , y >. e. Fix ( `' Apply o. ( FullFun F o. Restrict ) ) )
30 opex 
 |-  <. f , y >. e. _V
31 30 elfix 
 |-  ( <. f , y >. e. Fix ( `' Apply o. ( FullFun F o. Restrict ) ) <-> <. f , y >. ( `' Apply o. ( FullFun F o. Restrict ) ) <. f , y >. )
32 30 30 brco 
 |-  ( <. 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 
 |-  ( ( <. f , y >. ( FullFun F o. Restrict ) x /\ x `' Apply <. f , y >. ) <-> ( x `' Apply <. f , y >. /\ <. f , y >. ( FullFun F o. Restrict ) x ) )
34 5 30 brcnv 
 |-  ( x `' Apply <. f , y >. <-> <. f , y >. Apply x )
35 3 17 5 brapply 
 |-  ( <. f , y >. Apply x <-> x = ( f ` y ) )
36 34 35 bitri 
 |-  ( x `' Apply <. f , y >. <-> x = ( f ` y ) )
37 36 anbi1i 
 |-  ( ( x `' Apply <. f , y >. /\ <. f , y >. ( FullFun F o. Restrict ) x ) <-> ( x = ( f ` y ) /\ <. f , y >. ( FullFun F o. Restrict ) x ) )
38 33 37 bitri 
 |-  ( ( <. f , y >. ( FullFun F o. Restrict ) x /\ x `' Apply <. f , y >. ) <-> ( x = ( f ` y ) /\ <. f , y >. ( FullFun F o. Restrict ) x ) )
39 38 exbii 
 |-  ( 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 
 |-  ( f ` y ) e. _V
41 breq2 
 |-  ( x = ( f ` y ) -> ( <. f , y >. ( FullFun F o. Restrict ) x <-> <. f , y >. ( FullFun F o. Restrict ) ( f ` y ) ) )
42 40 41 ceqsexv 
 |-  ( E. x ( x = ( f ` y ) /\ <. f , y >. ( FullFun F o. Restrict ) x ) <-> <. f , y >. ( FullFun F o. Restrict ) ( f ` y ) )
43 39 42 bitri 
 |-  ( E. x ( <. f , y >. ( FullFun F o. Restrict ) x /\ x `' Apply <. f , y >. ) <-> <. f , y >. ( FullFun F o. Restrict ) ( f ` y ) )
44 30 40 brco 
 |-  ( <. f , y >. ( FullFun F o. Restrict ) ( f ` y ) <-> E. x ( <. f , y >. Restrict x /\ x FullFun F ( f ` y ) ) )
45 3 17 5 brrestrict 
 |-  ( <. f , y >. Restrict x <-> x = ( f |` y ) )
46 45 anbi1i 
 |-  ( ( <. f , y >. Restrict x /\ x FullFun F ( f ` y ) ) <-> ( x = ( f |` y ) /\ x FullFun F ( f ` y ) ) )
47 46 exbii 
 |-  ( E. x ( <. f , y >. Restrict x /\ x FullFun F ( f ` y ) ) <-> E. x ( x = ( f |` y ) /\ x FullFun F ( f ` y ) ) )
48 3 resex 
 |-  ( f |` y ) e. _V
49 breq1 
 |-  ( x = ( f |` y ) -> ( x FullFun F ( f ` y ) <-> ( f |` y ) FullFun F ( f ` y ) ) )
50 48 49 ceqsexv 
 |-  ( E. x ( x = ( f |` y ) /\ x FullFun F ( f ` y ) ) <-> ( f |` y ) FullFun F ( f ` y ) )
51 47 50 bitri 
 |-  ( E. x ( <. f , y >. Restrict x /\ x FullFun F ( f ` y ) ) <-> ( f |` y ) FullFun F ( f ` y ) )
52 48 40 brfullfun 
 |-  ( ( f |` y ) FullFun F ( f ` y ) <-> ( f ` y ) = ( F ` ( f |` y ) ) )
53 44 51 52 3bitri 
 |-  ( <. f , y >. ( FullFun F o. Restrict ) ( f ` y ) <-> ( f ` y ) = ( F ` ( f |` y ) ) )
54 32 43 53 3bitri 
 |-  ( <. f , y >. ( `' Apply o. ( FullFun F o. Restrict ) ) <. f , y >. <-> ( f ` y ) = ( F ` ( f |` y ) ) )
55 29 31 54 3bitri 
 |-  ( f Fix ( `' Apply o. ( FullFun F o. Restrict ) ) y <-> ( f ` y ) = ( F ` ( f |` y ) ) )
56 55 notbii 
 |-  ( -. f Fix ( `' Apply o. ( FullFun F o. Restrict ) ) y <-> -. ( f ` y ) = ( F ` ( f |` y ) ) )
57 28 56 anbi12i 
 |-  ( ( f ( `' _E o. Domain ) y /\ -. f Fix ( `' Apply o. ( FullFun F o. Restrict ) ) y ) <-> ( y e. dom f /\ -. ( f ` y ) = ( F ` ( f |` y ) ) ) )
58 16 57 bitri 
 |-  ( f ( ( `' _E o. Domain ) \ Fix ( `' Apply o. ( FullFun F o. Restrict ) ) ) y <-> ( y e. dom f /\ -. ( f ` y ) = ( F ` ( f |` y ) ) ) )
59 58 exbii 
 |-  ( 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 ) ) ) )
60 15 59 bitri 
 |-  ( 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 
 |-  ( E. y e. dom f -. ( f ` y ) = ( F ` ( f |` y ) ) <-> E. y ( y e. dom f /\ -. ( f ` y ) = ( F ` ( f |` y ) ) ) )
62 rexnal 
 |-  ( E. y e. dom f -. ( f ` y ) = ( F ` ( f |` y ) ) <-> -. A. y e. dom f ( f ` y ) = ( F ` ( f |` y ) ) )
63 60 61 62 3bitr2ri 
 |-  ( -. A. y e. dom f ( f ` y ) = ( F ` ( f |` y ) ) <-> f e. dom ( ( `' _E o. Domain ) \ Fix ( `' Apply o. ( FullFun F o. Restrict ) ) ) )
64 63 con1bii 
 |-  ( -. f e. dom ( ( `' _E o. Domain ) \ Fix ( `' Apply o. ( FullFun F o. Restrict ) ) ) <-> A. y e. dom f ( f ` y ) = ( F ` ( f |` y ) ) )
65 14 64 anbi12i 
 |-  ( ( 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 
 |-  ( ( ( 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 ) ) ) ) )
67 65 66 bitri 
 |-  ( ( 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 
 |-  ( x = dom f -> ( x e. On <-> dom f e. On ) )
69 raleq 
 |-  ( x = dom f -> ( A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) <-> A. y e. dom f ( f ` y ) = ( F ` ( f |` y ) ) ) )
70 68 69 anbi12d 
 |-  ( 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 ) ) ) ) )
71 70 anbi2d 
 |-  ( 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 ) ) ) ) ) )
72 21 71 ceqsexv 
 |-  ( 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 
 |-  ( f Fn x <-> ( Fun f /\ dom f = x ) )
74 eqcom 
 |-  ( dom f = x <-> x = dom f )
75 74 anbi2i 
 |-  ( ( Fun f /\ dom f = x ) <-> ( Fun f /\ x = dom f ) )
76 ancom 
 |-  ( ( Fun f /\ x = dom f ) <-> ( x = dom f /\ Fun f ) )
77 73 75 76 3bitri 
 |-  ( f Fn x <-> ( x = dom f /\ Fun f ) )
78 77 anbi1i 
 |-  ( ( 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 
 |-  ( ( 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 
 |-  ( ( ( 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 ) ) ) ) ) )
81 78 79 80 3bitr3ri 
 |-  ( ( 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 ) ) ) ) )
82 81 exbii 
 |-  ( 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 ) ) ) ) )
83 67 72 82 3bitr2i 
 |-  ( ( 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 
 |-  ( 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 
 |-  ( 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 ) ) ) ) )
86 83 84 85 3bitr4i 
 |-  ( 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 ) ) ) )
87 86 abbi2i 
 |-  ( ( 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 ) ) ) }
88 87 unieqi 
 |-  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 ) ) ) }
89 1 88 eqtr4i 
 |-  recs ( F ) = U. ( ( Funs i^i ( `' Domain " On ) ) \ dom ( ( `' _E o. Domain ) \ Fix ( `' Apply o. ( FullFun F o. Restrict ) ) ) )