This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ackbij2lem2

Description: Lemma for ackbij2 . (Contributed by Stefan O'Rear, 18-Nov-2014)

Ref Expression
Hypotheses ackbij.f 
|- F = ( x e. ( ~P _om i^i Fin ) |-> ( card ` U_ y e. x ( { y } X. ~P y ) ) )
ackbij.g 
|- G = ( x e. _V |-> ( y e. ~P dom x |-> ( F ` ( x " y ) ) ) )
Assertion ackbij2lem2 
|- ( A e. _om -> ( rec ( G , (/) ) ` A ) : ( R1 ` A ) -1-1-onto-> ( card ` ( R1 ` A ) ) )

Proof

Step Hyp Ref Expression
1 ackbij.f 
 |-  F = ( x e. ( ~P _om i^i Fin ) |-> ( card ` U_ y e. x ( { y } X. ~P y ) ) )
2 ackbij.g 
 |-  G = ( x e. _V |-> ( y e. ~P dom x |-> ( F ` ( x " y ) ) ) )
3 fveq2 
 |-  ( a = (/) -> ( rec ( G , (/) ) ` a ) = ( rec ( G , (/) ) ` (/) ) )
4 fveq2 
 |-  ( a = (/) -> ( R1 ` a ) = ( R1 ` (/) ) )
5 2fveq3 
 |-  ( a = (/) -> ( card ` ( R1 ` a ) ) = ( card ` ( R1 ` (/) ) ) )
6 3 4 5 f1oeq123d 
 |-  ( a = (/) -> ( ( rec ( G , (/) ) ` a ) : ( R1 ` a ) -1-1-onto-> ( card ` ( R1 ` a ) ) <-> ( rec ( G , (/) ) ` (/) ) : ( R1 ` (/) ) -1-1-onto-> ( card ` ( R1 ` (/) ) ) ) )
7 fveq2 
 |-  ( a = b -> ( rec ( G , (/) ) ` a ) = ( rec ( G , (/) ) ` b ) )
8 fveq2 
 |-  ( a = b -> ( R1 ` a ) = ( R1 ` b ) )
9 2fveq3 
 |-  ( a = b -> ( card ` ( R1 ` a ) ) = ( card ` ( R1 ` b ) ) )
10 7 8 9 f1oeq123d 
 |-  ( a = b -> ( ( rec ( G , (/) ) ` a ) : ( R1 ` a ) -1-1-onto-> ( card ` ( R1 ` a ) ) <-> ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) ) )
11 fveq2 
 |-  ( a = suc b -> ( rec ( G , (/) ) ` a ) = ( rec ( G , (/) ) ` suc b ) )
12 fveq2 
 |-  ( a = suc b -> ( R1 ` a ) = ( R1 ` suc b ) )
13 2fveq3 
 |-  ( a = suc b -> ( card ` ( R1 ` a ) ) = ( card ` ( R1 ` suc b ) ) )
14 11 12 13 f1oeq123d 
 |-  ( a = suc b -> ( ( rec ( G , (/) ) ` a ) : ( R1 ` a ) -1-1-onto-> ( card ` ( R1 ` a ) ) <-> ( rec ( G , (/) ) ` suc b ) : ( R1 ` suc b ) -1-1-onto-> ( card ` ( R1 ` suc b ) ) ) )
15 fveq2 
 |-  ( a = A -> ( rec ( G , (/) ) ` a ) = ( rec ( G , (/) ) ` A ) )
16 fveq2 
 |-  ( a = A -> ( R1 ` a ) = ( R1 ` A ) )
17 2fveq3 
 |-  ( a = A -> ( card ` ( R1 ` a ) ) = ( card ` ( R1 ` A ) ) )
18 15 16 17 f1oeq123d 
 |-  ( a = A -> ( ( rec ( G , (/) ) ` a ) : ( R1 ` a ) -1-1-onto-> ( card ` ( R1 ` a ) ) <-> ( rec ( G , (/) ) ` A ) : ( R1 ` A ) -1-1-onto-> ( card ` ( R1 ` A ) ) ) )
