Step | Hyp | Ref
| Expression |
1 | | nnltp1c 6262 |
. . . . . . . . . . . 12
![(](lp.gif) Nn c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) |
2 | | nnnc 6146 |
. . . . . . . . . . . . 13
![(](lp.gif) Nn NC ![)](rp.gif) |
3 | | peano2 4403 |
. . . . . . . . . . . . . 14
![(](lp.gif) Nn ![(](lp.gif)
1c
Nn ![)](rp.gif) |
4 | | nnnc 6146 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif)
1c
Nn ![(](lp.gif) 1c NC ![)](rp.gif) |
5 | 3, 4 | syl 15 |
. . . . . . . . . . . . 13
![(](lp.gif) Nn ![(](lp.gif)
1c
NC ![)](rp.gif) |
6 | | ltlenlec 6207 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) NC ![(](lp.gif) 1c NC ![(](lp.gif) c ![(](lp.gif) 1c ![(](lp.gif) c ![(](lp.gif) 1c ![(](lp.gif) 1c c ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
7 | 2, 5, 6 | syl2anc 642 |
. . . . . . . . . . . 12
![(](lp.gif) Nn ![(](lp.gif) c ![(](lp.gif) 1c ![(](lp.gif) c ![(](lp.gif) 1c ![(](lp.gif) 1c c ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
8 | 1, 7 | mpbid 201 |
. . . . . . . . . . 11
![(](lp.gif) Nn ![(](lp.gif) c ![(](lp.gif) 1c ![(](lp.gif) 1c c ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
9 | 8 | simprd 449 |
. . . . . . . . . 10
![(](lp.gif) Nn ![(](lp.gif) 1c c ![A](_ca.gif) ![)](rp.gif) |
10 | 9 | adantr 451 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) 1c c ![A](_ca.gif) ![)](rp.gif) |
11 | 10 | intnand 882 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Nn Nn 1c c ![(](lp.gif)
1c
![(](lp.gif) 1c c ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
12 | 11 | a1d 22 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![(](lp.gif)
1c
Nn 1c c ![(](lp.gif) 1c ![(](lp.gif) 1c c ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
13 | | breq2 4643 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) 1c 1c c 1c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
14 | | breq1 4642 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) c ![(](lp.gif) 1c c ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
15 | 13, 14 | anbi12d 691 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c c c ![A](_ca.gif) 1c c ![(](lp.gif)
1c
![(](lp.gif) 1c c ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
16 | 15 | elrab 2994 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif)
1c
![{](lbrace.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) 1c
Nn 1c c ![(](lp.gif)
1c
![(](lp.gif) 1c c ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
17 | 16 | notbii 287 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif)
1c
![{](lbrace.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
1c
Nn 1c c ![(](lp.gif)
1c
![(](lp.gif) 1c c ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
18 | | imnan 411 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
Nn 1c c ![(](lp.gif) 1c ![(](lp.gif) 1c c ![A](_ca.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
1c
Nn 1c c ![(](lp.gif)
1c
![(](lp.gif) 1c c ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
19 | 17, 18 | bitr4i 243 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif)
1c
![{](lbrace.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) 1c
Nn 1c c ![(](lp.gif)
1c
![(](lp.gif) 1c c ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
20 | 12, 19 | sylibr 203 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) 1c ![{](lbrace.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) |
21 | 3 | adantr 451 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) 1c
Nn ![)](rp.gif) |
22 | | elcomplg 3218 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif)
1c
Nn ![(](lp.gif) ![(](lp.gif) 1c
∼ ![{](lbrace.gif) Nn 1c c
c ![A](_ca.gif) ![)](rp.gif) ![(](lp.gif) 1c
![{](lbrace.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
23 | 21, 22 | syl 15 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![(](lp.gif)
1c
∼ ![{](lbrace.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![(](lp.gif) 1c
![{](lbrace.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
24 | 20, 23 | mpbird 223 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) 1c
∼ ![{](lbrace.gif) Nn 1c c
c ![A](_ca.gif) ![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) |
25 | | nnnc 6146 |
. . . . . . . . . . . . . 14
![(](lp.gif) Nn NC ![)](rp.gif) |
26 | | ncslesuc 6267 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) c ![(](lp.gif)
1c
![(](lp.gif) c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
27 | 25, 2, 26 | syl2an 463 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) c ![(](lp.gif)
1c
![(](lp.gif) c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
28 | 27 | expcom 424 |
. . . . . . . . . . . 12
![(](lp.gif) Nn ![(](lp.gif) Nn ![(](lp.gif) c ![(](lp.gif)
1c
![(](lp.gif) c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
29 | 28 | adantrd 454 |
. . . . . . . . . . 11
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) Nn 1c
c ![x](_x.gif) ![(](lp.gif) c ![(](lp.gif) 1c ![(](lp.gif) c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
30 | 29 | adantr 451 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![(](lp.gif) Nn 1c c ![x](_x.gif)
![(](lp.gif) c ![(](lp.gif)
1c
![(](lp.gif) c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
31 | 30 | pm5.32d 620 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn 1c c ![x](_x.gif)
c ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) Nn 1c c ![x](_x.gif)
![(](lp.gif) c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
32 | | anass 630 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn 1c c ![x](_x.gif)
c ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) Nn 1c c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
33 | | andi 837 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn 1c c ![x](_x.gif)
![(](lp.gif) c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn 1c c ![x](_x.gif)
c ![A](_ca.gif)
![(](lp.gif) ![(](lp.gif)
Nn 1c c ![x](_x.gif)
![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
34 | | anass 630 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn 1c c ![x](_x.gif)
c ![A](_ca.gif)
![(](lp.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
35 | 34 | orbi1i 506 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn 1c
c ![x](_x.gif)
c ![A](_ca.gif) ![(](lp.gif) ![(](lp.gif) Nn 1c c ![x](_x.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
Nn 1c c ![x](_x.gif)
![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
36 | 33, 35 | bitri 240 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn 1c c ![x](_x.gif)
![(](lp.gif) c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
Nn 1c c ![x](_x.gif)
![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
37 | 31, 32, 36 | 3bitr3g 278 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![(](lp.gif) Nn 1c c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
Nn 1c c ![x](_x.gif)
![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
38 | | 1cnc 6139 |
. . . . . . . . . . . . . . . 16
1c
NC |
39 | | addlecncs 6209 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) 1c NC NC 1c c 1c ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
40 | 38, 2, 39 | sylancr 644 |
. . . . . . . . . . . . . . 15
![(](lp.gif) Nn 1c c 1c ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
41 | | addccom 4406 |
. . . . . . . . . . . . . . 15
![(](lp.gif) 1c
1c
![A](_ca.gif) ![)](rp.gif) |
42 | 40, 41 | syl6breqr 4679 |
. . . . . . . . . . . . . 14
![(](lp.gif) Nn 1c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) |
43 | 3, 42 | jca 518 |
. . . . . . . . . . . . 13
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) 1c Nn 1c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
44 | | eleq1 2413 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) Nn ![(](lp.gif)
1c
Nn ![)](rp.gif) ![)](rp.gif) |
45 | | breq2 4643 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) 1c 1c c 1c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
46 | 44, 45 | anbi12d 691 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) Nn 1c
c ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) 1c Nn 1c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
47 | 43, 46 | syl5ibrcom 213 |
. . . . . . . . . . . 12
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif)
Nn 1c c ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
48 | 47 | adantr 451 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) Nn 1c c ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
49 | 48 | pm4.71rd 616 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) Nn 1c c ![x](_x.gif)
![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
50 | 49 | bicomd 192 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn 1c c ![x](_x.gif)
![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
51 | 50 | orbi2d 682 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
Nn 1c c ![x](_x.gif)
![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
52 | 37, 51 | bitrd 244 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![(](lp.gif) Nn 1c c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
53 | | breq2 4643 |
. . . . . . . . 9
![(](lp.gif) 1c c 1c c ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
54 | | breq1 4642 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) c ![(](lp.gif)
1c
c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
55 | 53, 54 | anbi12d 691 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) 1c c c ![(](lp.gif) 1c![)](rp.gif)
1c
c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
56 | 55 | elrab 2994 |
. . . . . . 7
![(](lp.gif) ![{](lbrace.gif) Nn 1c c
c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) Nn 1c c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
57 | | elun 3220 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![{](lbrace.gif) ![(](lp.gif) 1c![)](rp.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) Nn 1c c
c ![A](_ca.gif) ![)](rp.gif) ![{](lbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
58 | | breq1 4642 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) c c ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
59 | 53, 58 | anbi12d 691 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) 1c c c ![A](_ca.gif) 1c c c ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
60 | 59 | elrab 2994 |
. . . . . . . . 9
![(](lp.gif) ![{](lbrace.gif) Nn 1c c
c ![A](_ca.gif) ![)](rp.gif) ![(](lp.gif) Nn 1c c
c ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
61 | | elsn 3748 |
. . . . . . . . 9
![(](lp.gif) ![{](lbrace.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) |
62 | 60, 61 | orbi12i 507 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![{](lbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
63 | 57, 62 | bitri 240 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![{](lbrace.gif) ![(](lp.gif) 1c![)](rp.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
64 | 52, 56, 63 | 3bitr4g 279 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![{](lbrace.gif) Nn 1c c
c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) Nn 1c c
c ![A](_ca.gif) ![)](rp.gif) ![{](lbrace.gif) ![(](lp.gif) 1c![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
65 | 64 | eqrdv 2351 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Nn Nn ![{](lbrace.gif) Nn 1c c c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![{](lbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
66 | | sneq 3744 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) 1c ![{](lbrace.gif) ![y](_y.gif) ![{](lbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) |
67 | 66 | uneq2d 3418 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![{](lbrace.gif) Nn 1c c
c ![A](_ca.gif) ![)](rp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif)
Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![{](lbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
68 | 67 | eqeq2d 2364 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![{](lbrace.gif) Nn 1c c
c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) Nn 1c c c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![{](lbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
69 | 68 | rspcev 2955 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
∼ ![{](lbrace.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![{](lbrace.gif) Nn 1c c c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![{](lbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) ![E.](exists.gif) ∼ ![{](lbrace.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![{](lbrace.gif) Nn 1c c
c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
70 | 24, 65, 69 | syl2anc 642 |
. . . 4
![(](lp.gif) ![(](lp.gif) Nn Nn ![E.](exists.gif) ∼ ![{](lbrace.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![{](lbrace.gif) Nn 1c c c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
71 | | compleq 3243 |
. . . . . 6
![(](lp.gif) ![{](lbrace.gif) Nn 1c c
c ![A](_ca.gif) ![)](rp.gif) ∼
∼ ![{](lbrace.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) |
72 | | uneq1 3411 |
. . . . . . 7
![(](lp.gif) ![{](lbrace.gif) Nn 1c c
c ![A](_ca.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif)
Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
73 | 72 | eqeq2d 2364 |
. . . . . 6
![(](lp.gif) ![{](lbrace.gif) Nn 1c c
c ![A](_ca.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif)
Nn 1c c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) Nn 1c c c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
74 | 71, 73 | rexeqbidv 2820 |
. . . . 5
![(](lp.gif) ![{](lbrace.gif) Nn 1c c
c ![A](_ca.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
∼ ![x](_x.gif) ![{](lbrace.gif) Nn 1c c c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![E.](exists.gif) ∼ ![{](lbrace.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![{](lbrace.gif) Nn 1c c c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
75 | 74 | rspcev 2955 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![E.](exists.gif) ∼ ![{](lbrace.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![{](lbrace.gif) Nn 1c c
c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![E.](exists.gif)
![E.](exists.gif)
∼ ![x](_x.gif) ![{](lbrace.gif)
Nn 1c c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
76 | 70, 75 | sylan2 460 |
. . 3
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![(](lp.gif) Nn Nn ![)](rp.gif) ![E.](exists.gif)
![E.](exists.gif) ∼ ![x](_x.gif) ![{](lbrace.gif) Nn 1c c
c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
77 | | elsuc 4413 |
. . 3
![(](lp.gif) ![{](lbrace.gif)
Nn 1c c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
1c
![E.](exists.gif) ![E.](exists.gif) ∼ ![x](_x.gif) ![{](lbrace.gif) Nn 1c c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
78 | 76, 77 | sylibr 203 |
. 2
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![(](lp.gif) Nn Nn ![)](rp.gif) ![{](lbrace.gif)
Nn 1c c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) |
79 | 78 | expcom 424 |
1
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![{](lbrace.gif)
Nn 1c c c ![A](_ca.gif) ![)](rp.gif) ![{](lbrace.gif) Nn 1c c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |