Step | Hyp | Ref
| Expression |
1 | | df-sik 4192 |
. . . . 5
⊢ SIk A = {t ∣ ∃z∃w(t =
⟪z, w⟫ ∧ ∃a∃b(z = {a} ∧ w = {b} ∧
⟪a, b⟫ ∈
A))} |
2 | | eqeq1 2359 |
. . . . . . 7
⊢ (z = x →
(z = {a} ↔ x =
{a})) |
3 | 2 | 3anbi1d 1256 |
. . . . . 6
⊢ (z = x →
((z = {a} ∧ w = {b} ∧ ⟪a,
b⟫ ∈ A) ↔
(x = {a} ∧ w = {b} ∧ ⟪a,
b⟫ ∈ A))) |
4 | 3 | 2exbidv 1628 |
. . . . 5
⊢ (z = x →
(∃a∃b(z = {a} ∧ w = {b} ∧
⟪a, b⟫ ∈
A) ↔ ∃a∃b(x = {a} ∧ w = {b} ∧
⟪a, b⟫ ∈
A))) |
5 | | eqeq1 2359 |
. . . . . . 7
⊢ (w = y →
(w = {b} ↔ y =
{b})) |
6 | 5 | 3anbi2d 1257 |
. . . . . 6
⊢ (w = y →
((x = {a} ∧ w = {b} ∧ ⟪a,
b⟫ ∈ A) ↔
(x = {a} ∧ y = {b} ∧ ⟪a,
b⟫ ∈ A))) |
7 | 6 | 2exbidv 1628 |
. . . . 5
⊢ (w = y →
(∃a∃b(x = {a} ∧ w = {b} ∧
⟪a, b⟫ ∈
A) ↔ ∃a∃b(x = {a} ∧ y = {b} ∧
⟪a, b⟫ ∈
A))) |
8 | | vex 2862 |
. . . . 5
⊢ x ∈
V |
9 | | vex 2862 |
. . . . 5
⊢ y ∈
V |
10 | 1, 4, 7, 8, 9 | opkelopkab 4246 |
. . . 4
⊢ (⟪x, y⟫
∈ SIk A ↔ ∃a∃b(x = {a} ∧ y = {b} ∧
⟪a, b⟫ ∈
A)) |
11 | | opkeq12 4061 |
. . . . . . 7
⊢ ((x = {a} ∧ y = {b}) → ⟪x, y⟫ =
⟪{a}, {b}⟫) |
12 | | vex 2862 |
. . . . . . . . 9
⊢ a ∈
V |
13 | 12 | snel1c 4140 |
. . . . . . . 8
⊢ {a} ∈
1c |
14 | | vex 2862 |
. . . . . . . . 9
⊢ b ∈
V |
15 | 14 | snel1c 4140 |
. . . . . . . 8
⊢ {b} ∈
1c |
16 | | opkelxpkg 4247 |
. . . . . . . . 9
⊢ (({a} ∈
1c ∧ {b} ∈
1c) → (⟪{a},
{b}⟫ ∈ (1c ×k
1c) ↔ ({a} ∈ 1c ∧ {b} ∈ 1c))) |
17 | 13, 15, 16 | mp2an 653 |
. . . . . . . 8
⊢ (⟪{a}, {b}⟫
∈ (1c
×k 1c) ↔ ({a} ∈
1c ∧ {b} ∈
1c)) |
18 | 13, 15, 17 | mpbir2an 886 |
. . . . . . 7
⊢ ⟪{a}, {b}⟫
∈ (1c
×k 1c) |
19 | 11, 18 | syl6eqel 2441 |
. . . . . 6
⊢ ((x = {a} ∧ y = {b}) → ⟪x, y⟫
∈ (1c
×k 1c)) |
20 | 19 | 3adant3 975 |
. . . . 5
⊢ ((x = {a} ∧ y = {b} ∧
⟪a, b⟫ ∈
A) → ⟪x, y⟫
∈ (1c
×k 1c)) |
21 | 20 | exlimivv 1635 |
. . . 4
⊢ (∃a∃b(x = {a} ∧ y = {b} ∧
⟪a, b⟫ ∈
A) → ⟪x, y⟫
∈ (1c
×k 1c)) |
22 | 10, 21 | sylbi 187 |
. . 3
⊢ (⟪x, y⟫
∈ SIk A → ⟪x, y⟫
∈ (1c
×k 1c)) |
23 | 22 | gen2 1547 |
. 2
⊢ ∀x∀y(⟪x,
y⟫ ∈ SIk A → ⟪x, y⟫
∈ (1c
×k 1c)) |
24 | | sikssvvk 4266 |
. . 3
⊢ SIk A ⊆ (V
×k V) |
25 | | ssrelk 4211 |
. . 3
⊢ ( SIk A ⊆ (V
×k V) → ( SIk A ⊆
(1c ×k 1c) ↔
∀x∀y(⟪x,
y⟫ ∈ SIk A → ⟪x, y⟫
∈ (1c
×k 1c)))) |
26 | 24, 25 | ax-mp 5 |
. 2
⊢ ( SIk A ⊆
(1c ×k 1c) ↔
∀x∀y(⟪x,
y⟫ ∈ SIk A → ⟪x, y⟫
∈ (1c
×k 1c))) |
27 | 23, 26 | mpbir 200 |
1
⊢ SIk A ⊆
(1c ×k
1c) |