Step | Hyp | Ref
| Expression |
1 | | tfrlemisucfn.3 |
. . . 4
⊢ (φ → z ∈
On) |
2 | | suceloni 4193 |
. . . 4
⊢ (z ∈ On → suc
z ∈
On) |
3 | 1, 2 | syl 14 |
. . 3
⊢ (φ → suc z ∈
On) |
4 | | tfrlemisucfn.1 |
. . . 4
⊢ A = {f ∣
∃x ∈ On (f Fn
x ∧ ∀y ∈ x (f‘y) =
(𝐹‘(f ↾ y)))} |
5 | | tfrlemisucfn.2 |
. . . 4
⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈
V)) |
6 | | tfrlemisucfn.4 |
. . . 4
⊢ (φ → g Fn z) |
7 | | tfrlemisucfn.5 |
. . . 4
⊢ (φ → g ∈ A) |
8 | 4, 5, 1, 6, 7 | tfrlemisucfn 5879 |
. . 3
⊢ (φ → (g ∪ {〈z, (𝐹‘g)〉}) Fn suc z) |
9 | | vex 2554 |
. . . . . 6
⊢ u ∈
V |
10 | 9 | elsuc 4109 |
. . . . 5
⊢ (u ∈ suc z ↔ (u
∈ z ∨ u = z)) |
11 | | vex 2554 |
. . . . . . . . . . 11
⊢ g ∈
V |
12 | 4, 11 | tfrlem3a 5866 |
. . . . . . . . . 10
⊢ (g ∈ A ↔ ∃v ∈ On (g Fn
v ∧ ∀u ∈ v (g‘u) =
(𝐹‘(g ↾ u)))) |
13 | 7, 12 | sylib 127 |
. . . . . . . . 9
⊢ (φ → ∃v ∈ On (g Fn
v ∧ ∀u ∈ v (g‘u) =
(𝐹‘(g ↾ u)))) |
14 | | simprrr 492 |
. . . . . . . . . 10
⊢ ((φ ∧
(v ∈ On
∧ (g Fn
v ∧ ∀u ∈ v (g‘u) =
(𝐹‘(g ↾ u)))))
→ ∀u ∈ v (g‘u) =
(𝐹‘(g ↾ u))) |
15 | | simprrl 491 |
. . . . . . . . . . . 12
⊢ ((φ ∧
(v ∈ On
∧ (g Fn
v ∧ ∀u ∈ v (g‘u) =
(𝐹‘(g ↾ u)))))
→ g Fn v) |
16 | 6 | adantr 261 |
. . . . . . . . . . . 12
⊢ ((φ ∧
(v ∈ On
∧ (g Fn
v ∧ ∀u ∈ v (g‘u) =
(𝐹‘(g ↾ u)))))
→ g Fn z) |
17 | | fndmu 4943 |
. . . . . . . . . . . 12
⊢
((g Fn v ∧ g Fn z) →
v = z) |
18 | 15, 16, 17 | syl2anc 391 |
. . . . . . . . . . 11
⊢ ((φ ∧
(v ∈ On
∧ (g Fn
v ∧ ∀u ∈ v (g‘u) =
(𝐹‘(g ↾ u)))))
→ v = z) |
19 | 18 | raleqdv 2505 |
. . . . . . . . . 10
⊢ ((φ ∧
(v ∈ On
∧ (g Fn
v ∧ ∀u ∈ v (g‘u) =
(𝐹‘(g ↾ u)))))
→ (∀u ∈ v (g‘u) =
(𝐹‘(g ↾ u))
↔ ∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u)))) |
20 | 14, 19 | mpbid 135 |
. . . . . . . . 9
⊢ ((φ ∧
(v ∈ On
∧ (g Fn
v ∧ ∀u ∈ v (g‘u) =
(𝐹‘(g ↾ u)))))
→ ∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u))) |
21 | 13, 20 | rexlimddv 2431 |
. . . . . . . 8
⊢ (φ → ∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u))) |
22 | 21 | r19.21bi 2401 |
. . . . . . 7
⊢ ((φ ∧ u ∈ z) → (g‘u) =
(𝐹‘(g ↾ u))) |
23 | | elirrv 4226 |
. . . . . . . . . . 11
⊢ ¬
u ∈
u |
24 | | elequ2 1598 |
. . . . . . . . . . 11
⊢ (z = u →
(u ∈
z ↔ u ∈ u)) |
25 | 23, 24 | mtbiri 599 |
. . . . . . . . . 10
⊢ (z = u →
¬ u ∈
z) |
26 | 25 | necon2ai 2253 |
. . . . . . . . 9
⊢ (u ∈ z → z ≠
u) |
27 | 26 | adantl 262 |
. . . . . . . 8
⊢ ((φ ∧ u ∈ z) → z ≠
u) |
28 | | fvunsng 5300 |
. . . . . . . 8
⊢
((u ∈ V ∧ z ≠ u) →
((g ∪ {〈z, (𝐹‘g)〉})‘u) = (g‘u)) |
29 | 9, 27, 28 | sylancr 393 |
. . . . . . 7
⊢ ((φ ∧ u ∈ z) → ((g
∪ {〈z, (𝐹‘g)〉})‘u) = (g‘u)) |
30 | | eloni 4078 |
. . . . . . . . . . . 12
⊢ (z ∈ On → Ord
z) |
31 | 1, 30 | syl 14 |
. . . . . . . . . . 11
⊢ (φ → Ord z) |
32 | | ordelss 4082 |
. . . . . . . . . . 11
⊢ ((Ord
z ∧
u ∈
z) → u ⊆ z) |
33 | 31, 32 | sylan 267 |
. . . . . . . . . 10
⊢ ((φ ∧ u ∈ z) → u
⊆ z) |
34 | | resabs1 4583 |
. . . . . . . . . 10
⊢ (u ⊆ z
→ (((g ∪ {〈z, (𝐹‘g)〉}) ↾ z) ↾ u) =
((g ∪ {〈z, (𝐹‘g)〉}) ↾ u)) |
35 | 33, 34 | syl 14 |
. . . . . . . . 9
⊢ ((φ ∧ u ∈ z) → (((g
∪ {〈z, (𝐹‘g)〉}) ↾ z) ↾ u) =
((g ∪ {〈z, (𝐹‘g)〉}) ↾ u)) |
36 | | elirrv 4226 |
. . . . . . . . . . . 12
⊢ ¬
z ∈
z |
37 | | fsnunres 5307 |
. . . . . . . . . . . 12
⊢
((g Fn z ∧ ¬ z ∈ z) → ((g
∪ {〈z, (𝐹‘g)〉}) ↾ z) = g) |
38 | 6, 36, 37 | sylancl 392 |
. . . . . . . . . . 11
⊢ (φ → ((g ∪ {〈z, (𝐹‘g)〉}) ↾ z) = g) |
39 | 38 | reseq1d 4554 |
. . . . . . . . . 10
⊢ (φ → (((g ∪ {〈z, (𝐹‘g)〉}) ↾ z) ↾ u) =
(g ↾ u)) |
40 | 39 | adantr 261 |
. . . . . . . . 9
⊢ ((φ ∧ u ∈ z) → (((g
∪ {〈z, (𝐹‘g)〉}) ↾ z) ↾ u) =
(g ↾ u)) |
41 | 35, 40 | eqtr3d 2071 |
. . . . . . . 8
⊢ ((φ ∧ u ∈ z) → ((g
∪ {〈z, (𝐹‘g)〉}) ↾ u) = (g ↾
u)) |
42 | 41 | fveq2d 5125 |
. . . . . . 7
⊢ ((φ ∧ u ∈ z) → (𝐹‘((g ∪ {〈z, (𝐹‘g)〉}) ↾ u)) = (𝐹‘(g ↾ u))) |
43 | 22, 29, 42 | 3eqtr4d 2079 |
. . . . . 6
⊢ ((φ ∧ u ∈ z) → ((g
∪ {〈z, (𝐹‘g)〉})‘u) = (𝐹‘((g ∪ {〈z, (𝐹‘g)〉}) ↾ u))) |
44 | 5 | tfrlem3-2d 5869 |
. . . . . . . . . 10
⊢ (φ → (Fun 𝐹 ∧ (𝐹‘g) ∈
V)) |
45 | 44 | simprd 107 |
. . . . . . . . 9
⊢ (φ → (𝐹‘g) ∈
V) |
46 | | fndm 4941 |
. . . . . . . . . . . 12
⊢ (g Fn z →
dom g = z) |
47 | 6, 46 | syl 14 |
. . . . . . . . . . 11
⊢ (φ → dom g = z) |
48 | 47 | eleq2d 2104 |
. . . . . . . . . 10
⊢ (φ → (z ∈ dom g ↔ z ∈ z)) |
49 | 36, 48 | mtbiri 599 |
. . . . . . . . 9
⊢ (φ → ¬ z ∈ dom g) |
50 | | fsnunfv 5306 |
. . . . . . . . 9
⊢
((z ∈ On ∧ (𝐹‘g) ∈ V ∧ ¬ z ∈ dom g) →
((g ∪ {〈z, (𝐹‘g)〉})‘z) = (𝐹‘g)) |
51 | 1, 45, 49, 50 | syl3anc 1134 |
. . . . . . . 8
⊢ (φ → ((g ∪ {〈z, (𝐹‘g)〉})‘z) = (𝐹‘g)) |
52 | 51 | adantr 261 |
. . . . . . 7
⊢ ((φ ∧ u = z) →
((g ∪ {〈z, (𝐹‘g)〉})‘z) = (𝐹‘g)) |
53 | | simpr 103 |
. . . . . . . 8
⊢ ((φ ∧ u = z) →
u = z) |
54 | 53 | fveq2d 5125 |
. . . . . . 7
⊢ ((φ ∧ u = z) →
((g ∪ {〈z, (𝐹‘g)〉})‘u) = ((g ∪
{〈z, (𝐹‘g)〉})‘z)) |
55 | | reseq2 4550 |
. . . . . . . . 9
⊢ (u = z →
((g ∪ {〈z, (𝐹‘g)〉}) ↾ u) = ((g ∪
{〈z, (𝐹‘g)〉}) ↾ z)) |
56 | 55, 38 | sylan9eqr 2091 |
. . . . . . . 8
⊢ ((φ ∧ u = z) →
((g ∪ {〈z, (𝐹‘g)〉}) ↾ u) = g) |
57 | 56 | fveq2d 5125 |
. . . . . . 7
⊢ ((φ ∧ u = z) →
(𝐹‘((g ∪ {〈z, (𝐹‘g)〉}) ↾ u)) = (𝐹‘g)) |
58 | 52, 54, 57 | 3eqtr4d 2079 |
. . . . . 6
⊢ ((φ ∧ u = z) →
((g ∪ {〈z, (𝐹‘g)〉})‘u) = (𝐹‘((g ∪ {〈z, (𝐹‘g)〉}) ↾ u))) |
59 | 43, 58 | jaodan 709 |
. . . . 5
⊢ ((φ ∧
(u ∈
z ∨
u = z))
→ ((g ∪ {〈z, (𝐹‘g)〉})‘u) = (𝐹‘((g ∪ {〈z, (𝐹‘g)〉}) ↾ u))) |
60 | 10, 59 | sylan2b 271 |
. . . 4
⊢ ((φ ∧ u ∈ suc z) → ((g
∪ {〈z, (𝐹‘g)〉})‘u) = (𝐹‘((g ∪ {〈z, (𝐹‘g)〉}) ↾ u))) |
61 | 60 | ralrimiva 2386 |
. . 3
⊢ (φ → ∀u ∈ suc z((g ∪
{〈z, (𝐹‘g)〉})‘u) = (𝐹‘((g ∪ {〈z, (𝐹‘g)〉}) ↾ u))) |
62 | | fneq2 4931 |
. . . . 5
⊢ (w = suc z →
((g ∪ {〈z, (𝐹‘g)〉}) Fn w
↔ (g ∪ {〈z, (𝐹‘g)〉}) Fn suc z)) |
63 | | raleq 2499 |
. . . . 5
⊢ (w = suc z →
(∀u
∈ w
((g ∪ {〈z, (𝐹‘g)〉})‘u) = (𝐹‘((g ∪ {〈z, (𝐹‘g)〉}) ↾ u)) ↔ ∀u ∈ suc z((g ∪
{〈z, (𝐹‘g)〉})‘u) = (𝐹‘((g ∪ {〈z, (𝐹‘g)〉}) ↾ u)))) |
64 | 62, 63 | anbi12d 442 |
. . . 4
⊢ (w = suc z →
(((g ∪ {〈z, (𝐹‘g)〉}) Fn w
∧ ∀u ∈ w ((g ∪ {〈z, (𝐹‘g)〉})‘u) = (𝐹‘((g ∪ {〈z, (𝐹‘g)〉}) ↾ u))) ↔ ((g
∪ {〈z, (𝐹‘g)〉}) Fn suc z ∧ ∀u ∈ suc z((g ∪
{〈z, (𝐹‘g)〉})‘u) = (𝐹‘((g ∪ {〈z, (𝐹‘g)〉}) ↾ u))))) |
65 | 64 | rspcev 2650 |
. . 3
⊢ ((suc
z ∈ On
∧ ((g
∪ {〈z, (𝐹‘g)〉}) Fn suc z ∧ ∀u ∈ suc z((g ∪
{〈z, (𝐹‘g)〉})‘u) = (𝐹‘((g ∪ {〈z, (𝐹‘g)〉}) ↾ u)))) → ∃w ∈ On ((g ∪
{〈z, (𝐹‘g)〉}) Fn w
∧ ∀u ∈ w ((g ∪ {〈z, (𝐹‘g)〉})‘u) = (𝐹‘((g ∪ {〈z, (𝐹‘g)〉}) ↾ u)))) |
66 | 3, 8, 61, 65 | syl12anc 1132 |
. 2
⊢ (φ → ∃w ∈ On ((g ∪
{〈z, (𝐹‘g)〉}) Fn w
∧ ∀u ∈ w ((g ∪ {〈z, (𝐹‘g)〉})‘u) = (𝐹‘((g ∪ {〈z, (𝐹‘g)〉}) ↾ u)))) |
67 | | vex 2554 |
. . . . . 6
⊢ z ∈
V |
68 | | opexg 3955 |
. . . . . 6
⊢
((z ∈ V ∧ (𝐹‘g) ∈ V) →
〈z, (𝐹‘g)〉 ∈
V) |
69 | 67, 45, 68 | sylancr 393 |
. . . . 5
⊢ (φ → 〈z, (𝐹‘g)〉 ∈
V) |
70 | | snexg 3927 |
. . . . 5
⊢
(〈z, (𝐹‘g)〉 ∈ V
→ {〈z, (𝐹‘g)〉} ∈
V) |
71 | 69, 70 | syl 14 |
. . . 4
⊢ (φ → {〈z, (𝐹‘g)〉} ∈
V) |
72 | | unexg 4144 |
. . . 4
⊢
((g ∈ V ∧
{〈z, (𝐹‘g)〉} ∈ V)
→ (g ∪ {〈z, (𝐹‘g)〉}) ∈
V) |
73 | 11, 71, 72 | sylancr 393 |
. . 3
⊢ (φ → (g ∪ {〈z, (𝐹‘g)〉}) ∈
V) |
74 | 4 | tfrlem3ag 5865 |
. . 3
⊢
((g ∪ {〈z, (𝐹‘g)〉}) ∈ V
→ ((g ∪ {〈z, (𝐹‘g)〉}) ∈
A ↔ ∃w ∈ On ((g ∪
{〈z, (𝐹‘g)〉}) Fn w
∧ ∀u ∈ w ((g ∪ {〈z, (𝐹‘g)〉})‘u) = (𝐹‘((g ∪ {〈z, (𝐹‘g)〉}) ↾ u))))) |
75 | 73, 74 | syl 14 |
. 2
⊢ (φ → ((g ∪ {〈z, (𝐹‘g)〉}) ∈
A ↔ ∃w ∈ On ((g ∪
{〈z, (𝐹‘g)〉}) Fn w
∧ ∀u ∈ w ((g ∪ {〈z, (𝐹‘g)〉})‘u) = (𝐹‘((g ∪ {〈z, (𝐹‘g)〉}) ↾ u))))) |
76 | 66, 75 | mpbird 156 |
1
⊢ (φ → (g ∪ {〈z, (𝐹‘g)〉}) ∈
A) |