Step | Hyp | Ref
| Expression |
1 | | vex 2862 |
. . . . 5
⊢ y ∈
V |
2 | | vex 2862 |
. . . . 5
⊢ z ∈
V |
3 | | opkelins3kg 4252 |
. . . . 5
⊢ ((y ∈ V ∧ z ∈ V) → (⟪y, z⟫
∈ Ins3k A ↔ ∃t∃u∃w(y = {{t}} ∧ z =
⟪u, w⟫ ∧
⟪t, u⟫ ∈
A))) |
4 | 1, 2, 3 | mp2an 653 |
. . . 4
⊢ (⟪y, z⟫
∈ Ins3k A ↔ ∃t∃u∃w(y = {{t}} ∧ z =
⟪u, w⟫ ∧
⟪t, u⟫ ∈
A)) |
5 | | opkeq12 4061 |
. . . . . . . 8
⊢ ((y = {{t}} ∧ z =
⟪u, w⟫) → ⟪y, z⟫ =
⟪{{t}}, ⟪u, w⟫⟫) |
6 | | vex 2862 |
. . . . . . . . . . 11
⊢ t ∈
V |
7 | 6 | snel1c 4140 |
. . . . . . . . . 10
⊢ {t} ∈
1c |
8 | | snelpw1 4146 |
. . . . . . . . . 10
⊢ ({{t}} ∈ ℘11c ↔
{t} ∈
1c) |
9 | 7, 8 | mpbir 200 |
. . . . . . . . 9
⊢ {{t}} ∈ ℘11c |
10 | | vex 2862 |
. . . . . . . . . 10
⊢ u ∈
V |
11 | | vex 2862 |
. . . . . . . . . 10
⊢ w ∈
V |
12 | 10, 11 | opkelxpk 4248 |
. . . . . . . . . 10
⊢ (⟪u, w⟫
∈ (V ×k V) ↔
(u ∈ V
∧ w ∈ V)) |
13 | 10, 11, 12 | mpbir2an 886 |
. . . . . . . . 9
⊢ ⟪u, w⟫
∈ (V ×k
V) |
14 | | snex 4111 |
. . . . . . . . . 10
⊢ {{t}} ∈
V |
15 | | opkex 4113 |
. . . . . . . . . 10
⊢ ⟪u, w⟫
∈ V |
16 | 14, 15 | opkelxpk 4248 |
. . . . . . . . 9
⊢ (⟪{{t}}, ⟪u,
w⟫⟫ ∈ (℘11c
×k (V ×k V)) ↔ ({{t}} ∈ ℘11c ∧ ⟪u,
w⟫ ∈ (V ×k
V))) |
17 | 9, 13, 16 | mpbir2an 886 |
. . . . . . . 8
⊢ ⟪{{t}}, ⟪u,
w⟫⟫ ∈ (℘11c
×k (V ×k V)) |
18 | 5, 17 | syl6eqel 2441 |
. . . . . . 7
⊢ ((y = {{t}} ∧ z =
⟪u, w⟫) → ⟪y, z⟫
∈ (℘11c
×k (V ×k V))) |
19 | 18 | 3adant3 975 |
. . . . . 6
⊢ ((y = {{t}} ∧ z =
⟪u, w⟫ ∧
⟪t, u⟫ ∈
A) → ⟪y, z⟫
∈ (℘11c
×k (V ×k V))) |
20 | 19 | exlimiv 1634 |
. . . . 5
⊢ (∃w(y = {{t}} ∧ z =
⟪u, w⟫ ∧
⟪t, u⟫ ∈
A) → ⟪y, z⟫
∈ (℘11c
×k (V ×k V))) |
21 | 20 | exlimivv 1635 |
. . . 4
⊢ (∃t∃u∃w(y = {{t}} ∧ z =
⟪u, w⟫ ∧
⟪t, u⟫ ∈
A) → ⟪y, z⟫
∈ (℘11c
×k (V ×k V))) |
22 | 4, 21 | sylbi 187 |
. . 3
⊢ (⟪y, z⟫
∈ Ins3k A → ⟪y, z⟫
∈ (℘11c
×k (V ×k V))) |
23 | 22 | gen2 1547 |
. 2
⊢ ∀y∀z(⟪y,
z⟫ ∈ Ins3k A → ⟪y, z⟫
∈ (℘11c
×k (V ×k V))) |
24 | | df-ins3k 4188 |
. . . 4
⊢ Ins3k A = {x ∣ ∃y∃z(x =
⟪y, z⟫ ∧ ∃t∃u∃w(y = {{t}} ∧ z =
⟪u, w⟫ ∧
⟪t, u⟫ ∈
A))} |
25 | 24 | opkabssvvki 4209 |
. . 3
⊢ Ins3k A ⊆ (V
×k V) |
26 | | ssrelk 4211 |
. . 3
⊢ ( Ins3k A ⊆ (V
×k V) → ( Ins3k A ⊆ (℘11c
×k (V ×k V)) ↔ ∀y∀z(⟪y,
z⟫ ∈ Ins3k A → ⟪y, z⟫
∈ (℘11c
×k (V ×k
V))))) |
27 | 25, 26 | ax-mp 5 |
. 2
⊢ ( Ins3k A ⊆ (℘11c
×k (V ×k V)) ↔ ∀y∀z(⟪y,
z⟫ ∈ Ins3k A → ⟪y, z⟫
∈ (℘11c
×k (V ×k V)))) |
28 | 23, 27 | mpbir 200 |
1
⊢ Ins3k A ⊆ (℘11c
×k (V ×k V)) |