Step | Hyp | Ref
| Expression |
1 | | complab 3524 |
. . . . . . 7
∼ ![{](lbrace.gif)
![(/)](varnothing.gif) ![{](lbrace.gif)
![(/)](varnothing.gif) ![}](rbrace.gif) |
2 | | df-sn 3741 |
. . . . . . . 8
![{](lbrace.gif) ![(/)](varnothing.gif) ![{](lbrace.gif)
![(/)](varnothing.gif) ![}](rbrace.gif) |
3 | 2 | compleqi 3244 |
. . . . . . 7
∼ ![{](lbrace.gif) ![(/)](varnothing.gif) ∼ ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) |
4 | | df-ne 2518 |
. . . . . . . 8
![(](lp.gif)
![(/)](varnothing.gif) ![)](rp.gif) |
5 | 4 | abbii 2465 |
. . . . . . 7
![{](lbrace.gif)
![(/)](varnothing.gif) ![{](lbrace.gif)
![(/)](varnothing.gif) ![}](rbrace.gif) |
6 | 1, 3, 5 | 3eqtr4ri 2384 |
. . . . . 6
![{](lbrace.gif)
![(/)](varnothing.gif) ∼ ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) |
7 | | snex 4111 |
. . . . . . 7
![{](lbrace.gif) ![(/)](varnothing.gif) ![_V](rmcv.gif) |
8 | 7 | complex 4104 |
. . . . . 6
∼ ![{](lbrace.gif) ![(/)](varnothing.gif) ![_V](rmcv.gif) |
9 | 6, 8 | eqeltri 2423 |
. . . . 5
![{](lbrace.gif)
![(/)](varnothing.gif) ![_V](rmcv.gif) |
10 | | neeq1 2524 |
. . . . 5
![(](lp.gif) 0c ![(](lp.gif)
0c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
11 | | neeq1 2524 |
. . . . 5
![(](lp.gif) ![(](lp.gif)
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
12 | | neeq1 2524 |
. . . . 5
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
13 | | neeq1 2524 |
. . . . 5
![(](lp.gif) ![(](lp.gif)
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
14 | | nulel0c 4422 |
. . . . . 6
0c |
15 | | ne0i 3556 |
. . . . . 6
![(](lp.gif) 0c 0c ![(/)](varnothing.gif) ![)](rp.gif) |
16 | 14, 15 | ax-mp 5 |
. . . . 5
0c ![(/)](varnothing.gif) |
17 | | n0 3559 |
. . . . . 6
![(](lp.gif)
![E.](exists.gif)
![m](_m.gif) ![)](rp.gif) |
18 | | vinf 4555 |
. . . . . . . . . . . . . . 15
Fin |
19 | | elunii 3896 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif)
Nn Nn ![)](rp.gif) |
20 | 19 | ancoms 439 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) Nn ![m](_m.gif) Nn ![)](rp.gif) |
21 | | df-fin 4380 |
. . . . . . . . . . . . . . . . 17
Fin Nn |
22 | 20, 21 | syl6eleqr 2444 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) Nn ![m](_m.gif) Fin ![)](rp.gif) |
23 | 22 | ex 423 |
. . . . . . . . . . . . . . 15
![(](lp.gif) Nn ![(](lp.gif) Fin ![)](rp.gif) ![)](rp.gif) |
24 | 18, 23 | mtoi 169 |
. . . . . . . . . . . . . 14
![(](lp.gif) Nn ![m](_m.gif) ![)](rp.gif) |
25 | | eleq1 2413 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif)
![m](_m.gif) ![)](rp.gif) ![)](rp.gif) |
26 | 25 | notbid 285 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif)
![m](_m.gif) ![)](rp.gif) ![)](rp.gif) |
27 | 24, 26 | syl5ibrcom 213 |
. . . . . . . . . . . . 13
![(](lp.gif) Nn ![(](lp.gif) ![m](_m.gif) ![)](rp.gif) ![)](rp.gif) |
28 | 27 | necon2ad 2564 |
. . . . . . . . . . . 12
![(](lp.gif) Nn ![(](lp.gif) ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) |
29 | 28 | imp 418 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) Nn ![m](_m.gif) ![_V](rmcv.gif) ![)](rp.gif) |
30 | | compleqb 3543 |
. . . . . . . . . . . 12
![(](lp.gif) ∼
∼ ![_V](rmcv.gif) ![)](rp.gif) |
31 | 30 | necon3bii 2548 |
. . . . . . . . . . 11
![(](lp.gif) ∼
∼ ![_V](rmcv.gif) ![)](rp.gif) |
32 | 29, 31 | sylib 188 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) Nn ![m](_m.gif) ∼ ∼ ![_V](rmcv.gif) ![)](rp.gif) |
33 | | complV 4070 |
. . . . . . . . . . 11
∼ ![(/)](varnothing.gif) |
34 | 33 | neeq2i 2527 |
. . . . . . . . . 10
∼ ∼ ∼ ![(/)](varnothing.gif) ![)](rp.gif) |
35 | 32, 34 | sylib 188 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Nn ![m](_m.gif) ∼ ![(/)](varnothing.gif) ![)](rp.gif) |
36 | | n0 3559 |
. . . . . . . . . 10
∼ ![E.](exists.gif) ∼ ![a](_a.gif) ![)](rp.gif) |
37 | | vex 2862 |
. . . . . . . . . . . . . . 15
![_V](rmcv.gif) |
38 | 37 | elcompl 3225 |
. . . . . . . . . . . . . 14
![(](lp.gif) ∼ ![a](_a.gif) ![)](rp.gif) |
39 | 37 | elsuci 4414 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif)
![a](_a.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) |
40 | | ne0i 3556 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c ![(](lp.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) |
41 | 39, 40 | syl 15 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif)
![a](_a.gif) ![(](lp.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) |
42 | 38, 41 | sylan2b 461 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif)
∼ ![a](_a.gif) ![(](lp.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) |
43 | 42 | ex 423 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif)
∼ ![(](lp.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
44 | 43 | adantl 452 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) Nn ![m](_m.gif) ![(](lp.gif) ∼ ![(](lp.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
45 | 44 | exlimdv 1636 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) Nn ![m](_m.gif) ![(](lp.gif) ![E.](exists.gif)
∼ ![(](lp.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
46 | 36, 45 | syl5bi 208 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Nn ![m](_m.gif) ∼ ![(](lp.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
47 | 35, 46 | mpd 14 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Nn ![m](_m.gif) ![(](lp.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) |
48 | 47 | ex 423 |
. . . . . . 7
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
49 | 48 | exlimdv 1636 |
. . . . . 6
![(](lp.gif) Nn ![(](lp.gif) ![E.](exists.gif) ![(](lp.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
50 | 17, 49 | syl5bi 208 |
. . . . 5
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
51 | 9, 10, 11, 12, 13, 16, 50 | finds 4411 |
. . . 4
![(](lp.gif) Nn ![(/)](varnothing.gif) ![)](rp.gif) |
52 | 51 | neneqd 2532 |
. . 3
![(](lp.gif) Nn ![(/)](varnothing.gif) ![)](rp.gif) |
53 | 52 | nrex 2716 |
. 2
![E.](exists.gif)
Nn ![(/)](varnothing.gif) |
54 | | risset 2661 |
. 2
![(](lp.gif) Nn ![E.](exists.gif) Nn ![(/)](varnothing.gif) ![)](rp.gif) |
55 | 53, 54 | mtbir 290 |
1
Nn |