| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cff1 10298 | . 2
⊢ (𝐴 ∈ On → ∃𝑔(𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤))) | 
| 2 |  | cfon 10295 | . . . . . . . . . . . 12
⊢
(cf‘𝐴) ∈
On | 
| 3 | 2 | oneli 6498 | . . . . . . . . . . 11
⊢ (𝑥 ∈ (cf‘𝐴) → 𝑥 ∈ On) | 
| 4 | 3 | 3ad2ant3 1136 | . . . . . . . . . 10
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → 𝑥 ∈ On) | 
| 5 |  | eleq1w 2824 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝑥 ∈ (cf‘𝐴) ↔ 𝑦 ∈ (cf‘𝐴))) | 
| 6 | 5 | 3anbi3d 1444 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ↔ (𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)))) | 
| 7 |  | fveq2 6906 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝐺‘𝑥) = (𝐺‘𝑦)) | 
| 8 | 7 | eleq1d 2826 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((𝐺‘𝑥) ∈ 𝐴 ↔ (𝐺‘𝑦) ∈ 𝐴)) | 
| 9 | 6, 8 | imbi12d 344 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) ∈ 𝐴) ↔ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ 𝐴))) | 
| 10 |  | simpl1 1192 | . . . . . . . . . . . . . . 15
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → 𝑔:(cf‘𝐴)–1-1→𝐴) | 
| 11 |  | simpl2 1193 | . . . . . . . . . . . . . . 15
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → 𝐴 ∈ On) | 
| 12 |  | ontr1 6430 | . . . . . . . . . . . . . . . . . 18
⊢
((cf‘𝐴) ∈
On → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → 𝑦 ∈ (cf‘𝐴))) | 
| 13 | 2, 12 | ax-mp 5 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → 𝑦 ∈ (cf‘𝐴)) | 
| 14 | 13 | ancoms 458 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ (cf‘𝐴)) | 
| 15 | 14 | 3ad2antl3 1188 | . . . . . . . . . . . . . . 15
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ (cf‘𝐴)) | 
| 16 |  | pm2.27 42 | . . . . . . . . . . . . . . 15
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ 𝐴) → (𝐺‘𝑦) ∈ 𝐴)) | 
| 17 | 10, 11, 15, 16 | syl3anc 1373 | . . . . . . . . . . . . . 14
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ 𝐴) → (𝐺‘𝑦) ∈ 𝐴)) | 
| 18 | 17 | ralimdva 3167 | . . . . . . . . . . . . 13
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ 𝐴) → ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴)) | 
| 19 |  | cfsmolem.3 | . . . . . . . . . . . . . . . . . . . 20
⊢ 𝐺 = (recs(𝐹) ↾ (cf‘𝐴)) | 
| 20 | 19 | fveq1i 6907 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐺‘𝑥) = ((recs(𝐹) ↾ (cf‘𝐴))‘𝑥) | 
| 21 |  | fvres 6925 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (cf‘𝐴) → ((recs(𝐹) ↾ (cf‘𝐴))‘𝑥) = (recs(𝐹)‘𝑥)) | 
| 22 | 20, 21 | eqtrid 2789 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (cf‘𝐴) → (𝐺‘𝑥) = (recs(𝐹)‘𝑥)) | 
| 23 |  | recsval 8444 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ On → (recs(𝐹)‘𝑥) = (𝐹‘(recs(𝐹) ↾ 𝑥))) | 
| 24 |  | recsfnon 8443 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
recs(𝐹) Fn
On | 
| 25 |  | fnfun 6668 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(recs(𝐹) Fn On
→ Fun recs(𝐹)) | 
| 26 | 24, 25 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ Fun
recs(𝐹) | 
| 27 |  | vex 3484 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑥 ∈ V | 
| 28 |  | resfunexg 7235 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((Fun
recs(𝐹) ∧ 𝑥 ∈ V) → (recs(𝐹) ↾ 𝑥) ∈ V) | 
| 29 | 26, 27, 28 | mp2an 692 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(recs(𝐹) ↾
𝑥) ∈
V | 
| 30 |  | dmeq 5914 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → dom 𝑧 = dom (recs(𝐹) ↾ 𝑥)) | 
| 31 | 30 | fveq2d 6910 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → (𝑔‘dom 𝑧) = (𝑔‘dom (recs(𝐹) ↾ 𝑥))) | 
| 32 |  | fveq1 6905 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → (𝑧‘𝑡) = ((recs(𝐹) ↾ 𝑥)‘𝑡)) | 
| 33 |  | suceq 6450 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑧‘𝑡) = ((recs(𝐹) ↾ 𝑥)‘𝑡) → suc (𝑧‘𝑡) = suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) | 
| 34 | 32, 33 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → suc (𝑧‘𝑡) = suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) | 
| 35 | 30, 34 | iuneq12d 5021 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → ∪
𝑡 ∈ dom 𝑧 suc (𝑧‘𝑡) = ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) | 
| 36 | 31, 35 | uneq12d 4169 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → ((𝑔‘dom 𝑧) ∪ ∪
𝑡 ∈ dom 𝑧 suc (𝑧‘𝑡)) = ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ ∪
𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡))) | 
| 37 |  | cfsmolem.2 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝐹 = (𝑧 ∈ V ↦ ((𝑔‘dom 𝑧) ∪ ∪
𝑡 ∈ dom 𝑧 suc (𝑧‘𝑡))) | 
| 38 |  | fvex 6919 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∈ V | 
| 39 | 29 | dmex 7931 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ dom
(recs(𝐹) ↾ 𝑥) ∈ V | 
| 40 |  | fvex 6919 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((recs(𝐹) ↾
𝑥)‘𝑡) ∈ V | 
| 41 | 40 | sucex 7826 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ suc
((recs(𝐹) ↾ 𝑥)‘𝑡) ∈ V | 
| 42 | 39, 41 | iunex 7993 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡) ∈ V | 
| 43 | 38, 42 | unex 7764 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ ∪
𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) ∈ V | 
| 44 | 36, 37, 43 | fvmpt 7016 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((recs(𝐹) ↾
𝑥) ∈ V → (𝐹‘(recs(𝐹) ↾ 𝑥)) = ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ ∪
𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡))) | 
| 45 | 29, 44 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹‘(recs(𝐹) ↾ 𝑥)) = ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ ∪
𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) | 
| 46 | 23, 45 | eqtrdi 2793 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ On → (recs(𝐹)‘𝑥) = ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ ∪
𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡))) | 
| 47 |  | onss 7805 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ On → 𝑥 ⊆ On) | 
| 48 |  | fnssres 6691 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((recs(𝐹) Fn On
∧ 𝑥 ⊆ On) →
(recs(𝐹) ↾ 𝑥) Fn 𝑥) | 
| 49 | 24, 47, 48 | sylancr 587 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ On → (recs(𝐹) ↾ 𝑥) Fn 𝑥) | 
| 50 |  | fndm 6671 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((recs(𝐹) ↾
𝑥) Fn 𝑥 → dom (recs(𝐹) ↾ 𝑥) = 𝑥) | 
| 51 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (dom
(recs(𝐹) ↾ 𝑥) = 𝑥 → (𝑔‘dom (recs(𝐹) ↾ 𝑥)) = (𝑔‘𝑥)) | 
| 52 |  | iuneq1 5008 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (dom
(recs(𝐹) ↾ 𝑥) = 𝑥 → ∪
𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = ∪ 𝑡 ∈ 𝑥 suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) | 
| 53 |  | fvres 6925 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 ∈ 𝑥 → ((recs(𝐹) ↾ 𝑥)‘𝑡) = (recs(𝐹)‘𝑡)) | 
| 54 |  | suceq 6450 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((recs(𝐹) ↾
𝑥)‘𝑡) = (recs(𝐹)‘𝑡) → suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = suc (recs(𝐹)‘𝑡)) | 
| 55 | 53, 54 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 ∈ 𝑥 → suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = suc (recs(𝐹)‘𝑡)) | 
| 56 | 55 | iuneq2i 5013 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ∪ 𝑡 ∈ 𝑥 suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = ∪ 𝑡 ∈ 𝑥 suc (recs(𝐹)‘𝑡) | 
| 57 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = 𝑡 → (recs(𝐹)‘𝑦) = (recs(𝐹)‘𝑡)) | 
| 58 |  | suceq 6450 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((recs(𝐹)‘𝑦) = (recs(𝐹)‘𝑡) → suc (recs(𝐹)‘𝑦) = suc (recs(𝐹)‘𝑡)) | 
| 59 | 57, 58 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = 𝑡 → suc (recs(𝐹)‘𝑦) = suc (recs(𝐹)‘𝑡)) | 
| 60 | 59 | cbviunv 5040 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = ∪ 𝑡 ∈ 𝑥 suc (recs(𝐹)‘𝑡) | 
| 61 | 56, 60 | eqtr4i 2768 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ∪ 𝑡 ∈ 𝑥 suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) | 
| 62 | 52, 61 | eqtrdi 2793 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (dom
(recs(𝐹) ↾ 𝑥) = 𝑥 → ∪
𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) | 
| 63 | 51, 62 | uneq12d 4169 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (dom
(recs(𝐹) ↾ 𝑥) = 𝑥 → ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ ∪
𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) = ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) | 
| 64 | 49, 50, 63 | 3syl 18 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ On → ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ ∪
𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) = ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) | 
| 65 | 46, 64 | eqtrd 2777 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ On → (recs(𝐹)‘𝑥) = ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) | 
| 66 | 3, 65 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (cf‘𝐴) → (recs(𝐹)‘𝑥) = ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) | 
| 67 | 22, 66 | eqtrd 2777 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (cf‘𝐴) → (𝐺‘𝑥) = ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) | 
| 68 | 67 | 3ad2ant2 1135 | . . . . . . . . . . . . . . . 16
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (𝐺‘𝑥) = ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) | 
| 69 |  | eloni 6394 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ On → Ord 𝐴) | 
| 70 | 69 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → Ord 𝐴) | 
| 71 | 70 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → Ord 𝐴) | 
| 72 |  | f1f 6804 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔:(cf‘𝐴)–1-1→𝐴 → 𝑔:(cf‘𝐴)⟶𝐴) | 
| 73 | 72 | ffvelcdmda 7104 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝑥 ∈ (cf‘𝐴)) → (𝑔‘𝑥) ∈ 𝐴) | 
| 74 | 73 | adantlr 715 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴)) → (𝑔‘𝑥) ∈ 𝐴) | 
| 75 | 74 | 3adant3 1133 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (𝑔‘𝑥) ∈ 𝐴) | 
| 76 | 19 | fveq1i 6907 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐺‘𝑦) = ((recs(𝐹) ↾ (cf‘𝐴))‘𝑦) | 
| 77 | 13 | fvresd 6926 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → ((recs(𝐹) ↾ (cf‘𝐴))‘𝑦) = (recs(𝐹)‘𝑦)) | 
| 78 | 76, 77 | eqtrid 2789 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑦) = (recs(𝐹)‘𝑦)) | 
| 79 | 78 | adantrl 716 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ 𝑥 ∧ (𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴))) → (𝐺‘𝑦) = (recs(𝐹)‘𝑦)) | 
| 80 | 79 | ancoms 458 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → (𝐺‘𝑦) = (recs(𝐹)‘𝑦)) | 
| 81 | 80 | eleq1d 2826 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 ↔ (recs(𝐹)‘𝑦) ∈ 𝐴)) | 
| 82 |  | ordsucss 7838 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (Ord
𝐴 → ((recs(𝐹)‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴)) | 
| 83 | 69, 82 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ∈ On → ((recs(𝐹)‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴)) | 
| 84 | 83 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹)‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴)) | 
| 85 | 81, 84 | sylbid 240 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴)) | 
| 86 | 85 | ralimdva 3167 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 → ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴)) | 
| 87 |  | iunss 5045 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 ↔ ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴) | 
| 88 | 86, 87 | imbitrrdi 252 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴)) | 
| 89 | 88 | 3impia 1118 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴) | 
| 90 |  | onelon 6409 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈ On ∧ (recs(𝐹)‘𝑦) ∈ 𝐴) → (recs(𝐹)‘𝑦) ∈ On) | 
| 91 | 90 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐴 ∈ On → ((recs(𝐹)‘𝑦) ∈ 𝐴 → (recs(𝐹)‘𝑦) ∈ On)) | 
| 92 | 91 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹)‘𝑦) ∈ 𝐴 → (recs(𝐹)‘𝑦) ∈ On)) | 
| 93 | 81, 92 | sylbid 240 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 → (recs(𝐹)‘𝑦) ∈ On)) | 
| 94 |  | onsuc 7831 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((recs(𝐹)‘𝑦) ∈ On → suc (recs(𝐹)‘𝑦) ∈ On) | 
| 95 | 93, 94 | syl6 35 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ∈ On)) | 
| 96 | 95 | ralimdva 3167 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 → ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On)) | 
| 97 | 96 | 3impia 1118 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On) | 
| 98 |  | iunon 8379 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ V ∧ ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On) | 
| 99 | 27, 97, 98 | sylancr 587 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On) | 
| 100 |  | simp1 1137 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → 𝐴 ∈ On) | 
| 101 |  | onsseleq 6425 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On ∧ 𝐴 ∈ On) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 ↔ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 ∨ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴))) | 
| 102 | 99, 100, 101 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 ↔ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 ∨ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴))) | 
| 103 |  | idd 24 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)) | 
| 104 |  | simpll 767 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → 𝑥 ∈ (cf‘𝐴)) | 
| 105 |  | simprr 773 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → 𝐴 ∈ On) | 
| 106 | 3 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → 𝑥 ∈ On) | 
| 107 | 3, 49 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥 ∈ (cf‘𝐴) → (recs(𝐹) ↾ 𝑥) Fn 𝑥) | 
| 108 | 107 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (recs(𝐹) ↾ 𝑥) Fn 𝑥) | 
| 109 | 78 | ancoms 458 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → (𝐺‘𝑦) = (recs(𝐹)‘𝑦)) | 
| 110 |  | fvres 6925 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑦 ∈ 𝑥 → ((recs(𝐹) ↾ 𝑥)‘𝑦) = (recs(𝐹)‘𝑦)) | 
| 111 | 110 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹) ↾ 𝑥)‘𝑦) = (recs(𝐹)‘𝑦)) | 
| 112 | 109, 111 | eqtr4d 2780 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → (𝐺‘𝑦) = ((recs(𝐹) ↾ 𝑥)‘𝑦)) | 
| 113 | 112 | eleq1d 2826 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 ↔ ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴)) | 
| 114 | 113 | ralbidva 3176 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥 ∈ (cf‘𝐴) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 ↔ ∀𝑦 ∈ 𝑥 ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴)) | 
| 115 | 114 | biimpa 476 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∀𝑦 ∈ 𝑥 ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴) | 
| 116 |  | ffnfv 7139 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ↔ ((recs(𝐹) ↾ 𝑥) Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴)) | 
| 117 | 108, 115,
116 | sylanbrc 583 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴) | 
| 118 |  | eleq2 2830 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 → (𝑡 ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ 𝐴)) | 
| 119 | 118 | biimpar 477 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝑡 ∈ 𝐴) → 𝑡 ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) | 
| 120 | 119 | adantrl 716 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → 𝑡 ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) | 
| 121 | 120 | 3adant1 1131 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → 𝑡 ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) | 
| 122 |  | onelon 6409 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) → 𝑡 ∈ On) | 
| 123 | 110 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢
(((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹) ↾ 𝑥)‘𝑦) = (recs(𝐹)‘𝑦)) | 
| 124 |  | ffvelcdm 7101 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢
(((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴) | 
| 125 | 123, 124 | eqeltrrd 2842 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢
(((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥) → (recs(𝐹)‘𝑦) ∈ 𝐴) | 
| 126 | 125, 90 | sylan2 593 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝐴 ∈ On ∧ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥)) → (recs(𝐹)‘𝑦) ∈ On) | 
| 127 | 126 | adantlr 715 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥)) → (recs(𝐹)‘𝑦) ∈ On) | 
| 128 |  | onsssuc 6474 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑡 ∈ On ∧ (recs(𝐹)‘𝑦) ∈ On) → (𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ suc (recs(𝐹)‘𝑦))) | 
| 129 | 122, 127,
128 | syl2an2r 685 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥)) → (𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ suc (recs(𝐹)‘𝑦))) | 
| 130 | 129 | anassrs 467 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴) ∧ 𝑦 ∈ 𝑥) → (𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ suc (recs(𝐹)‘𝑦))) | 
| 131 | 130 | rexbidva 3177 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ∈ suc (recs(𝐹)‘𝑦))) | 
| 132 |  | eliun 4995 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑡 ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ∈ suc (recs(𝐹)‘𝑦)) | 
| 133 | 131, 132 | bitr4di 289 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) | 
| 134 | 133 | ancoms 458 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) | 
| 135 | 134 | 3adant2 1132 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) | 
| 136 | 121, 135 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)) | 
| 137 | 136 | 3expa 1119 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)) | 
| 138 | 137 | anassrs 467 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) ∧ 𝐴 ∈ On) ∧ 𝑡 ∈ 𝐴) → ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)) | 
| 139 | 138 | ralrimiva 3146 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) ∧ 𝐴 ∈ On) → ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)) | 
| 140 | 139 | expl 457 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 → ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On) → ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))) | 
| 141 | 117, 140 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On) → ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))) | 
| 142 | 141 | imp 406 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)) | 
| 143 |  | feq1 6716 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (𝑓:𝑥⟶𝐴 ↔ (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴)) | 
| 144 |  | fveq1 6905 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (𝑓‘𝑦) = ((recs(𝐹) ↾ 𝑥)‘𝑦)) | 
| 145 | 144 | sseq2d 4016 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (𝑡 ⊆ (𝑓‘𝑦) ↔ 𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦))) | 
| 146 | 145 | rexbidv 3179 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦))) | 
| 147 | 110 | sseq2d 4016 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑦 ∈ 𝑥 → (𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦) ↔ 𝑡 ⊆ (recs(𝐹)‘𝑦))) | 
| 148 | 147 | rexbiia 3092 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(∃𝑦 ∈
𝑥 𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)) | 
| 149 | 146, 148 | bitrdi 287 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))) | 
| 150 | 149 | ralbidv 3178 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦) ↔ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))) | 
| 151 | 143, 150 | anbi12d 632 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → ((𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦)) ↔ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)))) | 
| 152 | 29, 151 | spcev 3606 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)) → ∃𝑓(𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦))) | 
| 153 | 117, 142,
152 | syl2an2r 685 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ∃𝑓(𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦))) | 
| 154 |  | cfflb 10299 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (∃𝑓(𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦)) → (cf‘𝐴) ⊆ 𝑥)) | 
| 155 | 154 | imp 406 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧ ∃𝑓(𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦))) → (cf‘𝐴) ⊆ 𝑥) | 
| 156 | 105, 106,
153, 155 | syl21anc 838 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → (cf‘𝐴) ⊆ 𝑥) | 
| 157 |  | ontri1 6418 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((cf‘𝐴)
∈ On ∧ 𝑥 ∈
On) → ((cf‘𝐴)
⊆ 𝑥 ↔ ¬
𝑥 ∈ (cf‘𝐴))) | 
| 158 | 2, 3, 157 | sylancr 587 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 ∈ (cf‘𝐴) → ((cf‘𝐴) ⊆ 𝑥 ↔ ¬ 𝑥 ∈ (cf‘𝐴))) | 
| 159 | 158 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ((cf‘𝐴) ⊆ 𝑥 ↔ ¬ 𝑥 ∈ (cf‘𝐴))) | 
| 160 | 156, 159 | mpbid 232 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ¬ 𝑥 ∈ (cf‘𝐴)) | 
| 161 | 104, 160 | pm2.21dd 195 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴) | 
| 162 | 161 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)) | 
| 163 | 162 | expcomd 416 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (𝐴 ∈ On → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))) | 
| 164 | 163 | com12 32 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 ∈ On → ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))) | 
| 165 | 164 | 3impib 1117 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)) | 
| 166 | 103, 165 | jaod 860 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 ∨ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)) | 
| 167 | 102, 166 | sylbid 240 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)) | 
| 168 | 89, 167 | mpd 15 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴) | 
| 169 | 168 | 3adant1l 1177 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴) | 
| 170 |  | ordunel 7847 | . . . . . . . . . . . . . . . . 17
⊢ ((Ord
𝐴 ∧ (𝑔‘𝑥) ∈ 𝐴 ∧ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴) → ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) ∈ 𝐴) | 
| 171 | 71, 75, 169, 170 | syl3anc 1373 | . . . . . . . . . . . . . . . 16
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) ∈ 𝐴) | 
| 172 | 68, 171 | eqeltrd 2841 | . . . . . . . . . . . . . . 15
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (𝐺‘𝑥) ∈ 𝐴) | 
| 173 | 172 | 3expia 1122 | . . . . . . . . . . . . . 14
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 → (𝐺‘𝑥) ∈ 𝐴)) | 
| 174 | 173 | 3impa 1110 | . . . . . . . . . . . . 13
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 → (𝐺‘𝑥) ∈ 𝐴)) | 
| 175 | 18, 174 | syldc 48 | . . . . . . . . . . . 12
⊢
(∀𝑦 ∈
𝑥 ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ 𝐴) → ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) ∈ 𝐴)) | 
| 176 | 175 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ 𝐴) → ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) ∈ 𝐴))) | 
| 177 | 9, 176 | tfis2 7878 | . . . . . . . . . 10
⊢ (𝑥 ∈ On → ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) ∈ 𝐴)) | 
| 178 | 4, 177 | mpcom 38 | . . . . . . . . 9
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) ∈ 𝐴) | 
| 179 | 178 | 3expia 1122 | . . . . . . . 8
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → (𝑥 ∈ (cf‘𝐴) → (𝐺‘𝑥) ∈ 𝐴)) | 
| 180 | 179 | ralrimiv 3145 | . . . . . . 7
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → ∀𝑥 ∈ (cf‘𝐴)(𝐺‘𝑥) ∈ 𝐴) | 
| 181 | 2 | onssi 7858 | . . . . . . . . 9
⊢
(cf‘𝐴) ⊆
On | 
| 182 |  | fnssres 6691 | . . . . . . . . . 10
⊢
((recs(𝐹) Fn On
∧ (cf‘𝐴) ⊆
On) → (recs(𝐹) ↾
(cf‘𝐴)) Fn
(cf‘𝐴)) | 
| 183 | 19 | fneq1i 6665 | . . . . . . . . . 10
⊢ (𝐺 Fn (cf‘𝐴) ↔ (recs(𝐹) ↾ (cf‘𝐴)) Fn (cf‘𝐴)) | 
| 184 | 182, 183 | sylibr 234 | . . . . . . . . 9
⊢
((recs(𝐹) Fn On
∧ (cf‘𝐴) ⊆
On) → 𝐺 Fn
(cf‘𝐴)) | 
| 185 | 24, 181, 184 | mp2an 692 | . . . . . . . 8
⊢ 𝐺 Fn (cf‘𝐴) | 
| 186 |  | ffnfv 7139 | . . . . . . . 8
⊢ (𝐺:(cf‘𝐴)⟶𝐴 ↔ (𝐺 Fn (cf‘𝐴) ∧ ∀𝑥 ∈ (cf‘𝐴)(𝐺‘𝑥) ∈ 𝐴)) | 
| 187 | 185, 186 | mpbiran 709 | . . . . . . 7
⊢ (𝐺:(cf‘𝐴)⟶𝐴 ↔ ∀𝑥 ∈ (cf‘𝐴)(𝐺‘𝑥) ∈ 𝐴) | 
| 188 | 180, 187 | sylibr 234 | . . . . . 6
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → 𝐺:(cf‘𝐴)⟶𝐴) | 
| 189 | 188 | adantlr 715 | . . . . 5
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) ∧ 𝐴 ∈ On) → 𝐺:(cf‘𝐴)⟶𝐴) | 
| 190 |  | onss 7805 | . . . . . . . 8
⊢ (𝐴 ∈ On → 𝐴 ⊆ On) | 
| 191 | 190 | adantl 481 | . . . . . . 7
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → 𝐴 ⊆ On) | 
| 192 | 2 | onordi 6495 | . . . . . . . 8
⊢ Ord
(cf‘𝐴) | 
| 193 |  | fvex 6919 | . . . . . . . . . . . . . . . . 17
⊢
(recs(𝐹)‘𝑦) ∈ V | 
| 194 | 193 | sucid 6466 | . . . . . . . . . . . . . . . 16
⊢
(recs(𝐹)‘𝑦) ∈ suc (recs(𝐹)‘𝑦) | 
| 195 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝑦 → (recs(𝐹)‘𝑡) = (recs(𝐹)‘𝑦)) | 
| 196 |  | suceq 6450 | . . . . . . . . . . . . . . . . . . 19
⊢
((recs(𝐹)‘𝑡) = (recs(𝐹)‘𝑦) → suc (recs(𝐹)‘𝑡) = suc (recs(𝐹)‘𝑦)) | 
| 197 | 195, 196 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 𝑦 → suc (recs(𝐹)‘𝑡) = suc (recs(𝐹)‘𝑦)) | 
| 198 | 197 | eliuni 4997 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ 𝑥 ∧ (recs(𝐹)‘𝑦) ∈ suc (recs(𝐹)‘𝑦)) → (recs(𝐹)‘𝑦) ∈ ∪
𝑡 ∈ 𝑥 suc (recs(𝐹)‘𝑡)) | 
| 199 | 198, 60 | eleqtrrdi 2852 | . . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝑥 ∧ (recs(𝐹)‘𝑦) ∈ suc (recs(𝐹)‘𝑦)) → (recs(𝐹)‘𝑦) ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) | 
| 200 | 194, 199 | mpan2 691 | . . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝑥 → (recs(𝐹)‘𝑦) ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) | 
| 201 |  | elun2 4183 | . . . . . . . . . . . . . . 15
⊢
((recs(𝐹)‘𝑦) ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) → (recs(𝐹)‘𝑦) ∈ ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) | 
| 202 | 200, 201 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝑥 → (recs(𝐹)‘𝑦) ∈ ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) | 
| 203 | 202 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (recs(𝐹)‘𝑦) ∈ ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) | 
| 204 | 3 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → 𝑥 ∈ On) | 
| 205 | 204, 65 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (recs(𝐹)‘𝑥) = ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) | 
| 206 | 203, 205 | eleqtrrd 2844 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (recs(𝐹)‘𝑦) ∈ (recs(𝐹)‘𝑥)) | 
| 207 | 22 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) = (recs(𝐹)‘𝑥)) | 
| 208 | 206, 78, 207 | 3eltr4d 2856 | . . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ (𝐺‘𝑥)) | 
| 209 | 208 | expcom 413 | . . . . . . . . . 10
⊢ (𝑥 ∈ (cf‘𝐴) → (𝑦 ∈ 𝑥 → (𝐺‘𝑦) ∈ (𝐺‘𝑥))) | 
| 210 | 209 | ralrimiv 3145 | . . . . . . . . 9
⊢ (𝑥 ∈ (cf‘𝐴) → ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ (𝐺‘𝑥)) | 
| 211 | 210 | rgen 3063 | . . . . . . . 8
⊢
∀𝑥 ∈
(cf‘𝐴)∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ (𝐺‘𝑥) | 
| 212 |  | issmo2 8389 | . . . . . . . . 9
⊢ (𝐺:(cf‘𝐴)⟶𝐴 → ((𝐴 ⊆ On ∧ Ord (cf‘𝐴) ∧ ∀𝑥 ∈ (cf‘𝐴)∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ (𝐺‘𝑥)) → Smo 𝐺)) | 
| 213 | 212 | com12 32 | . . . . . . . 8
⊢ ((𝐴 ⊆ On ∧ Ord
(cf‘𝐴) ∧
∀𝑥 ∈
(cf‘𝐴)∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ (𝐺‘𝑥)) → (𝐺:(cf‘𝐴)⟶𝐴 → Smo 𝐺)) | 
| 214 | 192, 211,
213 | mp3an23 1455 | . . . . . . 7
⊢ (𝐴 ⊆ On → (𝐺:(cf‘𝐴)⟶𝐴 → Smo 𝐺)) | 
| 215 | 191, 188,
214 | sylc 65 | . . . . . 6
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → Smo 𝐺) | 
| 216 | 215 | adantlr 715 | . . . . 5
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) ∧ 𝐴 ∈ On) → Smo 𝐺) | 
| 217 |  | fveq2 6906 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑤 → (𝑔‘𝑥) = (𝑔‘𝑤)) | 
| 218 |  | fveq2 6906 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑤 → (𝐺‘𝑥) = (𝐺‘𝑤)) | 
| 219 | 217, 218 | sseq12d 4017 | . . . . . . . . . 10
⊢ (𝑥 = 𝑤 → ((𝑔‘𝑥) ⊆ (𝐺‘𝑥) ↔ (𝑔‘𝑤) ⊆ (𝐺‘𝑤))) | 
| 220 |  | ssun1 4178 | . . . . . . . . . . 11
⊢ (𝑔‘𝑥) ⊆ ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) | 
| 221 | 220, 67 | sseqtrrid 4027 | . . . . . . . . . 10
⊢ (𝑥 ∈ (cf‘𝐴) → (𝑔‘𝑥) ⊆ (𝐺‘𝑥)) | 
| 222 | 219, 221 | vtoclga 3577 | . . . . . . . . 9
⊢ (𝑤 ∈ (cf‘𝐴) → (𝑔‘𝑤) ⊆ (𝐺‘𝑤)) | 
| 223 |  | sstr 3992 | . . . . . . . . . 10
⊢ ((𝑧 ⊆ (𝑔‘𝑤) ∧ (𝑔‘𝑤) ⊆ (𝐺‘𝑤)) → 𝑧 ⊆ (𝐺‘𝑤)) | 
| 224 | 223 | expcom 413 | . . . . . . . . 9
⊢ ((𝑔‘𝑤) ⊆ (𝐺‘𝑤) → (𝑧 ⊆ (𝑔‘𝑤) → 𝑧 ⊆ (𝐺‘𝑤))) | 
| 225 | 222, 224 | syl 17 | . . . . . . . 8
⊢ (𝑤 ∈ (cf‘𝐴) → (𝑧 ⊆ (𝑔‘𝑤) → 𝑧 ⊆ (𝐺‘𝑤))) | 
| 226 | 225 | reximia 3081 | . . . . . . 7
⊢
(∃𝑤 ∈
(cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤) → ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤)) | 
| 227 | 226 | ralimi 3083 | . . . . . 6
⊢
(∀𝑧 ∈
𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤) → ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤)) | 
| 228 | 227 | ad2antlr 727 | . . . . 5
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) ∧ 𝐴 ∈ On) → ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤)) | 
| 229 |  | fnex 7237 | . . . . . . 7
⊢ ((𝐺 Fn (cf‘𝐴) ∧ (cf‘𝐴) ∈ On) → 𝐺 ∈ V) | 
| 230 | 185, 2, 229 | mp2an 692 | . . . . . 6
⊢ 𝐺 ∈ V | 
| 231 |  | feq1 6716 | . . . . . . 7
⊢ (𝑓 = 𝐺 → (𝑓:(cf‘𝐴)⟶𝐴 ↔ 𝐺:(cf‘𝐴)⟶𝐴)) | 
| 232 |  | smoeq 8390 | . . . . . . 7
⊢ (𝑓 = 𝐺 → (Smo 𝑓 ↔ Smo 𝐺)) | 
| 233 |  | fveq1 6905 | . . . . . . . . . 10
⊢ (𝑓 = 𝐺 → (𝑓‘𝑤) = (𝐺‘𝑤)) | 
| 234 | 233 | sseq2d 4016 | . . . . . . . . 9
⊢ (𝑓 = 𝐺 → (𝑧 ⊆ (𝑓‘𝑤) ↔ 𝑧 ⊆ (𝐺‘𝑤))) | 
| 235 | 234 | rexbidv 3179 | . . . . . . . 8
⊢ (𝑓 = 𝐺 → (∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤) ↔ ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤))) | 
| 236 | 235 | ralbidv 3178 | . . . . . . 7
⊢ (𝑓 = 𝐺 → (∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤) ↔ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤))) | 
| 237 | 231, 232,
236 | 3anbi123d 1438 | . . . . . 6
⊢ (𝑓 = 𝐺 → ((𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤)) ↔ (𝐺:(cf‘𝐴)⟶𝐴 ∧ Smo 𝐺 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤)))) | 
| 238 | 230, 237 | spcev 3606 | . . . . 5
⊢ ((𝐺:(cf‘𝐴)⟶𝐴 ∧ Smo 𝐺 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤)) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤))) | 
| 239 | 189, 216,
228, 238 | syl3anc 1373 | . . . 4
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) ∧ 𝐴 ∈ On) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤))) | 
| 240 | 239 | expcom 413 | . . 3
⊢ (𝐴 ∈ On → ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤)))) | 
| 241 | 240 | exlimdv 1933 | . 2
⊢ (𝐴 ∈ On → (∃𝑔(𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤)))) | 
| 242 | 1, 241 | mpd 15 | 1
⊢ (𝐴 ∈ On → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤))) |