Step | Hyp | Ref
| Expression |
1 | | ncfinraise 4481 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Nn
![M](_cm.gif) ![E.](exists.gif) Nn ![(](lp.gif) 1
1 ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
2 | | anidm 625 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) 1
1
![n](_n.gif) 1
![n](_n.gif) ![)](rp.gif) |
3 | 2 | rexbii 2639 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) 1
1
![n](_n.gif) ![E.](exists.gif) Nn 1
![n](_n.gif) ![)](rp.gif) |
4 | 1, 3 | sylib 188 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Nn
![M](_cm.gif) ![E.](exists.gif) Nn 1 ![n](_n.gif) ![)](rp.gif) |
5 | 4 | 3anidm23 1241 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) Nn ![M](_cm.gif) ![E.](exists.gif) Nn 1 ![n](_n.gif) ![)](rp.gif) |
6 | 5 | ex 423 |
. . . . . 6
![(](lp.gif) Nn ![(](lp.gif) ![E.](exists.gif) Nn 1
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
7 | 6 | ancld 536 |
. . . . 5
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![E.](exists.gif) Nn 1
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
8 | 7 | eximdv 1622 |
. . . 4
![(](lp.gif) Nn ![(](lp.gif) ![E.](exists.gif) ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif) ![E.](exists.gif) Nn 1
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
9 | 8 | imp 418 |
. . 3
![(](lp.gif) ![(](lp.gif) Nn ![E.](exists.gif) ![M](_cm.gif) ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif) ![E.](exists.gif) Nn 1 ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
10 | | n0 3559 |
. . . 4
![(](lp.gif)
![E.](exists.gif)
![M](_cm.gif) ![)](rp.gif) |
11 | 10 | anbi2i 675 |
. . 3
![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) ![(](lp.gif)
Nn ![E.](exists.gif) ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) |
12 | | rexcom 2772 |
. . . 4
![(](lp.gif) ![E.](exists.gif)
Nn ![E.](exists.gif)
1 ![E.](exists.gif) ![E.](exists.gif) Nn 1 ![n](_n.gif) ![)](rp.gif) |
13 | | df-rex 2620 |
. . . 4
![(](lp.gif) ![E.](exists.gif)
![E.](exists.gif) Nn 1 ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif)
![E.](exists.gif) Nn 1
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
14 | 12, 13 | bitri 240 |
. . 3
![(](lp.gif) ![E.](exists.gif)
Nn ![E.](exists.gif)
1 ![E.](exists.gif) ![a](_a.gif) ![(](lp.gif)
![E.](exists.gif) Nn 1
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
15 | 9, 11, 14 | 3imtr4i 257 |
. 2
![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) ![E.](exists.gif) Nn ![E.](exists.gif) 1 ![n](_n.gif) ![)](rp.gif) |
16 | | pw1eq 4143 |
. . . . . . . 8
![(](lp.gif) 1 1 ![b](_b.gif) ![)](rp.gif) |
17 | 16 | eleq1d 2419 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) 1 1 ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
18 | 17 | cbvrexv 2836 |
. . . . . 6
![(](lp.gif) ![E.](exists.gif)
1 ![E.](exists.gif) 1
![p](_p.gif) ![)](rp.gif) |
19 | 18 | anbi2i 675 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
1 ![E.](exists.gif) 1 ![p](_p.gif) ![(](lp.gif) ![E.](exists.gif)
1 ![E.](exists.gif)
1 ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
20 | | reeanv 2778 |
. . . . 5
![(](lp.gif) ![E.](exists.gif)
![E.](exists.gif) ![(](lp.gif) 1 1 ![p](_p.gif) ![(](lp.gif) ![E.](exists.gif)
1 ![E.](exists.gif)
1 ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
21 | 19, 20 | bitr4i 243 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
1 ![E.](exists.gif) 1 ![p](_p.gif) ![E.](exists.gif) ![E.](exists.gif) ![(](lp.gif) 1 1 ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
22 | | simplll 734 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) ![(](lp.gif)
Nn
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![M](_cm.gif) ![(](lp.gif) 1 1 ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) Nn ![)](rp.gif) |
23 | | simprll 738 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) ![(](lp.gif)
Nn
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![M](_cm.gif) ![(](lp.gif) 1 1 ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![M](_cm.gif) ![)](rp.gif) |
24 | | simprlr 739 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) ![(](lp.gif)
Nn
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![M](_cm.gif) ![(](lp.gif) 1 1 ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![M](_cm.gif) ![)](rp.gif) |
25 | | ncfinraise 4481 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Nn
![M](_cm.gif) ![E.](exists.gif) Nn ![(](lp.gif) 1
1 ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) |
26 | 22, 23, 24, 25 | syl3anc 1182 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) ![(](lp.gif)
Nn
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![M](_cm.gif) ![(](lp.gif) 1 1 ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) Nn ![(](lp.gif) 1
1
![q](_q.gif) ![)](rp.gif) ![)](rp.gif) |
27 | | simp1rl 1020 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) ![(](lp.gif)
Nn
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![M](_cm.gif) ![(](lp.gif) 1 1 ![p](_p.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1 1 ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) Nn ![)](rp.gif) |
28 | | simp3l 983 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) ![(](lp.gif)
Nn
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![M](_cm.gif) ![(](lp.gif) 1 1 ![p](_p.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1 1 ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) Nn ![)](rp.gif) |
29 | | simp2rl 1024 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) ![(](lp.gif)
Nn
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![M](_cm.gif) ![(](lp.gif) 1 1 ![p](_p.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1 1 ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) 1
![n](_n.gif) ![)](rp.gif) |
30 | | simp3rl 1028 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) ![(](lp.gif)
Nn
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![M](_cm.gif) ![(](lp.gif) 1 1 ![p](_p.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1 1 ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) 1
![q](_q.gif) ![)](rp.gif) |
31 | | nnceleq 4430 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) 1
1 ![q](_q.gif) ![)](rp.gif) ![q](_q.gif) ![)](rp.gif) |
32 | 27, 28, 29, 30, 31 | syl22anc 1183 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) ![(](lp.gif)
Nn
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![M](_cm.gif) ![(](lp.gif) 1 1 ![p](_p.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1 1 ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![q](_q.gif) ![)](rp.gif) |
33 | | simp1rr 1021 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) ![(](lp.gif)
Nn
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![M](_cm.gif) ![(](lp.gif) 1 1 ![p](_p.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1 1 ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) Nn ![)](rp.gif) |
34 | | simp2rr 1025 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) ![(](lp.gif)
Nn
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![M](_cm.gif) ![(](lp.gif) 1 1 ![p](_p.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1 1 ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) 1
![p](_p.gif) ![)](rp.gif) |
35 | | simp3rr 1029 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) ![(](lp.gif)
Nn
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![M](_cm.gif) ![(](lp.gif) 1 1 ![p](_p.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1 1 ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) 1
![q](_q.gif) ![)](rp.gif) |
36 | | nnceleq 4430 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) 1
1 ![q](_q.gif) ![)](rp.gif) ![q](_q.gif) ![)](rp.gif) |
37 | 33, 28, 34, 35, 36 | syl22anc 1183 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) ![(](lp.gif)
Nn
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![M](_cm.gif) ![(](lp.gif) 1 1 ![p](_p.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1 1 ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![q](_q.gif) ![)](rp.gif) |
38 | 32, 37 | eqtr4d 2388 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) ![(](lp.gif)
Nn
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![M](_cm.gif) ![(](lp.gif) 1 1 ![p](_p.gif) ![)](rp.gif) ![(](lp.gif)
Nn ![(](lp.gif) 1 1 ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![p](_p.gif) ![)](rp.gif) |
39 | 38 | 3expa 1151 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) ![(](lp.gif) Nn Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![M](_cm.gif) ![(](lp.gif) 1 1 ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) Nn ![(](lp.gif) 1 1 ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![p](_p.gif) ![)](rp.gif) |
40 | 39 | exp32 588 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) ![(](lp.gif)
Nn
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![M](_cm.gif) ![(](lp.gif) 1 1 ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) 1
1 ![q](_q.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
41 | 40 | rexlimdv 2737 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) ![(](lp.gif)
Nn
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![M](_cm.gif) ![(](lp.gif) 1 1 ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif) 1
1 ![q](_q.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
42 | 26, 41 | mpd 14 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) ![(](lp.gif)
Nn
Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![M](_cm.gif) ![(](lp.gif) 1 1 ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![p](_p.gif) ![)](rp.gif) |
43 | 42 | exp32 588 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) ![(](lp.gif) Nn Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![M](_cm.gif) ![(](lp.gif) ![(](lp.gif) 1
1 ![p](_p.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
44 | 43 | rexlimdvv 2744 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) ![(](lp.gif) Nn Nn ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
![E.](exists.gif)
![(](lp.gif) 1
1
![p](_p.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
45 | 21, 44 | syl5bi 208 |
. . 3
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) ![(](lp.gif) Nn Nn ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![E.](exists.gif) 1 ![E.](exists.gif) 1 ![p](_p.gif)
![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
46 | 45 | ralrimivva 2706 |
. 2
![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) ![A.](forall.gif) Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![E.](exists.gif) 1
![E.](exists.gif) 1 ![p](_p.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
47 | | eleq2 2414 |
. . . 4
![(](lp.gif) ![(](lp.gif) 1 1 ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
48 | 47 | rexbidv 2635 |
. . 3
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
1 ![E.](exists.gif) 1
![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
49 | 48 | reu4 3030 |
. 2
![(](lp.gif) ![E!](_e1.gif) Nn ![E.](exists.gif) 1 ![(](lp.gif) ![E.](exists.gif)
Nn ![E.](exists.gif)
1 ![A.](forall.gif) Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![E.](exists.gif) 1
![E.](exists.gif) 1 ![p](_p.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
50 | 15, 46, 49 | sylanbrc 645 |
1
![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) ![E!](_e1.gif) Nn ![E.](exists.gif) 1 ![n](_n.gif) ![)](rp.gif) |