Step | Hyp | Ref
| Expression |
1 | | vex 2862 |
. . . . . 6
![_V](rmcv.gif) |
2 | 1 | elcompl 3225 |
. . . . 5
![(](lp.gif) ∼ ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) !["](backquote.gif) ![(](lp.gif) FullFun
↑c !["](backquote.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) !["](backquote.gif) ![(](lp.gif) FullFun ↑c !["](backquote.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
3 | | brres 4949 |
. . . . . . . . . 10
![(](lp.gif) ![t](_t.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif)
![(](lp.gif) ![t](_t.gif) ![1st](_1st.gif)
![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
4 | | eliniseg 5020 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 0c![}](rbrace.gif) ![t](_t.gif) 0c![)](rp.gif) |
5 | 4 | anbi2i 675 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![1st](_1st.gif)
![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 0c![}](rbrace.gif) ![)](rp.gif) ![(](lp.gif) ![t](_t.gif) ![1st](_1st.gif)
![t](_t.gif) 0c![)](rp.gif) ![)](rp.gif) |
6 | | 0cex 4392 |
. . . . . . . . . . 11
0c
![_V](rmcv.gif) |
7 | 1, 6 | op1st2nd 5790 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![t](_t.gif) ![1st](_1st.gif) ![t](_t.gif) 0c ![<.](langle.gif) ![m](_m.gif)
0c![>.](rangle.gif) ![)](rp.gif) |
8 | 3, 5, 7 | 3bitri 262 |
. . . . . . . . 9
![(](lp.gif) ![t](_t.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif)
![<.](langle.gif) ![m](_m.gif)
0c![>.](rangle.gif) ![)](rp.gif) |
9 | 8 | rexbii 2639 |
. . . . . . . 8
![(](lp.gif) ![E.](exists.gif)
![(](lp.gif) FullFun
↑c !["](backquote.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![t](_t.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif)
![E.](exists.gif) ![(](lp.gif) FullFun ↑c !["](backquote.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![<.](langle.gif) ![m](_m.gif)
0c![>.](rangle.gif) ![)](rp.gif) |
10 | | elima 4754 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) !["](backquote.gif) ![(](lp.gif) FullFun
↑c !["](backquote.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![E.](exists.gif) ![(](lp.gif) FullFun ↑c !["](backquote.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![t](_t.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![m](_m.gif) ![)](rp.gif) |
11 | | risset 2661 |
. . . . . . . 8
![(](lp.gif) ![<.](langle.gif) ![m](_m.gif)
0c ![(](lp.gif) FullFun
↑c !["](backquote.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![E.](exists.gif)
![(](lp.gif) FullFun
↑c !["](backquote.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif)
![<.](langle.gif) ![m](_m.gif) 0c![>.](rangle.gif) ![)](rp.gif) |
12 | 9, 10, 11 | 3bitr4i 268 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) !["](backquote.gif) ![(](lp.gif) FullFun
↑c !["](backquote.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![<.](langle.gif) ![m](_m.gif)
0c ![(](lp.gif) FullFun
↑c !["](backquote.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
13 | | eliniseg 5020 |
. . . . . . 7
![(](lp.gif) ![<.](langle.gif) ![m](_m.gif)
0c ![(](lp.gif) FullFun
↑c !["](backquote.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![<.](langle.gif) ![m](_m.gif)
0c FullFun ↑c ![(/)](varnothing.gif) ![)](rp.gif) |
14 | 1, 6 | brfullfunop 5867 |
. . . . . . 7
![(](lp.gif) ![<.](langle.gif) ![m](_m.gif)
0c FullFun ↑c ![(](lp.gif) ↑c
0c
![(/)](varnothing.gif) ![)](rp.gif) |
15 | 12, 13, 14 | 3bitri 262 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) !["](backquote.gif) ![(](lp.gif) FullFun
↑c !["](backquote.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![(](lp.gif)
↑c 0c ![(/)](varnothing.gif) ![)](rp.gif) |
16 | 15 | necon3bbii 2547 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) !["](backquote.gif) ![(](lp.gif) FullFun ↑c !["](backquote.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![(](lp.gif) ↑c
0c
![(/)](varnothing.gif) ![)](rp.gif) |
17 | 2, 16 | bitri 240 |
. . . 4
![(](lp.gif) ∼ ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) !["](backquote.gif) ![(](lp.gif) FullFun
↑c !["](backquote.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![(](lp.gif)
↑c 0c ![(/)](varnothing.gif) ![)](rp.gif) |
18 | 17 | abbi2i 2464 |
. . 3
∼ ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) !["](backquote.gif) ![(](lp.gif) FullFun ↑c !["](backquote.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![{](lbrace.gif)
![(](lp.gif) ↑c
0c
![(/)](varnothing.gif) ![}](rbrace.gif) |
19 | | 1stex 4739 |
. . . . . 6
![_V](rmcv.gif) |
20 | | 2ndex 5112 |
. . . . . . . 8
![_V](rmcv.gif) |
21 | 20 | cnvex 5102 |
. . . . . . 7
![`'](_cnv.gif) ![_V](rmcv.gif) |
22 | | snex 4111 |
. . . . . . 7
0c ![_V](rmcv.gif) |
23 | 21, 22 | imaex 4747 |
. . . . . 6
![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 0c![}](rbrace.gif) ![_V](rmcv.gif) |
24 | 19, 23 | resex 5117 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 0c![}](rbrace.gif) ![)](rp.gif)
![_V](rmcv.gif) |
25 | | ceex 6174 |
. . . . . . . 8
↑c ![_V](rmcv.gif) |
26 | 25 | fullfunex 5860 |
. . . . . . 7
FullFun ↑c ![_V](rmcv.gif) |
27 | 26 | cnvex 5102 |
. . . . . 6
FullFun ↑c ![_V](rmcv.gif) |
28 | | snex 4111 |
. . . . . 6
![{](lbrace.gif) ![(/)](varnothing.gif) ![_V](rmcv.gif) |
29 | 27, 28 | imaex 4747 |
. . . . 5
![(](lp.gif) FullFun
↑c !["](backquote.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
30 | 24, 29 | imaex 4747 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) !["](backquote.gif) ![(](lp.gif) FullFun ↑c !["](backquote.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![_V](rmcv.gif) |
31 | 30 | complex 4104 |
. . 3
∼ ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![2nd](_2nd.gif) !["](backquote.gif) 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) !["](backquote.gif) ![(](lp.gif) FullFun ↑c !["](backquote.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![_V](rmcv.gif) |
32 | 18, 31 | eqeltrri 2424 |
. 2
![{](lbrace.gif) ![(](lp.gif)
↑c 0c ![(/)](varnothing.gif) ![_V](rmcv.gif) |
33 | | oveq1 5530 |
. . 3
![(](lp.gif) 0c ![(](lp.gif)
↑c 0c 0c ↑c
0c![)](rp.gif) ![)](rp.gif) |
34 | 33 | neeq1d 2529 |
. 2
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ↑c
0c
0c
↑c 0c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
35 | | oveq1 5530 |
. . 3
![(](lp.gif) ![(](lp.gif) ↑c 0c ![(](lp.gif)
↑c 0c![)](rp.gif) ![)](rp.gif) |
36 | 35 | neeq1d 2529 |
. 2
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
↑c 0c
![(](lp.gif) ↑c
0c
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
37 | | oveq1 5530 |
. . 3
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
↑c 0c ![(](lp.gif) ![(](lp.gif) 1c ↑c 0c![)](rp.gif) ![)](rp.gif) |
38 | 37 | neeq1d 2529 |
. 2
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ↑c
0c
![(](lp.gif) ![(](lp.gif)
1c
↑c 0c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
39 | | oveq1 5530 |
. . 3
![(](lp.gif) ![(](lp.gif) ↑c 0c ![(](lp.gif)
↑c 0c![)](rp.gif) ![)](rp.gif) |
40 | 39 | neeq1d 2529 |
. 2
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
↑c 0c
![(](lp.gif) ↑c
0c
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
41 | | 0cnc 6138 |
. . 3
0c
NC |
42 | | pw10 4161 |
. . . 4
1 ![(/)](varnothing.gif) |
43 | | nulel0c 4422 |
. . . 4
0c |
44 | 42, 43 | eqeltri 2423 |
. . 3
1
0c |
45 | | ce0nnuli 6178 |
. . 3
![(](lp.gif) 0c NC 1 0c 0c ↑c
0c
![(/)](varnothing.gif) ![)](rp.gif) |
46 | 41, 44, 45 | mp2an 653 |
. 2
0c
↑c 0c ![(/)](varnothing.gif) |
47 | | nnnc 6146 |
. . 3
![(](lp.gif) Nn NC ![)](rp.gif) |
48 | | 1cnc 6139 |
. . . . . 6
1c
NC |
49 | | 0ex 4110 |
. . . . . . . 8
![_V](rmcv.gif) |
50 | 49 | pw1sn 4165 |
. . . . . . 7
1 ![{](lbrace.gif) ![(/)](varnothing.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![}](rbrace.gif) |
51 | 28 | snel1c 4140 |
. . . . . . 7
![{](lbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif)
1c |
52 | 50, 51 | eqeltri 2423 |
. . . . . 6
1 ![{](lbrace.gif) ![(/)](varnothing.gif) 1c |
53 | | ce0nnuli 6178 |
. . . . . 6
![(](lp.gif) 1c NC 1 ![{](lbrace.gif) ![(/)](varnothing.gif)
1c
1c
↑c 0c ![(/)](varnothing.gif) ![)](rp.gif) |
54 | 48, 52, 53 | mp2an 653 |
. . . . 5
1c
↑c 0c ![(/)](varnothing.gif) |
55 | 54 | jctr 526 |
. . . 4
![(](lp.gif) ![(](lp.gif) ↑c 0c ![(](lp.gif) ![(](lp.gif) ↑c 0c 1c
↑c 0c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
56 | | ce0addcnnul 6179 |
. . . . 5
![(](lp.gif) ![(](lp.gif) NC 1c NC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
↑c 0c
![(](lp.gif) ![(](lp.gif) ↑c 0c 1c ↑c
0c
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
57 | 48, 56 | mpan2 652 |
. . . 4
![(](lp.gif) NC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ↑c 0c ![(](lp.gif) ![(](lp.gif) ↑c
0c
1c
↑c 0c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
58 | 55, 57 | syl5ibr 212 |
. . 3
![(](lp.gif) NC ![(](lp.gif) ![(](lp.gif) ↑c
0c
![(](lp.gif) ![(](lp.gif)
1c
↑c 0c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
59 | 47, 58 | syl 15 |
. 2
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ↑c
0c
![(](lp.gif) ![(](lp.gif)
1c
↑c 0c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
60 | 32, 34, 36, 38, 40, 46, 59 | finds 4411 |
1
![(](lp.gif) Nn ![(](lp.gif)
↑c 0c ![(/)](varnothing.gif) ![)](rp.gif) |