19 f1o0 
 |-  (/) : (/) -1-1-onto-> (/)
20 0ex 
 |-  (/) e. _V
21 20 rdg0 
 |-  ( rec ( G , (/) ) ` (/) ) = (/)
22 f1oeq1 
 |-  ( ( rec ( G , (/) ) ` (/) ) = (/) -> ( ( rec ( G , (/) ) ` (/) ) : ( R1 ` (/) ) -1-1-onto-> ( card ` ( R1 ` (/) ) ) <-> (/) : ( R1 ` (/) ) -1-1-onto-> ( card ` ( R1 ` (/) ) ) ) )
23 21 22 ax-mp 
 |-  ( ( rec ( G , (/) ) ` (/) ) : ( R1 ` (/) ) -1-1-onto-> ( card ` ( R1 ` (/) ) ) <-> (/) : ( R1 ` (/) ) -1-1-onto-> ( card ` ( R1 ` (/) ) ) )
24 r10 
 |-  ( R1 ` (/) ) = (/)
25 24 fveq2i 
 |-  ( card ` ( R1 ` (/) ) ) = ( card ` (/) )
26 card0 
 |-  ( card ` (/) ) = (/)
27 25 26 eqtri 
 |-  ( card ` ( R1 ` (/) ) ) = (/)
28 f1oeq23 
 |-  ( ( ( R1 ` (/) ) = (/) /\ ( card ` ( R1 ` (/) ) ) = (/) ) -> ( (/) : ( R1 ` (/) ) -1-1-onto-> ( card ` ( R1 ` (/) ) ) <-> (/) : (/) -1-1-onto-> (/) ) )
29 24 27 28 mp2an 
 |-  ( (/) : ( R1 ` (/) ) -1-1-onto-> ( card ` ( R1 ` (/) ) ) <-> (/) : (/) -1-1-onto-> (/) )
30 23 29 bitri 
 |-  ( ( rec ( G , (/) ) ` (/) ) : ( R1 ` (/) ) -1-1-onto-> ( card ` ( R1 ` (/) ) ) <-> (/) : (/) -1-1-onto-> (/) )
31 19 30 mpbir 
 |-  ( rec ( G , (/) ) ` (/) ) : ( R1 ` (/) ) -1-1-onto-> ( card ` ( R1 ` (/) ) )
32 1 ackbij1lem17 
 |-  F : ( ~P _om i^i Fin ) -1-1-> _om
33 32 a1i 
 |-  ( b e. _om -> F : ( ~P _om i^i Fin ) -1-1-> _om )
34 r1fin 
 |-  ( b e. _om -> ( R1 ` b ) e. Fin )
35 ficardom 
 |-  ( ( R1 ` b ) e. Fin -> ( card ` ( R1 ` b ) ) e. _om )
36 34 35 syl 
 |-  ( b e. _om -> ( card ` ( R1 ` b ) ) e. _om )
37 ackbij2lem1 
 |-  ( ( card ` ( R1 ` b ) ) e. _om -> ~P ( card ` ( R1 ` b ) ) C_ ( ~P _om i^i Fin ) )
38 36 37 syl 
 |-  ( b e. _om -> ~P ( card ` ( R1 ` b ) ) C_ ( ~P _om i^i Fin ) )
