Metamath Proof Explorer


Theorem cfsmolem

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

Ref Expression
Hypotheses cfsmolem.2 𝐹 = ( 𝑧 ∈ V ↦ ( ( 𝑔 ‘ dom 𝑧 ) ∪ 𝑡 ∈ dom 𝑧 suc ( 𝑧𝑡 ) ) )
cfsmolem.3 𝐺 = ( recs ( 𝐹 ) ↾ ( cf ‘ 𝐴 ) )
Assertion cfsmolem ( 𝐴 ∈ On → ∃ 𝑓 ( 𝑓 : ( cf ‘ 𝐴 ) ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑧𝐴𝑤 ∈ ( cf ‘ 𝐴 ) 𝑧 ⊆ ( 𝑓𝑤 ) ) )

Proof

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