Metamath Proof Explorer

Theorem ackbij2lem3

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

Ref Expression
Hypotheses ackbij.f ⊢F=x∈𝒫ω∩Fin⟼card⁡⋃y∈xy×𝒫y
ackbij.g ⊢G=x∈V⟼y∈𝒫dom⁡x⟼F⁡xy
Assertion ackbij2lem3 ⊢A∈ω→rec⁡G∅⁡A⊆rec⁡G∅⁡suc⁡A

Proof

Step Hyp Ref Expression
1 ackbij.f ⊢F=x∈𝒫ω∩Fin⟼card⁡⋃y∈xy×𝒫y
2 ackbij.g ⊢G=x∈V⟼y∈𝒫dom⁡x⟼F⁡xy
3 fveq2 ⊢a=∅→rec⁡G∅⁡a=rec⁡G∅⁡∅
4 suceq ⊢a=∅→suc⁡a=suc⁡∅
5 4 fveq2d ⊢a=∅→rec⁡G∅⁡suc⁡a=rec⁡G∅⁡suc⁡∅
6 fveq2 ⊢a=∅→R1⁡a=R1⁡∅
7 5 6 reseq12d ⊢a=∅→rec⁡G∅⁡suc⁡a↾R1⁡a=rec⁡G∅⁡suc⁡∅↾R1⁡∅
8 3 7 eqeq12d ⊢a=∅→rec⁡G∅⁡a=rec⁡G∅⁡suc⁡a↾R1⁡a↔rec⁡G∅⁡∅=rec⁡G∅⁡suc⁡∅↾R1⁡∅
9 fveq2 ⊢a=b→rec⁡G∅⁡a=rec⁡G∅⁡b
10 suceq ⊢a=b→suc⁡a=suc⁡b
11 10 fveq2d ⊢a=b→rec⁡G∅⁡suc⁡a=rec⁡G∅⁡suc⁡b
12 fveq2 ⊢a=b→R1⁡a=R1⁡b
13 11 12 reseq12d ⊢a=b→rec⁡G∅⁡suc⁡a↾R1⁡a=rec⁡G∅⁡suc⁡b↾R1⁡b
14 9 13 eqeq12d ⊢a=b→rec⁡G∅⁡a=rec⁡G∅⁡suc⁡a↾R1⁡a↔rec⁡G∅⁡b=rec⁡G∅⁡suc⁡b↾R1⁡b
15 fveq2 ⊢a=suc⁡b→rec⁡G∅⁡a=rec⁡G∅⁡suc⁡b
16 suceq ⊢a=suc⁡b→suc⁡a=suc⁡suc⁡b
17 16 fveq2d ⊢a=suc⁡b→rec⁡G∅⁡suc⁡a=rec⁡G∅⁡suc⁡suc⁡b
18 fveq2 ⊢a=suc⁡b→R1⁡a=R1⁡suc⁡b
19 17 18 reseq12d ⊢a=suc⁡b→rec⁡G∅⁡suc⁡a↾R1⁡a=rec⁡G∅⁡suc⁡suc⁡b↾R1⁡suc⁡b
20 15 19 eqeq12d ⊢a=suc⁡b→rec⁡G∅⁡a=rec⁡G∅⁡suc⁡a↾R1⁡a↔rec⁡G∅⁡suc⁡b=rec⁡G∅⁡suc⁡suc⁡b↾R1⁡suc⁡b
21 fveq2 ⊢a=A→rec⁡G∅⁡a=rec⁡G∅⁡A
22 suceq ⊢a=A→suc⁡a=suc⁡A
23 22 fveq2d ⊢a=A→rec⁡G∅⁡suc⁡a=rec⁡G∅⁡suc⁡A
24 fveq2 ⊢a=A→R1⁡a=R1⁡A
25 23 24 reseq12d ⊢a=A→rec⁡G∅⁡suc⁡a↾R1⁡a=rec⁡G∅⁡suc⁡A↾R1⁡A
26 21 25 eqeq12d ⊢a=A→rec⁡G∅⁡a=rec⁡G∅⁡suc⁡a↾R1⁡a↔rec⁡G∅⁡A=rec⁡G∅⁡suc⁡A↾R1⁡A
27 res0 ⊢rec⁡G∅⁡suc⁡∅↾∅=∅
28 r10 ⊢R1⁡∅=∅
29 28 reseq2i ⊢rec⁡G∅⁡suc⁡∅↾R1⁡∅=rec⁡G∅⁡suc⁡∅↾∅
30 0ex ⊢∅∈V
31 30 rdg0 ⊢rec⁡G∅⁡∅=∅
32 27 29 31 3eqtr4ri ⊢rec⁡G∅⁡∅=rec⁡G∅⁡suc⁡∅↾R1⁡∅
33 peano2 ⊢b∈ω→suc⁡b∈ω
34 1 2 ackbij2lem2 ⊢suc⁡b∈ω→rec⁡G∅⁡suc⁡b:R1⁡suc⁡b⟶1-1 ontocard⁡R1⁡suc⁡b
35 33 34 syl ⊢b∈ω→rec⁡G∅⁡suc⁡b:R1⁡suc⁡b⟶1-1 ontocard⁡R1⁡suc⁡b
36 f1ofn ⊢rec⁡G∅⁡suc⁡b:R1⁡suc⁡b⟶1-1 ontocard⁡R1⁡suc⁡b→rec⁡G∅⁡suc⁡bFnR1⁡suc⁡b
37 35 36 syl ⊢b∈ω→rec⁡G∅⁡suc⁡bFnR1⁡suc⁡b
38 37 adantr ⊢b∈ω∧rec⁡G∅⁡b=rec⁡G∅⁡suc⁡b↾R1⁡b→rec⁡G∅⁡suc⁡bFnR1⁡suc⁡b
39 peano2 ⊢suc⁡b∈ω→suc⁡suc⁡b∈ω
40 1 2 ackbij2lem2 ⊢suc⁡suc⁡b∈ω→rec⁡G∅⁡suc⁡suc⁡b:R1⁡suc⁡suc⁡b⟶1-1 ontocard⁡R1⁡suc⁡suc⁡b
41 f1ofn ⊢rec⁡G∅⁡suc⁡suc⁡b:R1⁡suc⁡suc⁡b⟶1-1 ontocard⁡R1⁡suc⁡suc⁡b→rec⁡G∅⁡suc⁡suc⁡bFnR1⁡suc⁡suc⁡b
42 33 39 40 41 4syl ⊢b∈ω→rec⁡G∅⁡suc⁡suc⁡bFnR1⁡suc⁡suc⁡b
43 nnon ⊢suc⁡b∈ω→suc⁡b∈On
44 33 43 syl ⊢b∈ω→suc⁡b∈On
45 r1sssuc ⊢suc⁡b∈On→R1⁡suc⁡b⊆R1⁡suc⁡suc⁡b
46 44 45 syl ⊢b∈ω→R1⁡suc⁡b⊆R1⁡suc⁡suc⁡b
47 fnssres ⊢rec⁡G∅⁡suc⁡suc⁡bFnR1⁡suc⁡suc⁡b∧R1⁡suc⁡b⊆R1⁡suc⁡suc⁡b→rec⁡G∅⁡suc⁡suc⁡b↾R1⁡suc⁡bFnR1⁡suc⁡b
48 42 46 47 syl2anc ⊢b∈ω→rec⁡G∅⁡suc⁡suc⁡b↾R1⁡suc⁡bFnR1⁡suc⁡b
49 48 adantr ⊢b∈ω∧rec⁡G∅⁡b=rec⁡G∅⁡suc⁡b↾R1⁡b→rec⁡G∅⁡suc⁡suc⁡b↾R1⁡suc⁡bFnR1⁡suc⁡b
50 nnon ⊢b∈ω→b∈On
51 r1suc ⊢b∈On→R1⁡suc⁡b=𝒫R1⁡b
52 50 51 syl ⊢b∈ω→R1⁡suc⁡b=𝒫R1⁡b
53 52 eleq2d ⊢b∈ω→c∈R1⁡suc⁡b↔c∈𝒫R1⁡b
54 53 biimpa ⊢b∈ω∧c∈R1⁡suc⁡b→c∈𝒫R1⁡b
55 54 elpwid ⊢b∈ω∧c∈R1⁡suc⁡b→c⊆R1⁡b
56 resima2 ⊢c⊆R1⁡b→rec⁡G∅⁡suc⁡b↾R1⁡bc=rec⁡G∅⁡suc⁡bc
57 55 56 syl ⊢b∈ω∧c∈R1⁡suc⁡b→rec⁡G∅⁡suc⁡b↾R1⁡bc=rec⁡G∅⁡suc⁡bc
58 57 fveq2d ⊢b∈ω∧c∈R1⁡suc⁡b→F⁡rec⁡G∅⁡suc⁡b↾R1⁡bc=F⁡rec⁡G∅⁡suc⁡bc
59 fvex ⊢rec⁡G∅⁡suc⁡b∈V
60 59 resex ⊢rec⁡G∅⁡suc⁡b↾R1⁡b∈V
61 dmeq ⊢x=rec⁡G∅⁡suc⁡b↾R1⁡b→dom⁡x=dom⁡rec⁡G∅⁡suc⁡b↾R1⁡b
62 61 pweqd ⊢x=rec⁡G∅⁡suc⁡b↾R1⁡b→𝒫dom⁡x=𝒫dom⁡rec⁡G∅⁡suc⁡b↾R1⁡b
63 imaeq1 ⊢x=rec⁡G∅⁡suc⁡b↾R1⁡b→xy=rec⁡G∅⁡suc⁡b↾R1⁡by
64 63 fveq2d ⊢x=rec⁡G∅⁡suc⁡b↾R1⁡b→F⁡xy=F⁡rec⁡G∅⁡suc⁡b↾R1⁡by
65 62 64 mpteq12dv ⊢x=rec⁡G∅⁡suc⁡b↾R1⁡b→y∈𝒫dom⁡x⟼F⁡xy=y∈𝒫dom⁡rec⁡G∅⁡suc⁡b↾R1⁡b⟼F⁡rec⁡G∅⁡suc⁡b↾R1⁡by
66 60 dmex ⊢dom⁡rec⁡G∅⁡suc⁡b↾R1⁡b∈V
67 66 pwex ⊢𝒫dom⁡rec⁡G∅⁡suc⁡b↾R1⁡b∈V
68 67 mptex ⊢y∈𝒫dom⁡rec⁡G∅⁡suc⁡b↾R1⁡b⟼F⁡rec⁡G∅⁡suc⁡b↾R1⁡by∈V
69 65 2 68 fvmpt ⊢rec⁡G∅⁡suc⁡b↾R1⁡b∈V→G⁡rec⁡G∅⁡suc⁡b↾R1⁡b=y∈𝒫dom⁡rec⁡G∅⁡suc⁡b↾R1⁡b⟼F⁡rec⁡G∅⁡suc⁡b↾R1⁡by
70 60 69 ax-mp ⊢G⁡rec⁡G∅⁡suc⁡b↾R1⁡b=y∈𝒫dom⁡rec⁡G∅⁡suc⁡b↾R1⁡b⟼F⁡rec⁡G∅⁡suc⁡b↾R1⁡by
71 70 fveq1i ⊢G⁡rec⁡G∅⁡suc⁡b↾R1⁡b⁡c=y∈𝒫dom⁡rec⁡G∅⁡suc⁡b↾R1⁡b⟼F⁡rec⁡G∅⁡suc⁡b↾R1⁡by⁡c
72 r1sssuc ⊢b∈On→R1⁡b⊆R1⁡suc⁡b
73 50 72 syl ⊢b∈ω→R1⁡b⊆R1⁡suc⁡b
74 fnssres ⊢rec⁡G∅⁡suc⁡bFnR1⁡suc⁡b∧R1⁡b⊆R1⁡suc⁡b→rec⁡G∅⁡suc⁡b↾R1⁡bFnR1⁡b
75 37 73 74 syl2anc ⊢b∈ω→rec⁡G∅⁡suc⁡b↾R1⁡bFnR1⁡b
76 75 fndmd ⊢b∈ω→dom⁡rec⁡G∅⁡suc⁡b↾R1⁡b=R1⁡b
77 76 pweqd ⊢b∈ω→𝒫dom⁡rec⁡G∅⁡suc⁡b↾R1⁡b=𝒫R1⁡b
78 77 adantr ⊢b∈ω∧c∈R1⁡suc⁡b→𝒫dom⁡rec⁡G∅⁡suc⁡b↾R1⁡b=𝒫R1⁡b
79 54 78 eleqtrrd ⊢b∈ω∧c∈R1⁡suc⁡b→c∈𝒫dom⁡rec⁡G∅⁡suc⁡b↾R1⁡b
80 imaeq2 ⊢y=c→rec⁡G∅⁡suc⁡b↾R1⁡by=rec⁡G∅⁡suc⁡b↾R1⁡bc
81 80 fveq2d ⊢y=c→F⁡rec⁡G∅⁡suc⁡b↾R1⁡by=F⁡rec⁡G∅⁡suc⁡b↾R1⁡bc
82 eqid ⊢y∈𝒫dom⁡rec⁡G∅⁡suc⁡b↾R1⁡b⟼F⁡rec⁡G∅⁡suc⁡b↾R1⁡by=y∈𝒫dom⁡rec⁡G∅⁡suc⁡b↾R1⁡b⟼F⁡rec⁡G∅⁡suc⁡b↾R1⁡by
83 fvex ⊢F⁡rec⁡G∅⁡suc⁡b↾R1⁡bc∈V
84 81 82 83 fvmpt ⊢c∈𝒫dom⁡rec⁡G∅⁡suc⁡b↾R1⁡b→y∈𝒫dom⁡rec⁡G∅⁡suc⁡b↾R1⁡b⟼F⁡rec⁡G∅⁡suc⁡b↾R1⁡by⁡c=F⁡rec⁡G∅⁡suc⁡b↾R1⁡bc
85 79 84 syl ⊢b∈ω∧c∈R1⁡suc⁡b→y∈𝒫dom⁡rec⁡G∅⁡suc⁡b↾R1⁡b⟼F⁡rec⁡G∅⁡suc⁡b↾R1⁡by⁡c=F⁡rec⁡G∅⁡suc⁡b↾R1⁡bc
86 71 85 eqtrid ⊢b∈ω∧c∈R1⁡suc⁡b→G⁡rec⁡G∅⁡suc⁡b↾R1⁡b⁡c=F⁡rec⁡G∅⁡suc⁡b↾R1⁡bc
87 dmeq ⊢x=rec⁡G∅⁡suc⁡b→dom⁡x=dom⁡rec⁡G∅⁡suc⁡b
88 87 pweqd ⊢x=rec⁡G∅⁡suc⁡b→𝒫dom⁡x=𝒫dom⁡rec⁡G∅⁡suc⁡b
89 imaeq1 ⊢x=rec⁡G∅⁡suc⁡b→xy=rec⁡G∅⁡suc⁡by
90 89 fveq2d ⊢x=rec⁡G∅⁡suc⁡b→F⁡xy=F⁡rec⁡G∅⁡suc⁡by
91 88 90 mpteq12dv ⊢x=rec⁡G∅⁡suc⁡b→y∈𝒫dom⁡x⟼F⁡xy=y∈𝒫dom⁡rec⁡G∅⁡suc⁡b⟼F⁡rec⁡G∅⁡suc⁡by
92 59 dmex ⊢dom⁡rec⁡G∅⁡suc⁡b∈V
93 92 pwex ⊢𝒫dom⁡rec⁡G∅⁡suc⁡b∈V
94 93 mptex ⊢y∈𝒫dom⁡rec⁡G∅⁡suc⁡b⟼F⁡rec⁡G∅⁡suc⁡by∈V
95 91 2 94 fvmpt ⊢rec⁡G∅⁡suc⁡b∈V→G⁡rec⁡G∅⁡suc⁡b=y∈𝒫dom⁡rec⁡G∅⁡suc⁡b⟼F⁡rec⁡G∅⁡suc⁡by
96 59 95 ax-mp ⊢G⁡rec⁡G∅⁡suc⁡b=y∈𝒫dom⁡rec⁡G∅⁡suc⁡b⟼F⁡rec⁡G∅⁡suc⁡by
97 96 fveq1i ⊢G⁡rec⁡G∅⁡suc⁡b⁡c=y∈𝒫dom⁡rec⁡G∅⁡suc⁡b⟼F⁡rec⁡G∅⁡suc⁡by⁡c
98 r1tr ⊢Tr⁡R1⁡suc⁡b
99 98 a1i ⊢b∈ω→Tr⁡R1⁡suc⁡b
100 dftr4 ⊢Tr⁡R1⁡suc⁡b↔R1⁡suc⁡b⊆𝒫R1⁡suc⁡b
101 99 100 sylib ⊢b∈ω→R1⁡suc⁡b⊆𝒫R1⁡suc⁡b
102 101 sselda ⊢b∈ω∧c∈R1⁡suc⁡b→c∈𝒫R1⁡suc⁡b
103 f1odm ⊢rec⁡G∅⁡suc⁡b:R1⁡suc⁡b⟶1-1 ontocard⁡R1⁡suc⁡b→dom⁡rec⁡G∅⁡suc⁡b=R1⁡suc⁡b
104 35 103 syl ⊢b∈ω→dom⁡rec⁡G∅⁡suc⁡b=R1⁡suc⁡b
105 104 pweqd ⊢b∈ω→𝒫dom⁡rec⁡G∅⁡suc⁡b=𝒫R1⁡suc⁡b
106 105 adantr ⊢b∈ω∧c∈R1⁡suc⁡b→𝒫dom⁡rec⁡G∅⁡suc⁡b=𝒫R1⁡suc⁡b
107 102 106 eleqtrrd ⊢b∈ω∧c∈R1⁡suc⁡b→c∈𝒫dom⁡rec⁡G∅⁡suc⁡b
108 imaeq2 ⊢y=c→rec⁡G∅⁡suc⁡by=rec⁡G∅⁡suc⁡bc
109 108 fveq2d ⊢y=c→F⁡rec⁡G∅⁡suc⁡by=F⁡rec⁡G∅⁡suc⁡bc
110 eqid ⊢y∈𝒫dom⁡rec⁡G∅⁡suc⁡b⟼F⁡rec⁡G∅⁡suc⁡by=y∈𝒫dom⁡rec⁡G∅⁡suc⁡b⟼F⁡rec⁡G∅⁡suc⁡by
111 fvex ⊢F⁡rec⁡G∅⁡suc⁡bc∈V
112 109 110 111 fvmpt ⊢c∈𝒫dom⁡rec⁡G∅⁡suc⁡b→y∈𝒫dom⁡rec⁡G∅⁡suc⁡b⟼F⁡rec⁡G∅⁡suc⁡by⁡c=F⁡rec⁡G∅⁡suc⁡bc
113 107 112 syl ⊢b∈ω∧c∈R1⁡suc⁡b→y∈𝒫dom⁡rec⁡G∅⁡suc⁡b⟼F⁡rec⁡G∅⁡suc⁡by⁡c=F⁡rec⁡G∅⁡suc⁡bc
114 97 113 eqtrid ⊢b∈ω∧c∈R1⁡suc⁡b→G⁡rec⁡G∅⁡suc⁡b⁡c=F⁡rec⁡G∅⁡suc⁡bc
115 58 86 114 3eqtr4d ⊢b∈ω∧c∈R1⁡suc⁡b→G⁡rec⁡G∅⁡suc⁡b↾R1⁡b⁡c=G⁡rec⁡G∅⁡suc⁡b⁡c
116 115 adantlr ⊢b∈ω∧rec⁡G∅⁡b=rec⁡G∅⁡suc⁡b↾R1⁡b∧c∈R1⁡suc⁡b→G⁡rec⁡G∅⁡suc⁡b↾R1⁡b⁡c=G⁡rec⁡G∅⁡suc⁡b⁡c
117 fveq2 ⊢rec⁡G∅⁡b=rec⁡G∅⁡suc⁡b↾R1⁡b→G⁡rec⁡G∅⁡b=G⁡rec⁡G∅⁡suc⁡b↾R1⁡b
118 117 fveq1d ⊢rec⁡G∅⁡b=rec⁡G∅⁡suc⁡b↾R1⁡b→G⁡rec⁡G∅⁡b⁡c=G⁡rec⁡G∅⁡suc⁡b↾R1⁡b⁡c
119 118 ad2antlr ⊢b∈ω∧rec⁡G∅⁡b=rec⁡G∅⁡suc⁡b↾R1⁡b∧c∈R1⁡suc⁡b→G⁡rec⁡G∅⁡b⁡c=G⁡rec⁡G∅⁡suc⁡b↾R1⁡b⁡c
120 rdgsuc ⊢suc⁡b∈On→rec⁡G∅⁡suc⁡suc⁡b=G⁡rec⁡G∅⁡suc⁡b
121 44 120 syl ⊢b∈ω→rec⁡G∅⁡suc⁡suc⁡b=G⁡rec⁡G∅⁡suc⁡b
122 121 fveq1d ⊢b∈ω→rec⁡G∅⁡suc⁡suc⁡b⁡c=G⁡rec⁡G∅⁡suc⁡b⁡c
123 122 ad2antrr ⊢b∈ω∧rec⁡G∅⁡b=rec⁡G∅⁡suc⁡b↾R1⁡b∧c∈R1⁡suc⁡b→rec⁡G∅⁡suc⁡suc⁡b⁡c=G⁡rec⁡G∅⁡suc⁡b⁡c
124 116 119 123 3eqtr4rd ⊢b∈ω∧rec⁡G∅⁡b=rec⁡G∅⁡suc⁡b↾R1⁡b∧c∈R1⁡suc⁡b→rec⁡G∅⁡suc⁡suc⁡b⁡c=G⁡rec⁡G∅⁡b⁡c
125 fvres ⊢c∈R1⁡suc⁡b→rec⁡G∅⁡suc⁡suc⁡b↾R1⁡suc⁡b⁡c=rec⁡G∅⁡suc⁡suc⁡b⁡c
126 125 adantl ⊢b∈ω∧rec⁡G∅⁡b=rec⁡G∅⁡suc⁡b↾R1⁡b∧c∈R1⁡suc⁡b→rec⁡G∅⁡suc⁡suc⁡b↾R1⁡suc⁡b⁡c=rec⁡G∅⁡suc⁡suc⁡b⁡c
127 rdgsuc ⊢b∈On→rec⁡G∅⁡suc⁡b=G⁡rec⁡G∅⁡b
128 50 127 syl ⊢b∈ω→rec⁡G∅⁡suc⁡b=G⁡rec⁡G∅⁡b
129 128 fveq1d ⊢b∈ω→rec⁡G∅⁡suc⁡b⁡c=G⁡rec⁡G∅⁡b⁡c
130 129 ad2antrr ⊢b∈ω∧rec⁡G∅⁡b=rec⁡G∅⁡suc⁡b↾R1⁡b∧c∈R1⁡suc⁡b→rec⁡G∅⁡suc⁡b⁡c=G⁡rec⁡G∅⁡b⁡c
131 124 126 130 3eqtr4rd ⊢b∈ω∧rec⁡G∅⁡b=rec⁡G∅⁡suc⁡b↾R1⁡b∧c∈R1⁡suc⁡b→rec⁡G∅⁡suc⁡b⁡c=rec⁡G∅⁡suc⁡suc⁡b↾R1⁡suc⁡b⁡c
132 38 49 131 eqfnfvd ⊢b∈ω∧rec⁡G∅⁡b=rec⁡G∅⁡suc⁡b↾R1⁡b→rec⁡G∅⁡suc⁡b=rec⁡G∅⁡suc⁡suc⁡b↾R1⁡suc⁡b
133 132 ex ⊢b∈ω→rec⁡G∅⁡b=rec⁡G∅⁡suc⁡b↾R1⁡b→rec⁡G∅⁡suc⁡b=rec⁡G∅⁡suc⁡suc⁡b↾R1⁡suc⁡b
134 8 14 20 26 32 133 finds ⊢A∈ω→rec⁡G∅⁡A=rec⁡G∅⁡suc⁡A↾R1⁡A
135 resss ⊢rec⁡G∅⁡suc⁡A↾R1⁡A⊆rec⁡G∅⁡suc⁡A
136 134 135 eqsstrdi ⊢A∈ω→rec⁡G∅⁡A⊆rec⁡G∅⁡suc⁡A