Step | Hyp | Ref
| Expression |
1 | | cff1 9394 |
. 2
⊢ (𝐴 ∈ On → ∃𝑔(𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤))) |
2 | | cfon 9391 |
. . . . . . . . . . . 12
⊢
(cf‘𝐴) ∈
On |
3 | 2 | oneli 6069 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (cf‘𝐴) → 𝑥 ∈ On) |
4 | 3 | 3ad2ant3 1171 |
. . . . . . . . . 10
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → 𝑥 ∈ On) |
5 | | eleq1w 2888 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝑥 ∈ (cf‘𝐴) ↔ 𝑦 ∈ (cf‘𝐴))) |
6 | 5 | 3anbi3d 1572 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ↔ (𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)))) |
7 | | fveq2 6432 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝐺‘𝑥) = (𝐺‘𝑦)) |
8 | 7 | eleq1d 2890 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((𝐺‘𝑥) ∈ 𝐴 ↔ (𝐺‘𝑦) ∈ 𝐴)) |
9 | 6, 8 | imbi12d 336 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) ∈ 𝐴) ↔ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ 𝐴))) |
10 | | simpl1 1248 |
. . . . . . . . . . . . . . 15
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → 𝑔:(cf‘𝐴)–1-1→𝐴) |
11 | | simpl2 1250 |
. . . . . . . . . . . . . . 15
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → 𝐴 ∈ On) |
12 | | ontr1 6008 |
. . . . . . . . . . . . . . . . . 18
⊢
((cf‘𝐴) ∈
On → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → 𝑦 ∈ (cf‘𝐴))) |
13 | 2, 12 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → 𝑦 ∈ (cf‘𝐴)) |
14 | 13 | ancoms 452 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ (cf‘𝐴)) |
15 | 14 | 3ad2antl3 1244 |
. . . . . . . . . . . . . . 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 1496 |
. . . . . . . . . . . . . 14
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ 𝐴) → (𝐺‘𝑦) ∈ 𝐴)) |
18 | 17 | ralimdva 3170 |
. . . . . . . . . . . . 13
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ 𝐴) → ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴)) |
19 | | cfsmolem.3 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐺 = (recs(𝐹) ↾ (cf‘𝐴)) |
20 | 19 | fveq1i 6433 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐺‘𝑥) = ((recs(𝐹) ↾ (cf‘𝐴))‘𝑥) |
21 | | fvres 6451 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (cf‘𝐴) → ((recs(𝐹) ↾ (cf‘𝐴))‘𝑥) = (recs(𝐹)‘𝑥)) |
22 | 20, 21 | syl5eq 2872 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (cf‘𝐴) → (𝐺‘𝑥) = (recs(𝐹)‘𝑥)) |
23 | | recsval 7765 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ On → (recs(𝐹)‘𝑥) = (𝐹‘(recs(𝐹) ↾ 𝑥))) |
24 | | recsfnon 7764 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
recs(𝐹) Fn
On |
25 | | fnfun 6220 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(recs(𝐹) Fn On
→ Fun recs(𝐹)) |
26 | 24, 25 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ Fun
recs(𝐹) |
27 | | vex 3416 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑥 ∈ V |
28 | | resfunexg 6734 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((Fun
recs(𝐹) ∧ 𝑥 ∈ V) → (recs(𝐹) ↾ 𝑥) ∈ V) |
29 | 26, 27, 28 | mp2an 685 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(recs(𝐹) ↾
𝑥) ∈
V |
30 | | dmeq 5555 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → dom 𝑧 = dom (recs(𝐹) ↾ 𝑥)) |
31 | 30 | fveq2d 6436 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → (𝑔‘dom 𝑧) = (𝑔‘dom (recs(𝐹) ↾ 𝑥))) |
32 | | fveq1 6431 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → (𝑧‘𝑡) = ((recs(𝐹) ↾ 𝑥)‘𝑡)) |
33 | | suceq 6027 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑧‘𝑡) = ((recs(𝐹) ↾ 𝑥)‘𝑡) → suc (𝑧‘𝑡) = suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → suc (𝑧‘𝑡) = suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) |
35 | 30, 34 | iuneq12d 4765 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → ∪
𝑡 ∈ dom 𝑧 suc (𝑧‘𝑡) = ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) |
36 | 31, 35 | uneq12d 3994 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = (recs(𝐹) ↾ 𝑥) → ((𝑔‘dom 𝑧) ∪ ∪
𝑡 ∈ dom 𝑧 suc (𝑧‘𝑡)) = ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ ∪
𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡))) |
37 | | cfsmolem.2 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝐹 = (𝑧 ∈ V ↦ ((𝑔‘dom 𝑧) ∪ ∪
𝑡 ∈ dom 𝑧 suc (𝑧‘𝑡))) |
38 | | fvex 6445 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∈ V |
39 | 29 | dmex 7360 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ dom
(recs(𝐹) ↾ 𝑥) ∈ V |
40 | | fvex 6445 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((recs(𝐹) ↾
𝑥)‘𝑡) ∈ V |
41 | 40 | sucex 7271 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ suc
((recs(𝐹) ↾ 𝑥)‘𝑡) ∈ V |
42 | 39, 41 | iunex 7407 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ∪ 𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡) ∈ V |
43 | 38, 42 | unex 7215 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ ∪
𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) ∈ V |
44 | 36, 37, 43 | fvmpt 6528 |
. . . . . . . . . . . . . . . . . . . . . 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 | syl6eq 2876 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ On → (recs(𝐹)‘𝑥) = ((𝑔‘dom (recs(𝐹) ↾ 𝑥)) ∪ ∪
𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡))) |
47 | | onss 7250 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ On → 𝑥 ⊆ On) |
48 | | fnssres 6236 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((recs(𝐹) Fn On
∧ 𝑥 ⊆ On) →
(recs(𝐹) ↾ 𝑥) Fn 𝑥) |
49 | 24, 47, 48 | sylancr 583 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ On → (recs(𝐹) ↾ 𝑥) Fn 𝑥) |
50 | | fndm 6222 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((recs(𝐹) ↾
𝑥) Fn 𝑥 → dom (recs(𝐹) ↾ 𝑥) = 𝑥) |
51 | | fveq2 6432 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (dom
(recs(𝐹) ↾ 𝑥) = 𝑥 → (𝑔‘dom (recs(𝐹) ↾ 𝑥)) = (𝑔‘𝑥)) |
52 | | iuneq1 4753 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (dom
(recs(𝐹) ↾ 𝑥) = 𝑥 → ∪
𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = ∪ 𝑡 ∈ 𝑥 suc ((recs(𝐹) ↾ 𝑥)‘𝑡)) |
53 | | fvres 6451 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 ∈ 𝑥 → ((recs(𝐹) ↾ 𝑥)‘𝑡) = (recs(𝐹)‘𝑡)) |
54 | | suceq 6027 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((recs(𝐹) ↾
𝑥)‘𝑡) = (recs(𝐹)‘𝑡) → suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = suc (recs(𝐹)‘𝑡)) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 ∈ 𝑥 → suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = suc (recs(𝐹)‘𝑡)) |
56 | 55 | iuneq2i 4758 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ∪ 𝑡 ∈ 𝑥 suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = ∪ 𝑡 ∈ 𝑥 suc (recs(𝐹)‘𝑡) |
57 | | fveq2 6432 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = 𝑡 → (recs(𝐹)‘𝑦) = (recs(𝐹)‘𝑡)) |
58 | | suceq 6027 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((recs(𝐹)‘𝑦) = (recs(𝐹)‘𝑡) → suc (recs(𝐹)‘𝑦) = suc (recs(𝐹)‘𝑡)) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = 𝑡 → suc (recs(𝐹)‘𝑦) = suc (recs(𝐹)‘𝑡)) |
60 | 59 | cbviunv 4778 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = ∪ 𝑡 ∈ 𝑥 suc (recs(𝐹)‘𝑡) |
61 | 56, 60 | eqtr4i 2851 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ∪ 𝑡 ∈ 𝑥 suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) |
62 | 52, 61 | syl6eq 2876 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (dom
(recs(𝐹) ↾ 𝑥) = 𝑥 → ∪
𝑡 ∈ dom (recs(𝐹) ↾ 𝑥)suc ((recs(𝐹) ↾ 𝑥)‘𝑡) = ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) |
63 | 51, 62 | uneq12d 3994 |
. . . . . . . . . . . . . . . . . . . . 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 2860 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ On → (recs(𝐹)‘𝑥) = ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) |
66 | 3, 65 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (cf‘𝐴) → (recs(𝐹)‘𝑥) = ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) |
67 | 22, 66 | eqtrd 2860 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (cf‘𝐴) → (𝐺‘𝑥) = ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) |
68 | 67 | 3ad2ant2 1170 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (𝐺‘𝑥) = ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) |
69 | | eloni 5972 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ On → Ord 𝐴) |
70 | 69 | adantl 475 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → Ord 𝐴) |
71 | 70 | 3ad2ant1 1169 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → Ord 𝐴) |
72 | | f1f 6337 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔:(cf‘𝐴)–1-1→𝐴 → 𝑔:(cf‘𝐴)⟶𝐴) |
73 | 72 | ffvelrnda 6607 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝑥 ∈ (cf‘𝐴)) → (𝑔‘𝑥) ∈ 𝐴) |
74 | 73 | adantlr 708 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴)) → (𝑔‘𝑥) ∈ 𝐴) |
75 | 74 | 3adant3 1168 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (𝑔‘𝑥) ∈ 𝐴) |
76 | 19 | fveq1i 6433 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐺‘𝑦) = ((recs(𝐹) ↾ (cf‘𝐴))‘𝑦) |
77 | 13 | fvresd 6452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → ((recs(𝐹) ↾ (cf‘𝐴))‘𝑦) = (recs(𝐹)‘𝑦)) |
78 | 76, 77 | syl5eq 2872 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑦) = (recs(𝐹)‘𝑦)) |
79 | 78 | adantrl 709 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ 𝑥 ∧ (𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴))) → (𝐺‘𝑦) = (recs(𝐹)‘𝑦)) |
80 | 79 | ancoms 452 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → (𝐺‘𝑦) = (recs(𝐹)‘𝑦)) |
81 | 80 | eleq1d 2890 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 ↔ (recs(𝐹)‘𝑦) ∈ 𝐴)) |
82 | | ordsucss 7278 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (Ord
𝐴 → ((recs(𝐹)‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴)) |
83 | 69, 82 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ∈ On → ((recs(𝐹)‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴)) |
84 | 83 | ad2antrr 719 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹)‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴)) |
85 | 81, 84 | sylbid 232 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ⊆ 𝐴)) |
86 | 85 | ralimdva 3170 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 → ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴)) |
87 | | iunss 4780 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 ↔ ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴) |
88 | 86, 87 | syl6ibr 244 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴)) |
89 | 88 | 3impia 1151 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴) |
90 | | onelon 5987 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈ On ∧ (recs(𝐹)‘𝑦) ∈ 𝐴) → (recs(𝐹)‘𝑦) ∈ On) |
91 | 90 | ex 403 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐴 ∈ On → ((recs(𝐹)‘𝑦) ∈ 𝐴 → (recs(𝐹)‘𝑦) ∈ On)) |
92 | 91 | ad2antrr 719 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹)‘𝑦) ∈ 𝐴 → (recs(𝐹)‘𝑦) ∈ On)) |
93 | 81, 92 | sylbid 232 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 → (recs(𝐹)‘𝑦) ∈ On)) |
94 | | suceloni 7273 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((recs(𝐹)‘𝑦) ∈ On → suc (recs(𝐹)‘𝑦) ∈ On) |
95 | 93, 94 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 → suc (recs(𝐹)‘𝑦) ∈ On)) |
96 | 95 | ralimdva 3170 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 → ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On)) |
97 | 96 | 3impia 1151 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On) |
98 | | iunon 7701 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ V ∧ ∀𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On) |
99 | 27, 98 | mpan 683 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑦 ∈
𝑥 suc (recs(𝐹)‘𝑦) ∈ On → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On) |
100 | 97, 99 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On) |
101 | | simp1 1172 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → 𝐴 ∈ On) |
102 | | onsseleq 6003 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ On ∧ 𝐴 ∈ On) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 ↔ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 ∨ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴))) |
103 | 100, 101,
102 | syl2anc 581 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 ↔ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 ∨ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴))) |
104 | | idd 24 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)) |
105 | | simpll 785 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → 𝑥 ∈ (cf‘𝐴)) |
106 | | simprr 791 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → 𝐴 ∈ On) |
107 | 3 | ad2antrr 719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → 𝑥 ∈ On) |
108 | 3, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥 ∈ (cf‘𝐴) → (recs(𝐹) ↾ 𝑥) Fn 𝑥) |
109 | 108 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (recs(𝐹) ↾ 𝑥) Fn 𝑥) |
110 | 78 | ancoms 452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → (𝐺‘𝑦) = (recs(𝐹)‘𝑦)) |
111 | | fvres 6451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑦 ∈ 𝑥 → ((recs(𝐹) ↾ 𝑥)‘𝑦) = (recs(𝐹)‘𝑦)) |
112 | 111 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹) ↾ 𝑥)‘𝑦) = (recs(𝐹)‘𝑦)) |
113 | 110, 112 | eqtr4d 2863 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → (𝐺‘𝑦) = ((recs(𝐹) ↾ 𝑥)‘𝑦)) |
114 | 113 | eleq1d 2890 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ 𝑦 ∈ 𝑥) → ((𝐺‘𝑦) ∈ 𝐴 ↔ ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴)) |
115 | 114 | ralbidva 3193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥 ∈ (cf‘𝐴) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 ↔ ∀𝑦 ∈ 𝑥 ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴)) |
116 | 115 | biimpa 470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∀𝑦 ∈ 𝑥 ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴) |
117 | | ffnfv 6636 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ↔ ((recs(𝐹) ↾ 𝑥) Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴)) |
118 | 109, 116,
117 | sylanbrc 580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴) |
119 | | eleq2 2894 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 → (𝑡 ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ 𝐴)) |
120 | 119 | biimpar 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝑡 ∈ 𝐴) → 𝑡 ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) |
121 | 120 | adantrl 709 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → 𝑡 ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) |
122 | 121 | 3adant1 1166 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → 𝑡 ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) |
123 | | onelon 5987 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) → 𝑡 ∈ On) |
124 | 111 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢
(((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹) ↾ 𝑥)‘𝑦) = (recs(𝐹)‘𝑦)) |
125 | | ffvelrn 6605 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢
(((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥) → ((recs(𝐹) ↾ 𝑥)‘𝑦) ∈ 𝐴) |
126 | 124, 125 | eqeltrrd 2906 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢
(((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥) → (recs(𝐹)‘𝑦) ∈ 𝐴) |
127 | 126, 90 | sylan2 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝐴 ∈ On ∧ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥)) → (recs(𝐹)‘𝑦) ∈ On) |
128 | 127 | adantlr 708 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥)) → (recs(𝐹)‘𝑦) ∈ On) |
129 | | onsssuc 6049 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑡 ∈ On ∧ (recs(𝐹)‘𝑦) ∈ On) → (𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ suc (recs(𝐹)‘𝑦))) |
130 | 123, 128,
129 | syl2an2r 677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ 𝑦 ∈ 𝑥)) → (𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ suc (recs(𝐹)‘𝑦))) |
131 | 130 | anassrs 461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴) ∧ 𝑦 ∈ 𝑥) → (𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ suc (recs(𝐹)‘𝑦))) |
132 | 131 | rexbidva 3258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ∈ suc (recs(𝐹)‘𝑦))) |
133 | | eliun 4743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑡 ∈ ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ∈ suc (recs(𝐹)‘𝑦)) |
134 | 132, 133 | syl6bbr 281 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝐴 ∈ On ∧ 𝑡 ∈ 𝐴) ∧ (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) |
135 | 134 | ancoms 452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) |
136 | 135 | 3adant2 1167 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦) ↔ 𝑡 ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) |
137 | 122, 136 | mpbird 249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)) |
138 | 137 | 3expa 1153 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) ∧ (𝐴 ∈ On ∧ 𝑡 ∈ 𝐴)) → ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)) |
139 | 138 | anassrs 461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) ∧ 𝐴 ∈ On) ∧ 𝑡 ∈ 𝐴) → ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)) |
140 | 139 | ralrimiva 3174 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) ∧ 𝐴 ∈ On) → ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)) |
141 | 140 | expl 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 → ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On) → ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))) |
142 | 118, 141 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On) → ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))) |
143 | 142 | imp 397 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)) |
144 | | feq1 6258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (𝑓:𝑥⟶𝐴 ↔ (recs(𝐹) ↾ 𝑥):𝑥⟶𝐴)) |
145 | | fveq1 6431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (𝑓‘𝑦) = ((recs(𝐹) ↾ 𝑥)‘𝑦)) |
146 | 145 | sseq2d 3857 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (𝑡 ⊆ (𝑓‘𝑦) ↔ 𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦))) |
147 | 146 | rexbidv 3261 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦))) |
148 | 111 | sseq2d 3857 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑦 ∈ 𝑥 → (𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦) ↔ 𝑡 ⊆ (recs(𝐹)‘𝑦))) |
149 | 148 | rexbiia 3249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(∃𝑦 ∈
𝑥 𝑡 ⊆ ((recs(𝐹) ↾ 𝑥)‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)) |
150 | 147, 149 | syl6bb 279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦) ↔ ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))) |
151 | 150 | ralbidv 3194 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → (∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦) ↔ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦))) |
152 | 144, 151 | anbi12d 626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑓 = (recs(𝐹) ↾ 𝑥) → ((𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦)) ↔ ((recs(𝐹) ↾ 𝑥):𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)))) |
153 | 29, 152 | spcev 3516 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((recs(𝐹) ↾
𝑥):𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (recs(𝐹)‘𝑦)) → ∃𝑓(𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦))) |
154 | 118, 143,
153 | syl2an2r 677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ∃𝑓(𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦))) |
155 | | cfflb 9395 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (∃𝑓(𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦)) → (cf‘𝐴) ⊆ 𝑥)) |
156 | 155 | imp 397 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐴 ∈ On ∧ 𝑥 ∈ On) ∧ ∃𝑓(𝑓:𝑥⟶𝐴 ∧ ∀𝑡 ∈ 𝐴 ∃𝑦 ∈ 𝑥 𝑡 ⊆ (𝑓‘𝑦))) → (cf‘𝐴) ⊆ 𝑥) |
157 | 106, 107,
154, 156 | syl21anc 873 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → (cf‘𝐴) ⊆ 𝑥) |
158 | | ontri1 5996 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((cf‘𝐴)
∈ On ∧ 𝑥 ∈
On) → ((cf‘𝐴)
⊆ 𝑥 ↔ ¬
𝑥 ∈ (cf‘𝐴))) |
159 | 2, 3, 158 | sylancr 583 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 ∈ (cf‘𝐴) → ((cf‘𝐴) ⊆ 𝑥 ↔ ¬ 𝑥 ∈ (cf‘𝐴))) |
160 | 159 | ad2antrr 719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ((cf‘𝐴) ⊆ 𝑥 ↔ ¬ 𝑥 ∈ (cf‘𝐴))) |
161 | 157, 160 | mpbid 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ¬ 𝑥 ∈ (cf‘𝐴)) |
162 | 105, 161 | pm2.21dd 187 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) ∧ (∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On)) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴) |
163 | 162 | ex 403 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 ∧ 𝐴 ∈ On) → ∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)) |
164 | 163 | expcomd 408 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (𝐴 ∈ On → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))) |
165 | 164 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 ∈ On → ((𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴))) |
166 | 165 | 3impib 1150 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴 → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)) |
167 | 104, 166 | jaod 892 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ((∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴 ∨ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) = 𝐴) → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)) |
168 | 103, 167 | sylbid 232 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (∪ 𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ⊆ 𝐴 → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴)) |
169 | 89, 168 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴) |
170 | 169 | 3adant1l 1227 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴) |
171 | | ordunel 7287 |
. . . . . . . . . . . . . . . . 17
⊢ ((Ord
𝐴 ∧ (𝑔‘𝑥) ∈ 𝐴 ∧ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) ∈ 𝐴) → ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) ∈ 𝐴) |
172 | 71, 75, 170, 171 | syl3anc 1496 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) ∈ 𝐴) |
173 | 68, 172 | eqeltrd 2905 |
. . . . . . . . . . . . . . 15
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴) ∧ ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴) → (𝐺‘𝑥) ∈ 𝐴) |
174 | 173 | 3expia 1156 |
. . . . . . . . . . . . . 14
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 → (𝐺‘𝑥) ∈ 𝐴)) |
175 | 174 | 3impa 1142 |
. . . . . . . . . . . . 13
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ 𝐴 → (𝐺‘𝑥) ∈ 𝐴)) |
176 | 18, 175 | syldc 48 |
. . . . . . . . . . . 12
⊢
(∀𝑦 ∈
𝑥 ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ 𝐴) → ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) ∈ 𝐴)) |
177 | 176 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑦 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ 𝐴) → ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) ∈ 𝐴))) |
178 | 9, 177 | tfis2 7316 |
. . . . . . . . . 10
⊢ (𝑥 ∈ On → ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) ∈ 𝐴)) |
179 | 4, 178 | mpcom 38 |
. . . . . . . . 9
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) ∈ 𝐴) |
180 | 179 | 3expia 1156 |
. . . . . . . 8
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → (𝑥 ∈ (cf‘𝐴) → (𝐺‘𝑥) ∈ 𝐴)) |
181 | 180 | ralrimiv 3173 |
. . . . . . 7
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → ∀𝑥 ∈ (cf‘𝐴)(𝐺‘𝑥) ∈ 𝐴) |
182 | 2 | onssi 7297 |
. . . . . . . . 9
⊢
(cf‘𝐴) ⊆
On |
183 | | fnssres 6236 |
. . . . . . . . . 10
⊢
((recs(𝐹) Fn On
∧ (cf‘𝐴) ⊆
On) → (recs(𝐹) ↾
(cf‘𝐴)) Fn
(cf‘𝐴)) |
184 | 19 | fneq1i 6217 |
. . . . . . . . . 10
⊢ (𝐺 Fn (cf‘𝐴) ↔ (recs(𝐹) ↾ (cf‘𝐴)) Fn (cf‘𝐴)) |
185 | 183, 184 | sylibr 226 |
. . . . . . . . 9
⊢
((recs(𝐹) Fn On
∧ (cf‘𝐴) ⊆
On) → 𝐺 Fn
(cf‘𝐴)) |
186 | 24, 182, 185 | mp2an 685 |
. . . . . . . 8
⊢ 𝐺 Fn (cf‘𝐴) |
187 | | ffnfv 6636 |
. . . . . . . 8
⊢ (𝐺:(cf‘𝐴)⟶𝐴 ↔ (𝐺 Fn (cf‘𝐴) ∧ ∀𝑥 ∈ (cf‘𝐴)(𝐺‘𝑥) ∈ 𝐴)) |
188 | 186, 187 | mpbiran 702 |
. . . . . . 7
⊢ (𝐺:(cf‘𝐴)⟶𝐴 ↔ ∀𝑥 ∈ (cf‘𝐴)(𝐺‘𝑥) ∈ 𝐴) |
189 | 181, 188 | sylibr 226 |
. . . . . 6
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → 𝐺:(cf‘𝐴)⟶𝐴) |
190 | 189 | adantlr 708 |
. . . . 5
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) ∧ 𝐴 ∈ On) → 𝐺:(cf‘𝐴)⟶𝐴) |
191 | | onss 7250 |
. . . . . . . 8
⊢ (𝐴 ∈ On → 𝐴 ⊆ On) |
192 | 191 | adantl 475 |
. . . . . . 7
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → 𝐴 ⊆ On) |
193 | 2 | onordi 6066 |
. . . . . . . 8
⊢ Ord
(cf‘𝐴) |
194 | | fvex 6445 |
. . . . . . . . . . . . . . . . 17
⊢
(recs(𝐹)‘𝑦) ∈ V |
195 | 194 | sucid 6041 |
. . . . . . . . . . . . . . . 16
⊢
(recs(𝐹)‘𝑦) ∈ suc (recs(𝐹)‘𝑦) |
196 | | fveq2 6432 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝑦 → (recs(𝐹)‘𝑡) = (recs(𝐹)‘𝑦)) |
197 | | suceq 6027 |
. . . . . . . . . . . . . . . . . . 19
⊢
((recs(𝐹)‘𝑡) = (recs(𝐹)‘𝑦) → suc (recs(𝐹)‘𝑡) = suc (recs(𝐹)‘𝑦)) |
198 | 196, 197 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 𝑦 → suc (recs(𝐹)‘𝑡) = suc (recs(𝐹)‘𝑦)) |
199 | 198 | eliuni 4745 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ 𝑥 ∧ (recs(𝐹)‘𝑦) ∈ suc (recs(𝐹)‘𝑦)) → (recs(𝐹)‘𝑦) ∈ ∪
𝑡 ∈ 𝑥 suc (recs(𝐹)‘𝑡)) |
200 | 199, 60 | syl6eleqr 2916 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝑥 ∧ (recs(𝐹)‘𝑦) ∈ suc (recs(𝐹)‘𝑦)) → (recs(𝐹)‘𝑦) ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) |
201 | 195, 200 | mpan2 684 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝑥 → (recs(𝐹)‘𝑦) ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) |
202 | | elun2 4007 |
. . . . . . . . . . . . . . 15
⊢
((recs(𝐹)‘𝑦) ∈ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦) → (recs(𝐹)‘𝑦) ∈ ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) |
203 | 201, 202 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝑥 → (recs(𝐹)‘𝑦) ∈ ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) |
204 | 203 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (recs(𝐹)‘𝑦) ∈ ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) |
205 | 3 | adantl 475 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → 𝑥 ∈ On) |
206 | 205, 65 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (recs(𝐹)‘𝑥) = ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦))) |
207 | 204, 206 | eleqtrrd 2908 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (recs(𝐹)‘𝑦) ∈ (recs(𝐹)‘𝑥)) |
208 | 22 | adantl 475 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑥) = (recs(𝐹)‘𝑥)) |
209 | 207, 78, 208 | 3eltr4d 2920 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ (cf‘𝐴)) → (𝐺‘𝑦) ∈ (𝐺‘𝑥)) |
210 | 209 | expcom 404 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (cf‘𝐴) → (𝑦 ∈ 𝑥 → (𝐺‘𝑦) ∈ (𝐺‘𝑥))) |
211 | 210 | ralrimiv 3173 |
. . . . . . . . 9
⊢ (𝑥 ∈ (cf‘𝐴) → ∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ (𝐺‘𝑥)) |
212 | 211 | rgen 3130 |
. . . . . . . 8
⊢
∀𝑥 ∈
(cf‘𝐴)∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ (𝐺‘𝑥) |
213 | | issmo2 7711 |
. . . . . . . . 9
⊢ (𝐺:(cf‘𝐴)⟶𝐴 → ((𝐴 ⊆ On ∧ Ord (cf‘𝐴) ∧ ∀𝑥 ∈ (cf‘𝐴)∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ (𝐺‘𝑥)) → Smo 𝐺)) |
214 | 213 | com12 32 |
. . . . . . . 8
⊢ ((𝐴 ⊆ On ∧ Ord
(cf‘𝐴) ∧
∀𝑥 ∈
(cf‘𝐴)∀𝑦 ∈ 𝑥 (𝐺‘𝑦) ∈ (𝐺‘𝑥)) → (𝐺:(cf‘𝐴)⟶𝐴 → Smo 𝐺)) |
215 | 193, 212,
214 | mp3an23 1583 |
. . . . . . 7
⊢ (𝐴 ⊆ On → (𝐺:(cf‘𝐴)⟶𝐴 → Smo 𝐺)) |
216 | 192, 189,
215 | sylc 65 |
. . . . . 6
⊢ ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ 𝐴 ∈ On) → Smo 𝐺) |
217 | 216 | adantlr 708 |
. . . . 5
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) ∧ 𝐴 ∈ On) → Smo 𝐺) |
218 | | fveq2 6432 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑤 → (𝑔‘𝑥) = (𝑔‘𝑤)) |
219 | | fveq2 6432 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑤 → (𝐺‘𝑥) = (𝐺‘𝑤)) |
220 | 218, 219 | sseq12d 3858 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑤 → ((𝑔‘𝑥) ⊆ (𝐺‘𝑥) ↔ (𝑔‘𝑤) ⊆ (𝐺‘𝑤))) |
221 | | ssun1 4002 |
. . . . . . . . . . 11
⊢ (𝑔‘𝑥) ⊆ ((𝑔‘𝑥) ∪ ∪
𝑦 ∈ 𝑥 suc (recs(𝐹)‘𝑦)) |
222 | 221, 67 | syl5sseqr 3878 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (cf‘𝐴) → (𝑔‘𝑥) ⊆ (𝐺‘𝑥)) |
223 | 220, 222 | vtoclga 3488 |
. . . . . . . . 9
⊢ (𝑤 ∈ (cf‘𝐴) → (𝑔‘𝑤) ⊆ (𝐺‘𝑤)) |
224 | | sstr 3834 |
. . . . . . . . . 10
⊢ ((𝑧 ⊆ (𝑔‘𝑤) ∧ (𝑔‘𝑤) ⊆ (𝐺‘𝑤)) → 𝑧 ⊆ (𝐺‘𝑤)) |
225 | 224 | expcom 404 |
. . . . . . . . 9
⊢ ((𝑔‘𝑤) ⊆ (𝐺‘𝑤) → (𝑧 ⊆ (𝑔‘𝑤) → 𝑧 ⊆ (𝐺‘𝑤))) |
226 | 223, 225 | syl 17 |
. . . . . . . 8
⊢ (𝑤 ∈ (cf‘𝐴) → (𝑧 ⊆ (𝑔‘𝑤) → 𝑧 ⊆ (𝐺‘𝑤))) |
227 | 226 | reximia 3216 |
. . . . . . 7
⊢
(∃𝑤 ∈
(cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤) → ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤)) |
228 | 227 | ralimi 3160 |
. . . . . 6
⊢
(∀𝑧 ∈
𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤) → ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤)) |
229 | 228 | ad2antlr 720 |
. . . . 5
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) ∧ 𝐴 ∈ On) → ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤)) |
230 | | fnex 6736 |
. . . . . . 7
⊢ ((𝐺 Fn (cf‘𝐴) ∧ (cf‘𝐴) ∈ On) → 𝐺 ∈ V) |
231 | 186, 2, 230 | mp2an 685 |
. . . . . 6
⊢ 𝐺 ∈ V |
232 | | feq1 6258 |
. . . . . . 7
⊢ (𝑓 = 𝐺 → (𝑓:(cf‘𝐴)⟶𝐴 ↔ 𝐺:(cf‘𝐴)⟶𝐴)) |
233 | | smoeq 7712 |
. . . . . . 7
⊢ (𝑓 = 𝐺 → (Smo 𝑓 ↔ Smo 𝐺)) |
234 | | fveq1 6431 |
. . . . . . . . . 10
⊢ (𝑓 = 𝐺 → (𝑓‘𝑤) = (𝐺‘𝑤)) |
235 | 234 | sseq2d 3857 |
. . . . . . . . 9
⊢ (𝑓 = 𝐺 → (𝑧 ⊆ (𝑓‘𝑤) ↔ 𝑧 ⊆ (𝐺‘𝑤))) |
236 | 235 | rexbidv 3261 |
. . . . . . . 8
⊢ (𝑓 = 𝐺 → (∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤) ↔ ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤))) |
237 | 236 | ralbidv 3194 |
. . . . . . 7
⊢ (𝑓 = 𝐺 → (∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤) ↔ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤))) |
238 | 232, 233,
237 | 3anbi123d 1566 |
. . . . . 6
⊢ (𝑓 = 𝐺 → ((𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤)) ↔ (𝐺:(cf‘𝐴)⟶𝐴 ∧ Smo 𝐺 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤)))) |
239 | 231, 238 | spcev 3516 |
. . . . 5
⊢ ((𝐺:(cf‘𝐴)⟶𝐴 ∧ Smo 𝐺 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝐺‘𝑤)) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤))) |
240 | 190, 217,
229, 239 | syl3anc 1496 |
. . . 4
⊢ (((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) ∧ 𝐴 ∈ On) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤))) |
241 | 240 | expcom 404 |
. . 3
⊢ (𝐴 ∈ On → ((𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤)))) |
242 | 241 | exlimdv 2034 |
. 2
⊢ (𝐴 ∈ On → (∃𝑔(𝑔:(cf‘𝐴)–1-1→𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑔‘𝑤)) → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤)))) |
243 | 1, 242 | mpd 15 |
1
⊢ (𝐴 ∈ On → ∃𝑓(𝑓:(cf‘𝐴)⟶𝐴 ∧ Smo 𝑓 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ (cf‘𝐴)𝑧 ⊆ (𝑓‘𝑤))) |