Step | Hyp | Ref
| Expression |
1 | | ins3keq 4219 |
. . 3
⊢ (x = A →
Ins3k x = Ins3k A) |
2 | 1 | eleq1d 2419 |
. 2
⊢ (x = A → (
Ins3k x ∈ V ↔ Ins3k A ∈
V)) |
3 | | ax-ins3 4085 |
. . 3
⊢ ∃y∀z∀w∀t(⟪{{z}},
⟪w, t⟫⟫ ∈ y ↔
⟪z, w⟫ ∈
x) |
4 | | inss1 3475 |
. . . . . . . 8
⊢ ((℘11c
×k (V ×k V)) ∩ y) ⊆ (℘11c
×k (V ×k V)) |
5 | | ins3kss 4280 |
. . . . . . . 8
⊢ Ins3k x ⊆ (℘11c
×k (V ×k V)) |
6 | 4, 5 | insklem 4304 |
. . . . . . 7
⊢ (((℘11c
×k (V ×k V)) ∩ y) = Ins3k x ↔ ∀z∀w∀t(⟪{{z}},
⟪w, t⟫⟫ ∈ ((℘11c
×k (V ×k V)) ∩ y) ↔ ⟪{{z}}, ⟪w,
t⟫⟫ ∈ Ins3k x)) |
7 | | vex 2862 |
. . . . . . . . . . . . . 14
⊢ z ∈
V |
8 | 7 | snel1c 4140 |
. . . . . . . . . . . . 13
⊢ {z} ∈
1c |
9 | | snelpw1 4146 |
. . . . . . . . . . . . 13
⊢ ({{z}} ∈ ℘11c ↔
{z} ∈
1c) |
10 | 8, 9 | mpbir 200 |
. . . . . . . . . . . 12
⊢ {{z}} ∈ ℘11c |
11 | | vex 2862 |
. . . . . . . . . . . . 13
⊢ w ∈
V |
12 | | vex 2862 |
. . . . . . . . . . . . 13
⊢ t ∈
V |
13 | 11, 12 | opkelxpk 4248 |
. . . . . . . . . . . . 13
⊢ (⟪w, t⟫
∈ (V ×k V) ↔
(w ∈ V
∧ t ∈ V)) |
14 | 11, 12, 13 | mpbir2an 886 |
. . . . . . . . . . . 12
⊢ ⟪w, t⟫
∈ (V ×k
V) |
15 | | snex 4111 |
. . . . . . . . . . . . 13
⊢ {{z}} ∈
V |
16 | | opkex 4113 |
. . . . . . . . . . . . 13
⊢ ⟪w, t⟫
∈ V |
17 | 15, 16 | opkelxpk 4248 |
. . . . . . . . . . . 12
⊢ (⟪{{z}}, ⟪w,
t⟫⟫ ∈ (℘11c
×k (V ×k V)) ↔ ({{z}} ∈ ℘11c ∧ ⟪w,
t⟫ ∈ (V ×k
V))) |
18 | 10, 14, 17 | mpbir2an 886 |
. . . . . . . . . . 11
⊢ ⟪{{z}}, ⟪w,
t⟫⟫ ∈ (℘11c
×k (V ×k V)) |
19 | | elin 3219 |
. . . . . . . . . . 11
⊢ (⟪{{z}}, ⟪w,
t⟫⟫ ∈ ((℘11c
×k (V ×k V)) ∩ y) ↔ (⟪{{z}}, ⟪w,
t⟫⟫ ∈ (℘11c
×k (V ×k V)) ∧ ⟪{{z}},
⟪w, t⟫⟫ ∈ y)) |
20 | 18, 19 | mpbiran 884 |
. . . . . . . . . 10
⊢ (⟪{{z}}, ⟪w,
t⟫⟫ ∈ ((℘11c
×k (V ×k V)) ∩ y) ↔ ⟪{{z}}, ⟪w,
t⟫⟫ ∈ y) |
21 | 7, 11, 12 | otkelins3k 4256 |
. . . . . . . . . 10
⊢ (⟪{{z}}, ⟪w,
t⟫⟫ ∈ Ins3k x ↔ ⟪z, w⟫
∈ x) |
22 | 20, 21 | bibi12i 306 |
. . . . . . . . 9
⊢
((⟪{{z}}, ⟪w, t⟫⟫ ∈ ((℘11c
×k (V ×k V)) ∩ y) ↔ ⟪{{z}}, ⟪w,
t⟫⟫ ∈ Ins3k x) ↔ (⟪{{z}}, ⟪w,
t⟫⟫ ∈ y ↔
⟪z, w⟫ ∈
x)) |
23 | 22 | 2albii 1567 |
. . . . . . . 8
⊢ (∀w∀t(⟪{{z}},
⟪w, t⟫⟫ ∈ ((℘11c
×k (V ×k V)) ∩ y) ↔ ⟪{{z}}, ⟪w,
t⟫⟫ ∈ Ins3k x) ↔ ∀w∀t(⟪{{z}},
⟪w, t⟫⟫ ∈ y ↔
⟪z, w⟫ ∈
x)) |
24 | 23 | albii 1566 |
. . . . . . 7
⊢ (∀z∀w∀t(⟪{{z}},
⟪w, t⟫⟫ ∈ ((℘11c
×k (V ×k V)) ∩ y) ↔ ⟪{{z}}, ⟪w,
t⟫⟫ ∈ Ins3k x) ↔ ∀z∀w∀t(⟪{{z}},
⟪w, t⟫⟫ ∈ y ↔
⟪z, w⟫ ∈
x)) |
25 | 6, 24 | bitri 240 |
. . . . . 6
⊢ (((℘11c
×k (V ×k V)) ∩ y) = Ins3k x ↔ ∀z∀w∀t(⟪{{z}},
⟪w, t⟫⟫ ∈ y ↔
⟪z, w⟫ ∈
x)) |
26 | 25 | biimpri 197 |
. . . . 5
⊢ (∀z∀w∀t(⟪{{z}},
⟪w, t⟫⟫ ∈ y ↔
⟪z, w⟫ ∈
x) → ((℘11c
×k (V ×k V)) ∩ y) = Ins3k x) |
27 | | 1cex 4142 |
. . . . . . . 8
⊢
1c ∈
V |
28 | 27 | pw1ex 4303 |
. . . . . . 7
⊢ ℘11c ∈ V |
29 | | vvex 4109 |
. . . . . . . 8
⊢ V ∈ V |
30 | 29, 29 | xpkex 4289 |
. . . . . . 7
⊢ (V
×k V) ∈
V |
31 | 28, 30 | xpkex 4289 |
. . . . . 6
⊢ (℘11c
×k (V ×k V)) ∈ V |
32 | | vex 2862 |
. . . . . 6
⊢ y ∈
V |
33 | 31, 32 | inex 4105 |
. . . . 5
⊢ ((℘11c
×k (V ×k V)) ∩ y) ∈
V |
34 | 26, 33 | syl6eqelr 2442 |
. . . 4
⊢ (∀z∀w∀t(⟪{{z}},
⟪w, t⟫⟫ ∈ y ↔
⟪z, w⟫ ∈
x) → Ins3k x ∈
V) |
35 | 34 | exlimiv 1634 |
. . 3
⊢ (∃y∀z∀w∀t(⟪{{z}},
⟪w, t⟫⟫ ∈ y ↔
⟪z, w⟫ ∈
x) → Ins3k x ∈
V) |
36 | 3, 35 | ax-mp 5 |
. 2
⊢ Ins3k x ∈
V |
37 | 2, 36 | vtoclg 2914 |
1
⊢ (A ∈ V → Ins3k A ∈
V) |