39 f1ores 
 |-  ( ( F : ( ~P _om i^i Fin ) -1-1-> _om /\ ~P ( card ` ( R1 ` b ) ) C_ ( ~P _om i^i Fin ) ) -> ( F |` ~P ( card ` ( R1 ` b ) ) ) : ~P ( card ` ( R1 ` b ) ) -1-1-onto-> ( F " ~P ( card ` ( R1 ` b ) ) ) )
40 33 38 39 syl2anc 
 |-  ( b e. _om -> ( F |` ~P ( card ` ( R1 ` b ) ) ) : ~P ( card ` ( R1 ` b ) ) -1-1-onto-> ( F " ~P ( card ` ( R1 ` b ) ) ) )
41 1 ackbij1b 
 |-  ( ( card ` ( R1 ` b ) ) e. _om -> ( F " ~P ( card ` ( R1 ` b ) ) ) = ( card ` ~P ( card ` ( R1 ` b ) ) ) )
42 36 41 syl 
 |-  ( b e. _om -> ( F " ~P ( card ` ( R1 ` b ) ) ) = ( card ` ~P ( card ` ( R1 ` b ) ) ) )
43 ficardid 
 |-  ( ( R1 ` b ) e. Fin -> ( card ` ( R1 ` b ) ) ~~ ( R1 ` b ) )
44 pwen 
 |-  ( ( card ` ( R1 ` b ) ) ~~ ( R1 ` b ) -> ~P ( card ` ( R1 ` b ) ) ~~ ~P ( R1 ` b ) )
45 carden2b 
 |-  ( ~P ( card ` ( R1 ` b ) ) ~~ ~P ( R1 ` b ) -> ( card ` ~P ( card ` ( R1 ` b ) ) ) = ( card ` ~P ( R1 ` b ) ) )
46 34 43 44 45 4syl 
 |-  ( b e. _om -> ( card ` ~P ( card ` ( R1 ` b ) ) ) = ( card ` ~P ( R1 ` b ) ) )
47 42 46 eqtrd 
 |-  ( b e. _om -> ( F " ~P ( card ` ( R1 ` b ) ) ) = ( card ` ~P ( R1 ` b ) ) )
48 47 f1oeq3d 
 |-  ( b e. _om -> ( ( F |` ~P ( card ` ( R1 ` b ) ) ) : ~P ( card ` ( R1 ` b ) ) -1-1-onto-> ( F " ~P ( card ` ( R1 ` b ) ) ) <-> ( F |` ~P ( card ` ( R1 ` b ) ) ) : ~P ( card ` ( R1 ` b ) ) -1-1-onto-> ( card ` ~P ( R1 ` b ) ) ) )
49 40 48 mpbid 
 |-  ( b e. _om -> ( F |` ~P ( card ` ( R1 ` b ) ) ) : ~P ( card ` ( R1 ` b ) ) -1-1-onto-> ( card ` ~P ( R1 ` b ) ) )
50 49 adantr 
 |-  ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) ) -> ( F |` ~P ( card ` ( R1 ` b ) ) ) : ~P ( card ` ( R1 ` b ) ) -1-1-onto-> ( card ` ~P ( R1 ` b ) ) )
51 f1opw 
 |-  ( ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) -> ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) : ~P ( R1 ` b ) -1-1-onto-> ~P ( card ` ( R1 ` b ) ) )
52 51 adantl 
 |-  ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) ) -> ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) : ~P ( R1 ` b ) -1-1-onto-> ~P ( card ` ( R1 ` b ) ) )
53 f1oco 
 |-  ( ( ( F |` ~P ( card ` ( R1 ` b ) ) ) : ~P ( card ` ( R1 ` b ) ) -1-1-onto-> ( card ` ~P ( R1 ` b ) ) /\ ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) : ~P ( R1 ` b ) -1-1-onto-> ~P ( card ` ( R1 ` b ) ) ) -> ( ( F |` ~P ( card ` ( R1 ` b ) ) ) o. ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ) : ~P ( R1 ` b ) -1-1-onto-> ( card ` ~P ( R1 ` b ) ) )
54 50 52 53 syl2anc 
 |-  ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) ) -> ( ( F |` ~P ( card ` ( R1 ` b ) ) ) o. ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ) : ~P ( R1 ` b ) -1-1-onto-> ( card ` ~P ( R1 ` b ) ) )
55 frsuc 
 |-  ( b e. _om -> ( ( rec ( G , (/) ) |` _om ) ` suc b ) = ( G ` ( ( rec ( G , (/) ) |` _om ) ` b ) ) )
56 peano2 
 |-  ( b e. _om -> suc b e. _om )
57 56 fvresd 
 |-  ( b e. _om -> ( ( rec ( G , (/) ) |` _om ) ` suc b ) = ( rec ( G , (/) ) ` suc b ) )
58 fvres 
 |-  ( b e. _om -> ( ( rec ( G , (/) ) |` _om ) ` b ) = ( rec ( G , (/) ) ` b ) )
59 58 fveq2d 
 |-  ( b e. _om -> ( G ` ( ( rec ( G , (/) ) |` _om ) ` b ) ) = ( G ` ( rec ( G , (/) ) ` b ) ) )
60 fvex 
 |-  ( rec ( G , (/) ) ` b ) e. _V
61 dmeq 
 |-  ( x = ( rec ( G , (/) ) ` b ) -> dom x = dom ( rec ( G , (/) ) ` b ) )
62 61 pweqd 
 |-  ( x = ( rec ( G , (/) ) ` b ) -> ~P dom x = ~P dom ( rec ( G , (/) ) ` b ) )
63 imaeq1 
 |-  ( x = ( rec ( G , (/) ) ` b ) -> ( x " y ) = ( ( rec ( G , (/) ) ` b ) " y ) )
64 63 fveq2d 
 |-  ( x = ( rec ( G , (/) ) ` b ) -> ( F ` ( x " y ) ) = ( F ` ( ( rec ( G , (/) ) ` b ) " y ) ) )
65 62 64 mpteq12dv 
 |-  ( x = ( rec ( G , (/) ) ` b ) -> ( y e. ~P dom x |-> ( F ` ( x " y ) ) ) = ( y e. ~P dom ( rec ( G , (/) ) ` b ) |-> ( F ` ( ( rec ( G , (/) ) ` b ) " y ) ) ) )
66 60 dmex 
 |-  dom ( rec ( G , (/) ) ` b ) e. _V
67 66 pwex 
 |-  ~P dom ( rec ( G , (/) ) ` b ) e. _V
68 67 mptex 
 |-  ( y e. ~P dom ( rec ( G , (/) ) ` b ) |-> ( F ` ( ( rec ( G , (/) ) ` b ) " y ) ) ) e. _V
69 65 2 68 fvmpt 
 |-  ( ( rec ( G , (/) ) ` b ) e. _V -> ( G ` ( rec ( G , (/) ) ` b ) ) = ( y e. ~P dom ( rec ( G , (/) ) ` b ) |-> ( F ` ( ( rec ( G , (/) ) ` b ) " y ) ) ) )
70 60 69 ax-mp 
 |-  ( G ` ( rec ( G , (/) ) ` b ) ) = ( y e. ~P dom ( rec ( G , (/) ) ` b ) |-> ( F ` ( ( rec ( G , (/) ) ` b ) " y ) ) )
71 59 70 eqtrdi 
 |-  ( b e. _om -> ( G ` ( ( rec ( G , (/) ) |` _om ) ` b ) ) = ( y e. ~P dom ( rec ( G , (/) ) ` b ) |-> ( F ` ( ( rec ( G , (/) ) ` b ) " y ) ) ) )
72 55 57 71 3eqtr3d 
 |-  ( b e. _om -> ( rec ( G , (/) ) ` suc b ) = ( y e. ~P dom ( rec ( G , (/) ) ` b ) |-> ( F ` ( ( rec ( G , (/) ) ` b ) " y ) ) ) )
73 72 adantr 
 |-  ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) ) -> ( rec ( G , (/) ) ` suc b ) = ( y e. ~P dom ( rec ( G , (/) ) ` b ) |-> ( F ` ( ( rec ( G , (/) ) ` b ) " y ) ) ) )
74 f1odm 
 |-  ( ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) -> dom ( rec ( G , (/) ) ` b ) = ( R1 ` b ) )
75 74 adantl 
 |-  ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) ) -> dom ( rec ( G , (/) ) ` b ) = ( R1 ` b ) )
76 75 pweqd 
 |-  ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) ) -> ~P dom ( rec ( G , (/) ) ` b ) = ~P ( R1 ` b ) )
77 76 mpteq1d 
 |-  ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) ) -> ( y e. ~P dom ( rec ( G , (/) ) ` b ) |-> ( F ` ( ( rec ( G , (/) ) ` b ) " y ) ) ) = ( y e. ~P ( R1 ` b ) |-> ( F ` ( ( rec ( G , (/) ) ` b ) " y ) ) ) )
78 fvex 
 |-  ( F ` ( ( rec ( G , (/) ) ` b ) " y ) ) e. _V
79 eqid 
 |-  ( y e. ~P ( R1 ` b ) |-> ( F ` ( ( rec ( G , (/) ) ` b ) " y ) ) ) = ( y e. ~P ( R1 ` b ) |-> ( F ` ( ( rec ( G , (/) ) ` b ) " y ) ) )
80 78 79 fnmpti 
 |-  ( y e. ~P ( R1 ` b ) |-> ( F ` ( ( rec ( G , (/) ) ` b ) " y ) ) ) Fn ~P ( R1 ` b )
81 80 a1i 
 |-  ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) ) -> ( y e. ~P ( R1 ` b ) |-> ( F ` ( ( rec ( G , (/) ) ` b ) " y ) ) ) Fn ~P ( R1 ` b ) )
82 f1ofn 
 |-  ( ( ( F |` ~P ( card ` ( R1 ` b ) ) ) o. ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ) : ~P ( R1 ` b ) -1-1-onto-> ( card ` ~P ( R1 ` b ) ) -> ( ( F |` ~P ( card ` ( R1 ` b ) ) ) o. ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ) Fn ~P ( R1 ` b ) )
83 54 82 syl 
 |-  ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) ) -> ( ( F |` ~P ( card ` ( R1 ` b ) ) ) o. ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ) Fn ~P ( R1 ` b ) )
84 f1of 
 |-  ( ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) : ~P ( R1 ` b ) -1-1-onto-> ~P ( card ` ( R1 ` b ) ) -> ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) : ~P ( R1 ` b ) --> ~P ( card ` ( R1 ` b ) ) )
85 52 84 syl 
 |-  ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) ) -> ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) : ~P ( R1 ` b ) --> ~P ( card ` ( R1 ` b ) ) )
86 85 ffvelcdmda 
 |-  ( ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) ) /\ c e. ~P ( R1 ` b ) ) -> ( ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ` c ) e. ~P ( card ` ( R1 ` b ) ) )
87 86 fvresd 
 |-  ( ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) ) /\ c e. ~P ( R1 ` b ) ) -> ( ( F |` ~P ( card ` ( R1 ` b ) ) ) ` ( ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ` c ) ) = ( F ` ( ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ` c ) ) )
88 imaeq2 
 |-  ( a = c -> ( ( rec ( G , (/) ) ` b ) " a ) = ( ( rec ( G , (/) ) ` b ) " c ) )
89 eqid 
 |-  ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) = ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) )
90 60 imaex 
 |-  ( ( rec ( G , (/) ) ` b ) " c ) e. _V
91 88 89 90 fvmpt 
 |-  ( c e. ~P ( R1 ` b ) -> ( ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ` c ) = ( ( rec ( G , (/) ) ` b ) " c ) )
92 91 adantl 
 |-  ( ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) ) /\ c e. ~P ( R1 ` b ) ) -> ( ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ` c ) = ( ( rec ( G , (/) ) ` b ) " c ) )
93 92 fveq2d 
 |-  ( ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) ) /\ c e. ~P ( R1 ` b ) ) -> ( F ` ( ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ` c ) ) = ( F ` ( ( rec ( G , (/) ) ` b ) " c ) ) )
94 87 93 eqtrd 
 |-  ( ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) ) /\ c e. ~P ( R1 ` b ) ) -> ( ( F |` ~P ( card ` ( R1 ` b ) ) ) ` ( ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ` c ) ) = ( F ` ( ( rec ( G , (/) ) ` b ) " c ) ) )
95 fvco3 
 |-  ( ( ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) : ~P ( R1 ` b ) --> ~P ( card ` ( R1 ` b ) ) /\ c e. ~P ( R1 ` b ) ) -> ( ( ( F |` ~P ( card ` ( R1 ` b ) ) ) o. ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ) ` c ) = ( ( F |` ~P ( card ` ( R1 ` b ) ) ) ` ( ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ` c ) ) )
96 85 95 sylan 
 |-  ( ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) ) /\ c e. ~P ( R1 ` b ) ) -> ( ( ( F |` ~P ( card ` ( R1 ` b ) ) ) o. ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ) ` c ) = ( ( F |` ~P ( card ` ( R1 ` b ) ) ) ` ( ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ` c ) ) )
97 imaeq2 
 |-  ( y = c -> ( ( rec ( G , (/) ) ` b ) " y ) = ( ( rec ( G , (/) ) ` b ) " c ) )
98 97 fveq2d 
 |-  ( y = c -> ( F ` ( ( rec ( G , (/) ) ` b ) " y ) ) = ( F ` ( ( rec ( G , (/) ) ` b ) " c ) ) )
99 fvex 
 |-  ( F ` ( ( rec ( G , (/) ) ` b ) " c ) ) e. _V
100 98 79 99 fvmpt 
 |-  ( c e. ~P ( R1 ` b ) -> ( ( y e. ~P ( R1 ` b ) |-> ( F ` ( ( rec ( G , (/) ) ` b ) " y ) ) ) ` c ) = ( F ` ( ( rec ( G , (/) ) ` b ) " c ) ) )
101 100 adantl 
 |-  ( ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) ) /\ c e. ~P ( R1 ` b ) ) -> ( ( y e. ~P ( R1 ` b ) |-> ( F ` ( ( rec ( G , (/) ) ` b ) " y ) ) ) ` c ) = ( F ` ( ( rec ( G , (/) ) ` b ) " c ) ) )
102 94 96 101 3eqtr4rd 
 |-  ( ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) ) /\ c e. ~P ( R1 ` b ) ) -> ( ( y e. ~P ( R1 ` b ) |-> ( F ` ( ( rec ( G , (/) ) ` b ) " y ) ) ) ` c ) = ( ( ( F |` ~P ( card ` ( R1 ` b ) ) ) o. ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ) ` c ) )
103 81 83 102 eqfnfvd 
 |-  ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) ) -> ( y e. ~P ( R1 ` b ) |-> ( F ` ( ( rec ( G , (/) ) ` b ) " y ) ) ) = ( ( F |` ~P ( card ` ( R1 ` b ) ) ) o. ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ) )
