Proof of Theorem sbthlem1
Step | Hyp | Ref
| Expression |
1 | | df-f1 4792 |
. . . . . . . . 9
![(](lp.gif) ![R](_cr.gif) ![:](colon.gif) ![R](_cr.gif) ![-1-1->](onetoone.gif) ![(](lp.gif) ![R](_cr.gif) ![:](colon.gif) ![R](_cr.gif) ![-->](longrightarrow.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![)](rp.gif) ![)](rp.gif) |
2 | | ssid 3290 |
. . . . . . . . . . . 12
![R](_cr.gif) |
3 | | df-f 4791 |
. . . . . . . . . . . 12
![(](lp.gif) ![R](_cr.gif) ![:](colon.gif) ![R](_cr.gif) ![-->](longrightarrow.gif) ![(](lp.gif)
![R](_cr.gif) ![)](rp.gif) ![)](rp.gif) |
4 | 2, 3 | mpbiran2 885 |
. . . . . . . . . . 11
![(](lp.gif) ![R](_cr.gif) ![:](colon.gif) ![R](_cr.gif) ![-->](longrightarrow.gif) ![R](_cr.gif) ![)](rp.gif) |
5 | | funfn 5136 |
. . . . . . . . . . 11
![(](lp.gif) ![R](_cr.gif) ![)](rp.gif) |
6 | 4, 5 | bitr4i 243 |
. . . . . . . . . 10
![(](lp.gif) ![R](_cr.gif) ![:](colon.gif) ![R](_cr.gif) ![-->](longrightarrow.gif) ![R](_cr.gif) ![)](rp.gif) |
7 | 6 | anbi1i 676 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) ![:](colon.gif) ![R](_cr.gif) ![-->](longrightarrow.gif) ![`'](_cnv.gif) ![R](_cr.gif)
![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![)](rp.gif) ![)](rp.gif) |
8 | 1, 7 | bitri 240 |
. . . . . . . 8
![(](lp.gif) ![R](_cr.gif) ![:](colon.gif) ![R](_cr.gif) ![-1-1->](onetoone.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![)](rp.gif) ![)](rp.gif) |
9 | 8 | biimpri 197 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif)
![R](_cr.gif) ![:](colon.gif) ![R](_cr.gif) ![-1-1->](onetoone.gif) ![R](_cr.gif) ![)](rp.gif) |
10 | | sbthlem1.4 |
. . . . . . . . 9
![(](lp.gif)
![G](_cg.gif) ![)](rp.gif) |
11 | | inss1 3475 |
. . . . . . . . . 10
![(](lp.gif) ![G](_cg.gif) ![X](_cx.gif) |
12 | | sstr 3280 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![G](_cg.gif) ![R](_cr.gif) ![(](lp.gif) ![G](_cg.gif) ![R](_cr.gif) ![)](rp.gif) |
13 | 11, 12 | mpan 651 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![G](_cg.gif) ![R](_cr.gif) ![)](rp.gif) |
14 | 10, 13 | syl5eqss 3315 |
. . . . . . . 8
![(](lp.gif) ![R](_cr.gif) ![)](rp.gif) |
15 | 14 | adantr 451 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif)
![X](_cx.gif)
![R](_cr.gif) ![)](rp.gif) |
16 | | f1ores 5300 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) ![:](colon.gif) ![R](_cr.gif) ![-1-1->](onetoone.gif) ![R](_cr.gif) ![(](lp.gif) ![A](_ca.gif) ![)](rp.gif) ![:](colon.gif) ![A](_ca.gif) ![-1-1-onto->](onetooneonto.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
17 | 9, 15, 16 | syl2an 463 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![(](lp.gif) ![A](_ca.gif) ![)](rp.gif) ![:](colon.gif) ![A](_ca.gif) ![-1-1-onto->](onetooneonto.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
18 | | sbthlem1.1 |
. . . . . . . 8
![_V](rmcv.gif) |
19 | | sbthlem1.2 |
. . . . . . . . . 10
![_V](rmcv.gif) |
20 | | sbthlem1.3 |
. . . . . . . . . . 11
Clos1
![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) ![)](rp.gif) ![R](_cr.gif) ![)](rp.gif) |
21 | 18 | rnex 5107 |
. . . . . . . . . . . . 13
![_V](rmcv.gif) |
22 | 19, 21 | difex 4107 |
. . . . . . . . . . . 12
![(](lp.gif) ![R](_cr.gif) ![_V](rmcv.gif) |
23 | 22, 18 | clos1ex 5876 |
. . . . . . . . . . 11
Clos1 ![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) ![)](rp.gif) ![R](_cr.gif)
![_V](rmcv.gif) |
24 | 20, 23 | eqeltri 2423 |
. . . . . . . . . 10
![_V](rmcv.gif) |
25 | 19, 24 | inex 4105 |
. . . . . . . . 9
![(](lp.gif) ![G](_cg.gif) ![_V](rmcv.gif) |
26 | 10, 25 | eqeltri 2423 |
. . . . . . . 8
![_V](rmcv.gif) |
27 | 18, 26 | resex 5117 |
. . . . . . 7
![(](lp.gif) ![A](_ca.gif) ![_V](rmcv.gif) |
28 | 27 | f1oen 6033 |
. . . . . 6
![(](lp.gif) ![(](lp.gif)
![A](_ca.gif) ![)](rp.gif) ![:](colon.gif) ![A](_ca.gif) ![-1-1-onto->](onetooneonto.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif)
![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
29 | 17, 28 | syl 15 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
30 | | sbthlem1.6 |
. . . . . . . . 9
![(](lp.gif) ![G](_cg.gif) ![)](rp.gif) |
31 | 22, 18, 20 | clos1baseima 5883 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![R](_cr.gif)
![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) |
32 | 31 | ineq2i 3454 |
. . . . . . . . 9
![(](lp.gif) ![G](_cg.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![R](_cr.gif)
![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
33 | | indi 3501 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![R](_cr.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
34 | | disjdif 3622 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) ![)](rp.gif) ![(/)](varnothing.gif) |
35 | 34 | uneq1i 3414 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
36 | | uncom 3408 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![)](rp.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
37 | | un0 3575 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![)](rp.gif) ![(/)](varnothing.gif)
![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) |
38 | 36, 37 | eqtri 2373 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) |
39 | 33, 35, 38 | 3eqtri 2377 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) |
40 | 30, 32, 39 | 3eqtri 2377 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) |
41 | | inss2 3476 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![)](rp.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![)](rp.gif) |
42 | 41 | a1i 10 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![)](rp.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) |
43 | 40, 42 | syl5eqss 3315 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) |
44 | | imassrn 5009 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![R](_cr.gif) |
45 | | simprr 733 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![X](_cx.gif) ![)](rp.gif) |
46 | 44, 45 | syl5ss 3283 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![X](_cx.gif) ![)](rp.gif) |
47 | | difss 3393 |
. . . . . . . . . . . . 13
![(](lp.gif) ![R](_cr.gif) ![X](_cx.gif) |
48 | 46, 47 | jctil 523 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
![R](_cr.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![X](_cx.gif) ![)](rp.gif) ![)](rp.gif) |
49 | | unss 3437 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![R](_cr.gif)
![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![X](_cx.gif) ![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![)](rp.gif) ![X](_cx.gif) ![)](rp.gif) |
50 | 48, 49 | sylib 188 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
![R](_cr.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![)](rp.gif) ![X](_cx.gif) ![)](rp.gif) |
51 | 31, 50 | syl5eqss 3315 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![X](_cx.gif) ![)](rp.gif) |
52 | | sseqin2 3474 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![G](_cg.gif)
![G](_cg.gif) ![)](rp.gif) |
53 | 51, 52 | sylib 188 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![(](lp.gif) ![G](_cg.gif) ![G](_cg.gif) ![)](rp.gif) |
54 | 10, 53 | syl5eq 2397 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![G](_cg.gif) ![)](rp.gif) |
55 | 54 | imaeq2d 4942 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) |
56 | 43, 55 | sseqtr4d 3308 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
57 | | ssun2 3427 |
. . . . . . . . . . 11
![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![(](lp.gif) ![(](lp.gif)
![R](_cr.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) |
58 | 57, 31 | sseqtr4i 3304 |
. . . . . . . . . 10
![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif) ![G](_cg.gif) |
59 | 55 | sseq1d 3298 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![G](_cg.gif)
![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) |
60 | 58, 59 | mpbiri 224 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif) ![G](_cg.gif) ![)](rp.gif) |
61 | | imassrn 5009 |
. . . . . . . . 9
![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif) ![R](_cr.gif) |
62 | 60, 61 | jctil 523 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif) ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) |
63 | | ssin 3477 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif) ![G](_cg.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif) ![(](lp.gif) ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) |
64 | 62, 63 | sylib 188 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif) ![(](lp.gif) ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) |
65 | 64, 30 | syl6sseqr 3318 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif) ![C](_cc.gif) ![)](rp.gif) |
66 | 56, 65 | eqssd 3289 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
67 | 29, 66 | breqtrrd 4665 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![C](_cc.gif) ![)](rp.gif) |
68 | | sbthlem1.5 |
. . . . . . 7
![(](lp.gif)
![G](_cg.gif) ![)](rp.gif) |
69 | 19, 24 | difex 4107 |
. . . . . . 7
![(](lp.gif) ![G](_cg.gif) ![_V](rmcv.gif) |
70 | 68, 69 | eqeltri 2423 |
. . . . . 6
![_V](rmcv.gif) |
71 | 70 | enrflx 6035 |
. . . . 5
![B](_cb.gif) |
72 | | difsscompl 3549 |
. . . . . . . . . 10
![(](lp.gif) ![G](_cg.gif) ∼ ![G](_cg.gif) |
73 | 72 | a1i 10 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![(](lp.gif) ![G](_cg.gif) ∼ ![G](_cg.gif) ![)](rp.gif) |
74 | | df-dif 3215 |
. . . . . . . . . . 11
![(](lp.gif) ![G](_cg.gif) ![(](lp.gif) ∼
![G](_cg.gif) ![)](rp.gif) |
75 | 20 | clos1base 5878 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![R](_cr.gif) ![G](_cg.gif) |
76 | | sscon34 3661 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) ∼
∼ ![(](lp.gif) ![R](_cr.gif) ![)](rp.gif) ![)](rp.gif) |
77 | 75, 76 | mpbi 199 |
. . . . . . . . . . . . 13
∼ ∼ ![(](lp.gif) ![R](_cr.gif) ![)](rp.gif) |
78 | | df-dif 3215 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![R](_cr.gif) ![(](lp.gif) ∼ ![R](_cr.gif) ![)](rp.gif) |
79 | 78 | compleqi 3244 |
. . . . . . . . . . . . . 14
∼ ![(](lp.gif) ![R](_cr.gif) ∼ ![(](lp.gif)
∼ ![R](_cr.gif) ![)](rp.gif) |
80 | | iinun 3548 |
. . . . . . . . . . . . . 14
∼ ![(](lp.gif) ∼ ![R](_cr.gif) ∼
∼ ∼ ![R](_cr.gif) ![)](rp.gif) |
81 | | dblcompl 3227 |
. . . . . . . . . . . . . . 15
∼ ∼ ![R](_cr.gif) |
82 | 81 | uneq2i 3415 |
. . . . . . . . . . . . . 14
∼ ∼ ∼ ![R](_cr.gif) ∼ ![R](_cr.gif) ![)](rp.gif) |
83 | 79, 80, 82 | 3eqtri 2377 |
. . . . . . . . . . . . 13
∼ ![(](lp.gif) ![R](_cr.gif) ∼
![R](_cr.gif) ![)](rp.gif) |
84 | 77, 83 | sseqtri 3303 |
. . . . . . . . . . . 12
∼ ∼ ![R](_cr.gif) ![)](rp.gif) |
85 | | sslin 3481 |
. . . . . . . . . . . 12
∼ ∼
![R](_cr.gif)
![(](lp.gif) ∼ ![G](_cg.gif) ![(](lp.gif)
∼ ![R](_cr.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
86 | 84, 85 | ax-mp 5 |
. . . . . . . . . . 11
![(](lp.gif) ∼ ![G](_cg.gif) ![(](lp.gif) ∼ ![R](_cr.gif) ![)](rp.gif) ![)](rp.gif) |
87 | 74, 86 | eqsstri 3301 |
. . . . . . . . . 10
![(](lp.gif) ![G](_cg.gif) ![(](lp.gif) ∼ ![R](_cr.gif) ![)](rp.gif) ![)](rp.gif) |
88 | | indi 3501 |
. . . . . . . . . . . 12
![(](lp.gif)
∼ ![R](_cr.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ∼ ![X](_cx.gif) ![(](lp.gif) ![R](_cr.gif) ![)](rp.gif) ![)](rp.gif) |
89 | | incompl 4073 |
. . . . . . . . . . . . 13
![(](lp.gif) ∼ ![X](_cx.gif) ![(/)](varnothing.gif) |
90 | 89 | uneq1i 3414 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ∼
![X](_cx.gif) ![(](lp.gif) ![R](_cr.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) ![)](rp.gif) ![)](rp.gif) |
91 | | uncom 3408 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![R](_cr.gif)
![(/)](varnothing.gif) ![)](rp.gif) |
92 | | un0 3575 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) ![(/)](varnothing.gif) ![(](lp.gif) ![R](_cr.gif) ![)](rp.gif) |
93 | 91, 92 | eqtri 2373 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) ![)](rp.gif) ![(](lp.gif) ![R](_cr.gif) ![)](rp.gif) |
94 | 88, 90, 93 | 3eqtri 2377 |
. . . . . . . . . . 11
![(](lp.gif)
∼ ![R](_cr.gif) ![)](rp.gif) ![(](lp.gif) ![R](_cr.gif) ![)](rp.gif) |
95 | | inss2 3476 |
. . . . . . . . . . 11
![(](lp.gif) ![R](_cr.gif) ![R](_cr.gif) |
96 | 94, 95 | eqsstri 3301 |
. . . . . . . . . 10
![(](lp.gif)
∼ ![R](_cr.gif) ![)](rp.gif) ![R](_cr.gif) |
97 | 87, 96 | sstri 3281 |
. . . . . . . . 9
![(](lp.gif) ![G](_cg.gif) ![R](_cr.gif) |
98 | 73, 97 | jctil 523 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
![G](_cg.gif) ![(](lp.gif) ![G](_cg.gif) ∼ ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) |
99 | | ssin 3477 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![G](_cg.gif) ![(](lp.gif)
![G](_cg.gif) ∼ ![G](_cg.gif) ![(](lp.gif) ![G](_cg.gif) ![(](lp.gif) ∼
![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) |
100 | 98, 99 | sylib 188 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![(](lp.gif) ![G](_cg.gif) ![(](lp.gif) ∼ ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) |
101 | | sbthlem1.7 |
. . . . . . . 8
![(](lp.gif) ![G](_cg.gif) ![)](rp.gif) |
102 | | df-dif 3215 |
. . . . . . . 8
![(](lp.gif) ![G](_cg.gif) ![(](lp.gif) ∼ ![G](_cg.gif) ![)](rp.gif) |
103 | 101, 102 | eqtri 2373 |
. . . . . . 7
![(](lp.gif) ∼ ![G](_cg.gif) ![)](rp.gif) |
104 | 100, 68, 103 | 3sstr4g 3312 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![D](_cd.gif) ![)](rp.gif) |
105 | | ssdif 3401 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![G](_cg.gif) ![(](lp.gif) ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) |
106 | 45, 105 | syl 15 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![(](lp.gif) ![G](_cg.gif) ![(](lp.gif) ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) |
107 | 106, 101,
68 | 3sstr4g 3312 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![B](_cb.gif) ![)](rp.gif) |
108 | 104, 107 | eqssd 3289 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![D](_cd.gif) ![)](rp.gif) |
109 | 71, 108 | syl5breq 4674 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![D](_cd.gif) ![)](rp.gif) |
110 | 10, 68 | ineq12i 3455 |
. . . . . 6
![(](lp.gif) ![B](_cb.gif) ![(](lp.gif) ![(](lp.gif) ![G](_cg.gif) ![(](lp.gif) ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) |
111 | | inindif 4075 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![G](_cg.gif) ![(](lp.gif) ![G](_cg.gif) ![)](rp.gif)
![(/)](varnothing.gif) |
112 | 110, 111 | eqtri 2373 |
. . . . 5
![(](lp.gif) ![B](_cb.gif) ![(/)](varnothing.gif) |
113 | 30, 101 | ineq12i 3455 |
. . . . . 6
![(](lp.gif) ![D](_cd.gif) ![(](lp.gif) ![(](lp.gif) ![G](_cg.gif)
![(](lp.gif) ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) |
114 | | inindif 4075 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![G](_cg.gif) ![(](lp.gif) ![G](_cg.gif) ![)](rp.gif) ![(/)](varnothing.gif) |
115 | 113, 114 | eqtri 2373 |
. . . . 5
![(](lp.gif) ![D](_cd.gif) ![(/)](varnothing.gif) |
116 | | unen 6048 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![D](_cd.gif) ![(](lp.gif) ![(](lp.gif) ![B](_cb.gif)
![(](lp.gif) ![D](_cd.gif) ![(/)](varnothing.gif) ![)](rp.gif) ![(](lp.gif) ![B](_cb.gif) ![(](lp.gif)
![D](_cd.gif) ![)](rp.gif) ![)](rp.gif) |
117 | 112, 115,
116 | mpanr12 666 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![D](_cd.gif) ![(](lp.gif)
![B](_cb.gif) ![(](lp.gif) ![D](_cd.gif) ![)](rp.gif) ![)](rp.gif) |
118 | 67, 109, 117 | syl2anc 642 |
. . 3
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![(](lp.gif) ![B](_cb.gif) ![(](lp.gif)
![D](_cd.gif) ![)](rp.gif) ![)](rp.gif) |
119 | | ensym 6037 |
. . 3
![(](lp.gif) ![(](lp.gif) ![B](_cb.gif) ![(](lp.gif) ![D](_cd.gif) ![(](lp.gif) ![D](_cd.gif) ![(](lp.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
120 | 118, 119 | sylib 188 |
. 2
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![(](lp.gif) ![D](_cd.gif) ![(](lp.gif)
![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
121 | 30, 101 | uneq12i 3416 |
. . 3
![(](lp.gif) ![D](_cd.gif) ![(](lp.gif) ![(](lp.gif) ![G](_cg.gif) ![(](lp.gif) ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) |
122 | | inundif 3628 |
. . 3
![(](lp.gif) ![(](lp.gif) ![G](_cg.gif) ![(](lp.gif) ![G](_cg.gif) ![)](rp.gif) ![R](_cr.gif) |
123 | 121, 122 | eqtri 2373 |
. 2
![(](lp.gif) ![D](_cd.gif) ![R](_cr.gif) |
124 | 10, 68 | uneq12i 3416 |
. . 3
![(](lp.gif) ![B](_cb.gif) ![(](lp.gif) ![(](lp.gif) ![G](_cg.gif)
![(](lp.gif) ![G](_cg.gif) ![)](rp.gif) ![)](rp.gif) |
125 | | inundif 3628 |
. . 3
![(](lp.gif) ![(](lp.gif) ![G](_cg.gif) ![(](lp.gif) ![G](_cg.gif) ![)](rp.gif) ![X](_cx.gif) |
126 | 124, 125 | eqtri 2373 |
. 2
![(](lp.gif) ![B](_cb.gif) ![X](_cx.gif) |
127 | 120, 123,
126 | 3brtr3g 4670 |
1
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![`'](_cnv.gif) ![R](_cr.gif) ![(](lp.gif)
![X](_cx.gif) ![)](rp.gif)
![X](_cx.gif) ![)](rp.gif) |