Step | Hyp | Ref
| Expression |
1 | | insklem.1 |
. . 3
⊢ A ⊆ (℘11c
×k (V ×k V)) |
2 | | insklem.2 |
. . 3
⊢ B ⊆ (℘11c
×k (V ×k V)) |
3 | | ssofeq 4077 |
. . 3
⊢ ((A ⊆ (℘11c
×k (V ×k V)) ∧ B ⊆ (℘11c
×k (V ×k V))) → (A = B ↔
∀w
∈ (℘11c
×k (V ×k V))(w ∈ A ↔ w ∈ B))) |
4 | 1, 2, 3 | mp2an 653 |
. 2
⊢ (A = B ↔
∀w
∈ (℘11c
×k (V ×k V))(w ∈ A ↔ w ∈ B)) |
5 | | 19.23v 1891 |
. . . . 5
⊢ (∀x(∃y∃z w = ⟪{{x}}, ⟪y,
z⟫⟫ → (w ∈ A ↔ w ∈ B)) ↔
(∃x∃y∃z w = ⟪{{x}}, ⟪y,
z⟫⟫ → (w ∈ A ↔ w ∈ B))) |
6 | | 19.23vv 1892 |
. . . . . 6
⊢ (∀y∀z(w = ⟪{{x}}, ⟪y,
z⟫⟫ → (w ∈ A ↔ w ∈ B)) ↔
(∃y∃z w = ⟪{{x}}, ⟪y,
z⟫⟫ → (w ∈ A ↔ w ∈ B))) |
7 | 6 | albii 1566 |
. . . . 5
⊢ (∀x∀y∀z(w = ⟪{{x}}, ⟪y,
z⟫⟫ → (w ∈ A ↔ w ∈ B)) ↔
∀x(∃y∃z w =
⟪{{x}}, ⟪y, z⟫⟫ → (w ∈ A ↔ w ∈ B))) |
8 | | 19.42vv 1907 |
. . . . . . . . . 10
⊢ (∃y∃z(t ∈ ℘11c ∧ u =
⟪y, z⟫) ↔ (t ∈ ℘11c ∧ ∃y∃z u =
⟪y, z⟫)) |
9 | 8 | anbi2i 675 |
. . . . . . . . 9
⊢ ((w = ⟪t,
u⟫ ∧ ∃y∃z(t ∈ ℘11c ∧ u =
⟪y, z⟫)) ↔ (w = ⟪t,
u⟫ ∧ (t ∈ ℘11c ∧ ∃y∃z u =
⟪y, z⟫))) |
10 | | 19.42vv 1907 |
. . . . . . . . 9
⊢ (∃y∃z(w = ⟪t,
u⟫ ∧ (t ∈ ℘11c ∧ u =
⟪y, z⟫)) ↔ (w = ⟪t,
u⟫ ∧ ∃y∃z(t ∈ ℘11c ∧ u =
⟪y, z⟫))) |
11 | | elvvk 4207 |
. . . . . . . . . . 11
⊢ (u ∈ (V
×k V) ↔ ∃y∃z u = ⟪y,
z⟫) |
12 | 11 | anbi2i 675 |
. . . . . . . . . 10
⊢ ((t ∈ ℘11c ∧ u ∈ (V ×k V)) ↔
(t ∈
℘11c ∧ ∃y∃z u =
⟪y, z⟫)) |
13 | 12 | anbi2i 675 |
. . . . . . . . 9
⊢ ((w = ⟪t,
u⟫ ∧ (t ∈ ℘11c ∧ u ∈ (V ×k V))) ↔
(w = ⟪t, u⟫
∧ (t ∈ ℘11c ∧ ∃y∃z u =
⟪y, z⟫))) |
14 | 9, 10, 13 | 3bitr4ri 269 |
. . . . . . . 8
⊢ ((w = ⟪t,
u⟫ ∧ (t ∈ ℘11c ∧ u ∈ (V ×k V))) ↔ ∃y∃z(w = ⟪t,
u⟫ ∧ (t ∈ ℘11c ∧ u =
⟪y, z⟫))) |
15 | 14 | 2exbii 1583 |
. . . . . . 7
⊢ (∃t∃u(w = ⟪t,
u⟫ ∧ (t ∈ ℘11c ∧ u ∈ (V ×k V))) ↔ ∃t∃u∃y∃z(w = ⟪t,
u⟫ ∧ (t ∈ ℘11c ∧ u =
⟪y, z⟫))) |
16 | | elxpk 4196 |
. . . . . . 7
⊢ (w ∈ (℘11c
×k (V ×k V)) ↔ ∃t∃u(w = ⟪t,
u⟫ ∧ (t ∈ ℘11c ∧ u ∈ (V ×k
V)))) |
17 | | exrot3 1744 |
. . . . . . . 8
⊢ (∃x∃y∃z w = ⟪{{x}}, ⟪y,
z⟫⟫ ↔ ∃y∃z∃x w = ⟪{{x}}, ⟪y,
z⟫⟫) |
18 | | exancom 1586 |
. . . . . . . . . . . 12
⊢ (∃t(w = ⟪t,
⟪y, z⟫⟫ ∧
t ∈ ℘11c) ↔ ∃t(t ∈ ℘11c ∧ w =
⟪t, ⟪y, z⟫⟫)) |
19 | | elpw11c 4147 |
. . . . . . . . . . . . . . 15
⊢ (t ∈ ℘11c ↔ ∃x t = {{x}}) |
20 | 19 | anbi1i 676 |
. . . . . . . . . . . . . 14
⊢ ((t ∈ ℘11c ∧ w =
⟪t, ⟪y, z⟫⟫) ↔ (∃x t = {{x}} ∧ w =
⟪t, ⟪y, z⟫⟫)) |
21 | | 19.41v 1901 |
. . . . . . . . . . . . . 14
⊢ (∃x(t = {{x}} ∧ w =
⟪t, ⟪y, z⟫⟫) ↔ (∃x t = {{x}} ∧ w =
⟪t, ⟪y, z⟫⟫)) |
22 | 20, 21 | bitr4i 243 |
. . . . . . . . . . . . 13
⊢ ((t ∈ ℘11c ∧ w =
⟪t, ⟪y, z⟫⟫) ↔ ∃x(t = {{x}} ∧ w =
⟪t, ⟪y, z⟫⟫)) |
23 | 22 | exbii 1582 |
. . . . . . . . . . . 12
⊢ (∃t(t ∈ ℘11c ∧ w =
⟪t, ⟪y, z⟫⟫) ↔ ∃t∃x(t = {{x}} ∧ w =
⟪t, ⟪y, z⟫⟫)) |
24 | 18, 23 | bitri 240 |
. . . . . . . . . . 11
⊢ (∃t(w = ⟪t,
⟪y, z⟫⟫ ∧
t ∈ ℘11c) ↔ ∃t∃x(t = {{x}} ∧ w =
⟪t, ⟪y, z⟫⟫)) |
25 | | ancom 437 |
. . . . . . . . . . . . . . 15
⊢ ((t ∈ ℘11c ∧ u =
⟪y, z⟫) ↔ (u = ⟪y,
z⟫ ∧ t ∈ ℘11c)) |
26 | 25 | anbi2i 675 |
. . . . . . . . . . . . . 14
⊢ ((w = ⟪t,
u⟫ ∧ (t ∈ ℘11c ∧ u =
⟪y, z⟫)) ↔ (w = ⟪t,
u⟫ ∧ (u =
⟪y, z⟫ ∧
t ∈ ℘11c))) |
27 | | an12 772 |
. . . . . . . . . . . . . 14
⊢ ((w = ⟪t,
u⟫ ∧ (u =
⟪y, z⟫ ∧
t ∈ ℘11c)) ↔
(u = ⟪y, z⟫
∧ (w =
⟪t, u⟫ ∧
t ∈ ℘11c))) |
28 | 26, 27 | bitri 240 |
. . . . . . . . . . . . 13
⊢ ((w = ⟪t,
u⟫ ∧ (t ∈ ℘11c ∧ u =
⟪y, z⟫)) ↔ (u = ⟪y,
z⟫ ∧ (w =
⟪t, u⟫ ∧
t ∈ ℘11c))) |
29 | 28 | 2exbii 1583 |
. . . . . . . . . . . 12
⊢ (∃t∃u(w = ⟪t,
u⟫ ∧ (t ∈ ℘11c ∧ u =
⟪y, z⟫)) ↔ ∃t∃u(u = ⟪y,
z⟫ ∧ (w =
⟪t, u⟫ ∧
t ∈ ℘11c))) |
30 | | opkex 4113 |
. . . . . . . . . . . . . 14
⊢ ⟪y, z⟫
∈ V |
31 | | opkeq2 4060 |
. . . . . . . . . . . . . . . 16
⊢ (u = ⟪y,
z⟫ → ⟪t, u⟫ =
⟪t, ⟪y, z⟫⟫) |
32 | 31 | eqeq2d 2364 |
. . . . . . . . . . . . . . 15
⊢ (u = ⟪y,
z⟫ → (w = ⟪t,
u⟫ ↔ w = ⟪t,
⟪y, z⟫⟫)) |
33 | 32 | anbi1d 685 |
. . . . . . . . . . . . . 14
⊢ (u = ⟪y,
z⟫ → ((w = ⟪t,
u⟫ ∧ t ∈ ℘11c) ↔
(w = ⟪t, ⟪y,
z⟫⟫ ∧ t ∈ ℘11c))) |
34 | 30, 33 | ceqsexv 2894 |
. . . . . . . . . . . . 13
⊢ (∃u(u = ⟪y,
z⟫ ∧ (w =
⟪t, u⟫ ∧
t ∈ ℘11c)) ↔
(w = ⟪t, ⟪y,
z⟫⟫ ∧ t ∈ ℘11c)) |
35 | 34 | exbii 1582 |
. . . . . . . . . . . 12
⊢ (∃t∃u(u = ⟪y,
z⟫ ∧ (w =
⟪t, u⟫ ∧
t ∈ ℘11c)) ↔ ∃t(w = ⟪t,
⟪y, z⟫⟫ ∧
t ∈ ℘11c)) |
36 | 29, 35 | bitri 240 |
. . . . . . . . . . 11
⊢ (∃t∃u(w = ⟪t,
u⟫ ∧ (t ∈ ℘11c ∧ u =
⟪y, z⟫)) ↔ ∃t(w = ⟪t,
⟪y, z⟫⟫ ∧
t ∈ ℘11c)) |
37 | | snex 4111 |
. . . . . . . . . . . . . 14
⊢ {{x}} ∈
V |
38 | | opkeq1 4059 |
. . . . . . . . . . . . . . 15
⊢ (t = {{x}} →
⟪t, ⟪y, z⟫⟫ = ⟪{{x}}, ⟪y,
z⟫⟫) |
39 | 38 | eqeq2d 2364 |
. . . . . . . . . . . . . 14
⊢ (t = {{x}} →
(w = ⟪t, ⟪y,
z⟫⟫ ↔ w = ⟪{{x}}, ⟪y,
z⟫⟫)) |
40 | 37, 39 | ceqsexv 2894 |
. . . . . . . . . . . . 13
⊢ (∃t(t = {{x}} ∧ w =
⟪t, ⟪y, z⟫⟫) ↔ w = ⟪{{x}}, ⟪y,
z⟫⟫) |
41 | 40 | exbii 1582 |
. . . . . . . . . . . 12
⊢ (∃x∃t(t = {{x}} ∧ w =
⟪t, ⟪y, z⟫⟫) ↔ ∃x w = ⟪{{x}}, ⟪y,
z⟫⟫) |
42 | | excom 1741 |
. . . . . . . . . . . 12
⊢ (∃x∃t(t = {{x}} ∧ w =
⟪t, ⟪y, z⟫⟫) ↔ ∃t∃x(t = {{x}} ∧ w =
⟪t, ⟪y, z⟫⟫)) |
43 | 41, 42 | bitr3i 242 |
. . . . . . . . . . 11
⊢ (∃x w = ⟪{{x}}, ⟪y,
z⟫⟫ ↔ ∃t∃x(t = {{x}} ∧ w =
⟪t, ⟪y, z⟫⟫)) |
44 | 24, 36, 43 | 3bitr4ri 269 |
. . . . . . . . . 10
⊢ (∃x w = ⟪{{x}}, ⟪y,
z⟫⟫ ↔ ∃t∃u(w = ⟪t,
u⟫ ∧ (t ∈ ℘11c ∧ u =
⟪y, z⟫))) |
45 | 44 | 2exbii 1583 |
. . . . . . . . 9
⊢ (∃y∃z∃x w = ⟪{{x}}, ⟪y,
z⟫⟫ ↔ ∃y∃z∃t∃u(w = ⟪t,
u⟫ ∧ (t ∈ ℘11c ∧ u =
⟪y, z⟫))) |
46 | | exrot4 1745 |
. . . . . . . . 9
⊢ (∃y∃z∃t∃u(w = ⟪t,
u⟫ ∧ (t ∈ ℘11c ∧ u =
⟪y, z⟫)) ↔ ∃t∃u∃y∃z(w = ⟪t,
u⟫ ∧ (t ∈ ℘11c ∧ u =
⟪y, z⟫))) |
47 | 45, 46 | bitri 240 |
. . . . . . . 8
⊢ (∃y∃z∃x w = ⟪{{x}}, ⟪y,
z⟫⟫ ↔ ∃t∃u∃y∃z(w = ⟪t,
u⟫ ∧ (t ∈ ℘11c ∧ u =
⟪y, z⟫))) |
48 | 17, 47 | bitri 240 |
. . . . . . 7
⊢ (∃x∃y∃z w = ⟪{{x}}, ⟪y,
z⟫⟫ ↔ ∃t∃u∃y∃z(w = ⟪t,
u⟫ ∧ (t ∈ ℘11c ∧ u =
⟪y, z⟫))) |
49 | 15, 16, 48 | 3bitr4i 268 |
. . . . . 6
⊢ (w ∈ (℘11c
×k (V ×k V)) ↔ ∃x∃y∃z w = ⟪{{x}}, ⟪y,
z⟫⟫) |
50 | 49 | imbi1i 315 |
. . . . 5
⊢ ((w ∈ (℘11c
×k (V ×k V)) → (w ∈ A ↔ w ∈ B)) ↔
(∃x∃y∃z w = ⟪{{x}}, ⟪y,
z⟫⟫ → (w ∈ A ↔ w ∈ B))) |
51 | 5, 7, 50 | 3bitr4ri 269 |
. . . 4
⊢ ((w ∈ (℘11c
×k (V ×k V)) → (w ∈ A ↔ w ∈ B)) ↔
∀x∀y∀z(w = ⟪{{x}}, ⟪y,
z⟫⟫ → (w ∈ A ↔ w ∈ B))) |
52 | 51 | albii 1566 |
. . 3
⊢ (∀w(w ∈ (℘11c
×k (V ×k V)) → (w ∈ A ↔ w ∈ B)) ↔
∀w∀x∀y∀z(w = ⟪{{x}}, ⟪y,
z⟫⟫ → (w ∈ A ↔ w ∈ B))) |
53 | | df-ral 2619 |
. . 3
⊢ (∀w ∈ (℘11c
×k (V ×k V))(w ∈ A ↔ w ∈ B) ↔
∀w(w ∈ (℘11c
×k (V ×k V)) → (w ∈ A ↔ w ∈ B))) |
54 | | alcom 1737 |
. . . 4
⊢ (∀w∀x∀y∀z(w = ⟪{{x}}, ⟪y,
z⟫⟫ → (w ∈ A ↔ w ∈ B)) ↔
∀x∀w∀y∀z(w = ⟪{{x}}, ⟪y,
z⟫⟫ → (w ∈ A ↔ w ∈ B))) |
55 | | alrot3 1738 |
. . . . 5
⊢ (∀w∀y∀z(w = ⟪{{x}}, ⟪y,
z⟫⟫ → (w ∈ A ↔ w ∈ B)) ↔
∀y∀z∀w(w = ⟪{{x}}, ⟪y,
z⟫⟫ → (w ∈ A ↔ w ∈ B))) |
56 | 55 | albii 1566 |
. . . 4
⊢ (∀x∀w∀y∀z(w = ⟪{{x}}, ⟪y,
z⟫⟫ → (w ∈ A ↔ w ∈ B)) ↔
∀x∀y∀z∀w(w = ⟪{{x}}, ⟪y,
z⟫⟫ → (w ∈ A ↔ w ∈ B))) |
57 | | opkex 4113 |
. . . . . . 7
⊢ ⟪{{x}}, ⟪y,
z⟫⟫ ∈ V |
58 | | eleq1 2413 |
. . . . . . . 8
⊢ (w = ⟪{{x}}, ⟪y,
z⟫⟫ → (w ∈ A ↔ ⟪{{x}}, ⟪y,
z⟫⟫ ∈ A)) |
59 | | eleq1 2413 |
. . . . . . . 8
⊢ (w = ⟪{{x}}, ⟪y,
z⟫⟫ → (w ∈ B ↔ ⟪{{x}}, ⟪y,
z⟫⟫ ∈ B)) |
60 | 58, 59 | bibi12d 312 |
. . . . . . 7
⊢ (w = ⟪{{x}}, ⟪y,
z⟫⟫ → ((w ∈ A ↔ w ∈ B) ↔
(⟪{{x}}, ⟪y, z⟫⟫ ∈ A ↔
⟪{{x}}, ⟪y, z⟫⟫ ∈ B))) |
61 | 57, 60 | ceqsalv 2885 |
. . . . . 6
⊢ (∀w(w = ⟪{{x}}, ⟪y,
z⟫⟫ → (w ∈ A ↔ w ∈ B)) ↔
(⟪{{x}}, ⟪y, z⟫⟫ ∈ A ↔
⟪{{x}}, ⟪y, z⟫⟫ ∈ B)) |
62 | 61 | albii 1566 |
. . . . 5
⊢ (∀z∀w(w = ⟪{{x}}, ⟪y,
z⟫⟫ → (w ∈ A ↔ w ∈ B)) ↔
∀z(⟪{{x}},
⟪y, z⟫⟫ ∈ A ↔
⟪{{x}}, ⟪y, z⟫⟫ ∈ B)) |
63 | 62 | 2albii 1567 |
. . . 4
⊢ (∀x∀y∀z∀w(w = ⟪{{x}}, ⟪y,
z⟫⟫ → (w ∈ A ↔ w ∈ B)) ↔
∀x∀y∀z(⟪{{x}},
⟪y, z⟫⟫ ∈ A ↔
⟪{{x}}, ⟪y, z⟫⟫ ∈ B)) |
64 | 54, 56, 63 | 3bitrri 263 |
. . 3
⊢ (∀x∀y∀z(⟪{{x}},
⟪y, z⟫⟫ ∈ A ↔
⟪{{x}}, ⟪y, z⟫⟫ ∈ B) ↔
∀w∀x∀y∀z(w = ⟪{{x}}, ⟪y,
z⟫⟫ → (w ∈ A ↔ w ∈ B))) |
65 | 52, 53, 64 | 3bitr4i 268 |
. 2
⊢ (∀w ∈ (℘11c
×k (V ×k V))(w ∈ A ↔ w ∈ B) ↔
∀x∀y∀z(⟪{{x}},
⟪y, z⟫⟫ ∈ A ↔
⟪{{x}}, ⟪y, z⟫⟫ ∈ B)) |
66 | 4, 65 | bitri 240 |
1
⊢ (A = B ↔
∀x∀y∀z(⟪{{x}},
⟪y, z⟫⟫ ∈ A ↔
⟪{{x}}, ⟪y, z⟫⟫ ∈ B)) |