104 77 103 eqtrd 
 |-  ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) ) -> ( y e. ~P dom ( rec ( G , (/) ) ` b ) |-> ( F ` ( ( rec ( G , (/) ) ` b ) " y ) ) ) = ( ( F |` ~P ( card ` ( R1 ` b ) ) ) o. ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ) )
105 73 104 eqtrd 
 |-  ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) ) -> ( rec ( G , (/) ) ` suc b ) = ( ( F |` ~P ( card ` ( R1 ` b ) ) ) o. ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ) )
106 f1oeq1 
 |-  ( ( rec ( G , (/) ) ` suc b ) = ( ( F |` ~P ( card ` ( R1 ` b ) ) ) o. ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ) -> ( ( rec ( G , (/) ) ` suc b ) : ( R1 ` suc b ) -1-1-onto-> ( card ` ( R1 ` suc b ) ) <-> ( ( F |` ~P ( card ` ( R1 ` b ) ) ) o. ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ) : ( R1 ` suc b ) -1-1-onto-> ( card ` ( R1 ` suc b ) ) ) )
107 105 106 syl 
 |-  ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) ) -> ( ( rec ( G , (/) ) ` suc b ) : ( R1 ` suc b ) -1-1-onto-> ( card ` ( R1 ` suc b ) ) <-> ( ( F |` ~P ( card ` ( R1 ` b ) ) ) o. ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ) : ( R1 ` suc b ) -1-1-onto-> ( card ` ( R1 ` suc b ) ) ) )
