Step | Hyp | Ref
| Expression |
1 | | cff1 9902 |
. 2
⊢ (𝐴 ∈ On → ∃𝑔(𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤))) |
2 | | cfon 9899 |
. . . . . . . . . . . 12
⊢
(cf‘𝐴) ∈
On |
3 | 2 | oneli 6342 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (cf‘𝐴) → 𝑥 ∈ On) |
4 | 3 | 3ad2ant3 1137 |
. . . . . . . . . 10
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → 𝑥 ∈ On) |
5 | | eleq1w 2822 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝑥 ∈ (cf‘𝐴) ↔ 𝑦 ∈ (cf‘𝐴))) |
6 | 5 | 3anbi3d 1444 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ↔ (𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)))) |
7 | | fveq2 6739 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝐺‘𝑥) = (𝐺‘𝑦)) |
8 | 7 | eleq1d 2824 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((𝐺‘𝑥) ∈ 𝐴 ↔ (𝐺‘𝑦) ∈ 𝐴)) |
9 | 6, 8 | imbi12d 348 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) ∈ 𝐴) ↔ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ 𝐴))) |
10 | | simpl1 1193 |
. . . . . . . . . . . . . . 15
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → 𝑔:(cf‘𝐴)–1-1→𝐴) |
11 | | simpl2 1194 |
. . . . . . . . . . . . . . 15
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → 𝐴 ∈ On) |
12 | | ontr1 6280 |
. . . . . . . . . . . . . . . . . 18
⊢
((cf‘𝐴) ∈
On → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → 𝑦 ∈ (cf‘𝐴))) |
13 | 2, 12 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → 𝑦 ∈ (cf‘𝐴)) |
14 | 13 | ancoms 462 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ (cf‘𝐴)) |
15 | 14 | 3ad2antl3 1189 |
. . . . . . . . . . . . . . 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 3103 |
. . . . . . . . . . . . 13
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ 𝐴) → ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴)) |
19 | | cfsmolem.3 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐺 = (recs(𝐹) ↾ (cf‘𝐴)) |
20 | 19 | fveq1i 6740 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐺‘𝑥) = ((recs(𝐹) ↾ (cf‘𝐴))‘𝑥) |
21 | | fvres 6758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (cf‘𝐴) → ((recs(𝐹) ↾ (cf‘𝐴))‘𝑥) = (recs(𝐹)‘𝑥)) |
22 | 20, 21 | eqtrid 2791 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (cf‘𝐴) → (𝐺‘𝑥) = (recs(𝐹)‘𝑥)) |
23 | | recsval 8164 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ On → (recs(𝐹)‘𝑥) = (𝐹‘(recs(𝐹) ↾ 𝑥))) |
24 | | recsfnon 8163 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
recs(𝐹) Fn
On |
25 | | fnfun 6500 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(recs(𝐹) Fn On
→ Fun recs(𝐹)) |
26 | 24, 25 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ Fun
recs(𝐹) |
27 | | vex 3427 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑥 ∈ V |
28 | | resfunexg 7053 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((Fun
recs(𝐹) ∧ 𝑥 ∈ V) → (recs(𝐹) ↾ 𝑥) ∈ V) |
29 | 26, 27, 28 | mp2an 692 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(recs(𝐹) ↾
𝑥) ∈
V |
30 | | dmeq 5790 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → dom 𝑧 = dom (recs(𝐹) ↾ 𝑥)) |
31 | 30 | fveq2d 6743 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → (𝑔‘dom 𝑧) = (𝑔‘dom (recs(𝐹) ↾ 𝑥))) |
32 | | fveq1 6738 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → (𝑧‘𝑡) = ((recs(𝐹) ↾ 𝑥)‘𝑡)) |
33 | | suceq 6299 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑧‘𝑡) = ((recs(𝐹) ↾ 𝑥)‘𝑡) → suc (𝑧‘𝑡) = suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → suc (𝑧‘𝑡) = suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) |
35 | 30, 34 | iuneq12d 4949 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → ∪
𝑡 ∈ dom 𝑧 suc (𝑧‘𝑡) = ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) |
36 | 31, 35 | uneq12d 4095 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → ((𝑔‘dom 𝑧) ∪ ∪
𝑡 ∈ dom 𝑧 suc (𝑧‘𝑡)) = ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ ∪
𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡))) |
37 | | cfsmolem.2 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝐹 = (𝑧 ∈ V ↦ ((𝑔‘dom 𝑧) ∪ ∪
𝑡 ∈ dom 𝑧 suc (𝑧‘𝑡))) |
38 | | fvex 6752 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∈ V |
39 | 29 | dmex 7711 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ dom
(recs(𝐹) ↾ 𝑥) ∈ V |
40 | | fvex 6752 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((recs(𝐹) ↾
𝑥)‘𝑡) ∈ V |
41 | 40 | sucex 7612 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ suc
((recs(𝐹) ↾ 𝑥)‘𝑡) ∈ V |
42 | 39, 41 | iunex 7763 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡) ∈ V |
43 | 38, 42 | unex 7553 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ ∪
𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) ∈ V |
44 | 36, 37, 43 | fvmpt 6840 |
. . . . . . . . . . . . . . . . . . . . . 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 2796 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ On → (recs(𝐹)‘𝑥) = ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ ∪
𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡))) |
47 | | onss 7590 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ On → 𝑥 ⊆ On) |
48 | | fnssres 6522 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((recs(𝐹) Fn On
∧ 𝑥 ⊆ On) →
(recs(𝐹) ↾ 𝑥) Fn 𝑥) |
49 | 24, 47, 48 | sylancr 590 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ On → (recs(𝐹) ↾ 𝑥) Fn 𝑥) |
50 | | fndm 6503 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((recs(𝐹) ↾
𝑥) Fn 𝑥 → dom (recs(𝐹) ↾ 𝑥) = 𝑥) |
51 | | fveq2 6739 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (dom
(recs(𝐹) ↾ 𝑥) = 𝑥 → (𝑔‘dom (recs(𝐹) ↾ 𝑥)) = (𝑔‘𝑥)) |
52 | | iuneq1 4937 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (dom
(recs(𝐹) ↾ 𝑥) = 𝑥 → ∪
𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = ∪ 𝑡 ∈ 𝑥 suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) |
53 | | fvres 6758 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 ∈ 𝑥 → ((recs(𝐹) ↾ 𝑥)‘𝑡) = (recs(𝐹)‘𝑡)) |
54 | | suceq 6299 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((recs(𝐹) ↾
𝑥)‘𝑡) = (recs(𝐹)‘𝑡) → suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = suc (recs(𝐹)‘𝑡)) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 ∈ 𝑥 → suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = suc (recs(𝐹)‘𝑡)) |
56 | 55 | iuneq2i 4942 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ∪ 𝑡 ∈ 𝑥 suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = ∪ 𝑡 ∈ 𝑥 suc (recs(𝐹)‘𝑡) |
57 | | fveq2 6739 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = 𝑡 → (recs(𝐹)‘𝑦) = (recs(𝐹)‘𝑡)) |
58 | | suceq 6299 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((recs(𝐹)‘𝑦) = (recs(𝐹)‘𝑡) → suc (recs(𝐹)‘𝑦) = suc (recs(𝐹)‘𝑡)) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = 𝑡 → suc (recs(𝐹)‘𝑦) = suc (recs(𝐹)‘𝑡)) |
60 | 59 | cbviunv 4966 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = ∪ 𝑡 ∈ 𝑥 suc (recs(𝐹)‘𝑡) |
61 | 56, 60 | eqtr4i 2770 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ∪ 𝑡 ∈ 𝑥 suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) |
62 | 52, 61 | eqtrdi 2796 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (dom
(recs(𝐹) ↾ 𝑥) = 𝑥 → ∪
𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) |
63 | 51, 62 | uneq12d 4095 |
. . . . . . . . . . . . . . . . . . . . 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 2779 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ On → (recs(𝐹)‘𝑥) = ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) |
66 | 3, 65 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (cf‘𝐴) → (recs(𝐹)‘𝑥) = ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) |
67 | 22, 66 | eqtrd 2779 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (cf‘𝐴) → (𝐺‘𝑥) = ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) |
68 | 67 | 3ad2ant2 1136 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (𝐺‘𝑥) = ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) |
69 | | eloni 6244 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ On → Ord 𝐴) |
70 | 69 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → Ord 𝐴) |
71 | 70 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → Ord 𝐴) |
72 | | f1f 6637 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔:(cf‘𝐴)–1-1→𝐴 → 𝑔:(cf‘𝐴)⟶𝐴) |
73 | 72 | ffvelrnda 6926 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝑥 ∈ (cf‘𝐴)) → (𝑔‘𝑥) ∈ 𝐴) |
74 | 73 | adantlr 715 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴)) → (𝑔‘𝑥) ∈ 𝐴) |
75 | 74 | 3adant3 1134 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (𝑔‘𝑥) ∈ 𝐴) |
76 | 19 | fveq1i 6740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐺‘𝑦) = ((recs(𝐹) ↾ (cf‘𝐴))‘𝑦) |
77 | 13 | fvresd 6759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → ((recs(𝐹) ↾ (cf‘𝐴))‘𝑦) = (recs(𝐹)‘𝑦)) |
78 | 76, 77 | eqtrid 2791 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑦) = (recs(𝐹)‘𝑦)) |
79 | 78 | adantrl 716 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ 𝑥 ∧ (𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴))) → (𝐺‘𝑦) = (recs(𝐹)‘𝑦)) |
80 | 79 | ancoms 462 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → (𝐺‘𝑦) = (recs(𝐹)‘𝑦)) |
81 | 80 | eleq1d 2824 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 ↔ (recs(𝐹)‘𝑦) ∈ 𝐴)) |
82 | | ordsucss 7619 |
. . . . . . . . . . . . . . . . . . . . . . . . 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 243 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴)) |
86 | 85 | ralimdva 3103 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 → ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴)) |
87 | | iunss 4971 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 ↔ ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴) |
88 | 86, 87 | syl6ibr 255 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴)) |
89 | 88 | 3impia 1119 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴) |
90 | | onelon 6259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈ On ∧ (recs(𝐹)‘𝑦) ∈ 𝐴) → (recs(𝐹)‘𝑦) ∈ On) |
91 | 90 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐴 ∈ On → ((recs(𝐹)‘𝑦) ∈ 𝐴 → (recs(𝐹)‘𝑦) ∈ On)) |
92 | 91 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹)‘𝑦) ∈ 𝐴 → (recs(𝐹)‘𝑦) ∈ On)) |
93 | 81, 92 | sylbid 243 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 → (recs(𝐹)‘𝑦) ∈ On)) |
94 | | suceloni 7614 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((recs(𝐹)‘𝑦) ∈ On → suc (recs(𝐹)‘𝑦) ∈ On) |
95 | 93, 94 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ∈ On)) |
96 | 95 | ralimdva 3103 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 → ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On)) |
97 | 96 | 3impia 1119 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On) |
98 | | iunon 8100 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ V ∧ ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On) |
99 | 27, 97, 98 | sylancr 590 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On) |
100 | | simp1 1138 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → 𝐴 ∈ On) |
101 | | onsseleq 6275 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On ∧ 𝐴 ∈ On) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 ↔ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 ∨ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴))) |
102 | 99, 100, 101 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . 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 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (recs(𝐹) ↾ 𝑥) Fn 𝑥) |
109 | 78 | ancoms 462 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → (𝐺‘𝑦) = (recs(𝐹)‘𝑦)) |
110 | | fvres 6758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑦 ∈ 𝑥 → ((recs(𝐹) ↾ 𝑥)‘𝑦) = (recs(𝐹)‘𝑦)) |
111 | 110 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹) ↾ 𝑥)‘𝑦) = (recs(𝐹)‘𝑦)) |
112 | 109, 111 | eqtr4d 2782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → (𝐺‘𝑦) = ((recs(𝐹) ↾ 𝑥)‘𝑦)) |
113 | 112 | eleq1d 2824 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 ↔ ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴)) |
114 | 113 | ralbidva 3120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥 ∈ (cf‘𝐴) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 ↔ ∀𝑦 ∈ 𝑥 ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴)) |
115 | 114 | biimpa 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∀𝑦 ∈ 𝑥 ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴) |
116 | | ffnfv 6957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ↔ ((recs(𝐹) ↾ 𝑥) Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴)) |
117 | 108, 115,
116 | sylanbrc 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴) |
118 | | eleq2 2828 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 → (𝑡 ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ 𝐴)) |
119 | 118 | biimpar 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝑡 ∈ 𝐴) → 𝑡 ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) |
120 | 119 | adantrl 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → 𝑡 ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) |
121 | 120 | 3adant1 1132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → 𝑡 ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) |
122 | | onelon 6259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) → 𝑡 ∈ On) |
123 | 110 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢
(((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹) ↾ 𝑥)‘𝑦) = (recs(𝐹)‘𝑦)) |
124 | | ffvelrn 6924 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢
(((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴) |
125 | 123, 124 | eqeltrrd 2841 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢
(((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥) → (recs(𝐹)‘𝑦) ∈ 𝐴) |
126 | 125, 90 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝐴 ∈ On ∧ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥)) → (recs(𝐹)‘𝑦) ∈ On) |
127 | 126 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥)) → (recs(𝐹)‘𝑦) ∈ On) |
128 | | onsssuc 6321 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑡 ∈ On ∧ (recs(𝐹)‘𝑦) ∈ On) → (𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ suc (recs(𝐹)‘𝑦))) |
129 | 122, 127,
128 | syl2an2r 685 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥)) → (𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ suc (recs(𝐹)‘𝑦))) |
130 | 129 | anassrs 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴) ∧ 𝑦 ∈ 𝑥) → (𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ suc (recs(𝐹)‘𝑦))) |
131 | 130 | rexbidva 3225 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ∈ suc (recs(𝐹)‘𝑦))) |
132 | | eliun 4925 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑡 ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ∈ suc (recs(𝐹)‘𝑦)) |
133 | 131, 132 | bitr4di 292 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) |
134 | 133 | ancoms 462 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) |
135 | 134 | 3adant2 1133 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) |
136 | 121, 135 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)) |
137 | 136 | 3expa 1120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)) |
138 | 137 | anassrs 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) ∧ 𝐴 ∈ On) ∧ 𝑡 ∈ 𝐴) → ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)) |
139 | 138 | ralrimiva 3108 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) ∧ 𝐴 ∈ On) → ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)) |
140 | 139 | expl 461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 → ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On) → ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))) |
141 | 117, 140 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On) → ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))) |
142 | 141 | imp 410 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)) |
143 | | feq1 6548 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (𝑓:𝑥⟶𝐴 ↔ (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴)) |
144 | | fveq1 6738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (𝑓‘𝑦) = ((recs(𝐹) ↾ 𝑥)‘𝑦)) |
145 | 144 | sseq2d 3950 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (𝑡 ⊆ (𝑓‘𝑦) ↔ 𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦))) |
146 | 145 | rexbidv 3226 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦))) |
147 | 110 | sseq2d 3950 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑦 ∈ 𝑥 → (𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦) ↔ 𝑡 ⊆ (recs(𝐹)‘𝑦))) |
148 | 147 | rexbiia 3177 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(∃𝑦 ∈
𝑥 𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)) |
149 | 146, 148 | bitrdi 290 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))) |
150 | 149 | ralbidv 3121 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦) ↔ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))) |
151 | 143, 150 | anbi12d 634 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → ((𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦)) ↔ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)))) |
152 | 29, 151 | spcev 3536 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)) → ∃𝑓(𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦))) |
153 | 117, 142,
152 | syl2an2r 685 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ∃𝑓(𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦))) |
154 | | cfflb 9903 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (∃𝑓(𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦)) → (cf‘𝐴) ⊆ 𝑥)) |
155 | 154 | imp 410 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧ ∃𝑓(𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦))) → (cf‘𝐴) ⊆ 𝑥) |
156 | 105, 106,
153, 155 | syl21anc 838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → (cf‘𝐴) ⊆ 𝑥) |
157 | | ontri1 6268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((cf‘𝐴)
∈ On ∧ 𝑥 ∈
On) → ((cf‘𝐴)
⊆ 𝑥 ↔ ¬
𝑥 ∈ (cf‘𝐴))) |
158 | 2, 3, 157 | sylancr 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 ∈ (cf‘𝐴) → ((cf‘𝐴) ⊆ 𝑥 ↔ ¬ 𝑥 ∈ (cf‘𝐴))) |
159 | 158 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ((cf‘𝐴) ⊆ 𝑥 ↔ ¬ 𝑥 ∈ (cf‘𝐴))) |
160 | 156, 159 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ¬ 𝑥 ∈ (cf‘𝐴)) |
161 | 104, 160 | pm2.21dd 198 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴) |
162 | 161 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)) |
163 | 162 | expcomd 420 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (𝐴 ∈ On → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))) |
164 | 163 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 ∈ On → ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))) |
165 | 164 | 3impib 1118 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)) |
166 | 103, 165 | jaod 859 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 ∨ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)) |
167 | 102, 166 | sylbid 243 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)) |
168 | 89, 167 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴) |
169 | 168 | 3adant1l 1178 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴) |
170 | | ordunel 7628 |
. . . . . . . . . . . . . . . . 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 2840 |
. . . . . . . . . . . . . . 15
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (𝐺‘𝑥) ∈ 𝐴) |
173 | 172 | 3expia 1123 |
. . . . . . . . . . . . . 14
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 → (𝐺‘𝑥) ∈ 𝐴)) |
174 | 173 | 3impa 1112 |
. . . . . . . . . . . . 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 7657 |
. . . . . . . . . 10
⊢ (𝑥 ∈ On → ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) ∈ 𝐴)) |
178 | 4, 177 | mpcom 38 |
. . . . . . . . 9
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) ∈ 𝐴) |
179 | 178 | 3expia 1123 |
. . . . . . . 8
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → (𝑥 ∈ (cf‘𝐴) → (𝐺‘𝑥) ∈ 𝐴)) |
180 | 179 | ralrimiv 3107 |
. . . . . . 7
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → ∀𝑥 ∈ (cf‘𝐴)(𝐺‘𝑥) ∈ 𝐴) |
181 | 2 | onssi 7638 |
. . . . . . . . 9
⊢
(cf‘𝐴) ⊆
On |
182 | | fnssres 6522 |
. . . . . . . . . 10
⊢
((recs(𝐹) Fn On
∧ (cf‘𝐴) ⊆
On) → (recs(𝐹) ↾
(cf‘𝐴)) Fn
(cf‘𝐴)) |
183 | 19 | fneq1i 6497 |
. . . . . . . . . 10
⊢ (𝐺 Fn (cf‘𝐴) ↔ (recs(𝐹) ↾ (cf‘𝐴)) Fn (cf‘𝐴)) |
184 | 182, 183 | sylibr 237 |
. . . . . . . . 9
⊢
((recs(𝐹) Fn On
∧ (cf‘𝐴) ⊆
On) → 𝐺 Fn
(cf‘𝐴)) |
185 | 24, 181, 184 | mp2an 692 |
. . . . . . . 8
⊢ 𝐺 Fn (cf‘𝐴) |
186 | | ffnfv 6957 |
. . . . . . . 8
⊢ (𝐺:(cf‘𝐴)⟶𝐴 ↔ (𝐺 Fn (cf‘𝐴) ∧ ∀𝑥 ∈ (cf‘𝐴)(𝐺‘𝑥) ∈ 𝐴)) |
187 | 185, 186 | mpbiran 709 |
. . . . . . 7
⊢ (𝐺:(cf‘𝐴)⟶𝐴 ↔ ∀𝑥 ∈ (cf‘𝐴)(𝐺‘𝑥) ∈ 𝐴) |
188 | 180, 187 | sylibr 237 |
. . . . . 6
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → 𝐺:(cf‘𝐴)⟶𝐴) |
189 | 188 | adantlr 715 |
. . . . 5
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) ∧ 𝐴 ∈ On) → 𝐺:(cf‘𝐴)⟶𝐴) |
190 | | onss 7590 |
. . . . . . . 8
⊢ (𝐴 ∈ On → 𝐴 ⊆ On) |
191 | 190 | adantl 485 |
. . . . . . 7
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → 𝐴 ⊆ On) |
192 | 2 | onordi 6339 |
. . . . . . . 8
⊢ Ord
(cf‘𝐴) |
193 | | fvex 6752 |
. . . . . . . . . . . . . . . . 17
⊢
(recs(𝐹)‘𝑦) ∈ V |
194 | 193 | sucid 6313 |
. . . . . . . . . . . . . . . 16
⊢
(recs(𝐹)‘𝑦) ∈ suc (recs(𝐹)‘𝑦) |
195 | | fveq2 6739 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝑦 → (recs(𝐹)‘𝑡) = (recs(𝐹)‘𝑦)) |
196 | | suceq 6299 |
. . . . . . . . . . . . . . . . . . 19
⊢
((recs(𝐹)‘𝑡) = (recs(𝐹)‘𝑦) → suc (recs(𝐹)‘𝑡) = suc (recs(𝐹)‘𝑦)) |
197 | 195, 196 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 𝑦 → suc (recs(𝐹)‘𝑡) = suc (recs(𝐹)‘𝑦)) |
198 | 197 | eliuni 4927 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ 𝑥 ∧ (recs(𝐹)‘𝑦) ∈ suc (recs(𝐹)‘𝑦)) → (recs(𝐹)‘𝑦) ∈ ∪
𝑡 ∈ 𝑥 suc (recs(𝐹)‘𝑡)) |
199 | 198, 60 | eleqtrrdi 2851 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝑥 ∧ (recs(𝐹)‘𝑦) ∈ suc (recs(𝐹)‘𝑦)) → (recs(𝐹)‘𝑦) ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) |
200 | 194, 199 | mpan2 691 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝑥 → (recs(𝐹)‘𝑦) ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) |
201 | | elun2 4108 |
. . . . . . . . . . . . . . 15
⊢
((recs(𝐹)‘𝑦) ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) → (recs(𝐹)‘𝑦) ∈ ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) |
202 | 200, 201 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝑥 → (recs(𝐹)‘𝑦) ∈ ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) |
203 | 202 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (recs(𝐹)‘𝑦) ∈ ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) |
204 | 3 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → 𝑥 ∈ On) |
205 | 204, 65 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (recs(𝐹)‘𝑥) = ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) |
206 | 203, 205 | eleqtrrd 2843 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (recs(𝐹)‘𝑦) ∈ (recs(𝐹)‘𝑥)) |
207 | 22 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) = (recs(𝐹)‘𝑥)) |
208 | 206, 78, 207 | 3eltr4d 2855 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ (𝐺‘𝑥)) |
209 | 208 | expcom 417 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (cf‘𝐴) → (𝑦 ∈ 𝑥 → (𝐺‘𝑦) ∈ (𝐺‘𝑥))) |
210 | 209 | ralrimiv 3107 |
. . . . . . . . 9
⊢ (𝑥 ∈ (cf‘𝐴) → ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ (𝐺‘𝑥)) |
211 | 210 | rgen 3074 |
. . . . . . . 8
⊢
∀𝑥 ∈
(cf‘𝐴)∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ (𝐺‘𝑥) |
212 | | issmo2 8110 |
. . . . . . . . 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 6739 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑤 → (𝑔‘𝑥) = (𝑔‘𝑤)) |
218 | | fveq2 6739 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑤 → (𝐺‘𝑥) = (𝐺‘𝑤)) |
219 | 217, 218 | sseq12d 3951 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑤 → ((𝑔‘𝑥) ⊆ (𝐺‘𝑥) ↔ (𝑔‘𝑤) ⊆ (𝐺‘𝑤))) |
220 | | ssun1 4103 |
. . . . . . . . . . 11
⊢ (𝑔‘𝑥) ⊆ ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) |
221 | 220, 67 | sseqtrrid 3971 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (cf‘𝐴) → (𝑔‘𝑥) ⊆ (𝐺‘𝑥)) |
222 | 219, 221 | vtoclga 3504 |
. . . . . . . . 9
⊢ (𝑤 ∈ (cf‘𝐴) → (𝑔‘𝑤) ⊆ (𝐺‘𝑤)) |
223 | | sstr 3926 |
. . . . . . . . . 10
⊢ ((𝑧 ⊆ (𝑔‘𝑤) ∧ (𝑔‘𝑤) ⊆ (𝐺‘𝑤)) → 𝑧 ⊆ (𝐺‘𝑤)) |
224 | 223 | expcom 417 |
. . . . . . . . 9
⊢ ((𝑔‘𝑤) ⊆ (𝐺‘𝑤) → (𝑧 ⊆ (𝑔‘𝑤) → 𝑧 ⊆ (𝐺‘𝑤))) |
225 | 222, 224 | syl 17 |
. . . . . . . 8
⊢ (𝑤 ∈ (cf‘𝐴) → (𝑧 ⊆ (𝑔‘𝑤) → 𝑧 ⊆ (𝐺‘𝑤))) |
226 | 225 | reximia 3173 |
. . . . . . 7
⊢
(∃𝑤 ∈
(cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤) → ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤)) |
227 | 226 | ralimi 3087 |
. . . . . 6
⊢
(∀𝑧 ∈
𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤) → ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤)) |
228 | 227 | ad2antlr 727 |
. . . . 5
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) ∧ 𝐴 ∈ On) → ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤)) |
229 | | fnex 7055 |
. . . . . . 7
⊢ ((𝐺 Fn (cf‘𝐴) ∧ (cf‘𝐴) ∈ On) → 𝐺 ∈ V) |
230 | 185, 2, 229 | mp2an 692 |
. . . . . 6
⊢ 𝐺 ∈ V |
231 | | feq1 6548 |
. . . . . . 7
⊢ (𝑓 = 𝐺 → (𝑓:(cf‘𝐴)⟶𝐴 ↔ 𝐺:(cf‘𝐴)⟶𝐴)) |
232 | | smoeq 8111 |
. . . . . . 7
⊢ (𝑓 = 𝐺 → (Smo 𝑓 ↔ Smo 𝐺)) |
233 | | fveq1 6738 |
. . . . . . . . . 10
⊢ (𝑓 = 𝐺 → (𝑓‘𝑤) = (𝐺‘𝑤)) |
234 | 233 | sseq2d 3950 |
. . . . . . . . 9
⊢ (𝑓 = 𝐺 → (𝑧 ⊆ (𝑓‘𝑤) ↔ 𝑧 ⊆ (𝐺‘𝑤))) |
235 | 234 | rexbidv 3226 |
. . . . . . . 8
⊢ (𝑓 = 𝐺 → (∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤) ↔ ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤))) |
236 | 235 | ralbidv 3121 |
. . . . . . 7
⊢ (𝑓 = 𝐺 → (∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤) ↔ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤))) |
237 | 231, 232,
236 | 3anbi123d 1438 |
. . . . . 6
⊢ (𝑓 = 𝐺 → ((𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤)) ↔ (𝐺:(cf‘𝐴)⟶𝐴 ∧ Smo 𝐺 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤)))) |
238 | 230, 237 | spcev 3536 |
. . . . 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 417 |
. . 3
⊢ (𝐴 ∈ On → ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤)))) |
241 | 240 | exlimdv 1941 |
. 2
⊢ (𝐴 ∈ On → (∃𝑔(𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤)))) |
242 | 1, 241 | mpd 15 |
1
⊢ (𝐴 ∈ On → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤))) |