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