108 nnon 
 |-  ( b e. _om -> b e. On )
109 r1suc 
 |-  ( b e. On -> ( R1 ` suc b ) = ~P ( R1 ` b ) )
110 108 109 syl 
 |-  ( b e. _om -> ( R1 ` suc b ) = ~P ( R1 ` b ) )
111 110 fveq2d 
 |-  ( b e. _om -> ( card ` ( R1 ` suc b ) ) = ( card ` ~P ( R1 ` b ) ) )
112 f1oeq23 
 |-  ( ( ( R1 ` suc b ) = ~P ( R1 ` b ) /\ ( card ` ( R1 ` suc b ) ) = ( card ` ~P ( R1 ` b ) ) ) -> ( ( ( F |` ~P ( card ` ( R1 ` b ) ) ) o. ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ) : ( R1 ` suc b ) -1-1-onto-> ( card ` ( R1 ` suc b ) ) <-> ( ( F |` ~P ( card ` ( R1 ` b ) ) ) o. ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ) : ~P ( R1 ` b ) -1-1-onto-> ( card ` ~P ( R1 ` b ) ) ) )
113 110 111 112 syl2anc 
 |-  ( b e. _om -> ( ( ( F |` ~P ( card ` ( R1 ` b ) ) ) o. ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ) : ( R1 ` suc b ) -1-1-onto-> ( card ` ( R1 ` suc b ) ) <-> ( ( F |` ~P ( card ` ( R1 ` b ) ) ) o. ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ) : ~P ( R1 ` b ) -1-1-onto-> ( card ` ~P ( R1 ` b ) ) ) )
114 113 adantr 
 |-  ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) ) -> ( ( ( F |` ~P ( card ` ( R1 ` b ) ) ) o. ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ) : ( R1 ` suc b ) -1-1-onto-> ( card ` ( R1 ` suc b ) ) <-> ( ( F |` ~P ( card ` ( R1 ` b ) ) ) o. ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ) : ~P ( R1 ` b ) -1-1-onto-> ( card ` ~P ( R1 ` b ) ) ) )
115 107 114 bitrd 
 |-  ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) ) -> ( ( rec ( G , (/) ) ` suc b ) : ( R1 ` suc b ) -1-1-onto-> ( card ` ( R1 ` suc b ) ) <-> ( ( F |` ~P ( card ` ( R1 ` b ) ) ) o. ( a e. ~P ( R1 ` b ) |-> ( ( rec ( G , (/) ) ` b ) " a ) ) ) : ~P ( R1 ` b ) -1-1-onto-> ( card ` ~P ( R1 ` b ) ) ) )
116 54 115 mpbird 
 |-  ( ( b e. _om /\ ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) ) -> ( rec ( G , (/) ) ` suc b ) : ( R1 ` suc b ) -1-1-onto-> ( card ` ( R1 ` suc b ) ) )
117 116 ex 
 |-  ( b e. _om -> ( ( rec ( G , (/) ) ` b ) : ( R1 ` b ) -1-1-onto-> ( card ` ( R1 ` b ) ) -> ( rec ( G , (/) ) ` suc b ) : ( R1 ` suc b ) -1-1-onto-> ( card ` ( R1 ` suc b ) ) ) )
118 6 10 14 18 31 117 finds 
 |-  ( A e. _om -> ( rec ( G , (/) ) ` A ) : ( R1 ` A ) -1-1-onto-> ( card ` ( R1 ` A ) ) )