Step | Hyp | Ref
| Expression |
1 | | sikexlem.1 |
. . 3
⊢ A ⊆
(1c ×k
1c) |
2 | | sikexlem.2 |
. . 3
⊢ B ⊆
(1c ×k
1c) |
3 | | ssofeq 4077 |
. . 3
⊢ ((A ⊆
(1c ×k 1c) ∧ B ⊆ (1c ×k
1c)) → (A = B ↔ ∀z ∈ (1c ×k
1c)(z ∈ A ↔
z ∈
B))) |
4 | 1, 2, 3 | mp2an 653 |
. 2
⊢ (A = B ↔
∀z
∈ (1c
×k 1c)(z ∈ A ↔ z ∈ B)) |
5 | | df-ral 2619 |
. . 3
⊢ (∀z ∈ (1c ×k
1c)(z ∈ A ↔
z ∈
B) ↔ ∀z(z ∈
(1c ×k 1c) →
(z ∈
A ↔ z ∈ B))) |
6 | | elxpk 4196 |
. . . . . . . 8
⊢ (z ∈
(1c ×k 1c) ↔
∃w∃t(z = ⟪w,
t⟫ ∧ (w ∈ 1c ∧ t ∈ 1c))) |
7 | | el1c 4139 |
. . . . . . . . . . . . . 14
⊢ (w ∈
1c ↔ ∃x w = {x}) |
8 | | el1c 4139 |
. . . . . . . . . . . . . 14
⊢ (t ∈
1c ↔ ∃y t = {y}) |
9 | 7, 8 | anbi12i 678 |
. . . . . . . . . . . . 13
⊢ ((w ∈
1c ∧ t ∈
1c) ↔ (∃x w = {x} ∧ ∃y t = {y})) |
10 | | eeanv 1913 |
. . . . . . . . . . . . 13
⊢ (∃x∃y(w = {x} ∧ t = {y}) ↔ (∃x w = {x} ∧ ∃y t = {y})) |
11 | 9, 10 | bitr4i 243 |
. . . . . . . . . . . 12
⊢ ((w ∈
1c ∧ t ∈
1c) ↔ ∃x∃y(w = {x} ∧ t = {y})) |
12 | 11 | anbi2i 675 |
. . . . . . . . . . 11
⊢ ((z = ⟪w,
t⟫ ∧ (w ∈ 1c ∧ t ∈ 1c)) ↔ (z = ⟪w,
t⟫ ∧ ∃x∃y(w = {x} ∧ t = {y}))) |
13 | | df-3an 936 |
. . . . . . . . . . . . . 14
⊢ ((w = {x} ∧ t = {y} ∧ z = ⟪w,
t⟫) ↔ ((w = {x} ∧ t = {y}) ∧ z = ⟪w,
t⟫)) |
14 | | ancom 437 |
. . . . . . . . . . . . . 14
⊢ (((w = {x} ∧ t = {y}) ∧ z = ⟪w,
t⟫) ↔ (z = ⟪w,
t⟫ ∧ (w = {x} ∧ t = {y}))) |
15 | 13, 14 | bitri 240 |
. . . . . . . . . . . . 13
⊢ ((w = {x} ∧ t = {y} ∧ z = ⟪w,
t⟫) ↔ (z = ⟪w,
t⟫ ∧ (w = {x} ∧ t = {y}))) |
16 | 15 | 2exbii 1583 |
. . . . . . . . . . . 12
⊢ (∃x∃y(w = {x} ∧ t = {y} ∧ z = ⟪w,
t⟫) ↔ ∃x∃y(z = ⟪w,
t⟫ ∧ (w = {x} ∧ t = {y}))) |
17 | | 19.42vv 1907 |
. . . . . . . . . . . 12
⊢ (∃x∃y(z = ⟪w,
t⟫ ∧ (w = {x} ∧ t = {y})) ↔
(z = ⟪w, t⟫
∧ ∃x∃y(w = {x} ∧ t = {y}))) |
18 | 16, 17 | bitri 240 |
. . . . . . . . . . 11
⊢ (∃x∃y(w = {x} ∧ t = {y} ∧ z = ⟪w,
t⟫) ↔ (z = ⟪w,
t⟫ ∧ ∃x∃y(w = {x} ∧ t = {y}))) |
19 | 12, 18 | bitr4i 243 |
. . . . . . . . . 10
⊢ ((z = ⟪w,
t⟫ ∧ (w ∈ 1c ∧ t ∈ 1c)) ↔ ∃x∃y(w = {x} ∧ t = {y} ∧ z = ⟪w,
t⟫)) |
20 | 19 | 2exbii 1583 |
. . . . . . . . 9
⊢ (∃w∃t(z = ⟪w,
t⟫ ∧ (w ∈ 1c ∧ t ∈ 1c)) ↔ ∃w∃t∃x∃y(w = {x} ∧ t = {y} ∧ z = ⟪w,
t⟫)) |
21 | | exrot4 1745 |
. . . . . . . . 9
⊢ (∃x∃y∃w∃t(w = {x} ∧ t = {y} ∧ z = ⟪w,
t⟫) ↔ ∃w∃t∃x∃y(w = {x} ∧ t = {y} ∧ z = ⟪w,
t⟫)) |
22 | 20, 21 | bitr4i 243 |
. . . . . . . 8
⊢ (∃w∃t(z = ⟪w,
t⟫ ∧ (w ∈ 1c ∧ t ∈ 1c)) ↔ ∃x∃y∃w∃t(w = {x} ∧ t = {y} ∧ z = ⟪w,
t⟫)) |
23 | | snex 4111 |
. . . . . . . . . 10
⊢ {x} ∈
V |
24 | | snex 4111 |
. . . . . . . . . 10
⊢ {y} ∈
V |
25 | | opkeq1 4059 |
. . . . . . . . . . 11
⊢ (w = {x} →
⟪w, t⟫ = ⟪{x}, t⟫) |
26 | 25 | eqeq2d 2364 |
. . . . . . . . . 10
⊢ (w = {x} →
(z = ⟪w, t⟫
↔ z = ⟪{x}, t⟫)) |
27 | | opkeq2 4060 |
. . . . . . . . . . 11
⊢ (t = {y} →
⟪{x}, t⟫ = ⟪{x}, {y}⟫) |
28 | 27 | eqeq2d 2364 |
. . . . . . . . . 10
⊢ (t = {y} →
(z = ⟪{x}, t⟫
↔ z = ⟪{x}, {y}⟫)) |
29 | 23, 24, 26, 28 | ceqsex2v 2896 |
. . . . . . . . 9
⊢ (∃w∃t(w = {x} ∧ t = {y} ∧ z = ⟪w,
t⟫) ↔ z = ⟪{x},
{y}⟫) |
30 | 29 | 2exbii 1583 |
. . . . . . . 8
⊢ (∃x∃y∃w∃t(w = {x} ∧ t = {y} ∧ z = ⟪w,
t⟫) ↔ ∃x∃y z = ⟪{x},
{y}⟫) |
31 | 6, 22, 30 | 3bitri 262 |
. . . . . . 7
⊢ (z ∈
(1c ×k 1c) ↔
∃x∃y z = ⟪{x},
{y}⟫) |
32 | 31 | imbi1i 315 |
. . . . . 6
⊢ ((z ∈
(1c ×k 1c) →
(z ∈
A ↔ z ∈ B)) ↔ (∃x∃y z = ⟪{x},
{y}⟫ → (z ∈ A ↔ z ∈ B))) |
33 | | 19.23vv 1892 |
. . . . . 6
⊢ (∀x∀y(z = ⟪{x},
{y}⟫ → (z ∈ A ↔ z ∈ B)) ↔
(∃x∃y z = ⟪{x},
{y}⟫ → (z ∈ A ↔ z ∈ B))) |
34 | 32, 33 | bitr4i 243 |
. . . . 5
⊢ ((z ∈
(1c ×k 1c) →
(z ∈
A ↔ z ∈ B)) ↔ ∀x∀y(z = ⟪{x},
{y}⟫ → (z ∈ A ↔ z ∈ B))) |
35 | 34 | albii 1566 |
. . . 4
⊢ (∀z(z ∈
(1c ×k 1c) →
(z ∈
A ↔ z ∈ B)) ↔ ∀z∀x∀y(z = ⟪{x},
{y}⟫ → (z ∈ A ↔ z ∈ B))) |
36 | | alrot3 1738 |
. . . 4
⊢ (∀z∀x∀y(z = ⟪{x},
{y}⟫ → (z ∈ A ↔ z ∈ B)) ↔
∀x∀y∀z(z = ⟪{x},
{y}⟫ → (z ∈ A ↔ z ∈ B))) |
37 | 35, 36 | bitri 240 |
. . 3
⊢ (∀z(z ∈
(1c ×k 1c) →
(z ∈
A ↔ z ∈ B)) ↔ ∀x∀y∀z(z = ⟪{x},
{y}⟫ → (z ∈ A ↔ z ∈ B))) |
38 | | opkex 4113 |
. . . . 5
⊢ ⟪{x}, {y}⟫
∈ V |
39 | | eleq1 2413 |
. . . . . 6
⊢ (z = ⟪{x},
{y}⟫ → (z ∈ A ↔ ⟪{x}, {y}⟫
∈ A)) |
40 | | eleq1 2413 |
. . . . . 6
⊢ (z = ⟪{x},
{y}⟫ → (z ∈ B ↔ ⟪{x}, {y}⟫
∈ B)) |
41 | 39, 40 | bibi12d 312 |
. . . . 5
⊢ (z = ⟪{x},
{y}⟫ → ((z ∈ A ↔ z ∈ B) ↔
(⟪{x}, {y}⟫ ∈
A ↔ ⟪{x}, {y}⟫
∈ B))) |
42 | 38, 41 | ceqsalv 2885 |
. . . 4
⊢ (∀z(z = ⟪{x},
{y}⟫ → (z ∈ A ↔ z ∈ B)) ↔
(⟪{x}, {y}⟫ ∈
A ↔ ⟪{x}, {y}⟫
∈ B)) |
43 | 42 | 2albii 1567 |
. . 3
⊢ (∀x∀y∀z(z = ⟪{x},
{y}⟫ → (z ∈ A ↔ z ∈ B)) ↔
∀x∀y(⟪{x},
{y}⟫ ∈ A ↔
⟪{x}, {y}⟫ ∈
B)) |
44 | 5, 37, 43 | 3bitri 262 |
. 2
⊢ (∀z ∈ (1c ×k
1c)(z ∈ A ↔
z ∈
B) ↔ ∀x∀y(⟪{x},
{y}⟫ ∈ A ↔
⟪{x}, {y}⟫ ∈
B)) |
45 | 4, 44 | bitri 240 |
1
⊢ (A = B ↔
∀x∀y(⟪{x},
{y}⟫ ∈ A ↔
⟪{x}, {y}⟫ ∈
B)) |