Step | Hyp | Ref
| Expression |
1 | | tfrlemi14d.1 |
. . . 4
⊢ A = {f ∣
∃x ∈ On (f Fn
x ∧ ∀y ∈ x (f‘y) =
(𝐹‘(f ↾ y)))} |
2 | 1 | tfrlem8 5875 |
. . 3
⊢ Ord dom
recs(𝐹) |
3 | | ordsson 4184 |
. . 3
⊢ (Ord dom
recs(𝐹) → dom
recs(𝐹) ⊆
On) |
4 | 2, 3 | mp1i 10 |
. 2
⊢ (φ → dom recs(𝐹) ⊆ On) |
5 | | tfrlemi14d.2 |
. . . . . . . 8
⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈
V)) |
6 | 1, 5 | tfrlemi1 5887 |
. . . . . . 7
⊢ ((φ ∧ z ∈ On) →
∃g(g Fn z ∧ ∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u)))) |
7 | 5 | ad2antrr 457 |
. . . . . . . . 9
⊢ (((φ ∧ z ∈ On) ∧ (g Fn z ∧ ∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u))))
→ ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈
V)) |
8 | | simplr 482 |
. . . . . . . . 9
⊢ (((φ ∧ z ∈ On) ∧ (g Fn z ∧ ∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u))))
→ z ∈ On) |
9 | | simprl 483 |
. . . . . . . . 9
⊢ (((φ ∧ z ∈ On) ∧ (g Fn z ∧ ∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u))))
→ g Fn z) |
10 | | fneq2 4931 |
. . . . . . . . . . . . 13
⊢ (w = z →
(g Fn w
↔ g Fn z)) |
11 | | raleq 2499 |
. . . . . . . . . . . . 13
⊢ (w = z →
(∀u
∈ w
(g‘u) = (𝐹‘(g ↾ u))
↔ ∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u)))) |
12 | 10, 11 | anbi12d 442 |
. . . . . . . . . . . 12
⊢ (w = z →
((g Fn w ∧ ∀u ∈ w (g‘u) =
(𝐹‘(g ↾ u)))
↔ (g Fn z ∧ ∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u))))) |
13 | 12 | rspcev 2650 |
. . . . . . . . . . 11
⊢
((z ∈ On ∧ (g Fn z ∧ ∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u))))
→ ∃w ∈ On (g Fn w ∧ ∀u ∈ w (g‘u) =
(𝐹‘(g ↾ u)))) |
14 | 13 | adantll 445 |
. . . . . . . . . 10
⊢ (((φ ∧ z ∈ On) ∧ (g Fn z ∧ ∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u))))
→ ∃w ∈ On (g Fn w ∧ ∀u ∈ w (g‘u) =
(𝐹‘(g ↾ u)))) |
15 | | vex 2554 |
. . . . . . . . . . 11
⊢ g ∈
V |
16 | 1, 15 | tfrlem3a 5866 |
. . . . . . . . . 10
⊢ (g ∈ A ↔ ∃w ∈ On (g Fn
w ∧ ∀u ∈ w (g‘u) =
(𝐹‘(g ↾ u)))) |
17 | 14, 16 | sylibr 137 |
. . . . . . . . 9
⊢ (((φ ∧ z ∈ On) ∧ (g Fn z ∧ ∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u))))
→ g ∈ A) |
18 | 1, 7, 8, 9, 17 | tfrlemisucaccv 5880 |
. . . . . . . 8
⊢ (((φ ∧ z ∈ On) ∧ (g Fn z ∧ ∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u))))
→ (g ∪ {〈z, (𝐹‘g)〉}) ∈
A) |
19 | | vex 2554 |
. . . . . . . . . . . 12
⊢ z ∈
V |
20 | 5 | tfrlem3-2d 5869 |
. . . . . . . . . . . . 13
⊢ (φ → (Fun 𝐹 ∧ (𝐹‘g) ∈
V)) |
21 | 20 | simprd 107 |
. . . . . . . . . . . 12
⊢ (φ → (𝐹‘g) ∈
V) |
22 | | opexg 3955 |
. . . . . . . . . . . 12
⊢
((z ∈ V ∧ (𝐹‘g) ∈ V) →
〈z, (𝐹‘g)〉 ∈
V) |
23 | 19, 21, 22 | sylancr 393 |
. . . . . . . . . . 11
⊢ (φ → 〈z, (𝐹‘g)〉 ∈
V) |
24 | | snidg 3392 |
. . . . . . . . . . 11
⊢
(〈z, (𝐹‘g)〉 ∈ V
→ 〈z, (𝐹‘g)〉 ∈
{〈z, (𝐹‘g)〉}) |
25 | | elun2 3105 |
. . . . . . . . . . 11
⊢
(〈z, (𝐹‘g)〉 ∈
{〈z, (𝐹‘g)〉} → 〈z, (𝐹‘g)〉 ∈
(g ∪ {〈z, (𝐹‘g)〉})) |
26 | 23, 24, 25 | 3syl 17 |
. . . . . . . . . 10
⊢ (φ → 〈z, (𝐹‘g)〉 ∈
(g ∪ {〈z, (𝐹‘g)〉})) |
27 | 26 | ad2antrr 457 |
. . . . . . . . 9
⊢ (((φ ∧ z ∈ On) ∧ (g Fn z ∧ ∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u))))
→ 〈z, (𝐹‘g)〉 ∈
(g ∪ {〈z, (𝐹‘g)〉})) |
28 | | opeldmg 4483 |
. . . . . . . . . . 11
⊢
((z ∈ V ∧ (𝐹‘g) ∈ V) →
(〈z, (𝐹‘g)〉 ∈
(g ∪ {〈z, (𝐹‘g)〉}) → z ∈ dom (g ∪ {〈z, (𝐹‘g)〉}))) |
29 | 19, 21, 28 | sylancr 393 |
. . . . . . . . . 10
⊢ (φ → (〈z, (𝐹‘g)〉 ∈
(g ∪ {〈z, (𝐹‘g)〉}) → z ∈ dom (g ∪ {〈z, (𝐹‘g)〉}))) |
30 | 29 | ad2antrr 457 |
. . . . . . . . 9
⊢ (((φ ∧ z ∈ On) ∧ (g Fn z ∧ ∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u))))
→ (〈z, (𝐹‘g)〉 ∈
(g ∪ {〈z, (𝐹‘g)〉}) → z ∈ dom (g ∪ {〈z, (𝐹‘g)〉}))) |
31 | 27, 30 | mpd 13 |
. . . . . . . 8
⊢ (((φ ∧ z ∈ On) ∧ (g Fn z ∧ ∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u))))
→ z ∈ dom (g ∪
{〈z, (𝐹‘g)〉})) |
32 | | dmeq 4478 |
. . . . . . . . . 10
⊢ (ℎ = (g ∪ {〈z, (𝐹‘g)〉}) → dom ℎ = dom (g
∪ {〈z, (𝐹‘g)〉})) |
33 | 32 | eleq2d 2104 |
. . . . . . . . 9
⊢ (ℎ = (g ∪ {〈z, (𝐹‘g)〉}) → (z ∈ dom ℎ ↔ z ∈ dom (g ∪ {〈z, (𝐹‘g)〉}))) |
34 | 33 | rspcev 2650 |
. . . . . . . 8
⊢
(((g ∪ {〈z, (𝐹‘g)〉}) ∈
A ∧
z ∈ dom
(g ∪ {〈z, (𝐹‘g)〉})) → ∃ℎ
∈ A
z ∈ dom
ℎ) |
35 | 18, 31, 34 | syl2anc 391 |
. . . . . . 7
⊢ (((φ ∧ z ∈ On) ∧ (g Fn z ∧ ∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u))))
→ ∃ℎ ∈ A z ∈ dom ℎ) |
36 | 6, 35 | exlimddv 1775 |
. . . . . 6
⊢ ((φ ∧ z ∈ On) →
∃ℎ ∈ A z ∈ dom ℎ) |
37 | | eliun 3652 |
. . . . . 6
⊢ (z ∈ ∪ ℎ
∈ A dom
ℎ ↔ ∃ℎ
∈ A
z ∈ dom
ℎ) |
38 | 36, 37 | sylibr 137 |
. . . . 5
⊢ ((φ ∧ z ∈ On) →
z ∈
∪ ℎ ∈ A dom ℎ) |
39 | 38 | ex 108 |
. . . 4
⊢ (φ → (z ∈ On →
z ∈
∪ ℎ ∈ A dom ℎ)) |
40 | 39 | ssrdv 2945 |
. . 3
⊢ (φ → On ⊆ ∪ ℎ
∈ A dom
ℎ) |
41 | 1 | recsfval 5872 |
. . . . 5
⊢
recs(𝐹) = ∪ A |
42 | 41 | dmeqi 4479 |
. . . 4
⊢ dom
recs(𝐹) = dom ∪ A |
43 | | dmuni 4488 |
. . . 4
⊢ dom ∪ A = ∪ ℎ
∈ A dom
ℎ |
44 | 42, 43 | eqtri 2057 |
. . 3
⊢ dom
recs(𝐹) = ∪ ℎ
∈ A dom
ℎ |
45 | 40, 44 | syl6sseqr 2986 |
. 2
⊢ (φ → On ⊆ dom recs(𝐹)) |
46 | 4, 45 | eqssd 2956 |
1
⊢ (φ → dom recs(𝐹) = On) |