Step | Hyp | Ref
| Expression |
1 | | nchoicelem5 6293 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) NC ![(](lp.gif) ↑c
0c
NC
Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
2 | | incom 3448 |
. . . . . . . . . . 11
![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif) Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![)](rp.gif) |
3 | 2 | eqeq1i 2360 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif) Spac ![`](backtick.gif) 2c
↑c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif)
![(](lp.gif) Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif)
![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
![(/)](varnothing.gif) ![)](rp.gif) |
4 | | disjsn 3786 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif)
Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
5 | 3, 4 | bitri 240 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif) Spac ![`](backtick.gif) 2c
↑c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif)
Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
6 | 1, 5 | sylibr 203 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) NC ![(](lp.gif) ↑c
0c
NC ![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif) Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
7 | | snex 4111 |
. . . . . . . . 9
![{](lbrace.gif) ![M](_cm.gif)
![_V](rmcv.gif) |
8 | | fvex 5339 |
. . . . . . . . 9
Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif)
![_V](rmcv.gif) |
9 | 7, 8 | ncdisjun 6136 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif) Spac ![`](backtick.gif) 2c
↑c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif)
Nc ![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif)
Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) Nc ![{](lbrace.gif) ![M](_cm.gif) Nc Spac ![`](backtick.gif) 2c
↑c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
10 | 6, 9 | syl 15 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) NC ![(](lp.gif) ↑c
0c
NC Nc ![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif)
Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) Nc ![{](lbrace.gif) ![M](_cm.gif) Nc Spac ![`](backtick.gif) 2c
↑c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
11 | | df1c3g 6141 |
. . . . . . . . . . 11
![(](lp.gif) NC 1c Nc ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![)](rp.gif) |
12 | 11 | adantr 451 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) NC ![(](lp.gif) ↑c
0c
NC
1c
Nc ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![)](rp.gif) |
13 | 12 | addceq2d 4390 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) NC ![(](lp.gif) ↑c
0c
NC Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif)
1c
Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif)
Nc ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
14 | | addccom 4406 |
. . . . . . . . 9
Nc ![{](lbrace.gif) ![M](_cm.gif) Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif)
Nc ![{](lbrace.gif) ![M](_cm.gif) ![}](rbrace.gif) ![)](rp.gif) |
15 | 13, 14 | syl6reqr 2404 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) NC ![(](lp.gif) ↑c
0c
NC Nc ![{](lbrace.gif) ![M](_cm.gif) Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif)
1c![)](rp.gif) ![)](rp.gif) |
16 | | 2nnc 6167 |
. . . . . . . . . . 11
2c
Nn |
17 | | ceclnn1 6189 |
. . . . . . . . . . 11
![(](lp.gif) 2c Nn NC ![(](lp.gif)
↑c 0c NC 2c ↑c ![M](_cm.gif)
NC ![)](rp.gif) |
18 | 16, 17 | mp3an1 1264 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) NC ![(](lp.gif) ↑c
0c
NC 2c
↑c ![M](_cm.gif) NC ![)](rp.gif) |
19 | | nchoicelem13 6301 |
. . . . . . . . . 10
![(](lp.gif) 2c ↑c
![M](_cm.gif) NC 1c c Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
20 | | 1cnc 6139 |
. . . . . . . . . . . 12
1c
NC |
21 | 8 | ncelncsi 6121 |
. . . . . . . . . . . 12
Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) NC |
22 | | dflec2 6210 |
. . . . . . . . . . . 12
![(](lp.gif) 1c NC Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) NC 1c c Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) ![E.](exists.gif) NC Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) 1c ![k](_k.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
23 | 20, 21, 22 | mp2an 653 |
. . . . . . . . . . 11
1c c Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) ![E.](exists.gif) NC Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) 1c ![k](_k.gif) ![)](rp.gif) ![)](rp.gif) |
24 | | addccom 4406 |
. . . . . . . . . . . . . 14
1c ![k](_k.gif)
![(](lp.gif) 1c![)](rp.gif) |
25 | | 0cnsuc 4401 |
. . . . . . . . . . . . . 14
![(](lp.gif) 1c 0c |
26 | 24, 25 | eqnetri 2533 |
. . . . . . . . . . . . 13
1c ![k](_k.gif) 0c |
27 | | neeq1 2524 |
. . . . . . . . . . . . 13
Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) 1c ![k](_k.gif) Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif)
0c 1c ![k](_k.gif) 0c![)](rp.gif) ![)](rp.gif) |
28 | 26, 27 | mpbiri 224 |
. . . . . . . . . . . 12
Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) 1c ![k](_k.gif) Nc Spac ![`](backtick.gif) 2c
↑c ![M](_cm.gif) ![)](rp.gif) 0c![)](rp.gif) |
29 | 28 | rexlimivw 2734 |
. . . . . . . . . . 11
![(](lp.gif) ![E.](exists.gif)
NC Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif)
1c ![k](_k.gif)
Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif)
0c![)](rp.gif) |
30 | 23, 29 | sylbi 187 |
. . . . . . . . . 10
1c c Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif)
0c![)](rp.gif) |
31 | 18, 19, 30 | 3syl 18 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) NC ![(](lp.gif) ↑c
0c
NC Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif)
0c![)](rp.gif) |
32 | | 0cnc 6138 |
. . . . . . . . . . 11
0c
NC |
33 | | peano4nc 6150 |
. . . . . . . . . . 11
![(](lp.gif) Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif)
NC 0c NC ![(](lp.gif) Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif)
1c
0c 1c Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif)
0c![)](rp.gif) ![)](rp.gif) |
34 | 21, 32, 33 | mp2an 653 |
. . . . . . . . . 10
![(](lp.gif) Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif)
1c
0c 1c Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif)
0c![)](rp.gif) |
35 | 34 | necon3bii 2548 |
. . . . . . . . 9
![(](lp.gif) Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif)
1c
0c 1c Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif)
0c![)](rp.gif) |
36 | 31, 35 | sylibr 203 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) NC ![(](lp.gif) ↑c
0c
NC Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif)
1c
0c 1c![)](rp.gif) ![)](rp.gif) |
37 | 15, 36 | eqnetrd 2534 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) NC ![(](lp.gif) ↑c
0c
NC Nc ![{](lbrace.gif) ![M](_cm.gif) Nc Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) 0c 1c![)](rp.gif) ![)](rp.gif) |
38 | 10, 37 | eqnetrd 2534 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) NC ![(](lp.gif) ↑c
0c
NC Nc ![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif)
Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) 0c 1c![)](rp.gif) ![)](rp.gif) |
39 | | addcid2 4407 |
. . . . . . . 8
0c
1c
1c |
40 | 39 | neeq2i 2527 |
. . . . . . 7
Nc ![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif)
Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) 0c 1c Nc ![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif) Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) 1c![)](rp.gif) |
41 | | df-ne 2518 |
. . . . . . 7
Nc ![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif)
Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) 1c
Nc ![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif)
Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) 1c![)](rp.gif) |
42 | 40, 41 | bitri 240 |
. . . . . 6
Nc ![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif)
Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) 0c 1c Nc ![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif) Spac ![`](backtick.gif) 2c
↑c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) 1c![)](rp.gif) |
43 | 38, 42 | sylib 188 |
. . . . 5
![(](lp.gif) ![(](lp.gif) NC ![(](lp.gif) ↑c
0c
NC Nc ![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif)
Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) 1c![)](rp.gif) |
44 | | nchoicelem6 6294 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) NC ![(](lp.gif) ↑c
0c
NC Spac ![`](backtick.gif) ![M](_cm.gif) ![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif) Spac ![`](backtick.gif) 2c
↑c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
45 | 44 | nceqd 6110 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) NC ![(](lp.gif) ↑c
0c
NC Nc Spac ![`](backtick.gif) ![M](_cm.gif)
Nc ![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif)
Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
46 | 45 | eqeq1d 2361 |
. . . . 5
![(](lp.gif) ![(](lp.gif) NC ![(](lp.gif) ↑c
0c
NC Nc Spac ![`](backtick.gif) ![M](_cm.gif)
1c
Nc ![(](lp.gif) ![{](lbrace.gif) ![M](_cm.gif)
Spac ![`](backtick.gif) 2c ↑c ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) 1c![)](rp.gif) ![)](rp.gif) |
47 | 43, 46 | mtbird 292 |
. . . 4
![(](lp.gif) ![(](lp.gif) NC ![(](lp.gif) ↑c
0c
NC Nc Spac ![`](backtick.gif) ![M](_cm.gif)
1c![)](rp.gif) |
48 | 47 | ex 423 |
. . 3
![(](lp.gif) NC ![(](lp.gif) ![(](lp.gif) ↑c
0c
NC Nc Spac ![`](backtick.gif) ![M](_cm.gif)
1c![)](rp.gif) ![)](rp.gif) |
49 | 48 | con2d 107 |
. 2
![(](lp.gif) NC Nc Spac ![`](backtick.gif) ![M](_cm.gif)
1c ![(](lp.gif) ↑c
0c
NC ![)](rp.gif) ![)](rp.gif) |
50 | 49 | imp 418 |
1
![(](lp.gif) ![(](lp.gif) NC Nc Spac ![`](backtick.gif) ![M](_cm.gif)
1c
![(](lp.gif) ↑c 0c NC ![)](rp.gif) |