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 ⁡ z suc ⁡ z ⁡ t
cfsmolem.3 ⊢ G = recs ⁡ F ↾ cf ⁡ A
Assertion cfsmolem ⊢ A ∈ On → ∃ f f : cf ⁡ A ⟶ A ∧ Smo ⁡ f ∧ ∀ z ∈ A ∃ w ∈ cf ⁡ A z ⊆ f ⁡ w

Proof

Step Hyp Ref Expression
1 cfsmolem.2 ⊢ F = z ∈ V ⟼ g ⁡ dom ⁡ z ∪ ⋃ t ∈ dom ⁡ z suc ⁡ z ⁡ t
2 cfsmolem.3 ⊢ G = recs ⁡ F ↾ cf ⁡ A
3 cff1 ⊢ A ∈ On → ∃ g g : cf ⁡ A ⟶ 1-1 A ∧ ∀ z ∈ A ∃ w ∈ cf ⁡ A z ⊆ g ⁡ w
4 cfon ⊢ cf ⁡ A ∈ On
5 4 oneli ⊢ x ∈ cf ⁡ A → x ∈ On
6 5 3ad2ant3 ⊢ g : cf ⁡ A ⟶ 1-1 A ∧ 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-1 A ∧ A ∈ On ∧ x ∈ cf ⁡ A ↔ g : cf ⁡ A ⟶ 1-1 A ∧ 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-1 A ∧ A ∈ On ∧ x ∈ cf ⁡ A → G ⁡ x ∈ A ↔ g : cf ⁡ A ⟶ 1-1 A ∧ A ∈ On ∧ y ∈ cf ⁡ A → G ⁡ y ∈ A
12 simpl1 ⊢ g : cf ⁡ A ⟶ 1-1 A ∧ A ∈ On ∧ x ∈ cf ⁡ A ∧ y ∈ x → g : cf ⁡ A ⟶ 1-1 A
13 simpl2 ⊢ g : cf ⁡ A ⟶ 1-1 A ∧ 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-1 A ∧ A ∈ On ∧ x ∈ cf ⁡ A ∧ y ∈ x → y ∈ cf ⁡ A
18 pm2.27 ⊢ g : cf ⁡ A ⟶ 1-1 A ∧ A ∈ On ∧ y ∈ cf ⁡ A → g : cf ⁡ A ⟶ 1-1 A ∧ A ∈ On ∧ y ∈ cf ⁡ A → G ⁡ y ∈ A → G ⁡ y ∈ A
19 12 13 17 18 syl3anc ⊢ g : cf ⁡ A ⟶ 1-1 A ∧ A ∈ On ∧ x ∈ cf ⁡ A ∧ y ∈ x → g : cf ⁡ A ⟶ 1-1 A ∧ A ∈ On ∧ y ∈ cf ⁡ A → G ⁡ y ∈ A → G ⁡ y ∈ A
20 19 ralimdva ⊢ g : cf ⁡ A ⟶ 1-1 A ∧ A ∈ On ∧ x ∈ cf ⁡ A → ∀ y ∈ x g : cf ⁡ A ⟶ 1-1 A ∧ A ∈ On ∧ y ∈ cf ⁡ A → G ⁡ y ∈ A → ∀ y ∈ x G ⁡ 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 syl5eq ⊢ x ∈ cf ⁡ A → G ⁡ x = recs ⁡ F ⁡ x
24 recsval ⊢ x ∈ On → recs ⁡ F ⁡ x = F ⁡ recs ⁡ F ↾ x
25 recsfnon ⊢ recs ⁡ F Fn On
26 fnfun ⊢ recs ⁡ F Fn On → 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 ⁡ z suc ⁡ z ⁡ t = ⋃ t ∈ dom ⁡ recs ⁡ F ↾ x suc ⁡ recs ⁡ F ↾ x ⁡ t
37 32 36 uneq12d ⊢ z = recs ⁡ F ↾ x → g ⁡ dom ⁡ z ∪ ⋃ t ∈ dom ⁡ z suc ⁡ z ⁡ t = g ⁡ dom ⁡ recs ⁡ F ↾ x ∪ ⋃ t ∈ dom ⁡ recs ⁡ F ↾ x suc ⁡ 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 ↾ x suc ⁡ recs ⁡ F ↾ x ⁡ t ∈ V
43 38 42 unex ⊢ g ⁡ dom ⁡ recs ⁡ F ↾ x ∪ ⋃ t ∈ dom ⁡ recs ⁡ F ↾ x suc ⁡ 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 ↾ x suc ⁡ recs ⁡ F ↾ x ⁡ t
45 30 44 ax-mp ⊢ F ⁡ recs ⁡ F ↾ x = g ⁡ dom ⁡ recs ⁡ F ↾ x ∪ ⋃ t ∈ dom ⁡ recs ⁡ F ↾ x suc ⁡ recs ⁡ F ↾ x ⁡ t
46 24 45 eqtrdi ⊢ x ∈ On → recs ⁡ F ⁡ x = g ⁡ dom ⁡ recs ⁡ F ↾ x ∪ ⋃ t ∈ dom ⁡ recs ⁡ F ↾ x suc ⁡ recs ⁡ F ↾ x ⁡ t
47 onss ⊢ x ∈ On → x ⊆ On
48 fnssres ⊢ recs ⁡ F Fn On ∧ x ⊆ On → recs ⁡ F ↾ x Fn x
49 25 47 48 sylancr ⊢ x ∈ On → recs ⁡ F ↾ x Fn x
50 fndm ⊢ recs ⁡ F ↾ x Fn x → 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 ↾ x suc ⁡ recs ⁡ F ↾ x ⁡ t = ⋃ t ∈ x suc ⁡ 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 ∈ x suc ⁡ recs ⁡ F ↾ x ⁡ t = ⋃ t ∈ x suc ⁡ 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 ∈ x suc ⁡ recs ⁡ F ⁡ y = ⋃ t ∈ x suc ⁡ recs ⁡ F ⁡ t
61 56 60 eqtr4i ⊢ ⋃ t ∈ x suc ⁡ recs ⁡ F ↾ x ⁡ t = ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y
62 52 61 eqtrdi ⊢ dom ⁡ recs ⁡ F ↾ x = x → ⋃ t ∈ dom ⁡ recs ⁡ F ↾ x suc ⁡ recs ⁡ F ↾ x ⁡ t = ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y
63 51 62 uneq12d ⊢ dom ⁡ recs ⁡ F ↾ x = x → g ⁡ dom ⁡ recs ⁡ F ↾ x ∪ ⋃ t ∈ dom ⁡ recs ⁡ F ↾ x suc ⁡ recs ⁡ F ↾ x ⁡ t = g ⁡ x ∪ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y
64 49 50 63 3syl ⊢ x ∈ On → g ⁡ dom ⁡ recs ⁡ F ↾ x ∪ ⋃ t ∈ dom ⁡ recs ⁡ F ↾ x suc ⁡ recs ⁡ F ↾ x ⁡ t = g ⁡ x ∪ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y
65 46 64 eqtrd ⊢ x ∈ On → recs ⁡ F ⁡ x = g ⁡ x ∪ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y
66 5 65 syl ⊢ x ∈ cf ⁡ A → recs ⁡ F ⁡ x = g ⁡ x ∪ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y
67 23 66 eqtrd ⊢ x ∈ cf ⁡ A → G ⁡ x = g ⁡ x ∪ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y
68 67 3ad2ant2 ⊢ g : cf ⁡ A ⟶ 1-1 A ∧ A ∈ On ∧ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A → G ⁡ x = g ⁡ x ∪ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y
69 eloni ⊢ A ∈ On → Ord ⁡ A
70 69 adantl ⊢ g : cf ⁡ A ⟶ 1-1 A ∧ A ∈ On → Ord ⁡ A
71 70 3ad2ant1 ⊢ g : cf ⁡ A ⟶ 1-1 A ∧ A ∈ On ∧ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A → Ord ⁡ A
72 f1f ⊢ g : cf ⁡ A ⟶ 1-1 A → g : cf ⁡ A ⟶ A
73 72 ffvelrnda ⊢ g : cf ⁡ A ⟶ 1-1 A ∧ x ∈ cf ⁡ A → g ⁡ x ∈ A
74 73 adantlr ⊢ g : cf ⁡ A ⟶ 1-1 A ∧ A ∈ On ∧ x ∈ cf ⁡ A → g ⁡ x ∈ A
75 74 3adant3 ⊢ g : cf ⁡ A ⟶ 1-1 A ∧ A ∈ On ∧ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ 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 syl5eq ⊢ 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 ∈ x G ⁡ y ∈ A → ∀ y ∈ x suc ⁡ recs ⁡ F ⁡ y ⊆ A
87 iunss ⊢ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y ⊆ A ↔ ∀ y ∈ x suc ⁡ recs ⁡ F ⁡ y ⊆ A
88 86 87 syl6ibr ⊢ A ∈ On ∧ x ∈ cf ⁡ A → ∀ y ∈ x G ⁡ y ∈ A → ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y ⊆ A
89 88 3impia ⊢ A ∈ On ∧ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A → ⋃ y ∈ x suc ⁡ 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 suceloni ⊢ 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 ∈ x G ⁡ y ∈ A → ∀ y ∈ x suc ⁡ recs ⁡ F ⁡ y ∈ On
97 96 3impia ⊢ A ∈ On ∧ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A → ∀ y ∈ x suc ⁡ recs ⁡ F ⁡ y ∈ On
98 iunon ⊢ x ∈ V ∧ ∀ y ∈ x suc ⁡ recs ⁡ F ⁡ y ∈ On → ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y ∈ On
99 28 97 98 sylancr ⊢ A ∈ On ∧ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A → ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y ∈ On
100 simp1 ⊢ A ∈ On ∧ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A → A ∈ On
101 onsseleq ⊢ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y ∈ On ∧ A ∈ On → ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y ⊆ A ↔ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y ∈ A ∨ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y = A
102 99 100 101 syl2anc ⊢ A ∈ On ∧ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A → ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y ⊆ A ↔ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y ∈ A ∨ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y = A
103 idd ⊢ A ∈ On ∧ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A → ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y ∈ A → ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y ∈ A
104 simpll ⊢ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A ∧ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y = A ∧ A ∈ On → x ∈ cf ⁡ A
105 simprr ⊢ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A ∧ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y = A ∧ A ∈ On → A ∈ On
106 5 ad2antrr ⊢ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A ∧ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y = A ∧ A ∈ On → x ∈ On
107 5 49 syl ⊢ x ∈ cf ⁡ A → recs ⁡ F ↾ x Fn x
108 107 adantr ⊢ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A → recs ⁡ F ↾ x Fn x
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 ∈ x G ⁡ y ∈ A ↔ ∀ y ∈ x recs ⁡ F ↾ x ⁡ y ∈ A
115 114 biimpa ⊢ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A → ∀ y ∈ x recs ⁡ F ↾ x ⁡ y ∈ A
116 ffnfv ⊢ recs ⁡ F ↾ x : x ⟶ A ↔ recs ⁡ F ↾ x Fn x ∧ ∀ y ∈ x recs ⁡ F ↾ x ⁡ y ∈ A
117 108 115 116 sylanbrc ⊢ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A → recs ⁡ F ↾ x : x ⟶ A
118 eleq2 ⊢ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y = A → t ∈ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y ↔ t ∈ A
119 118 biimpar ⊢ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y = A ∧ t ∈ A → t ∈ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y
120 119 adantrl ⊢ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y = A ∧ A ∈ On ∧ t ∈ A → t ∈ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y
121 120 3adant1 ⊢ recs ⁡ F ↾ x : x ⟶ A ∧ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y = A ∧ A ∈ On ∧ t ∈ A → t ∈ ⋃ y ∈ x suc ⁡ 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 ffvelrn ⊢ 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 ∈ x t ⊆ recs ⁡ F ⁡ y ↔ ∃ y ∈ x t ∈ suc ⁡ recs ⁡ F ⁡ y
132 eliun ⊢ t ∈ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y ↔ ∃ y ∈ x t ∈ suc ⁡ recs ⁡ F ⁡ y
133 131 132 bitr4di ⊢ A ∈ On ∧ t ∈ A ∧ recs ⁡ F ↾ x : x ⟶ A → ∃ y ∈ x t ⊆ recs ⁡ F ⁡ y ↔ t ∈ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y
134 133 ancoms ⊢ recs ⁡ F ↾ x : x ⟶ A ∧ A ∈ On ∧ t ∈ A → ∃ y ∈ x t ⊆ recs ⁡ F ⁡ y ↔ t ∈ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y
135 134 3adant2 ⊢ recs ⁡ F ↾ x : x ⟶ A ∧ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y = A ∧ A ∈ On ∧ t ∈ A → ∃ y ∈ x t ⊆ recs ⁡ F ⁡ y ↔ t ∈ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y
136 121 135 mpbird ⊢ recs ⁡ F ↾ x : x ⟶ A ∧ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y = A ∧ A ∈ On ∧ t ∈ A → ∃ y ∈ x t ⊆ recs ⁡ F ⁡ y
137 136 3expa ⊢ recs ⁡ F ↾ x : x ⟶ A ∧ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y = A ∧ A ∈ On ∧ t ∈ A → ∃ y ∈ x t ⊆ recs ⁡ F ⁡ y
138 137 anassrs ⊢ recs ⁡ F ↾ x : x ⟶ A ∧ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y = A ∧ A ∈ On ∧ t ∈ A → ∃ y ∈ x t ⊆ recs ⁡ F ⁡ y
139 138 ralrimiva ⊢ recs ⁡ F ↾ x : x ⟶ A ∧ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y = A ∧ A ∈ On → ∀ t ∈ A ∃ y ∈ x t ⊆ recs ⁡ F ⁡ y
140 139 expl ⊢ recs ⁡ F ↾ x : x ⟶ A → ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y = A ∧ A ∈ On → ∀ t ∈ A ∃ y ∈ x t ⊆ recs ⁡ F ⁡ y
141 117 140 syl ⊢ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A → ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y = A ∧ A ∈ On → ∀ t ∈ A ∃ y ∈ x t ⊆ recs ⁡ F ⁡ y
142 141 imp ⊢ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A ∧ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y = A ∧ A ∈ On → ∀ t ∈ A ∃ y ∈ x t ⊆ 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 ∈ x t ⊆ f ⁡ y ↔ ∃ y ∈ x t ⊆ recs ⁡ F ↾ x ⁡ y
147 110 sseq2d ⊢ y ∈ x → t ⊆ recs ⁡ F ↾ x ⁡ y ↔ t ⊆ recs ⁡ F ⁡ y
148 147 rexbiia ⊢ ∃ y ∈ x t ⊆ recs ⁡ F ↾ x ⁡ y ↔ ∃ y ∈ x t ⊆ recs ⁡ F ⁡ y
149 146 148 bitrdi ⊢ f = recs ⁡ F ↾ x → ∃ y ∈ x t ⊆ f ⁡ y ↔ ∃ y ∈ x t ⊆ recs ⁡ F ⁡ y
150 149 ralbidv ⊢ f = recs ⁡ F ↾ x → ∀ t ∈ A ∃ y ∈ x t ⊆ f ⁡ y ↔ ∀ t ∈ A ∃ y ∈ x t ⊆ recs ⁡ F ⁡ y
151 143 150 anbi12d ⊢ f = recs ⁡ F ↾ x → f : x ⟶ A ∧ ∀ t ∈ A ∃ y ∈ x t ⊆ f ⁡ y ↔ recs ⁡ F ↾ x : x ⟶ A ∧ ∀ t ∈ A ∃ y ∈ x t ⊆ recs ⁡ F ⁡ y
152 30 151 spcev ⊢ recs ⁡ F ↾ x : x ⟶ A ∧ ∀ t ∈ A ∃ y ∈ x t ⊆ recs ⁡ F ⁡ y → ∃ f f : x ⟶ A ∧ ∀ t ∈ A ∃ y ∈ x t ⊆ f ⁡ y
153 117 142 152 syl2an2r ⊢ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A ∧ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y = A ∧ A ∈ On → ∃ f f : x ⟶ A ∧ ∀ t ∈ A ∃ y ∈ x t ⊆ f ⁡ y
154 cfflb ⊢ A ∈ On ∧ x ∈ On → ∃ f f : x ⟶ A ∧ ∀ t ∈ A ∃ y ∈ x t ⊆ f ⁡ y → cf ⁡ A ⊆ x
155 154 imp ⊢ A ∈ On ∧ x ∈ On ∧ ∃ f f : x ⟶ A ∧ ∀ t ∈ A ∃ y ∈ x t ⊆ f ⁡ y → cf ⁡ A ⊆ x
156 105 106 153 155 syl21anc ⊢ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A ∧ ⋃ y ∈ x suc ⁡ 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 ∈ x G ⁡ y ∈ A ∧ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y = A ∧ A ∈ On → cf ⁡ A ⊆ x ↔ ¬ x ∈ cf ⁡ A
160 156 159 mpbid ⊢ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A ∧ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y = A ∧ A ∈ On → ¬ x ∈ cf ⁡ A
161 104 160 pm2.21dd ⊢ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A ∧ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y = A ∧ A ∈ On → ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y ∈ A
162 161 ex ⊢ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A → ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y = A ∧ A ∈ On → ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y ∈ A
163 162 expcomd ⊢ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A → A ∈ On → ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y = A → ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y ∈ A
164 163 com12 ⊢ A ∈ On → x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A → ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y = A → ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y ∈ A
165 164 3impib ⊢ A ∈ On ∧ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A → ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y = A → ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y ∈ A
166 103 165 jaod ⊢ A ∈ On ∧ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A → ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y ∈ A ∨ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y = A → ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y ∈ A
167 102 166 sylbid ⊢ A ∈ On ∧ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A → ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y ⊆ A → ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y ∈ A
168 89 167 mpd ⊢ A ∈ On ∧ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A → ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y ∈ A
169 168 3adant1l ⊢ g : cf ⁡ A ⟶ 1-1 A ∧ A ∈ On ∧ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A → ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y ∈ A
170 ordunel ⊢ Ord ⁡ A ∧ g ⁡ x ∈ A ∧ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y ∈ A → g ⁡ x ∪ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y ∈ A
171 71 75 169 170 syl3anc ⊢ g : cf ⁡ A ⟶ 1-1 A ∧ A ∈ On ∧ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A → g ⁡ x ∪ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y ∈ A
172 68 171 eqeltrd ⊢ g : cf ⁡ A ⟶ 1-1 A ∧ A ∈ On ∧ x ∈ cf ⁡ A ∧ ∀ y ∈ x G ⁡ y ∈ A → G ⁡ x ∈ A
173 172 3expia ⊢ g : cf ⁡ A ⟶ 1-1 A ∧ A ∈ On ∧ x ∈ cf ⁡ A → ∀ y ∈ x G ⁡ y ∈ A → G ⁡ x ∈ A
174 173 3impa ⊢ g : cf ⁡ A ⟶ 1-1 A ∧ A ∈ On ∧ x ∈ cf ⁡ A → ∀ y ∈ x G ⁡ y ∈ A → G ⁡ x ∈ A
175 20 174 syldc ⊢ ∀ y ∈ x g : cf ⁡ A ⟶ 1-1 A ∧ A ∈ On ∧ y ∈ cf ⁡ A → G ⁡ y ∈ A → g : cf ⁡ A ⟶ 1-1 A ∧ A ∈ On ∧ x ∈ cf ⁡ A → G ⁡ x ∈ A
176 175 a1i ⊢ x ∈ On → ∀ y ∈ x g : cf ⁡ A ⟶ 1-1 A ∧ A ∈ On ∧ y ∈ cf ⁡ A → G ⁡ y ∈ A → g : cf ⁡ A ⟶ 1-1 A ∧ A ∈ On ∧ x ∈ cf ⁡ A → G ⁡ x ∈ A
177 11 176 tfis2 ⊢ x ∈ On → g : cf ⁡ A ⟶ 1-1 A ∧ A ∈ On ∧ x ∈ cf ⁡ A → G ⁡ x ∈ A
178 6 177 mpcom ⊢ g : cf ⁡ A ⟶ 1-1 A ∧ A ∈ On ∧ x ∈ cf ⁡ A → G ⁡ x ∈ A
179 178 3expia ⊢ g : cf ⁡ A ⟶ 1-1 A ∧ A ∈ On → x ∈ cf ⁡ A → G ⁡ x ∈ A
180 179 ralrimiv ⊢ g : cf ⁡ A ⟶ 1-1 A ∧ A ∈ On → ∀ x ∈ cf ⁡ A G ⁡ x ∈ A
181 4 onssi ⊢ cf ⁡ A ⊆ On
182 fnssres ⊢ recs ⁡ F Fn On ∧ cf ⁡ A ⊆ On → recs ⁡ F ↾ cf ⁡ A Fn cf ⁡ A
183 2 fneq1i ⊢ G Fn cf ⁡ A ↔ recs ⁡ F ↾ cf ⁡ A Fn cf ⁡ A
184 182 183 sylibr ⊢ recs ⁡ F Fn On ∧ cf ⁡ A ⊆ On → G Fn cf ⁡ A
185 25 181 184 mp2an ⊢ G Fn cf ⁡ A
186 ffnfv ⊢ G : cf ⁡ A ⟶ A ↔ G Fn cf ⁡ A ∧ ∀ x ∈ cf ⁡ A G ⁡ x ∈ A
187 185 186 mpbiran ⊢ G : cf ⁡ A ⟶ A ↔ ∀ x ∈ cf ⁡ A G ⁡ x ∈ A
188 180 187 sylibr ⊢ g : cf ⁡ A ⟶ 1-1 A ∧ A ∈ On → G : cf ⁡ A ⟶ A
189 188 adantlr ⊢ g : cf ⁡ A ⟶ 1-1 A ∧ ∀ z ∈ A ∃ w ∈ cf ⁡ A z ⊆ g ⁡ w ∧ A ∈ On → G : cf ⁡ A ⟶ A
190 onss ⊢ A ∈ On → A ⊆ On
191 190 adantl ⊢ g : cf ⁡ A ⟶ 1-1 A ∧ 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 ∈ x suc ⁡ recs ⁡ F ⁡ t
199 198 60 eleqtrrdi ⊢ y ∈ x ∧ recs ⁡ F ⁡ y ∈ suc ⁡ recs ⁡ F ⁡ y → recs ⁡ F ⁡ y ∈ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y
200 194 199 mpan2 ⊢ y ∈ x → recs ⁡ F ⁡ y ∈ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y
201 elun2 ⊢ recs ⁡ F ⁡ y ∈ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y → recs ⁡ F ⁡ y ∈ g ⁡ x ∪ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y
202 200 201 syl ⊢ y ∈ x → recs ⁡ F ⁡ y ∈ g ⁡ x ∪ ⋃ y ∈ x suc ⁡ recs ⁡ F ⁡ y
203 202 adantr ⊢ y ∈ x ∧ x ∈ cf ⁡ A → recs ⁡ F ⁡ y ∈ g ⁡ x ∪ ⋃ y ∈ x suc ⁡ 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 ∈ x suc ⁡ 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 ∈ x G ⁡ y ∈ G ⁡ x
211 210 rgen ⊢ ∀ x ∈ cf ⁡ A ∀ y ∈ x G ⁡ y ∈ G ⁡ x
212 issmo2 ⊢ G : cf ⁡ A ⟶ A → A ⊆ On ∧ Ord ⁡ cf ⁡ A ∧ ∀ x ∈ cf ⁡ A ∀ y ∈ x G ⁡ y ∈ G ⁡ x → Smo ⁡ G
213 212 com12 ⊢ A ⊆ On ∧ Ord ⁡ cf ⁡ A ∧ ∀ x ∈ cf ⁡ A ∀ y ∈ x G ⁡ 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-1 A ∧ A ∈ On → Smo ⁡ G
216 215 adantlr ⊢ g : cf ⁡ A ⟶ 1-1 A ∧ ∀ z ∈ A ∃ w ∈ cf ⁡ A z ⊆ 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 ∈ x suc ⁡ 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 ⁡ A z ⊆ g ⁡ w → ∃ w ∈ cf ⁡ A z ⊆ G ⁡ w
227 226 ralimi ⊢ ∀ z ∈ A ∃ w ∈ cf ⁡ A z ⊆ g ⁡ w → ∀ z ∈ A ∃ w ∈ cf ⁡ A z ⊆ G ⁡ w
228 227 ad2antlr ⊢ g : cf ⁡ A ⟶ 1-1 A ∧ ∀ z ∈ A ∃ w ∈ cf ⁡ A z ⊆ g ⁡ w ∧ A ∈ On → ∀ z ∈ A ∃ w ∈ cf ⁡ A z ⊆ G ⁡ w
229 fnex ⊢ G Fn cf ⁡ 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 ⁡ A z ⊆ f ⁡ w ↔ ∃ w ∈ cf ⁡ A z ⊆ G ⁡ w
236 235 ralbidv ⊢ f = G → ∀ z ∈ A ∃ w ∈ cf ⁡ A z ⊆ f ⁡ w ↔ ∀ z ∈ A ∃ w ∈ cf ⁡ A z ⊆ G ⁡ w
237 231 232 236 3anbi123d ⊢ f = G → f : cf ⁡ A ⟶ A ∧ Smo ⁡ f ∧ ∀ z ∈ A ∃ w ∈ cf ⁡ A z ⊆ f ⁡ w ↔ G : cf ⁡ A ⟶ A ∧ Smo ⁡ G ∧ ∀ z ∈ A ∃ w ∈ cf ⁡ A z ⊆ G ⁡ w
238 230 237 spcev ⊢ G : cf ⁡ A ⟶ A ∧ Smo ⁡ G ∧ ∀ z ∈ A ∃ w ∈ cf ⁡ A z ⊆ G ⁡ w → ∃ f f : cf ⁡ A ⟶ A ∧ Smo ⁡ f ∧ ∀ z ∈ A ∃ w ∈ cf ⁡ A z ⊆ f ⁡ w
239 189 216 228 238 syl3anc ⊢ g : cf ⁡ A ⟶ 1-1 A ∧ ∀ z ∈ A ∃ w ∈ cf ⁡ A z ⊆ g ⁡ w ∧ A ∈ On → ∃ f f : cf ⁡ A ⟶ A ∧ Smo ⁡ f ∧ ∀ z ∈ A ∃ w ∈ cf ⁡ A z ⊆ f ⁡ w
240 239 expcom ⊢ A ∈ On → g : cf ⁡ A ⟶ 1-1 A ∧ ∀ z ∈ A ∃ w ∈ cf ⁡ A z ⊆ g ⁡ w → ∃ f f : cf ⁡ A ⟶ A ∧ Smo ⁡ f ∧ ∀ z ∈ A ∃ w ∈ cf ⁡ A z ⊆ f ⁡ w
241 240 exlimdv ⊢ A ∈ On → ∃ g g : cf ⁡ A ⟶ 1-1 A ∧ ∀ z ∈ A ∃ w ∈ cf ⁡ A z ⊆ g ⁡ w → ∃ f f : cf ⁡ A ⟶ A ∧ Smo ⁡ f ∧ ∀ z ∈ A ∃ w ∈ cf ⁡ A z ⊆ f ⁡ w
242 3 241 mpd ⊢ A ∈ On → ∃ f f : cf ⁡ A ⟶ A ∧ Smo ⁡ f ∧ ∀ z ∈ A ∃ w ∈ cf ⁡ A z ⊆ f ⁡ w