Step | Hyp | Ref
| Expression |
1 | | nulnnc 6118 |
. . . . . . 7
⊢ ¬ ∅ ∈ NC |
2 | | eleq1 2413 |
. . . . . . 7
⊢ (A = ∅ →
(A ∈
NC ↔ ∅
∈ NC
)) |
3 | 1, 2 | mtbiri 294 |
. . . . . 6
⊢ (A = ∅ →
¬ A ∈
NC ) |
4 | 3 | necon2ai 2561 |
. . . . 5
⊢ (A ∈ NC → A ≠
∅) |
5 | | n0 3559 |
. . . . 5
⊢ (A ≠ ∅ ↔
∃y
y ∈
A) |
6 | 4, 5 | sylib 188 |
. . . 4
⊢ (A ∈ NC → ∃y y ∈ A) |
7 | | vex 2862 |
. . . . . . . . . 10
⊢ y ∈
V |
8 | 7 | pw1ex 4303 |
. . . . . . . . 9
⊢ ℘1y ∈
V |
9 | 8 | ncelncsi 6121 |
. . . . . . . 8
⊢ Nc ℘1y ∈ NC |
10 | | eqid 2353 |
. . . . . . . 8
⊢ Nc ℘1y = Nc ℘1y |
11 | | eqeq1 2359 |
. . . . . . . . 9
⊢ (x = Nc ℘1y → (x =
Nc ℘1y ↔ Nc ℘1y = Nc ℘1y)) |
12 | 11 | rspcev 2955 |
. . . . . . . 8
⊢ (( Nc ℘1y ∈ NC ∧ Nc ℘1y = Nc ℘1y) → ∃x ∈ NC x = Nc ℘1y) |
13 | 9, 10, 12 | mp2an 653 |
. . . . . . 7
⊢ ∃x ∈ NC x = Nc ℘1y |
14 | 13 | jctr 526 |
. . . . . 6
⊢ (y ∈ A → (y
∈ A ∧ ∃x ∈ NC x = Nc ℘1y)) |
15 | 14 | a1i 10 |
. . . . 5
⊢ (A ∈ NC → (y ∈ A →
(y ∈
A ∧ ∃x ∈ NC x = Nc ℘1y))) |
16 | 15 | eximdv 1622 |
. . . 4
⊢ (A ∈ NC → (∃y y ∈ A →
∃y(y ∈ A ∧ ∃x ∈ NC x = Nc ℘1y))) |
17 | 6, 16 | mpd 14 |
. . 3
⊢ (A ∈ NC → ∃y(y ∈ A ∧ ∃x ∈ NC x = Nc ℘1y)) |
18 | | rexcom 2772 |
. . . 4
⊢ (∃x ∈ NC ∃y ∈ A x = Nc ℘1y ↔ ∃y ∈ A ∃x ∈ NC x = Nc ℘1y) |
19 | | df-rex 2620 |
. . . 4
⊢ (∃y ∈ A ∃x ∈ NC x = Nc ℘1y ↔ ∃y(y ∈ A ∧ ∃x ∈ NC x = Nc ℘1y)) |
20 | 18, 19 | bitri 240 |
. . 3
⊢ (∃x ∈ NC ∃y ∈ A x = Nc ℘1y ↔ ∃y(y ∈ A ∧ ∃x ∈ NC x = Nc ℘1y)) |
21 | 17, 20 | sylibr 203 |
. 2
⊢ (A ∈ NC → ∃x ∈ NC ∃y ∈ A x = Nc ℘1y) |
22 | | reeanv 2778 |
. . . 4
⊢ (∃y ∈ A ∃w ∈ A (x = Nc ℘1y ∧ z = Nc ℘1w) ↔ (∃y ∈ A x = Nc ℘1y ∧ ∃w ∈ A z = Nc ℘1w)) |
23 | | ncseqnc 6128 |
. . . . . . . . . . . 12
⊢ (A ∈ NC → (A = Nc y ↔ y ∈ A)) |
24 | 23 | biimpar 471 |
. . . . . . . . . . 11
⊢ ((A ∈ NC ∧ y ∈ A) → A =
Nc y) |
25 | 24 | adantrr 697 |
. . . . . . . . . 10
⊢ ((A ∈ NC ∧ (y ∈ A ∧ w ∈ A)) → A =
Nc y) |
26 | | ncseqnc 6128 |
. . . . . . . . . . . 12
⊢ (A ∈ NC → (A = Nc w ↔ w ∈ A)) |
27 | 26 | biimpar 471 |
. . . . . . . . . . 11
⊢ ((A ∈ NC ∧ w ∈ A) → A =
Nc w) |
28 | 27 | adantrl 696 |
. . . . . . . . . 10
⊢ ((A ∈ NC ∧ (y ∈ A ∧ w ∈ A)) → A =
Nc w) |
29 | 25, 28 | eqtr3d 2387 |
. . . . . . . . 9
⊢ ((A ∈ NC ∧ (y ∈ A ∧ w ∈ A)) → Nc y = Nc w) |
30 | 7 | ncpw1 6152 |
. . . . . . . . 9
⊢ ( Nc y = Nc w ↔ Nc ℘1y = Nc ℘1w) |
31 | 29, 30 | sylib 188 |
. . . . . . . 8
⊢ ((A ∈ NC ∧ (y ∈ A ∧ w ∈ A)) → Nc ℘1y = Nc ℘1w) |
32 | 31 | 3adant2 974 |
. . . . . . 7
⊢ ((A ∈ NC ∧ (x ∈ NC ∧ z ∈ NC ) ∧ (y ∈ A ∧ w ∈ A)) → Nc ℘1y = Nc ℘1w) |
33 | | eqeq2 2362 |
. . . . . . . . 9
⊢ ( Nc ℘1y = Nc ℘1w → (x =
Nc ℘1y ↔ x =
Nc ℘1w)) |
34 | 33 | anbi1d 685 |
. . . . . . . 8
⊢ ( Nc ℘1y = Nc ℘1w → ((x =
Nc ℘1y ∧ z = Nc ℘1w) ↔ (x =
Nc ℘1w ∧ z = Nc ℘1w))) |
35 | | eqtr3 2372 |
. . . . . . . 8
⊢ ((x = Nc ℘1w ∧ z = Nc ℘1w) → x =
z) |
36 | 34, 35 | syl6bi 219 |
. . . . . . 7
⊢ ( Nc ℘1y = Nc ℘1w → ((x =
Nc ℘1y ∧ z = Nc ℘1w) → x =
z)) |
37 | 32, 36 | syl 15 |
. . . . . 6
⊢ ((A ∈ NC ∧ (x ∈ NC ∧ z ∈ NC ) ∧ (y ∈ A ∧ w ∈ A)) → ((x =
Nc ℘1y ∧ z = Nc ℘1w) → x =
z)) |
38 | 37 | 3expa 1151 |
. . . . 5
⊢ (((A ∈ NC ∧ (x ∈ NC ∧ z ∈ NC )) ∧ (y ∈ A ∧ w ∈ A)) → ((x =
Nc ℘1y ∧ z = Nc ℘1w) → x =
z)) |
39 | 38 | rexlimdvva 2745 |
. . . 4
⊢ ((A ∈ NC ∧ (x ∈ NC ∧ z ∈ NC )) → (∃y ∈ A ∃w ∈ A (x = Nc ℘1y ∧ z = Nc ℘1w) → x =
z)) |
40 | 22, 39 | syl5bir 209 |
. . 3
⊢ ((A ∈ NC ∧ (x ∈ NC ∧ z ∈ NC )) → ((∃y ∈ A x = Nc ℘1y ∧ ∃w ∈ A z = Nc ℘1w) → x =
z)) |
41 | 40 | ralrimivva 2706 |
. 2
⊢ (A ∈ NC → ∀x ∈ NC ∀z ∈ NC ((∃y ∈ A x = Nc ℘1y ∧ ∃w ∈ A z = Nc ℘1w) → x =
z)) |
42 | | eqeq1 2359 |
. . . . 5
⊢ (x = z →
(x = Nc ℘1y ↔ z =
Nc ℘1y)) |
43 | 42 | rexbidv 2635 |
. . . 4
⊢ (x = z →
(∃y
∈ A
x = Nc ℘1y ↔ ∃y ∈ A z = Nc ℘1y)) |
44 | | pw1eq 4143 |
. . . . . . 7
⊢ (y = w →
℘1y = ℘1w) |
45 | 44 | nceqd 6110 |
. . . . . 6
⊢ (y = w →
Nc ℘1y = Nc ℘1w) |
46 | 45 | eqeq2d 2364 |
. . . . 5
⊢ (y = w →
(z = Nc ℘1y ↔ z =
Nc ℘1w)) |
47 | 46 | cbvrexv 2836 |
. . . 4
⊢ (∃y ∈ A z = Nc ℘1y ↔ ∃w ∈ A z = Nc ℘1w) |
48 | 43, 47 | syl6bb 252 |
. . 3
⊢ (x = z →
(∃y
∈ A
x = Nc ℘1y ↔ ∃w ∈ A z = Nc ℘1w)) |
49 | 48 | reu4 3030 |
. 2
⊢ (∃!x ∈ NC ∃y ∈ A x = Nc ℘1y ↔ (∃x ∈ NC ∃y ∈ A x = Nc ℘1y ∧ ∀x ∈ NC ∀z ∈ NC ((∃y ∈ A x = Nc ℘1y ∧ ∃w ∈ A z = Nc ℘1w) → x =
z))) |
50 | 21, 41, 49 | sylanbrc 645 |
1
⊢ (A ∈ NC → ∃!x ∈ NC ∃y ∈ A x = Nc ℘1y) |