Step | Hyp | Ref
| Expression |
1 | | simpr 103 |
. . . . . . 7
⊢
((z = w ∧ g = 𝑘) → g = 𝑘) |
2 | | simpl 102 |
. . . . . . 7
⊢
((z = w ∧ g = 𝑘) → z = w) |
3 | 1, 2 | fneq12d 4934 |
. . . . . 6
⊢
((z = w ∧ g = 𝑘) → (g Fn z ↔
𝑘 Fn w)) |
4 | 1 | fveq1d 5123 |
. . . . . . . 8
⊢
((z = w ∧ g = 𝑘) → (g‘u) =
(𝑘‘u)) |
5 | 1 | reseq1d 4554 |
. . . . . . . . 9
⊢
((z = w ∧ g = 𝑘) → (g ↾ u) =
(𝑘 ↾ u)) |
6 | 5 | fveq2d 5125 |
. . . . . . . 8
⊢
((z = w ∧ g = 𝑘) → (𝐹‘(g ↾ u)) =
(𝐹‘(𝑘 ↾ u))) |
7 | 4, 6 | eqeq12d 2051 |
. . . . . . 7
⊢
((z = w ∧ g = 𝑘) → ((g‘u) =
(𝐹‘(g ↾ u))
↔ (𝑘‘u) = (𝐹‘(𝑘 ↾ u)))) |
8 | 2, 7 | raleqbidv 2511 |
. . . . . 6
⊢
((z = w ∧ g = 𝑘) → (∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u))
↔ ∀u ∈ w (𝑘‘u)
= (𝐹‘(𝑘 ↾ u)))) |
9 | 3, 8 | anbi12d 442 |
. . . . 5
⊢
((z = w ∧ g = 𝑘) → ((g Fn z ∧ ∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u)))
↔ (𝑘 Fn w ∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u))))) |
10 | 9 | cbvexdva 1801 |
. . . 4
⊢ (z = w →
(∃g(g Fn z ∧ ∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u)))
↔ ∃𝑘(𝑘 Fn w
∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u))))) |
11 | 10 | imbi2d 219 |
. . 3
⊢ (z = w →
((φ → ∃g(g Fn z ∧ ∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u))))
↔ (φ → ∃𝑘(𝑘 Fn w
∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u)))))) |
12 | | fneq2 4931 |
. . . . . 6
⊢ (z = 𝐶 → (g Fn z ↔
g Fn 𝐶)) |
13 | | raleq 2499 |
. . . . . 6
⊢ (z = 𝐶 → (∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u))
↔ ∀u ∈ 𝐶 (g‘u) =
(𝐹‘(g ↾ u)))) |
14 | 12, 13 | anbi12d 442 |
. . . . 5
⊢ (z = 𝐶 → ((g Fn z ∧ ∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u)))
↔ (g Fn 𝐶 ∧ ∀u ∈ 𝐶 (g‘u) =
(𝐹‘(g ↾ u))))) |
15 | 14 | exbidv 1703 |
. . . 4
⊢ (z = 𝐶 → (∃g(g Fn z ∧ ∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u)))
↔ ∃g(g Fn 𝐶 ∧ ∀u ∈ 𝐶 (g‘u) =
(𝐹‘(g ↾ u))))) |
16 | 15 | imbi2d 219 |
. . 3
⊢ (z = 𝐶 → ((φ → ∃g(g Fn z ∧ ∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u))))
↔ (φ → ∃g(g Fn 𝐶 ∧ ∀u ∈ 𝐶 (g‘u) =
(𝐹‘(g ↾ u)))))) |
17 | | r19.21v 2390 |
. . . 4
⊢ (∀w ∈ z (φ → ∃𝑘(𝑘 Fn w
∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u)))) ↔ (φ → ∀w ∈ z ∃𝑘(𝑘 Fn w
∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u))))) |
18 | | tfrlemisucfn.1 |
. . . . . . . . 9
⊢ A = {f ∣
∃x ∈ On (f Fn
x ∧ ∀y ∈ x (f‘y) =
(𝐹‘(f ↾ y)))} |
19 | 18 | tfrlem3 5867 |
. . . . . . . 8
⊢ A = {g ∣
∃z ∈ On (g Fn
z ∧ ∀𝑒 ∈ z (g‘𝑒) = (𝐹‘(g ↾ 𝑒)))} |
20 | | tfrlemisucfn.2 |
. . . . . . . . . 10
⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈
V)) |
21 | | fveq2 5121 |
. . . . . . . . . . . . 13
⊢ (x = z →
(𝐹‘x) = (𝐹‘z)) |
22 | 21 | eleq1d 2103 |
. . . . . . . . . . . 12
⊢ (x = z →
((𝐹‘x) ∈ V ↔
(𝐹‘z) ∈
V)) |
23 | 22 | anbi2d 437 |
. . . . . . . . . . 11
⊢ (x = z →
((Fun 𝐹 ∧ (𝐹‘x) ∈ V) ↔
(Fun 𝐹 ∧ (𝐹‘z) ∈
V))) |
24 | 23 | cbvalv 1791 |
. . . . . . . . . 10
⊢ (∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V) ↔
∀z(Fun
𝐹 ∧ (𝐹‘z) ∈
V)) |
25 | 20, 24 | sylib 127 |
. . . . . . . . 9
⊢ (φ → ∀z(Fun 𝐹 ∧ (𝐹‘z) ∈
V)) |
26 | 25 | adantr 261 |
. . . . . . . 8
⊢ ((φ ∧
(z ∈ On
∧ ∀w ∈ z ∃𝑘(𝑘 Fn w
∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u))))) → ∀z(Fun 𝐹 ∧ (𝐹‘z) ∈
V)) |
27 | | simpr 103 |
. . . . . . . . . . . . 13
⊢ (((𝑡 = ℎ ∧ w = v) ∧ 𝑘
= f) → 𝑘 = f) |
28 | | simplr 482 |
. . . . . . . . . . . . 13
⊢ (((𝑡 = ℎ ∧ w = v) ∧ 𝑘
= f) → w = v) |
29 | 27, 28 | fneq12d 4934 |
. . . . . . . . . . . 12
⊢ (((𝑡 = ℎ ∧ w = v) ∧ 𝑘
= f) → (𝑘 Fn w
↔ f Fn v)) |
30 | 27 | eleq1d 2103 |
. . . . . . . . . . . 12
⊢ (((𝑡 = ℎ ∧ w = v) ∧ 𝑘
= f) → (𝑘 ∈ A ↔ f ∈ A)) |
31 | | simpll 481 |
. . . . . . . . . . . . 13
⊢ (((𝑡 = ℎ ∧ w = v) ∧ 𝑘
= f) → 𝑡 = ℎ) |
32 | 27 | fveq2d 5125 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑡 = ℎ ∧ w = v) ∧ 𝑘
= f) → (𝐹‘𝑘) = (𝐹‘f)) |
33 | 28, 32 | opeq12d 3548 |
. . . . . . . . . . . . . . 15
⊢ (((𝑡 = ℎ ∧ w = v) ∧ 𝑘
= f) → 〈w, (𝐹‘𝑘)〉 = 〈v, (𝐹‘f)〉) |
34 | 33 | sneqd 3380 |
. . . . . . . . . . . . . 14
⊢ (((𝑡 = ℎ ∧ w = v) ∧ 𝑘
= f) → {〈w, (𝐹‘𝑘)〉} = {〈v, (𝐹‘f)〉}) |
35 | 27, 34 | uneq12d 3092 |
. . . . . . . . . . . . 13
⊢ (((𝑡 = ℎ ∧ w = v) ∧ 𝑘
= f) → (𝑘 ∪ {〈w, (𝐹‘𝑘)〉}) = (f ∪ {〈v, (𝐹‘f)〉})) |
36 | 31, 35 | eqeq12d 2051 |
. . . . . . . . . . . 12
⊢ (((𝑡 = ℎ ∧ w = v) ∧ 𝑘
= f) → (𝑡 = (𝑘 ∪ {〈w, (𝐹‘𝑘)〉}) ↔ ℎ = (f
∪ {〈v, (𝐹‘f)〉}))) |
37 | 29, 30, 36 | 3anbi123d 1206 |
. . . . . . . . . . 11
⊢ (((𝑡 = ℎ ∧ w = v) ∧ 𝑘
= f) → ((𝑘 Fn w
∧ 𝑘 ∈ A ∧ 𝑡 = (𝑘 ∪ {〈w, (𝐹‘𝑘)〉})) ↔ (f Fn v ∧ f ∈ A ∧ ℎ
= (f ∪ {〈v, (𝐹‘f)〉})))) |
38 | 37 | cbvexdva 1801 |
. . . . . . . . . 10
⊢ ((𝑡 = ℎ ∧ w = v) →
(∃𝑘(𝑘 Fn w
∧ 𝑘 ∈ A ∧ 𝑡 = (𝑘 ∪ {〈w, (𝐹‘𝑘)〉})) ↔ ∃f(f Fn v ∧ f ∈ A ∧ ℎ
= (f ∪ {〈v, (𝐹‘f)〉})))) |
39 | 38 | cbvrexdva 2534 |
. . . . . . . . 9
⊢ (𝑡 = ℎ → (∃w ∈ z ∃𝑘(𝑘 Fn w
∧ 𝑘 ∈ A ∧ 𝑡 = (𝑘 ∪ {〈w, (𝐹‘𝑘)〉})) ↔ ∃v ∈ z ∃f(f Fn v ∧ f ∈ A ∧ ℎ
= (f ∪ {〈v, (𝐹‘f)〉})))) |
40 | 39 | cbvabv 2158 |
. . . . . . . 8
⊢ {𝑡 ∣ ∃w ∈ z ∃𝑘(𝑘 Fn w
∧ 𝑘 ∈ A ∧ 𝑡 = (𝑘 ∪ {〈w, (𝐹‘𝑘)〉}))} = {ℎ ∣ ∃v ∈ z ∃f(f Fn v ∧ f ∈ A ∧ ℎ
= (f ∪ {〈v, (𝐹‘f)〉}))} |
41 | | simpl 102 |
. . . . . . . . 9
⊢
((z ∈ On ∧ ∀w ∈ z ∃𝑘(𝑘 Fn w
∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u)))) → z
∈ On) |
42 | 41 | adantl 262 |
. . . . . . . 8
⊢ ((φ ∧
(z ∈ On
∧ ∀w ∈ z ∃𝑘(𝑘 Fn w
∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u))))) → z
∈ On) |
43 | | simpr 103 |
. . . . . . . . . 10
⊢
((z ∈ On ∧ ∀w ∈ z ∃𝑘(𝑘 Fn w
∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u)))) → ∀w ∈ z ∃𝑘(𝑘 Fn w
∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u)))) |
44 | | simpr 103 |
. . . . . . . . . . . . . 14
⊢
((w = v ∧ 𝑘 = f)
→ 𝑘 = f) |
45 | | simpl 102 |
. . . . . . . . . . . . . 14
⊢
((w = v ∧ 𝑘 = f)
→ w = v) |
46 | 44, 45 | fneq12d 4934 |
. . . . . . . . . . . . 13
⊢
((w = v ∧ 𝑘 = f)
→ (𝑘 Fn w ↔ f Fn
v)) |
47 | | simplr 482 |
. . . . . . . . . . . . . . . 16
⊢
(((w = v ∧ 𝑘 = f)
∧ u =
y) → 𝑘 = f) |
48 | | simpr 103 |
. . . . . . . . . . . . . . . 16
⊢
(((w = v ∧ 𝑘 = f)
∧ u =
y) → u = y) |
49 | 47, 48 | fveq12d 5127 |
. . . . . . . . . . . . . . 15
⊢
(((w = v ∧ 𝑘 = f)
∧ u =
y) → (𝑘‘u)
= (f‘y)) |
50 | 47, 48 | reseq12d 4556 |
. . . . . . . . . . . . . . . 16
⊢
(((w = v ∧ 𝑘 = f)
∧ u =
y) → (𝑘 ↾ u) = (f ↾
y)) |
51 | 50 | fveq2d 5125 |
. . . . . . . . . . . . . . 15
⊢
(((w = v ∧ 𝑘 = f)
∧ u =
y) → (𝐹‘(𝑘 ↾ u)) = (𝐹‘(f ↾ y))) |
52 | 49, 51 | eqeq12d 2051 |
. . . . . . . . . . . . . 14
⊢
(((w = v ∧ 𝑘 = f)
∧ u =
y) → ((𝑘‘u)
= (𝐹‘(𝑘 ↾ u)) ↔ (f‘y) =
(𝐹‘(f ↾ y)))) |
53 | | simpll 481 |
. . . . . . . . . . . . . 14
⊢
(((w = v ∧ 𝑘 = f)
∧ u =
y) → w = v) |
54 | 52, 53 | cbvraldva2 2531 |
. . . . . . . . . . . . 13
⊢
((w = v ∧ 𝑘 = f)
→ (∀u ∈ w (𝑘‘u)
= (𝐹‘(𝑘 ↾ u)) ↔ ∀y ∈ v (f‘y) =
(𝐹‘(f ↾ y)))) |
55 | 46, 54 | anbi12d 442 |
. . . . . . . . . . . 12
⊢
((w = v ∧ 𝑘 = f)
→ ((𝑘 Fn w ∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u))) ↔ (f
Fn v ∧
∀y
∈ v
(f‘y) = (𝐹‘(f ↾ y))))) |
56 | 55 | cbvexdva 1801 |
. . . . . . . . . . 11
⊢ (w = v →
(∃𝑘(𝑘 Fn w
∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u))) ↔ ∃f(f Fn v ∧ ∀y ∈ v (f‘y) =
(𝐹‘(f ↾ y))))) |
57 | 56 | cbvralv 2527 |
. . . . . . . . . 10
⊢ (∀w ∈ z ∃𝑘(𝑘 Fn w
∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u))) ↔ ∀v ∈ z ∃f(f Fn v ∧ ∀y ∈ v (f‘y) =
(𝐹‘(f ↾ y)))) |
58 | 43, 57 | sylib 127 |
. . . . . . . . 9
⊢
((z ∈ On ∧ ∀w ∈ z ∃𝑘(𝑘 Fn w
∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u)))) → ∀v ∈ z ∃f(f Fn v ∧ ∀y ∈ v (f‘y) =
(𝐹‘(f ↾ y)))) |
59 | 58 | adantl 262 |
. . . . . . . 8
⊢ ((φ ∧
(z ∈ On
∧ ∀w ∈ z ∃𝑘(𝑘 Fn w
∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u))))) → ∀v ∈ z ∃f(f Fn v ∧ ∀y ∈ v (f‘y) =
(𝐹‘(f ↾ y)))) |
60 | 19, 26, 40, 42, 59 | tfrlemiex 5886 |
. . . . . . 7
⊢ ((φ ∧
(z ∈ On
∧ ∀w ∈ z ∃𝑘(𝑘 Fn w
∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u))))) → ∃g(g Fn z ∧ ∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u)))) |
61 | 60 | expr 357 |
. . . . . 6
⊢ ((φ ∧ z ∈ On) →
(∀w
∈ z ∃𝑘(𝑘 Fn w
∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u))) → ∃g(g Fn z ∧ ∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u))))) |
62 | 61 | expcom 109 |
. . . . 5
⊢ (z ∈ On →
(φ → (∀w ∈ z ∃𝑘(𝑘 Fn w
∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u))) → ∃g(g Fn z ∧ ∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u)))))) |
63 | 62 | a2d 23 |
. . . 4
⊢ (z ∈ On →
((φ → ∀w ∈ z ∃𝑘(𝑘 Fn w
∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u)))) → (φ → ∃g(g Fn z ∧ ∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u)))))) |
64 | 17, 63 | syl5bi 141 |
. . 3
⊢ (z ∈ On →
(∀w
∈ z
(φ → ∃𝑘(𝑘 Fn w
∧ ∀u ∈ w (𝑘‘u) = (𝐹‘(𝑘 ↾ u)))) → (φ → ∃g(g Fn z ∧ ∀u ∈ z (g‘u) =
(𝐹‘(g ↾ u)))))) |
65 | 11, 16, 64 | tfis3 4252 |
. 2
⊢ (𝐶 ∈ On → (φ → ∃g(g Fn 𝐶 ∧ ∀u ∈ 𝐶 (g‘u) =
(𝐹‘(g ↾ u))))) |
66 | 65 | impcom 116 |
1
⊢ ((φ ∧ 𝐶 ∈ On) → ∃g(g Fn 𝐶 ∧ ∀u ∈ 𝐶 (g‘u) =
(𝐹‘(g ↾ u)))) |