Step | Hyp | Ref
| Expression |
1 | | vex 3203 |
. . . 4
⊢ 𝑥 ∈ V |
2 | | fr0g 7531 |
. . . 4
⊢ (𝑥 ∈ V → ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘∅) = 𝑥) |
3 | 1, 2 | ax-mp 5 |
. . 3
⊢
((rec((𝑣 ∈ V
↦ suc 𝑣), 𝑥) ↾
ω)‘∅) = 𝑥 |
4 | | frfnom 7530 |
. . . 4
⊢
(rec((𝑣 ∈ V
↦ suc 𝑣), 𝑥) ↾ ω) Fn
ω |
5 | | peano1 7085 |
. . . 4
⊢ ∅
∈ ω |
6 | | fnfvelrn 6356 |
. . . 4
⊢
(((rec((𝑣 ∈ V
↦ suc 𝑣), 𝑥) ↾ ω) Fn ω
∧ ∅ ∈ ω) → ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘∅) ∈ ran
(rec((𝑣 ∈ V ↦
suc 𝑣), 𝑥) ↾ ω)) |
7 | 4, 5, 6 | mp2an 708 |
. . 3
⊢
((rec((𝑣 ∈ V
↦ suc 𝑣), 𝑥) ↾
ω)‘∅) ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) |
8 | 3, 7 | eqeltrri 2698 |
. 2
⊢ 𝑥 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) |
9 | | fvelrnb 6243 |
. . . . 5
⊢
((rec((𝑣 ∈ V
↦ suc 𝑣), 𝑥) ↾ ω) Fn ω
→ (𝑧 ∈ ran
(rec((𝑣 ∈ V ↦
suc 𝑣), 𝑥) ↾ ω) ↔ ∃𝑓 ∈ ω ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) = 𝑧)) |
10 | 4, 9 | ax-mp 5 |
. . . 4
⊢ (𝑧 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) ↔ ∃𝑓 ∈ ω ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) = 𝑧) |
11 | | fvex 6201 |
. . . . . . . . . 10
⊢
((rec((𝑣 ∈ V
↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) ∈ V |
12 | 11 | sucid 5804 |
. . . . . . . . 9
⊢
((rec((𝑣 ∈ V
↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) ∈ suc ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) |
13 | 11 | sucex 7011 |
. . . . . . . . . 10
⊢ suc
((rec((𝑣 ∈ V ↦
suc 𝑣), 𝑥) ↾ ω)‘𝑓) ∈ V |
14 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(rec((𝑣 ∈ V
↦ suc 𝑣), 𝑥) ↾ ω) = (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) |
15 | | suceq 5790 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑣 → suc 𝑧 = suc 𝑣) |
16 | | suceq 5790 |
. . . . . . . . . . 11
⊢ (𝑧 = ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) → suc 𝑧 = suc ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓)) |
17 | 14, 15, 16 | frsucmpt2 7535 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ ω ∧ suc
((rec((𝑣 ∈ V ↦
suc 𝑣), 𝑥) ↾ ω)‘𝑓) ∈ V) → ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) = suc ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓)) |
18 | 13, 17 | mpan2 707 |
. . . . . . . . 9
⊢ (𝑓 ∈ ω →
((rec((𝑣 ∈ V ↦
suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) = suc ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓)) |
19 | 12, 18 | syl5eleqr 2708 |
. . . . . . . 8
⊢ (𝑓 ∈ ω →
((rec((𝑣 ∈ V ↦
suc 𝑣), 𝑥) ↾ ω)‘𝑓) ∈ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓)) |
20 | | eleq1 2689 |
. . . . . . . 8
⊢
(((rec((𝑣 ∈ V
↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) = 𝑧 → (((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) ∈ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ↔ 𝑧 ∈ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓))) |
21 | 19, 20 | syl5ib 234 |
. . . . . . 7
⊢
(((rec((𝑣 ∈ V
↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) = 𝑧 → (𝑓 ∈ ω → 𝑧 ∈ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓))) |
22 | | peano2b 7081 |
. . . . . . . . 9
⊢ (𝑓 ∈ ω ↔ suc 𝑓 ∈
ω) |
23 | | fnfvelrn 6356 |
. . . . . . . . . 10
⊢
(((rec((𝑣 ∈ V
↦ suc 𝑣), 𝑥) ↾ ω) Fn ω
∧ suc 𝑓 ∈ ω)
→ ((rec((𝑣 ∈ V
↦ suc 𝑣), 𝑥) ↾ ω)‘suc
𝑓) ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)) |
24 | 4, 23 | mpan 706 |
. . . . . . . . 9
⊢ (suc
𝑓 ∈ ω →
((rec((𝑣 ∈ V ↦
suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)) |
25 | 22, 24 | sylbi 207 |
. . . . . . . 8
⊢ (𝑓 ∈ ω →
((rec((𝑣 ∈ V ↦
suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)) |
26 | 25 | a1i 11 |
. . . . . . 7
⊢
(((rec((𝑣 ∈ V
↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) = 𝑧 → (𝑓 ∈ ω → ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))) |
27 | 21, 26 | jcad 555 |
. . . . . 6
⊢
(((rec((𝑣 ∈ V
↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) = 𝑧 → (𝑓 ∈ ω → (𝑧 ∈ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∧ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))) |
28 | | fvex 6201 |
. . . . . . 7
⊢
((rec((𝑣 ∈ V
↦ suc 𝑣), 𝑥) ↾ ω)‘suc
𝑓) ∈
V |
29 | | eleq2 2690 |
. . . . . . . 8
⊢ (𝑤 = ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) → (𝑧 ∈ 𝑤 ↔ 𝑧 ∈ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓))) |
30 | | eleq1 2689 |
. . . . . . . 8
⊢ (𝑤 = ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) → (𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) ↔ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))) |
31 | 29, 30 | anbi12d 747 |
. . . . . . 7
⊢ (𝑤 = ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) → ((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)) ↔ (𝑧 ∈ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∧ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))) |
32 | 28, 31 | spcev 3300 |
. . . . . 6
⊢ ((𝑧 ∈ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∧ ((rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)‘suc 𝑓) ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)) → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))) |
33 | 27, 32 | syl6com 37 |
. . . . 5
⊢ (𝑓 ∈ ω →
(((rec((𝑣 ∈ V ↦
suc 𝑣), 𝑥) ↾ ω)‘𝑓) = 𝑧 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))) |
34 | 33 | rexlimiv 3027 |
. . . 4
⊢
(∃𝑓 ∈
ω ((rec((𝑣 ∈ V
↦ suc 𝑣), 𝑥) ↾ ω)‘𝑓) = 𝑧 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))) |
35 | 10, 34 | sylbi 207 |
. . 3
⊢ (𝑧 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))) |
36 | 35 | ax-gen 1722 |
. 2
⊢
∀𝑧(𝑧 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))) |
37 | | fndm 5990 |
. . . . . 6
⊢
((rec((𝑣 ∈ V
↦ suc 𝑣), 𝑥) ↾ ω) Fn ω
→ dom (rec((𝑣 ∈ V
↦ suc 𝑣), 𝑥) ↾ ω) =
ω) |
38 | 4, 37 | ax-mp 5 |
. . . . 5
⊢ dom
(rec((𝑣 ∈ V ↦
suc 𝑣), 𝑥) ↾ ω) = ω |
39 | | inf0.1 |
. . . . 5
⊢ ω
∈ V |
40 | 38, 39 | eqeltri 2697 |
. . . 4
⊢ dom
(rec((𝑣 ∈ V ↦
suc 𝑣), 𝑥) ↾ ω) ∈ V |
41 | | fnfun 5988 |
. . . . 5
⊢
((rec((𝑣 ∈ V
↦ suc 𝑣), 𝑥) ↾ ω) Fn ω
→ Fun (rec((𝑣 ∈ V
↦ suc 𝑣), 𝑥) ↾
ω)) |
42 | 4, 41 | ax-mp 5 |
. . . 4
⊢ Fun
(rec((𝑣 ∈ V ↦
suc 𝑣), 𝑥) ↾ ω) |
43 | | funrnex 7133 |
. . . 4
⊢ (dom
(rec((𝑣 ∈ V ↦
suc 𝑣), 𝑥) ↾ ω) ∈ V → (Fun
(rec((𝑣 ∈ V ↦
suc 𝑣), 𝑥) ↾ ω) → ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) ∈
V)) |
44 | 40, 42, 43 | mp2 9 |
. . 3
⊢ ran
(rec((𝑣 ∈ V ↦
suc 𝑣), 𝑥) ↾ ω) ∈ V |
45 | | eleq2 2690 |
. . . 4
⊢ (𝑦 = ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))) |
46 | | eleq2 2690 |
. . . . . 6
⊢ (𝑦 = ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))) |
47 | | eleq2 2690 |
. . . . . . . 8
⊢ (𝑦 = ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → (𝑤 ∈ 𝑦 ↔ 𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))) |
48 | 47 | anbi2d 740 |
. . . . . . 7
⊢ (𝑦 = ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦) ↔ (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))) |
49 | 48 | exbidv 1850 |
. . . . . 6
⊢ (𝑦 = ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → (∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦) ↔ ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))) |
50 | 46, 49 | imbi12d 334 |
. . . . 5
⊢ (𝑦 = ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ((𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)) ↔ (𝑧 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))))) |
51 | 50 | albidv 1849 |
. . . 4
⊢ (𝑦 = ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → (∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)) ↔ ∀𝑧(𝑧 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω))))) |
52 | 45, 51 | anbi12d 747 |
. . 3
⊢ (𝑦 = ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ((𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))) ↔ (𝑥 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) ∧ ∀𝑧(𝑧 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))))) |
53 | 44, 52 | spcev 3300 |
. 2
⊢ ((𝑥 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) ∧ ∀𝑧(𝑧 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω)))) → ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)))) |
54 | 8, 36, 53 | mp2an 708 |
1
⊢
∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))) |