| Step | Hyp | Ref
| Expression |
| 1 | | rdg0g 8467 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (rec(𝐹, 𝐴)‘∅) = 𝐴) |
| 2 | | peano1 7910 |
. . . 4
⊢ ∅
∈ ω |
| 3 | | omelon 9686 |
. . . . 5
⊢ ω
∈ On |
| 4 | | limom 7903 |
. . . . 5
⊢ Lim
ω |
| 5 | | rdglimss 37378 |
. . . . 5
⊢
(((ω ∈ On ∧ Lim ω) ∧ ∅ ∈ ω)
→ (rec(𝐹, 𝐴)‘∅) ⊆
(rec(𝐹, 𝐴)‘ω)) |
| 6 | 3, 4, 5 | mpanl12 702 |
. . . 4
⊢ (∅
∈ ω → (rec(𝐹, 𝐴)‘∅) ⊆ (rec(𝐹, 𝐴)‘ω)) |
| 7 | 2, 6 | ax-mp 5 |
. . 3
⊢
(rec(𝐹, 𝐴)‘∅) ⊆
(rec(𝐹, 𝐴)‘ω) |
| 8 | 1, 7 | eqsstrrdi 4029 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (rec(𝐹, 𝐴)‘ω)) |
| 9 | | rdglim2a 8473 |
. . . . . . . 8
⊢ ((ω
∈ On ∧ Lim ω) → (rec(𝐹, 𝐴)‘ω) = ∪ 𝑢 ∈ ω (rec(𝐹, 𝐴)‘𝑢)) |
| 10 | 3, 4, 9 | mp2an 692 |
. . . . . . 7
⊢
(rec(𝐹, 𝐴)‘ω) = ∪ 𝑢 ∈ ω (rec(𝐹, 𝐴)‘𝑢) |
| 11 | 10 | eleq2i 2833 |
. . . . . 6
⊢ (𝑦 ∈ (rec(𝐹, 𝐴)‘ω) ↔ 𝑦 ∈ ∪
𝑢 ∈ ω (rec(𝐹, 𝐴)‘𝑢)) |
| 12 | | eliun 4995 |
. . . . . 6
⊢ (𝑦 ∈ ∪ 𝑢 ∈ ω (rec(𝐹, 𝐴)‘𝑢) ↔ ∃𝑢 ∈ ω 𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢)) |
| 13 | 11, 12 | bitri 275 |
. . . . 5
⊢ (𝑦 ∈ (rec(𝐹, 𝐴)‘ω) ↔ ∃𝑢 ∈ ω 𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢)) |
| 14 | | peano2 7912 |
. . . . . . . . 9
⊢ (𝑢 ∈ ω → suc 𝑢 ∈
ω) |
| 15 | | nnon 7893 |
. . . . . . . . . 10
⊢ (𝑢 ∈ ω → 𝑢 ∈ On) |
| 16 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) = (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) |
| 17 | 16 | elrnmpt1 5971 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ∧ 𝐵 ∈ 𝑊) → 𝐵 ∈ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)) |
| 18 | | elun2 4183 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) → 𝐵 ∈ ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵))) |
| 19 | 17, 18 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ∧ 𝐵 ∈ 𝑊) → 𝐵 ∈ ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵))) |
| 20 | | fvex 6919 |
. . . . . . . . . . . . . 14
⊢
(rec(𝐹, 𝐴)‘𝑢) ∈ V |
| 21 | | exrecfnlem.1 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐹 = (𝑧 ∈ V ↦ (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵))) |
| 22 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑦V |
| 23 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑦𝑧 |
| 24 | | nfmpt1 5250 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑦(𝑦 ∈ 𝑧 ↦ 𝐵) |
| 25 | 24 | nfrn 5963 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑦ran
(𝑦 ∈ 𝑧 ↦ 𝐵) |
| 26 | 23, 25 | nfun 4170 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑦(𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵)) |
| 27 | 22, 26 | nfmpt 5249 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑦(𝑧 ∈ V ↦ (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵))) |
| 28 | 21, 27 | nfcxfr 2903 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑦𝐹 |
| 29 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑦𝐴 |
| 30 | 28, 29 | nfrdg 8454 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑦rec(𝐹, 𝐴) |
| 31 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑦𝑢 |
| 32 | 30, 31 | nffv 6916 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑦(rec(𝐹, 𝐴)‘𝑢) |
| 33 | 32 | mptexgf 7242 |
. . . . . . . . . . . . . . . 16
⊢
((rec(𝐹, 𝐴)‘𝑢) ∈ V → (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) ∈ V) |
| 34 | 20, 33 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) ∈ V |
| 35 | 34 | rnex 7932 |
. . . . . . . . . . . . . 14
⊢ ran
(𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) ∈ V |
| 36 | 20, 35 | unex 7764 |
. . . . . . . . . . . . 13
⊢
((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)) ∈ V |
| 37 | | nfcv 2905 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑧𝐴 |
| 38 | | nfcv 2905 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑧𝑢 |
| 39 | | nfmpt1 5250 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑧(𝑧 ∈ V ↦ (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵))) |
| 40 | 21, 39 | nfcxfr 2903 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑧𝐹 |
| 41 | 40, 37 | nfrdg 8454 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑧rec(𝐹, 𝐴) |
| 42 | 41, 38 | nffv 6916 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑧(rec(𝐹, 𝐴)‘𝑢) |
| 43 | | nfcv 2905 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑧𝐵 |
| 44 | 42, 43 | nfmpt 5249 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑧(𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) |
| 45 | 44 | nfrn 5963 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑧ran
(𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵) |
| 46 | 42, 45 | nfun 4170 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑧((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)) |
| 47 | | rdgeq1 8451 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 = (𝑧 ∈ V ↦ (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵))) → rec(𝐹, 𝐴) = rec((𝑧 ∈ V ↦ (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵))), 𝐴)) |
| 48 | 21, 47 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ rec(𝐹, 𝐴) = rec((𝑧 ∈ V ↦ (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵))), 𝐴) |
| 49 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (rec(𝐹, 𝐴)‘𝑢) → 𝑧 = (rec(𝐹, 𝐴)‘𝑢)) |
| 50 | 32 | nfeq2 2923 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑦 𝑧 = (rec(𝐹, 𝐴)‘𝑢) |
| 51 | | eqidd 2738 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (rec(𝐹, 𝐴)‘𝑢) → 𝐵 = 𝐵) |
| 52 | 50, 49, 51 | mpteq12df 5228 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (rec(𝐹, 𝐴)‘𝑢) → (𝑦 ∈ 𝑧 ↦ 𝐵) = (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)) |
| 53 | 52 | rneqd 5949 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (rec(𝐹, 𝐴)‘𝑢) → ran (𝑦 ∈ 𝑧 ↦ 𝐵) = ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)) |
| 54 | 49, 53 | uneq12d 4169 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (rec(𝐹, 𝐴)‘𝑢) → (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵)) = ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵))) |
| 55 | 37, 38, 46, 48, 54 | rdgsucmptf 8468 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ On ∧ ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)) ∈ V) → (rec(𝐹, 𝐴)‘suc 𝑢) = ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵))) |
| 56 | 36, 55 | mpan2 691 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ On → (rec(𝐹, 𝐴)‘suc 𝑢) = ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵))) |
| 57 | 56 | eleq2d 2827 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ On → (𝐵 ∈ (rec(𝐹, 𝐴)‘suc 𝑢) ↔ 𝐵 ∈ ((rec(𝐹, 𝐴)‘𝑢) ∪ ran (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ↦ 𝐵)))) |
| 58 | 19, 57 | imbitrrid 246 |
. . . . . . . . . 10
⊢ (𝑢 ∈ On → ((𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ∧ 𝐵 ∈ 𝑊) → 𝐵 ∈ (rec(𝐹, 𝐴)‘suc 𝑢))) |
| 59 | 15, 58 | syl 17 |
. . . . . . . . 9
⊢ (𝑢 ∈ ω → ((𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ∧ 𝐵 ∈ 𝑊) → 𝐵 ∈ (rec(𝐹, 𝐴)‘suc 𝑢))) |
| 60 | | rdgellim 37377 |
. . . . . . . . . 10
⊢
(((ω ∈ On ∧ Lim ω) ∧ suc 𝑢 ∈ ω) → (𝐵 ∈ (rec(𝐹, 𝐴)‘suc 𝑢) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω))) |
| 61 | 3, 4, 60 | mpanl12 702 |
. . . . . . . . 9
⊢ (suc
𝑢 ∈ ω →
(𝐵 ∈ (rec(𝐹, 𝐴)‘suc 𝑢) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω))) |
| 62 | 14, 59, 61 | sylsyld 61 |
. . . . . . . 8
⊢ (𝑢 ∈ ω → ((𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) ∧ 𝐵 ∈ 𝑊) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω))) |
| 63 | 62 | expd 415 |
. . . . . . 7
⊢ (𝑢 ∈ ω → (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) → (𝐵 ∈ 𝑊 → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))) |
| 64 | 63 | com3r 87 |
. . . . . 6
⊢ (𝐵 ∈ 𝑊 → (𝑢 ∈ ω → (𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))) |
| 65 | 64 | rexlimdv 3153 |
. . . . 5
⊢ (𝐵 ∈ 𝑊 → (∃𝑢 ∈ ω 𝑦 ∈ (rec(𝐹, 𝐴)‘𝑢) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω))) |
| 66 | 13, 65 | biimtrid 242 |
. . . 4
⊢ (𝐵 ∈ 𝑊 → (𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω))) |
| 67 | 66 | alimi 1811 |
. . 3
⊢
(∀𝑦 𝐵 ∈ 𝑊 → ∀𝑦(𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω))) |
| 68 | | df-ral 3062 |
. . 3
⊢
(∀𝑦 ∈
(rec(𝐹, 𝐴)‘ω)𝐵 ∈ (rec(𝐹, 𝐴)‘ω) ↔ ∀𝑦(𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω))) |
| 69 | 67, 68 | sylibr 234 |
. 2
⊢
(∀𝑦 𝐵 ∈ 𝑊 → ∀𝑦 ∈ (rec(𝐹, 𝐴)‘ω)𝐵 ∈ (rec(𝐹, 𝐴)‘ω)) |
| 70 | | fvex 6919 |
. . 3
⊢
(rec(𝐹, 𝐴)‘ω) ∈
V |
| 71 | | sseq2 4010 |
. . . 4
⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ (rec(𝐹, 𝐴)‘ω))) |
| 72 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑦ω |
| 73 | 30, 72 | nffv 6916 |
. . . . . . 7
⊢
Ⅎ𝑦(rec(𝐹, 𝐴)‘ω) |
| 74 | 73 | nfeq2 2923 |
. . . . . 6
⊢
Ⅎ𝑦 𝑥 = (rec(𝐹, 𝐴)‘ω) |
| 75 | | eleq2 2830 |
. . . . . . 7
⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (rec(𝐹, 𝐴)‘ω))) |
| 76 | | eleq2 2830 |
. . . . . . 7
⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → (𝐵 ∈ 𝑥 ↔ 𝐵 ∈ (rec(𝐹, 𝐴)‘ω))) |
| 77 | 75, 76 | imbi12d 344 |
. . . . . 6
⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → ((𝑦 ∈ 𝑥 → 𝐵 ∈ 𝑥) ↔ (𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))) |
| 78 | 74, 77 | albid 2222 |
. . . . 5
⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → (∀𝑦(𝑦 ∈ 𝑥 → 𝐵 ∈ 𝑥) ↔ ∀𝑦(𝑦 ∈ (rec(𝐹, 𝐴)‘ω) → 𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))) |
| 79 | | df-ral 3062 |
. . . . 5
⊢
(∀𝑦 ∈
𝑥 𝐵 ∈ 𝑥 ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝐵 ∈ 𝑥)) |
| 80 | 78, 79, 68 | 3bitr4g 314 |
. . . 4
⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → (∀𝑦 ∈ 𝑥 𝐵 ∈ 𝑥 ↔ ∀𝑦 ∈ (rec(𝐹, 𝐴)‘ω)𝐵 ∈ (rec(𝐹, 𝐴)‘ω))) |
| 81 | 71, 80 | anbi12d 632 |
. . 3
⊢ (𝑥 = (rec(𝐹, 𝐴)‘ω) → ((𝐴 ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝐵 ∈ 𝑥) ↔ (𝐴 ⊆ (rec(𝐹, 𝐴)‘ω) ∧ ∀𝑦 ∈ (rec(𝐹, 𝐴)‘ω)𝐵 ∈ (rec(𝐹, 𝐴)‘ω)))) |
| 82 | 70, 81 | spcev 3606 |
. 2
⊢ ((𝐴 ⊆ (rec(𝐹, 𝐴)‘ω) ∧ ∀𝑦 ∈ (rec(𝐹, 𝐴)‘ω)𝐵 ∈ (rec(𝐹, 𝐴)‘ω)) → ∃𝑥(𝐴 ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝐵 ∈ 𝑥)) |
| 83 | 8, 69, 82 | syl2an 596 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦 𝐵 ∈ 𝑊) → ∃𝑥(𝐴 ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝐵 ∈ 𝑥)) |