Metamath Proof Explorer

Theorem cfsmolem

Description: Lemma for cfsmo . (Contributed by Mario Carneiro, 28-Feb-2013)

Ref Expression
Hypotheses cfsmolem.2 ⊢F=z∈V⟼g⁡dom⁡z∪⋃t∈dom⁡zsuc⁡z⁡t
cfsmolem.3 ⊢G=recs⁡F↾cf⁡A
Assertion cfsmolem ⊢A∈On→∃ff:cf⁡A⟶A∧Smo⁡f∧∀z∈A∃w∈cf⁡Az⊆f⁡w

Proof

Step Hyp Ref Expression
1 cfsmolem.2 ⊢F=z∈V⟼g⁡dom⁡z∪⋃t∈dom⁡zsuc⁡z⁡t
2 cfsmolem.3 ⊢G=recs⁡F↾cf⁡A
3 cff1 ⊢A∈On→∃gg:cf⁡A⟶1-1A∧∀z∈A∃w∈cf⁡Az⊆g⁡w
4 cfon ⊢cf⁡A∈On
5 4 oneli ⊢x∈cf⁡A→x∈On
6 5 3ad2ant3 ⊢g:cf⁡A⟶1-1A∧A∈On∧x∈cf⁡A→x∈On
7 eleq1w ⊢x=y→x∈cf⁡A↔y∈cf⁡A
8 7 3anbi3d ⊢x=y→g:cf⁡A⟶1-1A∧A∈On∧x∈cf⁡A↔g:cf⁡A⟶1-1A∧A∈On∧y∈cf⁡A
9 fveq2 ⊢x=y→G⁡x=G⁡y
10 9 eleq1d ⊢x=y→G⁡x∈A↔G⁡y∈A
11 8 10 imbi12d ⊢x=y→g:cf⁡A⟶1-1A∧A∈On∧x∈cf⁡A→G⁡x∈A↔g:cf⁡A⟶1-1A∧A∈On∧y∈cf⁡A→G⁡y∈A
12 simpl1 ⊢g:cf⁡A⟶1-1A∧A∈On∧x∈cf⁡A∧y∈x→g:cf⁡A⟶1-1A
13 simpl2 ⊢g:cf⁡A⟶1-1A∧A∈On∧x∈cf⁡A∧y∈x→A∈On
14 ontr1 ⊢cf⁡A∈On→y∈x∧x∈cf⁡A→y∈cf⁡A
15 4 14 ax-mp ⊢y∈x∧x∈cf⁡A→y∈cf⁡A
16 15 ancoms ⊢x∈cf⁡A∧y∈x→y∈cf⁡A
17 16 3ad2antl3 ⊢g:cf⁡A⟶1-1A∧A∈On∧x∈cf⁡A∧y∈x→y∈cf⁡A
18 pm2.27 ⊢g:cf⁡A⟶1-1A∧A∈On∧y∈cf⁡A→g:cf⁡A⟶1-1A∧A∈On∧y∈cf⁡A→G⁡y∈A→G⁡y∈A
19 12 13 17 18 syl3anc ⊢g:cf⁡A⟶1-1A∧A∈On∧x∈cf⁡A∧y∈x→g:cf⁡A⟶1-1A∧A∈On∧y∈cf⁡A→G⁡y∈A→G⁡y∈A
20 19 ralimdva ⊢g:cf⁡A⟶1-1A∧A∈On∧x∈cf⁡A→∀y∈xg:cf⁡A⟶1-1A∧A∈On∧y∈cf⁡A→G⁡y∈A→∀y∈xG⁡y∈A
21 2 fveq1i ⊢G⁡x=recs⁡F↾cf⁡A⁡x
22 fvres ⊢x∈cf⁡A→recs⁡F↾cf⁡A⁡x=recs⁡F⁡x
23 21 22 eqtrid ⊢x∈cf⁡A→G⁡x=recs⁡F⁡x
24 recsval ⊢x∈On→recs⁡F⁡x=F⁡recs⁡F↾x
25 recsfnon ⊢recs⁡FFnOn
26 fnfun ⊢recs⁡FFnOn→Fun⁡recs⁡F
27 25 26 ax-mp ⊢Fun⁡recs⁡F
28 vex ⊢x∈V
29 resfunexg ⊢Fun⁡recs⁡F∧x∈V→recs⁡F↾x∈V
30 27 28 29 mp2an ⊢recs⁡F↾x∈V
31 dmeq ⊢z=recs⁡F↾x→dom⁡z=dom⁡recs⁡F↾x
32 31 fveq2d ⊢z=recs⁡F↾x→g⁡dom⁡z=g⁡dom⁡recs⁡F↾x
33 fveq1 ⊢z=recs⁡F↾x→z⁡t=recs⁡F↾x⁡t
34 suceq ⊢z⁡t=recs⁡F↾x⁡t→suc⁡z⁡t=suc⁡recs⁡F↾x⁡t
35 33 34 syl ⊢z=recs⁡F↾x→suc⁡z⁡t=suc⁡recs⁡F↾x⁡t
36 31 35 iuneq12d ⊢z=recs⁡F↾x→⋃t∈dom⁡zsuc⁡z⁡t=⋃t∈dom⁡recs⁡F↾xsuc⁡recs⁡F↾x⁡t
37 32 36 uneq12d ⊢z=recs⁡F↾x→g⁡dom⁡z∪⋃t∈dom⁡zsuc⁡z⁡t=g⁡dom⁡recs⁡F↾x∪⋃t∈dom⁡recs⁡F↾xsuc⁡recs⁡F↾x⁡t
38 fvex ⊢g⁡dom⁡recs⁡F↾x∈V
39 30 dmex ⊢dom⁡recs⁡F↾x∈V
40 fvex ⊢recs⁡F↾x⁡t∈V
41 40 sucex ⊢suc⁡recs⁡F↾x⁡t∈V
42 39 41 iunex ⊢⋃t∈dom⁡recs⁡F↾xsuc⁡recs⁡F↾x⁡t∈V
43 38 42 unex ⊢g⁡dom⁡recs⁡F↾x∪⋃t∈dom⁡recs⁡F↾xsuc⁡recs⁡F↾x⁡t∈V
44 37 1 43 fvmpt ⊢recs⁡F↾x∈V→F⁡recs⁡F↾x=g⁡dom⁡recs⁡F↾x∪⋃t∈dom⁡recs⁡F↾xsuc⁡recs⁡F↾x⁡t
45 30 44 ax-mp ⊢F⁡recs⁡F↾x=g⁡dom⁡recs⁡F↾x∪⋃t∈dom⁡recs⁡F↾xsuc⁡recs⁡F↾x⁡t
46 24 45 eqtrdi ⊢x∈On→recs⁡F⁡x=g⁡dom⁡recs⁡F↾x∪⋃t∈dom⁡recs⁡F↾xsuc⁡recs⁡F↾x⁡t
47 onss ⊢x∈On→x⊆On
48 fnssres ⊢recs⁡FFnOn∧x⊆On→recs⁡F↾xFnx
49 25 47 48 sylancr ⊢x∈On→recs⁡F↾xFnx
50 fndm ⊢recs⁡F↾xFnx→dom⁡recs⁡F↾x=x
51 fveq2 ⊢dom⁡recs⁡F↾x=x→g⁡dom⁡recs⁡F↾x=g⁡x
52 iuneq1 ⊢dom⁡recs⁡F↾x=x→⋃t∈dom⁡recs⁡F↾xsuc⁡recs⁡F↾x⁡t=⋃t∈xsuc⁡recs⁡F↾x⁡t
53 fvres ⊢t∈x→recs⁡F↾x⁡t=recs⁡F⁡t
54 suceq ⊢recs⁡F↾x⁡t=recs⁡F⁡t→suc⁡recs⁡F↾x⁡t=suc⁡recs⁡F⁡t
55 53 54 syl ⊢t∈x→suc⁡recs⁡F↾x⁡t=suc⁡recs⁡F⁡t
56 55 iuneq2i ⊢⋃t∈xsuc⁡recs⁡F↾x⁡t=⋃t∈xsuc⁡recs⁡F⁡t
57 fveq2 ⊢y=t→recs⁡F⁡y=recs⁡F⁡t
58 suceq ⊢recs⁡F⁡y=recs⁡F⁡t→suc⁡recs⁡F⁡y=suc⁡recs⁡F⁡t
59 57 58 syl ⊢y=t→suc⁡recs⁡F⁡y=suc⁡recs⁡F⁡t
60 59 cbviunv ⊢⋃y∈xsuc⁡recs⁡F⁡y=⋃t∈xsuc⁡recs⁡F⁡t
61 56 60 eqtr4i ⊢⋃t∈xsuc⁡recs⁡F↾x⁡t=⋃y∈xsuc⁡recs⁡F⁡y
62 52 61 eqtrdi ⊢dom⁡recs⁡F↾x=x→⋃t∈dom⁡recs⁡F↾xsuc⁡recs⁡F↾x⁡t=⋃y∈xsuc⁡recs⁡F⁡y
63 51 62 uneq12d ⊢dom⁡recs⁡F↾x=x→g⁡dom⁡recs⁡F↾x∪⋃t∈dom⁡recs⁡F↾xsuc⁡recs⁡F↾x⁡t=g⁡x∪⋃y∈xsuc⁡recs⁡F⁡y
64 49 50 63 3syl ⊢x∈On→g⁡dom⁡recs⁡F↾x∪⋃t∈dom⁡recs⁡F↾xsuc⁡recs⁡F↾x⁡t=g⁡x∪⋃y∈xsuc⁡recs⁡F⁡y
65 46 64 eqtrd ⊢x∈On→recs⁡F⁡x=g⁡x∪⋃y∈xsuc⁡recs⁡F⁡y
66 5 65 syl ⊢x∈cf⁡A→recs⁡F⁡x=g⁡x∪⋃y∈xsuc⁡recs⁡F⁡y
67 23 66 eqtrd ⊢x∈cf⁡A→G⁡x=g⁡x∪⋃y∈xsuc⁡recs⁡F⁡y
68 67 3ad2ant2 ⊢g:cf⁡A⟶1-1A∧A∈On∧x∈cf⁡A∧∀y∈xG⁡y∈A→G⁡x=g⁡x∪⋃y∈xsuc⁡recs⁡F⁡y
69 eloni ⊢A∈On→Ord⁡A
70 69 adantl ⊢g:cf⁡A⟶1-1A∧A∈On→Ord⁡A
71 70 3ad2ant1 ⊢g:cf⁡A⟶1-1A∧A∈On∧x∈cf⁡A∧∀y∈xG⁡y∈A→Ord⁡A
72 f1f ⊢g:cf⁡A⟶1-1A→g:cf⁡A⟶A
73 72 ffvelcdmda ⊢g:cf⁡A⟶1-1A∧x∈cf⁡A→g⁡x∈A
74 73 adantlr ⊢g:cf⁡A⟶1-1A∧A∈On∧x∈cf⁡A→g⁡x∈A
75 74 3adant3 ⊢g:cf⁡A⟶1-1A∧A∈On∧x∈cf⁡A∧∀y∈xG⁡y∈A→g⁡x∈A
76 2 fveq1i ⊢G⁡y=recs⁡F↾cf⁡A⁡y
77 15 fvresd ⊢y∈x∧x∈cf⁡A→recs⁡F↾cf⁡A⁡y=recs⁡F⁡y
78 76 77 eqtrid ⊢y∈x∧x∈cf⁡A→G⁡y=recs⁡F⁡y
79 78 adantrl ⊢y∈x∧A∈On∧x∈cf⁡A→G⁡y=recs⁡F⁡y
80 79 ancoms ⊢A∈On∧x∈cf⁡A∧y∈x→G⁡y=recs⁡F⁡y
81 80 eleq1d ⊢A∈On∧x∈cf⁡A∧y∈x→G⁡y∈A↔recs⁡F⁡y∈A
82 ordsucss ⊢Ord⁡A→recs⁡F⁡y∈A→suc⁡recs⁡F⁡y⊆A
83 69 82 syl ⊢A∈On→recs⁡F⁡y∈A→suc⁡recs⁡F⁡y⊆A
84 83 ad2antrr ⊢A∈On∧x∈cf⁡A∧y∈x→recs⁡F⁡y∈A→suc⁡recs⁡F⁡y⊆A
85 81 84 sylbid ⊢A∈On∧x∈cf⁡A∧y∈x→G⁡y∈A→suc⁡recs⁡F⁡y⊆A
86 85 ralimdva ⊢A∈On∧x∈cf⁡A→∀y∈xG⁡y∈A→∀y∈xsuc⁡recs⁡F⁡y⊆A
87 iunss ⊢⋃y∈xsuc⁡recs⁡F⁡y⊆A↔∀y∈xsuc⁡recs⁡F⁡y⊆A
88 86 87 imbitrrdi ⊢A∈On∧x∈cf⁡A→∀y∈xG⁡y∈A→⋃y∈xsuc⁡recs⁡F⁡y⊆A
89 88 3impia ⊢A∈On∧x∈cf⁡A∧∀y∈xG⁡y∈A→⋃y∈xsuc⁡recs⁡F⁡y⊆A
90 onelon ⊢A∈On∧recs⁡F⁡y∈A→recs⁡F⁡y∈On
91 90 ex ⊢A∈On→recs⁡F⁡y∈A→recs⁡F⁡y∈On
92 91 ad2antrr ⊢A∈On∧x∈cf⁡A∧y∈x→recs⁡F⁡y∈A→recs⁡F⁡y∈On
93 81 92 sylbid ⊢A∈On∧x∈cf⁡A∧y∈x→G⁡y∈A→recs⁡F⁡y∈On
94 onsuc ⊢recs⁡F⁡y∈On→suc⁡recs⁡F⁡y∈On
95 93 94 syl6 ⊢A∈On∧x∈cf⁡A∧y∈x→G⁡y∈A→suc⁡recs⁡F⁡y∈On
96 95 ralimdva ⊢A∈On∧x∈cf⁡A→∀y∈xG⁡y∈A→∀y∈xsuc⁡recs⁡F⁡y∈On
97 96 3impia ⊢A∈On∧x∈cf⁡A∧∀y∈xG⁡y∈A→∀y∈xsuc⁡recs⁡F⁡y∈On
98 iunon ⊢x∈V∧∀y∈xsuc⁡recs⁡F⁡y∈On→⋃y∈xsuc⁡recs⁡F⁡y∈On
99 28 97 98 sylancr ⊢A∈On∧x∈cf⁡A∧∀y∈xG⁡y∈A→⋃y∈xsuc⁡recs⁡F⁡y∈On
100 simp1 ⊢A∈On∧x∈cf⁡A∧∀y∈xG⁡y∈A→A∈On
101 onsseleq ⊢⋃y∈xsuc⁡recs⁡F⁡y∈On∧A∈On→⋃y∈xsuc⁡recs⁡F⁡y⊆A↔⋃y∈xsuc⁡recs⁡F⁡y∈A∨⋃y∈xsuc⁡recs⁡F⁡y=A
102 99 100 101 syl2anc ⊢A∈On∧x∈cf⁡A∧∀y∈xG⁡y∈A→⋃y∈xsuc⁡recs⁡F⁡y⊆A↔⋃y∈xsuc⁡recs⁡F⁡y∈A∨⋃y∈xsuc⁡recs⁡F⁡y=A
103 idd ⊢A∈On∧x∈cf⁡A∧∀y∈xG⁡y∈A→⋃y∈xsuc⁡recs⁡F⁡y∈A→⋃y∈xsuc⁡recs⁡F⁡y∈A
104 simpll ⊢x∈cf⁡A∧∀y∈xG⁡y∈A∧⋃y∈xsuc⁡recs⁡F⁡y=A∧A∈On→x∈cf⁡A
105 simprr ⊢x∈cf⁡A∧∀y∈xG⁡y∈A∧⋃y∈xsuc⁡recs⁡F⁡y=A∧A∈On→A∈On
106 5 ad2antrr ⊢x∈cf⁡A∧∀y∈xG⁡y∈A∧⋃y∈xsuc⁡recs⁡F⁡y=A∧A∈On→x∈On
107 5 49 syl ⊢x∈cf⁡A→recs⁡F↾xFnx
108 107 adantr ⊢x∈cf⁡A∧∀y∈xG⁡y∈A→recs⁡F↾xFnx
109 78 ancoms ⊢x∈cf⁡A∧y∈x→G⁡y=recs⁡F⁡y
110 fvres ⊢y∈x→recs⁡F↾x⁡y=recs⁡F⁡y
111 110 adantl ⊢x∈cf⁡A∧y∈x→recs⁡F↾x⁡y=recs⁡F⁡y
112 109 111 eqtr4d ⊢x∈cf⁡A∧y∈x→G⁡y=recs⁡F↾x⁡y
113 112 eleq1d ⊢x∈cf⁡A∧y∈x→G⁡y∈A↔recs⁡F↾x⁡y∈A
114 113 ralbidva ⊢x∈cf⁡A→∀y∈xG⁡y∈A↔∀y∈xrecs⁡F↾x⁡y∈A
115 114 biimpa ⊢x∈cf⁡A∧∀y∈xG⁡y∈A→∀y∈xrecs⁡F↾x⁡y∈A
116 ffnfv ⊢recs⁡F↾x:x⟶A↔recs⁡F↾xFnx∧∀y∈xrecs⁡F↾x⁡y∈A
117 108 115 116 sylanbrc ⊢x∈cf⁡A∧∀y∈xG⁡y∈A→recs⁡F↾x:x⟶A
118 eleq2 ⊢⋃y∈xsuc⁡recs⁡F⁡y=A→t∈⋃y∈xsuc⁡recs⁡F⁡y↔t∈A
119 118 biimpar ⊢⋃y∈xsuc⁡recs⁡F⁡y=A∧t∈A→t∈⋃y∈xsuc⁡recs⁡F⁡y
120 119 adantrl ⊢⋃y∈xsuc⁡recs⁡F⁡y=A∧A∈On∧t∈A→t∈⋃y∈xsuc⁡recs⁡F⁡y
121 120 3adant1 ⊢recs⁡F↾x:x⟶A∧⋃y∈xsuc⁡recs⁡F⁡y=A∧A∈On∧t∈A→t∈⋃y∈xsuc⁡recs⁡F⁡y
122 onelon ⊢A∈On∧t∈A→t∈On
123 110 adantl ⊢recs⁡F↾x:x⟶A∧y∈x→recs⁡F↾x⁡y=recs⁡F⁡y
124 ffvelcdm ⊢recs⁡F↾x:x⟶A∧y∈x→recs⁡F↾x⁡y∈A
125 123 124 eqeltrrd ⊢recs⁡F↾x:x⟶A∧y∈x→recs⁡F⁡y∈A
126 125 90 sylan2 ⊢A∈On∧recs⁡F↾x:x⟶A∧y∈x→recs⁡F⁡y∈On
127 126 adantlr ⊢A∈On∧t∈A∧recs⁡F↾x:x⟶A∧y∈x→recs⁡F⁡y∈On
128 onsssuc ⊢t∈On∧recs⁡F⁡y∈On→t⊆recs⁡F⁡y↔t∈suc⁡recs⁡F⁡y
129 122 127 128 syl2an2r ⊢A∈On∧t∈A∧recs⁡F↾x:x⟶A∧y∈x→t⊆recs⁡F⁡y↔t∈suc⁡recs⁡F⁡y
130 129 anassrs ⊢A∈On∧t∈A∧recs⁡F↾x:x⟶A∧y∈x→t⊆recs⁡F⁡y↔t∈suc⁡recs⁡F⁡y
131 130 rexbidva ⊢A∈On∧t∈A∧recs⁡F↾x:x⟶A→∃y∈xt⊆recs⁡F⁡y↔∃y∈xt∈suc⁡recs⁡F⁡y
132 eliun ⊢t∈⋃y∈xsuc⁡recs⁡F⁡y↔∃y∈xt∈suc⁡recs⁡F⁡y
133 131 132 bitr4di ⊢A∈On∧t∈A∧recs⁡F↾x:x⟶A→∃y∈xt⊆recs⁡F⁡y↔t∈⋃y∈xsuc⁡recs⁡F⁡y
134 133 ancoms ⊢recs⁡F↾x:x⟶A∧A∈On∧t∈A→∃y∈xt⊆recs⁡F⁡y↔t∈⋃y∈xsuc⁡recs⁡F⁡y
135 134 3adant2 ⊢recs⁡F↾x:x⟶A∧⋃y∈xsuc⁡recs⁡F⁡y=A∧A∈On∧t∈A→∃y∈xt⊆recs⁡F⁡y↔t∈⋃y∈xsuc⁡recs⁡F⁡y
136 121 135 mpbird ⊢recs⁡F↾x:x⟶A∧⋃y∈xsuc⁡recs⁡F⁡y=A∧A∈On∧t∈A→∃y∈xt⊆recs⁡F⁡y
137 136 3expa ⊢recs⁡F↾x:x⟶A∧⋃y∈xsuc⁡recs⁡F⁡y=A∧A∈On∧t∈A→∃y∈xt⊆recs⁡F⁡y
138 137 anassrs ⊢recs⁡F↾x:x⟶A∧⋃y∈xsuc⁡recs⁡F⁡y=A∧A∈On∧t∈A→∃y∈xt⊆recs⁡F⁡y
139 138 ralrimiva ⊢recs⁡F↾x:x⟶A∧⋃y∈xsuc⁡recs⁡F⁡y=A∧A∈On→∀t∈A∃y∈xt⊆recs⁡F⁡y
140 139 expl ⊢recs⁡F↾x:x⟶A→⋃y∈xsuc⁡recs⁡F⁡y=A∧A∈On→∀t∈A∃y∈xt⊆recs⁡F⁡y
141 117 140 syl ⊢x∈cf⁡A∧∀y∈xG⁡y∈A→⋃y∈xsuc⁡recs⁡F⁡y=A∧A∈On→∀t∈A∃y∈xt⊆recs⁡F⁡y
142 141 imp ⊢x∈cf⁡A∧∀y∈xG⁡y∈A∧⋃y∈xsuc⁡recs⁡F⁡y=A∧A∈On→∀t∈A∃y∈xt⊆recs⁡F⁡y
143 feq1 ⊢f=recs⁡F↾x→f:x⟶A↔recs⁡F↾x:x⟶A
144 fveq1 ⊢f=recs⁡F↾x→f⁡y=recs⁡F↾x⁡y
145 144 sseq2d ⊢f=recs⁡F↾x→t⊆f⁡y↔t⊆recs⁡F↾x⁡y
146 145 rexbidv ⊢f=recs⁡F↾x→∃y∈xt⊆f⁡y↔∃y∈xt⊆recs⁡F↾x⁡y
147 110 sseq2d ⊢y∈x→t⊆recs⁡F↾x⁡y↔t⊆recs⁡F⁡y
148 147 rexbiia ⊢∃y∈xt⊆recs⁡F↾x⁡y↔∃y∈xt⊆recs⁡F⁡y
149 146 148 bitrdi ⊢f=recs⁡F↾x→∃y∈xt⊆f⁡y↔∃y∈xt⊆recs⁡F⁡y
150 149 ralbidv ⊢f=recs⁡F↾x→∀t∈A∃y∈xt⊆f⁡y↔∀t∈A∃y∈xt⊆recs⁡F⁡y
151 143 150 anbi12d ⊢f=recs⁡F↾x→f:x⟶A∧∀t∈A∃y∈xt⊆f⁡y↔recs⁡F↾x:x⟶A∧∀t∈A∃y∈xt⊆recs⁡F⁡y
152 30 151 spcev ⊢recs⁡F↾x:x⟶A∧∀t∈A∃y∈xt⊆recs⁡F⁡y→∃ff:x⟶A∧∀t∈A∃y∈xt⊆f⁡y
153 117 142 152 syl2an2r ⊢x∈cf⁡A∧∀y∈xG⁡y∈A∧⋃y∈xsuc⁡recs⁡F⁡y=A∧A∈On→∃ff:x⟶A∧∀t∈A∃y∈xt⊆f⁡y
154 cfflb ⊢A∈On∧x∈On→∃ff:x⟶A∧∀t∈A∃y∈xt⊆f⁡y→cf⁡A⊆x
155 154 imp ⊢A∈On∧x∈On∧∃ff:x⟶A∧∀t∈A∃y∈xt⊆f⁡y→cf⁡A⊆x
156 105 106 153 155 syl21anc ⊢x∈cf⁡A∧∀y∈xG⁡y∈A∧⋃y∈xsuc⁡recs⁡F⁡y=A∧A∈On→cf⁡A⊆x
157 ontri1 ⊢cf⁡A∈On∧x∈On→cf⁡A⊆x↔¬x∈cf⁡A
158 4 5 157 sylancr ⊢x∈cf⁡A→cf⁡A⊆x↔¬x∈cf⁡A
159 158 ad2antrr ⊢x∈cf⁡A∧∀y∈xG⁡y∈A∧⋃y∈xsuc⁡recs⁡F⁡y=A∧A∈On→cf⁡A⊆x↔¬x∈cf⁡A
160 156 159 mpbid ⊢x∈cf⁡A∧∀y∈xG⁡y∈A∧⋃y∈xsuc⁡recs⁡F⁡y=A∧A∈On→¬x∈cf⁡A
161 104 160 pm2.21dd ⊢x∈cf⁡A∧∀y∈xG⁡y∈A∧⋃y∈xsuc⁡recs⁡F⁡y=A∧A∈On→⋃y∈xsuc⁡recs⁡F⁡y∈A
162 161 ex ⊢x∈cf⁡A∧∀y∈xG⁡y∈A→⋃y∈xsuc⁡recs⁡F⁡y=A∧A∈On→⋃y∈xsuc⁡recs⁡F⁡y∈A
163 162 expcomd ⊢x∈cf⁡A∧∀y∈xG⁡y∈A→A∈On→⋃y∈xsuc⁡recs⁡F⁡y=A→⋃y∈xsuc⁡recs⁡F⁡y∈A
164 163 com12 ⊢A∈On→x∈cf⁡A∧∀y∈xG⁡y∈A→⋃y∈xsuc⁡recs⁡F⁡y=A→⋃y∈xsuc⁡recs⁡F⁡y∈A
165 164 3impib ⊢A∈On∧x∈cf⁡A∧∀y∈xG⁡y∈A→⋃y∈xsuc⁡recs⁡F⁡y=A→⋃y∈xsuc⁡recs⁡F⁡y∈A
166 103 165 jaod ⊢A∈On∧x∈cf⁡A∧∀y∈xG⁡y∈A→⋃y∈xsuc⁡recs⁡F⁡y∈A∨⋃y∈xsuc⁡recs⁡F⁡y=A→⋃y∈xsuc⁡recs⁡F⁡y∈A
167 102 166 sylbid ⊢A∈On∧x∈cf⁡A∧∀y∈xG⁡y∈A→⋃y∈xsuc⁡recs⁡F⁡y⊆A→⋃y∈xsuc⁡recs⁡F⁡y∈A
168 89 167 mpd ⊢A∈On∧x∈cf⁡A∧∀y∈xG⁡y∈A→⋃y∈xsuc⁡recs⁡F⁡y∈A
169 168 3adant1l ⊢g:cf⁡A⟶1-1A∧A∈On∧x∈cf⁡A∧∀y∈xG⁡y∈A→⋃y∈xsuc⁡recs⁡F⁡y∈A
170 ordunel ⊢Ord⁡A∧g⁡x∈A∧⋃y∈xsuc⁡recs⁡F⁡y∈A→g⁡x∪⋃y∈xsuc⁡recs⁡F⁡y∈A
171 71 75 169 170 syl3anc ⊢g:cf⁡A⟶1-1A∧A∈On∧x∈cf⁡A∧∀y∈xG⁡y∈A→g⁡x∪⋃y∈xsuc⁡recs⁡F⁡y∈A
172 68 171 eqeltrd ⊢g:cf⁡A⟶1-1A∧A∈On∧x∈cf⁡A∧∀y∈xG⁡y∈A→G⁡x∈A
173 172 3expia ⊢g:cf⁡A⟶1-1A∧A∈On∧x∈cf⁡A→∀y∈xG⁡y∈A→G⁡x∈A
174 173 3impa ⊢g:cf⁡A⟶1-1A∧A∈On∧x∈cf⁡A→∀y∈xG⁡y∈A→G⁡x∈A
175 20 174 syldc ⊢∀y∈xg:cf⁡A⟶1-1A∧A∈On∧y∈cf⁡A→G⁡y∈A→g:cf⁡A⟶1-1A∧A∈On∧x∈cf⁡A→G⁡x∈A
176 175 a1i ⊢x∈On→∀y∈xg:cf⁡A⟶1-1A∧A∈On∧y∈cf⁡A→G⁡y∈A→g:cf⁡A⟶1-1A∧A∈On∧x∈cf⁡A→G⁡x∈A
177 11 176 tfis2 ⊢x∈On→g:cf⁡A⟶1-1A∧A∈On∧x∈cf⁡A→G⁡x∈A
178 6 177 mpcom ⊢g:cf⁡A⟶1-1A∧A∈On∧x∈cf⁡A→G⁡x∈A
179 178 3expia ⊢g:cf⁡A⟶1-1A∧A∈On→x∈cf⁡A→G⁡x∈A
180 179 ralrimiv ⊢g:cf⁡A⟶1-1A∧A∈On→∀x∈cf⁡AG⁡x∈A
181 4 onssi ⊢cf⁡A⊆On
182 fnssres ⊢recs⁡FFnOn∧cf⁡A⊆On→recs⁡F↾cf⁡AFncf⁡A
183 2 fneq1i ⊢GFncf⁡A↔recs⁡F↾cf⁡AFncf⁡A
184 182 183 sylibr ⊢recs⁡FFnOn∧cf⁡A⊆On→GFncf⁡A
185 25 181 184 mp2an ⊢GFncf⁡A
186 ffnfv ⊢G:cf⁡A⟶A↔GFncf⁡A∧∀x∈cf⁡AG⁡x∈A
187 185 186 mpbiran ⊢G:cf⁡A⟶A↔∀x∈cf⁡AG⁡x∈A
188 180 187 sylibr ⊢g:cf⁡A⟶1-1A∧A∈On→G:cf⁡A⟶A
189 188 adantlr ⊢g:cf⁡A⟶1-1A∧∀z∈A∃w∈cf⁡Az⊆g⁡w∧A∈On→G:cf⁡A⟶A
190 onss ⊢A∈On→A⊆On
191 190 adantl ⊢g:cf⁡A⟶1-1A∧A∈On→A⊆On
192 4 onordi ⊢Ord⁡cf⁡A
193 fvex ⊢recs⁡F⁡y∈V
194 193 sucid ⊢recs⁡F⁡y∈suc⁡recs⁡F⁡y
195 fveq2 ⊢t=y→recs⁡F⁡t=recs⁡F⁡y
196 suceq ⊢recs⁡F⁡t=recs⁡F⁡y→suc⁡recs⁡F⁡t=suc⁡recs⁡F⁡y
197 195 196 syl ⊢t=y→suc⁡recs⁡F⁡t=suc⁡recs⁡F⁡y
198 197 eliuni ⊢y∈x∧recs⁡F⁡y∈suc⁡recs⁡F⁡y→recs⁡F⁡y∈⋃t∈xsuc⁡recs⁡F⁡t
199 198 60 eleqtrrdi ⊢y∈x∧recs⁡F⁡y∈suc⁡recs⁡F⁡y→recs⁡F⁡y∈⋃y∈xsuc⁡recs⁡F⁡y
200 194 199 mpan2 ⊢y∈x→recs⁡F⁡y∈⋃y∈xsuc⁡recs⁡F⁡y
201 elun2 ⊢recs⁡F⁡y∈⋃y∈xsuc⁡recs⁡F⁡y→recs⁡F⁡y∈g⁡x∪⋃y∈xsuc⁡recs⁡F⁡y
202 200 201 syl ⊢y∈x→recs⁡F⁡y∈g⁡x∪⋃y∈xsuc⁡recs⁡F⁡y
203 202 adantr ⊢y∈x∧x∈cf⁡A→recs⁡F⁡y∈g⁡x∪⋃y∈xsuc⁡recs⁡F⁡y
204 5 adantl ⊢y∈x∧x∈cf⁡A→x∈On
205 204 65 syl ⊢y∈x∧x∈cf⁡A→recs⁡F⁡x=g⁡x∪⋃y∈xsuc⁡recs⁡F⁡y
206 203 205 eleqtrrd ⊢y∈x∧x∈cf⁡A→recs⁡F⁡y∈recs⁡F⁡x
207 23 adantl ⊢y∈x∧x∈cf⁡A→G⁡x=recs⁡F⁡x
208 206 78 207 3eltr4d ⊢y∈x∧x∈cf⁡A→G⁡y∈G⁡x
209 208 expcom ⊢x∈cf⁡A→y∈x→G⁡y∈G⁡x
210 209 ralrimiv ⊢x∈cf⁡A→∀y∈xG⁡y∈G⁡x
211 210 rgen ⊢∀x∈cf⁡A∀y∈xG⁡y∈G⁡x
212 issmo2 ⊢G:cf⁡A⟶A→A⊆On∧Ord⁡cf⁡A∧∀x∈cf⁡A∀y∈xG⁡y∈G⁡x→Smo⁡G
213 212 com12 ⊢A⊆On∧Ord⁡cf⁡A∧∀x∈cf⁡A∀y∈xG⁡y∈G⁡x→G:cf⁡A⟶A→Smo⁡G
214 192 211 213 mp3an23 ⊢A⊆On→G:cf⁡A⟶A→Smo⁡G
215 191 188 214 sylc ⊢g:cf⁡A⟶1-1A∧A∈On→Smo⁡G
216 215 adantlr ⊢g:cf⁡A⟶1-1A∧∀z∈A∃w∈cf⁡Az⊆g⁡w∧A∈On→Smo⁡G
217 fveq2 ⊢x=w→g⁡x=g⁡w
218 fveq2 ⊢x=w→G⁡x=G⁡w
219 217 218 sseq12d ⊢x=w→g⁡x⊆G⁡x↔g⁡w⊆G⁡w
220 ssun1 ⊢g⁡x⊆g⁡x∪⋃y∈xsuc⁡recs⁡F⁡y
221 220 67 sseqtrrid ⊢x∈cf⁡A→g⁡x⊆G⁡x
222 219 221 vtoclga ⊢w∈cf⁡A→g⁡w⊆G⁡w
223 sstr ⊢z⊆g⁡w∧g⁡w⊆G⁡w→z⊆G⁡w
224 223 expcom ⊢g⁡w⊆G⁡w→z⊆g⁡w→z⊆G⁡w
225 222 224 syl ⊢w∈cf⁡A→z⊆g⁡w→z⊆G⁡w
226 225 reximia ⊢∃w∈cf⁡Az⊆g⁡w→∃w∈cf⁡Az⊆G⁡w
227 226 ralimi ⊢∀z∈A∃w∈cf⁡Az⊆g⁡w→∀z∈A∃w∈cf⁡Az⊆G⁡w
228 227 ad2antlr ⊢g:cf⁡A⟶1-1A∧∀z∈A∃w∈cf⁡Az⊆g⁡w∧A∈On→∀z∈A∃w∈cf⁡Az⊆G⁡w
229 fnex ⊢GFncf⁡A∧cf⁡A∈On→G∈V
230 185 4 229 mp2an ⊢G∈V
231 feq1 ⊢f=G→f:cf⁡A⟶A↔G:cf⁡A⟶A
232 smoeq ⊢f=G→Smo⁡f↔Smo⁡G
233 fveq1 ⊢f=G→f⁡w=G⁡w
234 233 sseq2d ⊢f=G→z⊆f⁡w↔z⊆G⁡w
235 234 rexbidv ⊢f=G→∃w∈cf⁡Az⊆f⁡w↔∃w∈cf⁡Az⊆G⁡w
236 235 ralbidv ⊢f=G→∀z∈A∃w∈cf⁡Az⊆f⁡w↔∀z∈A∃w∈cf⁡Az⊆G⁡w
237 231 232 236 3anbi123d ⊢f=G→f:cf⁡A⟶A∧Smo⁡f∧∀z∈A∃w∈cf⁡Az⊆f⁡w↔G:cf⁡A⟶A∧Smo⁡G∧∀z∈A∃w∈cf⁡Az⊆G⁡w
238 230 237 spcev ⊢G:cf⁡A⟶A∧Smo⁡G∧∀z∈A∃w∈cf⁡Az⊆G⁡w→∃ff:cf⁡A⟶A∧Smo⁡f∧∀z∈A∃w∈cf⁡Az⊆f⁡w
239 189 216 228 238 syl3anc ⊢g:cf⁡A⟶1-1A∧∀z∈A∃w∈cf⁡Az⊆g⁡w∧A∈On→∃ff:cf⁡A⟶A∧Smo⁡f∧∀z∈A∃w∈cf⁡Az⊆f⁡w
240 239 expcom ⊢A∈On→g:cf⁡A⟶1-1A∧∀z∈A∃w∈cf⁡Az⊆g⁡w→∃ff:cf⁡A⟶A∧Smo⁡f∧∀z∈A∃w∈cf⁡Az⊆f⁡w
241 240 exlimdv ⊢A∈On→∃gg:cf⁡A⟶1-1A∧∀z∈A∃w∈cf⁡Az⊆g⁡w→∃ff:cf⁡A⟶A∧Smo⁡f∧∀z∈A∃w∈cf⁡Az⊆f⁡w
242 3 241 mpd ⊢A∈On→∃ff:cf⁡A⟶A∧Smo⁡f∧∀z∈A∃w∈cf⁡Az⊆f⁡w