Step | Hyp | Ref
| Expression |
1 | | vex 2862 |
. . . . . . . 8
![_V](rmcv.gif) |
2 | 1 | elcompl 3225 |
. . . . . . 7
![(](lp.gif) ∼ ∼
∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c k ![)](rp.gif) k Nn
∼ ∼ ![(](lp.gif)
Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c k ![)](rp.gif) k Nn ![)](rp.gif) ![)](rp.gif) |
3 | 1 | elimak 4259 |
. . . . . . . . 9
![(](lp.gif) ∼ ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c k ![)](rp.gif) k Nn ![E.](exists.gif)
Nn ![<<](llangle.gif) ![n](_n.gif) ![p](_p.gif) ∼ ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c k ![)](rp.gif) ![)](rp.gif) |
4 | | opkex 4113 |
. . . . . . . . . . . 12
![<<](llangle.gif) ![n](_n.gif) ![p](_p.gif) ![_V](rmcv.gif) |
5 | 4 | elcompl 3225 |
. . . . . . . . . . 11
![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![p](_p.gif) ∼ ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c k ![<<](llangle.gif) ![n](_n.gif) ![p](_p.gif) ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c k ![)](rp.gif) ![)](rp.gif) |
6 | | elun 3220 |
. . . . . . . . . . . 12
![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![p](_p.gif) ∼ ![(](lp.gif)
Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c k ![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![p](_p.gif) ∼
![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![n](_n.gif) ![p](_p.gif) k ![)](rp.gif) ![)](rp.gif) |
7 | | vex 2862 |
. . . . . . . . . . . . . . . 16
![_V](rmcv.gif) |
8 | 7, 1 | ndisjrelk 4323 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![p](_p.gif) ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![p](_p.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
9 | 8 | notbii 287 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![p](_p.gif) ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![p](_p.gif)
![(/)](varnothing.gif) ![)](rp.gif) |
10 | 4 | elcompl 3225 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![p](_p.gif) ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![n](_n.gif) ![p](_p.gif) ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) |
11 | | df-ne 2518 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![(](lp.gif) ![p](_p.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
12 | 11 | con2bii 322 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![(](lp.gif) ![p](_p.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
13 | 9, 10, 12 | 3bitr4i 268 |
. . . . . . . . . . . . 13
![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![p](_p.gif) ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![p](_p.gif)
![(/)](varnothing.gif) ![)](rp.gif) |
14 | | opkelidkg 4274 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif)
![_V](rmcv.gif) ![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![p](_p.gif) k ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
15 | 7, 1, 14 | mp2an 653 |
. . . . . . . . . . . . 13
![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![p](_p.gif) k ![p](_p.gif) ![)](rp.gif) |
16 | 13, 15 | orbi12i 507 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![p](_p.gif) ∼ ![(](lp.gif)
Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![<<](llangle.gif) ![n](_n.gif) ![p](_p.gif) k ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
17 | | incom 3448 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![p](_p.gif) ![(](lp.gif) ![n](_n.gif) ![)](rp.gif) |
18 | 17 | eqeq1i 2360 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![(](lp.gif) ![n](_n.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
19 | | eqcom 2355 |
. . . . . . . . . . . . 13
![(](lp.gif) ![n](_n.gif) ![)](rp.gif) |
20 | 18, 19 | orbi12i 507 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![p](_p.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
21 | 6, 16, 20 | 3bitri 262 |
. . . . . . . . . . 11
![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![p](_p.gif) ∼ ![(](lp.gif)
Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c k ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
22 | 5, 21 | xchbinx 301 |
. . . . . . . . . 10
![(](lp.gif) ![<<](llangle.gif) ![n](_n.gif) ![p](_p.gif) ∼ ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c k ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
23 | 22 | rexbii 2639 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif)
Nn ![<<](llangle.gif) ![n](_n.gif) ![p](_p.gif) ∼ ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c k ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif)
![n](_n.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
24 | | rexnal 2625 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
25 | 3, 23, 24 | 3bitri 262 |
. . . . . . . 8
![(](lp.gif) ∼ ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c k ![)](rp.gif) k Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
26 | 25 | con2bii 322 |
. . . . . . 7
![(](lp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif)
∼ ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c k ![)](rp.gif) k Nn ![)](rp.gif) ![)](rp.gif) |
27 | 2, 26 | bitr4i 243 |
. . . . . 6
![(](lp.gif) ∼ ∼
∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c k ![)](rp.gif) k Nn ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
28 | 27 | abbi2i 2464 |
. . . . 5
∼ ∼ ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c k ![)](rp.gif) k Nn ![{](lbrace.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![)](rp.gif) ![}](rbrace.gif) |
29 | | ssetkex 4294 |
. . . . . . . . . . . . 13
Sk ![_V](rmcv.gif) |
30 | 29 | ins3kex 4308 |
. . . . . . . . . . . 12
Ins3k Sk ![_V](rmcv.gif) |
31 | 29 | ins2kex 4307 |
. . . . . . . . . . . 12
Ins2k Sk ![_V](rmcv.gif) |
32 | 30, 31 | inex 4105 |
. . . . . . . . . . 11
Ins3k Sk Ins2k Sk
![_V](rmcv.gif) |
33 | | 1cex 4142 |
. . . . . . . . . . . . 13
1c
![_V](rmcv.gif) |
34 | 33 | pw1ex 4303 |
. . . . . . . . . . . 12
1
1c
![_V](rmcv.gif) |
35 | 34 | pw1ex 4303 |
. . . . . . . . . . 11
1 1
1c
![_V](rmcv.gif) |
36 | 32, 35 | imakex 4300 |
. . . . . . . . . 10
![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c
![_V](rmcv.gif) |
37 | 36 | complex 4104 |
. . . . . . . . 9
∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c
![_V](rmcv.gif) |
38 | | idkex 4314 |
. . . . . . . . 9
k
![_V](rmcv.gif) |
39 | 37, 38 | unex 4106 |
. . . . . . . 8
∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c k ![_V](rmcv.gif) |
40 | 39 | complex 4104 |
. . . . . . 7
∼ ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c k ![_V](rmcv.gif) |
41 | | nncex 4396 |
. . . . . . 7
Nn ![_V](rmcv.gif) |
42 | 40, 41 | imakex 4300 |
. . . . . 6
∼ ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c k ![)](rp.gif) k Nn ![_V](rmcv.gif) |
43 | 42 | complex 4104 |
. . . . 5
∼ ∼ ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c k ![)](rp.gif) k Nn ![_V](rmcv.gif) |
44 | 28, 43 | eqeltrri 2424 |
. . . 4
![{](lbrace.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![)](rp.gif) ![_V](rmcv.gif) |
45 | | df-0c 4377 |
. . . . . . . . . . 11
0c
![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) |
46 | 45 | eqeq2i 2363 |
. . . . . . . . . 10
![(](lp.gif) 0c
![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) |
47 | 46 | biimpi 186 |
. . . . . . . . 9
![(](lp.gif) 0c ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) |
48 | 47 | ineq1d 3456 |
. . . . . . . 8
![(](lp.gif) 0c ![(](lp.gif) ![n](_n.gif)
![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
49 | 48 | eqeq1d 2361 |
. . . . . . 7
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![n](_n.gif) ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
50 | | incom 3448 |
. . . . . . . . 9
![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![n](_n.gif) ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) |
51 | 50 | eqeq1i 2360 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![n](_n.gif)
![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
52 | | disjsn 3786 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![n](_n.gif) ![)](rp.gif) |
53 | 51, 52 | bitri 240 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![n](_n.gif)
![n](_n.gif) ![)](rp.gif) |
54 | 49, 53 | syl6bb 252 |
. . . . . 6
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
55 | | eqeq1 2359 |
. . . . . . 7
![(](lp.gif) 0c ![(](lp.gif) 0c ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
56 | | eqcom 2355 |
. . . . . . 7
0c
0c![)](rp.gif) |
57 | 55, 56 | syl6bb 252 |
. . . . . 6
![(](lp.gif) 0c ![(](lp.gif)
0c![)](rp.gif) ![)](rp.gif) |
58 | 54, 57 | orbi12d 690 |
. . . . 5
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![(](lp.gif)
0c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
59 | 58 | ralbidv 2634 |
. . . 4
![(](lp.gif) 0c ![(](lp.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![A.](forall.gif) Nn ![(](lp.gif)
0c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
60 | | ineq1 3450 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
61 | 60 | eqeq1d 2361 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif)
![(](lp.gif) ![n](_n.gif) ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
62 | | eqeq1 2359 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
63 | 61, 62 | orbi12d 690 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
64 | 63 | ralbidv 2634 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
65 | | ineq2 3451 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) |
66 | 65 | eqeq1d 2361 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif)
![(](lp.gif) ![q](_q.gif) ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
67 | | equequ2 1686 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif)
![q](_q.gif) ![)](rp.gif) ![)](rp.gif) |
68 | 66, 67 | orbi12d 690 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
69 | 68 | cbvralv 2835 |
. . . . 5
![(](lp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![)](rp.gif) ![)](rp.gif) |
70 | 64, 69 | syl6bb 252 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
71 | | ineq1 3450 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![n](_n.gif)
![(](lp.gif) ![(](lp.gif) 1c ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
72 | 71 | eqeq1d 2361 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![(](lp.gif) ![(](lp.gif)
1c
![n](_n.gif)
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
73 | | eqeq1 2359 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif)
1c
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
74 | 72, 73 | orbi12d 690 |
. . . . 5
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![n](_n.gif) ![(](lp.gif) 1c ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
75 | 74 | ralbidv 2634 |
. . . 4
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![n](_n.gif) ![(](lp.gif)
1c
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
76 | | ineq1 3450 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![(](lp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
77 | 76 | eqeq1d 2361 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif)
![(](lp.gif) ![n](_n.gif) ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
78 | | eqeq1 2359 |
. . . . . 6
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
79 | 77, 78 | orbi12d 690 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
80 | 79 | ralbidv 2634 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
81 | | nnc0suc 4412 |
. . . . . . 7
![(](lp.gif) Nn ![(](lp.gif)
0c ![E.](exists.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
82 | | 0nelsuc 4400 |
. . . . . . . . . . . 12
![(](lp.gif)
1c![)](rp.gif) |
83 | | eleq2 2414 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
84 | 83 | biimpcd 215 |
. . . . . . . . . . . 12
![(](lp.gif)
![(](lp.gif)
![(](lp.gif) 1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
85 | 82, 84 | mtoi 169 |
. . . . . . . . . . 11
![(](lp.gif)
![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) |
86 | 85 | adantr 451 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) |
87 | 86 | nrexdv 2717 |
. . . . . . . . 9
![(](lp.gif)
![E.](exists.gif)
Nn ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
88 | | orel2 372 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) 0c ![E.](exists.gif) Nn ![(](lp.gif) 1c![)](rp.gif)
0c![)](rp.gif) ![)](rp.gif) |
89 | 87, 88 | syl 15 |
. . . . . . . 8
![(](lp.gif)
![(](lp.gif) ![(](lp.gif)
0c
![E.](exists.gif) Nn ![(](lp.gif)
1c![)](rp.gif) 0c![)](rp.gif) ![)](rp.gif) |
90 | 89 | com12 27 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif)
0c ![E.](exists.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif)
0c![)](rp.gif) ![)](rp.gif) |
91 | 81, 90 | sylbi 187 |
. . . . . 6
![(](lp.gif) Nn ![(](lp.gif)
0c![)](rp.gif) ![)](rp.gif) |
92 | | imor 401 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) 0c ![(](lp.gif)
0c![)](rp.gif) ![)](rp.gif) |
93 | 91, 92 | sylib 188 |
. . . . 5
![(](lp.gif) Nn ![(](lp.gif)
0c![)](rp.gif) ![)](rp.gif) |
94 | 93 | rgen 2679 |
. . . 4
![A.](forall.gif) Nn ![(](lp.gif)
0c![)](rp.gif) |
95 | | neq0 3560 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![n](_n.gif) ![E.](exists.gif) ![(](lp.gif) ![(](lp.gif)
1c
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
96 | | elin 3219 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) 1c
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
97 | | elsuc 4413 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) 1c ![E.](exists.gif)
![E.](exists.gif)
∼ ![b](_b.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
98 | | vex 2862 |
. . . . . . . . . . . . . . . . 17
![_V](rmcv.gif) |
99 | 98 | elcompl 3225 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ∼ ![b](_b.gif) ![)](rp.gif) |
100 | 99 | anbi2i 675 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif)
∼ ![b](_b.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif) ![)](rp.gif) |
101 | | simp1r 980 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif)
Nn ![)](rp.gif) |
102 | | nnc0suc 4412 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) Nn ![(](lp.gif)
0c ![E.](exists.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
103 | 101, 102 | sylib 188 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif)
![(](lp.gif)
0c ![E.](exists.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
104 | | ssun2 3427 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![{](lbrace.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif) |
105 | 98 | snid 3760 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) |
106 | 104, 105 | sselii 3270 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif) |
107 | | n0i 3555 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
108 | 106, 107 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(/)](varnothing.gif) |
109 | 45 | eleq2i 2417 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
0c
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) |
110 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![_V](rmcv.gif) |
111 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![{](lbrace.gif) ![x](_x.gif)
![_V](rmcv.gif) |
112 | 110, 111 | unex 4106 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![_V](rmcv.gif) |
113 | 112 | elsnc 3756 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![(/)](varnothing.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(/)](varnothing.gif) ![)](rp.gif) |
114 | 109, 113 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
0c
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
115 | 108, 114 | mtbir 290 |
. . . . . . . . . . . . . . . . . . . . . . 23
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
0c |
116 | | eleq2 2414 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) 0c![)](rp.gif) ![)](rp.gif) |
117 | 116 | biimpcd 215 |
. . . . . . . . . . . . . . . . . . . . . . 23
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 0c ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
0c![)](rp.gif) ![)](rp.gif) |
118 | 115, 117 | mtoi 169 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
0c![)](rp.gif) |
119 | 118 | adantl 452 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif)
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![n](_n.gif) 0c![)](rp.gif) |
120 | | orel1 371 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif)
0c ![(](lp.gif) ![(](lp.gif) 0c ![E.](exists.gif) Nn ![(](lp.gif) 1c![)](rp.gif)
![E.](exists.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
121 | 119, 120 | syl 15 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif)
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![n](_n.gif) ![(](lp.gif) ![(](lp.gif) 0c ![E.](exists.gif)
Nn ![(](lp.gif) 1c![)](rp.gif)
![E.](exists.gif) Nn ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
122 | | simpll 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
Nn ![)](rp.gif) |
123 | | simpr3r 1017 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif) ![)](rp.gif)
![b](_b.gif) ![)](rp.gif) |
124 | 123 | adantr 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![b](_b.gif) ![)](rp.gif) |
125 | | simpr 447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
126 | 110, 98 | nnsucelr 4428 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif)
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![p](_p.gif) ![)](rp.gif) |
127 | 122, 124,
125, 126 | syl12anc 1180 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![p](_p.gif) ![)](rp.gif) |
128 | 127 | ex 423 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
129 | | ineq2 3451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
![(](lp.gif) ![(](lp.gif) ![q](_q.gif) ![(](lp.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
130 | 129 | eqeq1d 2361 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![q](_q.gif)
![(](lp.gif) ![p](_p.gif) ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
131 | | equequ2 1686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
![(](lp.gif) ![(](lp.gif)
![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
132 | 130, 131 | orbi12d 690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
133 | 132 | rspccv 2952 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![(](lp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
134 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![(](lp.gif)
![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
135 | | n0i 3555 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![(](lp.gif) ![p](_p.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
136 | 134, 135 | sylbir 204 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
![(](lp.gif) ![(](lp.gif)
![p](_p.gif) ![(](lp.gif) ![p](_p.gif)
![(/)](varnothing.gif) ![)](rp.gif) |
137 | | pm2.53 362 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![p](_p.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
138 | 136, 137 | syl5 28 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![p](_p.gif) ![(](lp.gif) ![(](lp.gif)
![p](_p.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
139 | 138 | exp3a 425 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![p](_p.gif)
![p](_p.gif) ![(](lp.gif)
![(](lp.gif)
![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
140 | 133, 139 | syl6 29 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
![(](lp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
141 | 140 | com23 72 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
![(](lp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![(](lp.gif)
Nn ![(](lp.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
142 | 141 | imp 418 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
![(](lp.gif) ![(](lp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![m](_m.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
143 | 142 | adantrr 697 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
![(](lp.gif) ![(](lp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif)
![(](lp.gif)
Nn ![(](lp.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
144 | 143 | 3adant1 973 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif)
![(](lp.gif)
Nn ![(](lp.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
145 | 144 | impcom 419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
146 | 128, 145 | syld 40 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
147 | 146 | ex 423 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
148 | 147 | com3l 75 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c ![(](lp.gif) Nn ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
149 | 148 | imp 418 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif)
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![(](lp.gif)
Nn ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) |
150 | | addceq1 4383 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
151 | 149, 150 | syl6 29 |
. . . . . . . . . . . . . . . . . . . . . . 23
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif)
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![(](lp.gif)
Nn ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
152 | | eleq2 2414 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
153 | 152 | anbi2d 684 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif)
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif)
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
154 | | eqeq2 2362 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) 1c
![(](lp.gif) 1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
155 | 154 | imbi2d 307 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c ![n](_n.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
156 | 153, 155 | imbi12d 311 |
. . . . . . . . . . . . . . . . . . . . . . 23
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif)
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![n](_n.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c ![n](_n.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif)
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![(](lp.gif)
Nn ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
157 | 151, 156 | mpbiri 224 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif)
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![n](_n.gif) ![(](lp.gif) Nn ![(](lp.gif) 1c ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
158 | 157 | com3l 75 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif)
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![n](_n.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
159 | 158 | rexlimdv 2737 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif)
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![n](_n.gif) ![(](lp.gif) ![E.](exists.gif) Nn ![(](lp.gif)
1c
![(](lp.gif) 1c ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
160 | 121, 159 | syld 40 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif)
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![n](_n.gif) ![(](lp.gif) ![(](lp.gif) 0c ![E.](exists.gif)
Nn ![(](lp.gif) 1c![)](rp.gif)
![(](lp.gif) 1c ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
161 | 160 | ex 423 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![(](lp.gif) 0c ![E.](exists.gif)
Nn ![(](lp.gif) 1c![)](rp.gif)
![(](lp.gif) 1c ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
162 | 103, 161 | mpid 37 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif)
1c
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
163 | 162 | 3expa 1151 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![)](rp.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif)
1c
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
164 | | eleq1 2413 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif)
![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
165 | 164 | imbi1d 308 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif) 1c
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
166 | 163, 165 | syl5ibrcom 213 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![)](rp.gif) ![(](lp.gif)
![b](_b.gif) ![)](rp.gif) ![(](lp.gif)
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif)
1c
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
167 | 100, 166 | sylan2b 461 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![)](rp.gif) ![(](lp.gif)
∼ ![b](_b.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif)
![(](lp.gif)
1c
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
168 | 167 | rexlimdvva 2745 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif) ![E.](exists.gif)
∼ ![b](_b.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif)
![(](lp.gif)
1c
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
169 | 97, 168 | syl5bi 208 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![)](rp.gif) ![(](lp.gif)
![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) 1c ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
170 | 169 | imp3a 420 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![n](_n.gif) ![(](lp.gif) 1c ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
171 | 96, 170 | syl5bi 208 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![)](rp.gif) ![(](lp.gif)
![(](lp.gif) ![(](lp.gif)
1c
![n](_n.gif) ![(](lp.gif) 1c ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
172 | 171 | exlimdv 1636 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif) ![(](lp.gif) ![(](lp.gif) 1c ![n](_n.gif) ![(](lp.gif) 1c ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
173 | 95, 172 | syl5bi 208 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![n](_n.gif) ![(](lp.gif) 1c ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
174 | 173 | orrd 367 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![n](_n.gif) ![(](lp.gif)
1c
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
175 | 174 | exp31 587 |
. . . . . 6
![(](lp.gif) Nn ![(](lp.gif) Nn ![(](lp.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![n](_n.gif)
![(](lp.gif) 1c ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
176 | 175 | com23 72 |
. . . . 5
![(](lp.gif) Nn ![(](lp.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![n](_n.gif) ![(](lp.gif) 1c ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
177 | 176 | ralrimdv 2703 |
. . . 4
![(](lp.gif) Nn ![(](lp.gif) ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![q](_q.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![n](_n.gif) ![(](lp.gif) 1c ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
178 | 44, 59, 70, 75, 80, 94, 177 | finds 4411 |
. . 3
![(](lp.gif) Nn ![A.](forall.gif) Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
179 | | ineq2 3451 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![(](lp.gif) ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
180 | 179 | eqeq1d 2361 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif)
![(](lp.gif) ![N](_cn.gif) ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
181 | | eqeq2 2362 |
. . . . 5
![(](lp.gif) ![(](lp.gif)
![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
182 | 180, 181 | orbi12d 690 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif)
![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
183 | 182 | rspccv 2952 |
. . 3
![(](lp.gif) ![A.](forall.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) ![(](lp.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif)
![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
184 | 178, 183 | syl 15 |
. 2
![(](lp.gif) Nn ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif) ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
185 | 184 | imp 418 |
1
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![(](lp.gif) ![N](_cn.gif)
![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |