Step | Hyp | Ref
| Expression |
1 | | elncs 6119 |
. . . . 5
![(](lp.gif) NC ![E.](exists.gif) Nc ![x](_x.gif) ![)](rp.gif) |
2 | | elncs 6119 |
. . . . 5
![(](lp.gif) NC ![E.](exists.gif) Nc ![y](_y.gif) ![)](rp.gif) |
3 | 1, 2 | anbi12i 678 |
. . . 4
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) ![E.](exists.gif)
Nc ![E.](exists.gif)
Nc ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
4 | | eeanv 1913 |
. . . 4
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) Nc Nc ![y](_y.gif) ![(](lp.gif) ![E.](exists.gif)
Nc ![E.](exists.gif)
Nc ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
5 | 3, 4 | bitr4i 243 |
. . 3
![(](lp.gif) ![(](lp.gif) NC NC ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) Nc Nc ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
6 | | vex 2862 |
. . . . . . . 8
![_V](rmcv.gif) |
7 | | vex 2862 |
. . . . . . . 8
![_V](rmcv.gif) |
8 | 6, 7 | mucnc 6131 |
. . . . . . 7
Nc ·c Nc ![y](_y.gif) Nc ![(](lp.gif)
![y](_y.gif) ![)](rp.gif) |
9 | | df0c2 6137 |
. . . . . . 7
0c
Nc ![(/)](varnothing.gif) |
10 | 8, 9 | eqeq12i 2366 |
. . . . . 6
![(](lp.gif) Nc
·c Nc ![y](_y.gif)
0c Nc ![(](lp.gif) ![y](_y.gif) Nc ![(/)](varnothing.gif) ![)](rp.gif) |
11 | 6, 7 | xpex 5115 |
. . . . . . . . 9
![(](lp.gif) ![y](_y.gif) ![_V](rmcv.gif) |
12 | 11 | eqnc 6127 |
. . . . . . . 8
Nc ![(](lp.gif) ![y](_y.gif)
Nc ![(](lp.gif) ![y](_y.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
13 | | en0 6042 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![(](lp.gif) ![y](_y.gif)
![(/)](varnothing.gif) ![)](rp.gif) |
14 | 12, 13 | bitri 240 |
. . . . . . 7
Nc ![(](lp.gif) ![y](_y.gif)
Nc ![(](lp.gif) ![y](_y.gif)
![(/)](varnothing.gif) ![)](rp.gif) |
15 | | xpeq0 5046 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![y](_y.gif)
![(](lp.gif) ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
16 | | nceq 6108 |
. . . . . . . . 9
![(](lp.gif)
Nc Nc ![(/)](varnothing.gif) ![)](rp.gif) |
17 | | nceq 6108 |
. . . . . . . . 9
![(](lp.gif)
Nc Nc ![(/)](varnothing.gif) ![)](rp.gif) |
18 | 16, 17 | orim12i 502 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(/)](varnothing.gif) Nc Nc Nc Nc ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
19 | 15, 18 | sylbi 187 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![y](_y.gif)
Nc Nc Nc Nc ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
20 | 14, 19 | sylbi 187 |
. . . . . 6
Nc ![(](lp.gif) ![y](_y.gif)
Nc Nc Nc Nc
Nc ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
21 | 10, 20 | sylbi 187 |
. . . . 5
![(](lp.gif) Nc
·c Nc ![y](_y.gif)
0c Nc Nc Nc
Nc ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
22 | | oveq12 5532 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) Nc Nc ![y](_y.gif) ![(](lp.gif)
·c ![B](_cb.gif) Nc
·c Nc ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
23 | 22 | eqeq1d 2361 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Nc Nc ![y](_y.gif) ![(](lp.gif) ![(](lp.gif)
·c ![B](_cb.gif) 0c Nc ·c Nc ![y](_y.gif) 0c![)](rp.gif) ![)](rp.gif) |
24 | | eqeq1 2359 |
. . . . . . . . 9
![(](lp.gif) Nc ![(](lp.gif) 0c Nc
0c![)](rp.gif) ![)](rp.gif) |
25 | 24 | adantr 451 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Nc Nc ![y](_y.gif) ![(](lp.gif) 0c Nc
0c![)](rp.gif) ![)](rp.gif) |
26 | 9 | eqeq2i 2363 |
. . . . . . . 8
Nc
0c Nc Nc ![(/)](varnothing.gif) ![)](rp.gif) |
27 | 25, 26 | syl6bb 252 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) Nc Nc ![y](_y.gif) ![(](lp.gif) 0c Nc Nc ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
28 | | eqeq1 2359 |
. . . . . . . . 9
![(](lp.gif) Nc ![(](lp.gif) 0c Nc
0c![)](rp.gif) ![)](rp.gif) |
29 | 9 | eqeq2i 2363 |
. . . . . . . . 9
Nc
0c Nc Nc ![(/)](varnothing.gif) ![)](rp.gif) |
30 | 28, 29 | syl6bb 252 |
. . . . . . . 8
![(](lp.gif) Nc ![(](lp.gif) 0c Nc Nc ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
31 | 30 | adantl 452 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) Nc Nc ![y](_y.gif) ![(](lp.gif) 0c Nc Nc ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
32 | 27, 31 | orbi12d 690 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Nc Nc ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) 0c
0c
Nc Nc Nc
Nc ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
33 | 23, 32 | imbi12d 311 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Nc Nc ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ·c ![B](_cb.gif)
0c ![(](lp.gif) 0c
0c![)](rp.gif) ![(](lp.gif) Nc
·c Nc ![y](_y.gif)
0c Nc Nc Nc
Nc ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
34 | 21, 33 | mpbiri 224 |
. . . 4
![(](lp.gif) ![(](lp.gif) Nc Nc ![y](_y.gif) ![(](lp.gif) ![(](lp.gif)
·c ![B](_cb.gif) 0c ![(](lp.gif)
0c 0c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
35 | 34 | exlimivv 1635 |
. . 3
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) Nc Nc ![y](_y.gif) ![(](lp.gif) ![(](lp.gif)
·c ![B](_cb.gif) 0c ![(](lp.gif)
0c 0c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
36 | 5, 35 | sylbi 187 |
. 2
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) ![(](lp.gif) ·c ![B](_cb.gif)
0c
![(](lp.gif)
0c 0c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
37 | | 0cnc 6138 |
. . . . . . 7
0c
NC |
38 | | muccom 6134 |
. . . . . . 7
![(](lp.gif) 0c NC NC 0c ·c ![B](_cb.gif)
![(](lp.gif) ·c
0c![)](rp.gif) ![)](rp.gif) |
39 | 37, 38 | mpan 651 |
. . . . . 6
![(](lp.gif) NC 0c ·c ![B](_cb.gif)
![(](lp.gif) ·c
0c![)](rp.gif) ![)](rp.gif) |
40 | | muc0 6142 |
. . . . . 6
![(](lp.gif) NC ![(](lp.gif)
·c 0c 0c![)](rp.gif) |
41 | 39, 40 | eqtrd 2385 |
. . . . 5
![(](lp.gif) NC 0c ·c ![B](_cb.gif)
0c![)](rp.gif) |
42 | | oveq1 5530 |
. . . . . 6
![(](lp.gif) 0c ![(](lp.gif)
·c ![B](_cb.gif) 0c ·c
![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
43 | 42 | eqeq1d 2361 |
. . . . 5
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif)
·c ![B](_cb.gif) 0c 0c
·c ![B](_cb.gif) 0c![)](rp.gif) ![)](rp.gif) |
44 | 41, 43 | syl5ibrcom 213 |
. . . 4
![(](lp.gif) NC ![(](lp.gif) 0c ![(](lp.gif) ·c ![B](_cb.gif)
0c![)](rp.gif) ![)](rp.gif) |
45 | 44 | adantl 452 |
. . 3
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) 0c ![(](lp.gif)
·c ![B](_cb.gif) 0c![)](rp.gif) ![)](rp.gif) |
46 | | muc0 6142 |
. . . . 5
![(](lp.gif) NC ![(](lp.gif)
·c 0c 0c![)](rp.gif) |
47 | | oveq2 5531 |
. . . . . 6
![(](lp.gif) 0c ![(](lp.gif)
·c ![B](_cb.gif) ![(](lp.gif) ·c 0c![)](rp.gif) ![)](rp.gif) |
48 | 47 | eqeq1d 2361 |
. . . . 5
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif)
·c ![B](_cb.gif) 0c ![(](lp.gif) ·c
0c
0c![)](rp.gif) ![)](rp.gif) |
49 | 46, 48 | syl5ibrcom 213 |
. . . 4
![(](lp.gif) NC ![(](lp.gif) 0c ![(](lp.gif) ·c ![B](_cb.gif)
0c![)](rp.gif) ![)](rp.gif) |
50 | 49 | adantr 451 |
. . 3
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) 0c ![(](lp.gif)
·c ![B](_cb.gif) 0c![)](rp.gif) ![)](rp.gif) |
51 | 45, 50 | jaod 369 |
. 2
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) ![(](lp.gif)
0c 0c ![(](lp.gif)
·c ![B](_cb.gif) 0c![)](rp.gif) ![)](rp.gif) |
52 | 36, 51 | impbid 183 |
1
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) ![(](lp.gif) ·c ![B](_cb.gif)
0c
![(](lp.gif) 0c
0c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |