Step | Hyp | Ref
| Expression |
1 | | sneq 3744 |
. . . . . 6
⊢ (y = A →
{y} = {A}) |
2 | 1 | sneqd 3746 |
. . . . 5
⊢ (y = A →
{{y}} = {{A}}) |
3 | 2 | xpkeq2d 4205 |
. . . 4
⊢ (y = A → (V
×k {{y}}) = (V
×k {{A}})) |
4 | 3 | sseq1d 3298 |
. . 3
⊢ (y = A → ((V
×k {{y}}) ⊆ B ↔ (V
×k {{A}}) ⊆ B)) |
5 | | df-p6 4191 |
. . 3
⊢ P6 B = {y ∣ (V
×k {{y}}) ⊆ B} |
6 | 4, 5 | elab2g 2987 |
. 2
⊢ (A ∈ V → (A
∈ P6 B ↔ (V ×k {{A}}) ⊆ B)) |
7 | | xpkssvvk 4210 |
. . . 4
⊢ (V
×k {{A}}) ⊆ (V ×k
V) |
8 | | ssrelk 4211 |
. . . 4
⊢ ((V
×k {{A}}) ⊆ (V ×k V) → ((V
×k {{A}}) ⊆ B ↔
∀x∀y(⟪x,
y⟫ ∈ (V ×k {{A}}) → ⟪x, y⟫
∈ B))) |
9 | 7, 8 | ax-mp 5 |
. . 3
⊢ ((V
×k {{A}}) ⊆ B ↔
∀x∀y(⟪x,
y⟫ ∈ (V ×k {{A}}) → ⟪x, y⟫
∈ B)) |
10 | | vex 2862 |
. . . . . . . . 9
⊢ x ∈
V |
11 | | vex 2862 |
. . . . . . . . 9
⊢ y ∈
V |
12 | 10, 11 | opkelxpk 4248 |
. . . . . . . 8
⊢ (⟪x, y⟫
∈ (V ×k {{A}}) ↔ (x
∈ V ∧
y ∈
{{A}})) |
13 | 10 | biantrur 492 |
. . . . . . . 8
⊢ (y ∈ {{A}} ↔ (x
∈ V ∧
y ∈
{{A}})) |
14 | | df-sn 3741 |
. . . . . . . . 9
⊢ {{A}} = {y ∣ y =
{A}} |
15 | 14 | abeq2i 2460 |
. . . . . . . 8
⊢ (y ∈ {{A}} ↔ y =
{A}) |
16 | 12, 13, 15 | 3bitr2i 264 |
. . . . . . 7
⊢ (⟪x, y⟫
∈ (V ×k {{A}}) ↔ y =
{A}) |
17 | 16 | imbi1i 315 |
. . . . . 6
⊢ ((⟪x, y⟫
∈ (V ×k {{A}}) → ⟪x, y⟫
∈ B)
↔ (y = {A} → ⟪x, y⟫
∈ B)) |
18 | 17 | albii 1566 |
. . . . 5
⊢ (∀y(⟪x,
y⟫ ∈ (V ×k {{A}}) → ⟪x, y⟫
∈ B)
↔ ∀y(y = {A} → ⟪x, y⟫
∈ B)) |
19 | | snex 4111 |
. . . . . 6
⊢ {A} ∈
V |
20 | | opkeq2 4060 |
. . . . . . 7
⊢ (y = {A} →
⟪x, y⟫ = ⟪x, {A}⟫) |
21 | 20 | eleq1d 2419 |
. . . . . 6
⊢ (y = {A} →
(⟪x, y⟫ ∈
B ↔ ⟪x, {A}⟫
∈ B)) |
22 | 19, 21 | ceqsalv 2885 |
. . . . 5
⊢ (∀y(y = {A} →
⟪x, y⟫ ∈
B) ↔ ⟪x, {A}⟫
∈ B) |
23 | 18, 22 | bitri 240 |
. . . 4
⊢ (∀y(⟪x,
y⟫ ∈ (V ×k {{A}}) → ⟪x, y⟫
∈ B)
↔ ⟪x, {A}⟫ ∈
B) |
24 | 23 | albii 1566 |
. . 3
⊢ (∀x∀y(⟪x,
y⟫ ∈ (V ×k {{A}}) → ⟪x, y⟫
∈ B)
↔ ∀x⟪x,
{A}⟫ ∈ B) |
25 | 9, 24 | bitri 240 |
. 2
⊢ ((V
×k {{A}}) ⊆ B ↔
∀x⟪x,
{A}⟫ ∈ B) |
26 | 6, 25 | syl6bb 252 |
1
⊢ (A ∈ V → (A
∈ P6 B ↔ ∀x⟪x,
{A}⟫ ∈ B)) |