Proof of Theorem pw1eqadj
Step | Hyp | Ref
| Expression |
1 | | unieq 3900 |
. . . . 5
⊢ (℘1C = (A ∪
{B}) → ∪℘1C = ∪(A ∪ {B})) |
2 | | unipw1 4325 |
. . . . 5
⊢ ∪℘1C = C |
3 | | uniun 3910 |
. . . . 5
⊢ ∪(A ∪ {B}) = (∪A ∪ ∪{B}) |
4 | 1, 2, 3 | 3eqtr3g 2408 |
. . . 4
⊢ (℘1C = (A ∪
{B}) → C = (∪A ∪ ∪{B})) |
5 | | pw1eqadj.2 |
. . . . . . 7
⊢ B ∈
V |
6 | 5 | unisn 3907 |
. . . . . 6
⊢ ∪{B} = B |
7 | | pw1ss1c 4158 |
. . . . . . . 8
⊢ ℘1C ⊆
1c |
8 | | ssun2 3427 |
. . . . . . . . . 10
⊢ {B} ⊆ (A ∪ {B}) |
9 | 5 | snid 3760 |
. . . . . . . . . 10
⊢ B ∈ {B} |
10 | 8, 9 | sselii 3270 |
. . . . . . . . 9
⊢ B ∈ (A ∪ {B}) |
11 | | eleq2 2414 |
. . . . . . . . 9
⊢ (℘1C = (A ∪
{B}) → (B ∈ ℘1C ↔ B ∈ (A ∪
{B}))) |
12 | 10, 11 | mpbiri 224 |
. . . . . . . 8
⊢ (℘1C = (A ∪
{B}) → B ∈ ℘1C) |
13 | 7, 12 | sseldi 3271 |
. . . . . . 7
⊢ (℘1C = (A ∪
{B}) → B ∈
1c) |
14 | | el1c 4139 |
. . . . . . . 8
⊢ (B ∈
1c ↔ ∃x B = {x}) |
15 | | vex 2862 |
. . . . . . . . . . . . 13
⊢ x ∈
V |
16 | 15 | unisn 3907 |
. . . . . . . . . . . 12
⊢ ∪{x} = x |
17 | 16 | sneqi 3745 |
. . . . . . . . . . 11
⊢ {∪{x}} = {x} |
18 | 17 | eqcomi 2357 |
. . . . . . . . . 10
⊢ {x} = {∪{x}} |
19 | | id 19 |
. . . . . . . . . 10
⊢ (B = {x} →
B = {x}) |
20 | | unieq 3900 |
. . . . . . . . . . 11
⊢ (B = {x} →
∪B = ∪{x}) |
21 | 20 | sneqd 3746 |
. . . . . . . . . 10
⊢ (B = {x} →
{∪B} = {∪{x}}) |
22 | 18, 19, 21 | 3eqtr4a 2411 |
. . . . . . . . 9
⊢ (B = {x} →
B = {∪B}) |
23 | 22 | exlimiv 1634 |
. . . . . . . 8
⊢ (∃x B = {x} →
B = {∪B}) |
24 | 14, 23 | sylbi 187 |
. . . . . . 7
⊢ (B ∈
1c → B = {∪B}) |
25 | 13, 24 | syl 15 |
. . . . . 6
⊢ (℘1C = (A ∪
{B}) → B = {∪B}) |
26 | 6, 25 | syl5eq 2397 |
. . . . 5
⊢ (℘1C = (A ∪
{B}) → ∪{B} = {∪B}) |
27 | 26 | uneq2d 3418 |
. . . 4
⊢ (℘1C = (A ∪
{B}) → (∪A ∪ ∪{B}) = (∪A ∪ {∪B})) |
28 | 4, 27 | eqtrd 2385 |
. . 3
⊢ (℘1C = (A ∪
{B}) → C = (∪A ∪ {∪B})) |
29 | | ssun1 3426 |
. . . . . 6
⊢ A ⊆ (A ∪ {B}) |
30 | | sseq2 3293 |
. . . . . 6
⊢ (℘1C = (A ∪
{B}) → (A ⊆ ℘1C ↔ A ⊆ (A ∪
{B}))) |
31 | 29, 30 | mpbiri 224 |
. . . . 5
⊢ (℘1C = (A ∪
{B}) → A ⊆ ℘1C) |
32 | 31, 7 | syl6ss 3284 |
. . . 4
⊢ (℘1C = (A ∪
{B}) → A ⊆
1c) |
33 | | eqpw1uni 4330 |
. . . 4
⊢ (A ⊆
1c → A = ℘1∪A) |
34 | 32, 33 | syl 15 |
. . 3
⊢ (℘1C = (A ∪
{B}) → A = ℘1∪A) |
35 | | pw1eqadj.1 |
. . . . 5
⊢ A ∈
V |
36 | 35 | uniex 4317 |
. . . 4
⊢ ∪A ∈ V |
37 | 5 | uniex 4317 |
. . . 4
⊢ ∪B ∈ V |
38 | | sneq 3744 |
. . . . . . 7
⊢ (y = ∪B → {y} =
{∪B}) |
39 | | uneq12 3413 |
. . . . . . 7
⊢ ((x = ∪A ∧ {y} = {∪B}) → (x
∪ {y}) = (∪A ∪ {∪B})) |
40 | 38, 39 | sylan2 460 |
. . . . . 6
⊢ ((x = ∪A ∧ y = ∪B) → (x
∪ {y}) = (∪A ∪ {∪B})) |
41 | 40 | eqeq2d 2364 |
. . . . 5
⊢ ((x = ∪A ∧ y = ∪B) → (C =
(x ∪ {y}) ↔ C =
(∪A ∪ {∪B}))) |
42 | | pw1eq 4143 |
. . . . . . 7
⊢ (x = ∪A → ℘1x = ℘1∪A) |
43 | 42 | eqeq2d 2364 |
. . . . . 6
⊢ (x = ∪A → (A =
℘1x ↔ A =
℘1∪A)) |
44 | 43 | adantr 451 |
. . . . 5
⊢ ((x = ∪A ∧ y = ∪B) → (A =
℘1x ↔ A =
℘1∪A)) |
45 | 38 | eqeq2d 2364 |
. . . . . 6
⊢ (y = ∪B → (B =
{y} ↔ B = {∪B})) |
46 | 45 | adantl 452 |
. . . . 5
⊢ ((x = ∪A ∧ y = ∪B) → (B =
{y} ↔ B = {∪B})) |
47 | 41, 44, 46 | 3anbi123d 1252 |
. . . 4
⊢ ((x = ∪A ∧ y = ∪B) → ((C =
(x ∪ {y}) ∧ A = ℘1x ∧ B = {y}) ↔
(C = (∪A ∪ {∪B}) ∧ A = ℘1∪A ∧ B = {∪B}))) |
48 | 36, 37, 47 | spc2ev 2947 |
. . 3
⊢ ((C = (∪A ∪ {∪B}) ∧ A = ℘1∪A ∧ B = {∪B}) → ∃x∃y(C = (x ∪
{y}) ∧
A = ℘1x ∧ B = {y})) |
49 | 28, 34, 25, 48 | syl3anc 1182 |
. 2
⊢ (℘1C = (A ∪
{B}) → ∃x∃y(C = (x ∪
{y}) ∧
A = ℘1x ∧ B = {y})) |
50 | | pw1un 4163 |
. . . . 5
⊢ ℘1(x ∪ {y}) =
(℘1x ∪ ℘1{y}) |
51 | | vex 2862 |
. . . . . . 7
⊢ y ∈
V |
52 | 51 | pw1sn 4165 |
. . . . . 6
⊢ ℘1{y} = {{y}} |
53 | 52 | uneq2i 3415 |
. . . . 5
⊢ (℘1x ∪ ℘1{y}) = (℘1x ∪ {{y}}) |
54 | 50, 53 | eqtri 2373 |
. . . 4
⊢ ℘1(x ∪ {y}) =
(℘1x ∪ {{y}}) |
55 | | pw1eq 4143 |
. . . . . 6
⊢ (C = (x ∪
{y}) → ℘1C = ℘1(x ∪ {y})) |
56 | | sneq 3744 |
. . . . . . 7
⊢ (B = {y} →
{B} = {{y}}) |
57 | | uneq12 3413 |
. . . . . . 7
⊢ ((A = ℘1x ∧ {B} = {{y}})
→ (A ∪ {B}) = (℘1x ∪ {{y}})) |
58 | 56, 57 | sylan2 460 |
. . . . . 6
⊢ ((A = ℘1x ∧ B = {y}) →
(A ∪ {B}) = (℘1x ∪ {{y}})) |
59 | 55, 58 | eqeqan12d 2368 |
. . . . 5
⊢ ((C = (x ∪
{y}) ∧
(A = ℘1x ∧ B = {y})) →
(℘1C = (A ∪
{B}) ↔ ℘1(x ∪ {y}) =
(℘1x ∪ {{y}}))) |
60 | 59 | 3impb 1147 |
. . . 4
⊢ ((C = (x ∪
{y}) ∧
A = ℘1x ∧ B = {y}) →
(℘1C = (A ∪
{B}) ↔ ℘1(x ∪ {y}) =
(℘1x ∪ {{y}}))) |
61 | 54, 60 | mpbiri 224 |
. . 3
⊢ ((C = (x ∪
{y}) ∧
A = ℘1x ∧ B = {y}) →
℘1C = (A ∪
{B})) |
62 | 61 | exlimivv 1635 |
. 2
⊢ (∃x∃y(C = (x ∪
{y}) ∧
A = ℘1x ∧ B = {y}) →
℘1C = (A ∪
{B})) |
63 | 49, 62 | impbii 180 |
1
⊢ (℘1C = (A ∪
{B}) ↔ ∃x∃y(C = (x ∪
{y}) ∧
A = ℘1x ∧ B = {y})) |