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

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 ffvelcdmda ⊢ ( ( 𝑔 : ( 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 imbitrrdi ⊢ ( ( 𝐴 ∈ 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 onsuc ⊢ ( ( 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 ffvelcdm ⊢ ( ( ( 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 ‘ 𝐴 ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) )