Proof of Theorem sbthlem1
Step | Hyp | Ref
| Expression |
1 | | df-f1 4793 |
. . . . . . . . 9
              |
2 | | ssid 3291 |
. . . . . . . . . . . 12
 |
3 | | df-f 4792 |
. . . . . . . . . . . 12
     
   |
4 | 2, 3 | mpbiran2 885 |
. . . . . . . . . . 11
       |
5 | | funfn 5137 |
. . . . . . . . . . 11
   |
6 | 4, 5 | bitr4i 243 |
. . . . . . . . . 10
       |
7 | 6 | anbi1i 676 |
. . . . . . . . 9
       
     |
8 | 1, 7 | bitri 240 |
. . . . . . . 8
          |
9 | 8 | biimpri 197 |
. . . . . . 7
   
      |
10 | | sbthlem1.4 |
. . . . . . . . 9

  |
11 | | inss1 3476 |
. . . . . . . . . 10
   |
12 | | sstr 3281 |
. . . . . . . . . 10
         |
13 | 11, 12 | mpan 651 |
. . . . . . . . 9
     |
14 | 10, 13 | syl5eqss 3316 |
. . . . . . . 8
   |
15 | 14 | adantr 451 |
. . . . . . 7
 

  |
16 | | f1ores 5301 |
. . . . . . 7
                   |
17 | 9, 15, 16 | syl2an 463 |
. . . . . 6
     
 
            |
18 | | sbthlem1.1 |
. . . . . . . 8
 |
19 | | sbthlem1.2 |
. . . . . . . . . 10
 |
20 | | sbthlem1.3 |
. . . . . . . . . . 11
Clos1
      |
21 | 18 | rnex 5108 |
. . . . . . . . . . . . 13
 |
22 | 19, 21 | difex 4108 |
. . . . . . . . . . . 12
   |
23 | 22, 18 | clos1ex 5877 |
. . . . . . . . . . 11
Clos1     
 |
24 | 20, 23 | eqeltri 2423 |
. . . . . . . . . 10
 |
25 | 19, 24 | inex 4106 |
. . . . . . . . 9
   |
26 | 10, 25 | eqeltri 2423 |
. . . . . . . 8
 |
27 | 18, 26 | resex 5118 |
. . . . . . 7
   |
28 | 27 | f1oen 6034 |
. . . . . 6
 
        
      |
29 | 17, 28 | syl 15 |
. . . . 5
     
 
      |
30 | | sbthlem1.6 |
. . . . . . . . 9
   |
31 | 22, 18, 20 | clos1baseima 5884 |
. . . . . . . . . 10
  
      |
32 | 31 | ineq2i 3455 |
. . . . . . . . 9
     
       |
33 | | indi 3502 |
. . . . . . . . . 10
            
 
        |
34 | | disjdif 3623 |
. . . . . . . . . . 11
     |
35 | 34 | uneq1i 3415 |
. . . . . . . . . 10
                     |
36 | | uncom 3409 |
. . . . . . . . . . 11
                 |
37 | | un0 3576 |
. . . . . . . . . . 11
       
       |
38 | 36, 37 | eqtri 2373 |
. . . . . . . . . 10
               |
39 | 33, 35, 38 | 3eqtri 2377 |
. . . . . . . . 9
                 |
40 | 30, 32, 39 | 3eqtri 2377 |
. . . . . . . 8
       |
41 | | inss2 3477 |
. . . . . . . . 9
           |
42 | 41 | a1i 10 |
. . . . . . . 8
     
 
            |
43 | 40, 42 | syl5eqss 3316 |
. . . . . . 7
     
 
      |
44 | | imassrn 5010 |
. . . . . . . . . . . . . 14
     |
45 | | simprr 733 |
. . . . . . . . . . . . . 14
     
 
  |
46 | 44, 45 | syl5ss 3284 |
. . . . . . . . . . . . 13
     
 
      |
47 | | difss 3394 |
. . . . . . . . . . . . 13
   |
48 | 46, 47 | jctil 523 |
. . . . . . . . . . . 12
     
 
 
        |
49 | | unss 3438 |
. . . . . . . . . . . 12
   
               |
50 | 48, 49 | sylib 188 |
. . . . . . . . . . 11
     
 
 
        |
51 | 31, 50 | syl5eqss 3316 |
. . . . . . . . . 10
     
 
  |
52 | | sseqin2 3475 |
. . . . . . . . . 10
  
  |
53 | 51, 52 | sylib 188 |
. . . . . . . . 9
     
 
    |
54 | 10, 53 | syl5eq 2397 |
. . . . . . . 8
     
 
  |
55 | 54 | imaeq2d 4943 |
. . . . . . 7
     
 
          |
56 | 43, 55 | sseqtr4d 3309 |
. . . . . 6
     
 
      |
57 | | ssun2 3428 |
. . . . . . . . . . 11
     
       |
58 | 57, 31 | sseqtr4i 3305 |
. . . . . . . . . 10
     |
59 | 55 | sseq1d 3299 |
. . . . . . . . . 10
     
 
        
   |
60 | 58, 59 | mpbiri 224 |
. . . . . . . . 9
     
 
      |
61 | | imassrn 5010 |
. . . . . . . . 9
     |
62 | 60, 61 | jctil 523 |
. . . . . . . 8
     
 
            |
63 | | ssin 3478 |
. . . . . . . 8
                   |
64 | 62, 63 | sylib 188 |
. . . . . . 7
     
 
        |
65 | 64, 30 | syl6sseqr 3319 |
. . . . . 6
     
 
      |
66 | 56, 65 | eqssd 3290 |
. . . . 5
     
 
      |
67 | 29, 66 | breqtrrd 4666 |
. . . 4
     
 
  |
68 | | sbthlem1.5 |
. . . . . . 7

  |
69 | 19, 24 | difex 4108 |
. . . . . . 7
   |
70 | 68, 69 | eqeltri 2423 |
. . . . . 6
 |
71 | 70 | enrflx 6036 |
. . . . 5
 |
72 | | difsscompl 3550 |
. . . . . . . . . 10
  ∼  |
73 | 72 | a1i 10 |
. . . . . . . . 9
     
 
  ∼   |
74 | | df-dif 3216 |
. . . . . . . . . . 11
   ∼
  |
75 | 20 | clos1base 5879 |
. . . . . . . . . . . . . 14
   |
76 | | sscon34 3662 |
. . . . . . . . . . . . . 14
   ∼
∼     |
77 | 75, 76 | mpbi 199 |
. . . . . . . . . . . . 13
∼ ∼    |
78 | | df-dif 3216 |
. . . . . . . . . . . . . . 15
   ∼   |
79 | 78 | compleqi 3245 |
. . . . . . . . . . . . . 14
∼   ∼ 
∼   |
80 | | iinun 3549 |
. . . . . . . . . . . . . 14
∼  ∼  ∼
∼ ∼   |
81 | | dblcompl 3228 |
. . . . . . . . . . . . . . 15
∼ ∼  |
82 | 81 | uneq2i 3416 |
. . . . . . . . . . . . . 14
∼ ∼ ∼  ∼   |
83 | 79, 80, 82 | 3eqtri 2377 |
. . . . . . . . . . . . 13
∼   ∼
  |
84 | 77, 83 | sseqtri 3304 |
. . . . . . . . . . . 12
∼ ∼   |
85 | | sslin 3482 |
. . . . . . . . . . . 12
∼ ∼

 ∼  
∼     |
86 | 84, 85 | ax-mp 5 |
. . . . . . . . . . 11
 ∼   ∼    |
87 | 74, 86 | eqsstri 3302 |
. . . . . . . . . 10
   ∼    |
88 | | indi 3502 |
. . . . . . . . . . . 12

∼     ∼      |
89 | | incompl 4074 |
. . . . . . . . . . . . 13
 ∼   |
90 | 89 | uneq1i 3415 |
. . . . . . . . . . . 12
  ∼
         |
91 | | uncom 3409 |
. . . . . . . . . . . . 13
      
  |
92 | | un0 3576 |
. . . . . . . . . . . . 13
       |
93 | 91, 92 | eqtri 2373 |
. . . . . . . . . . . 12
       |
94 | 88, 90, 93 | 3eqtri 2377 |
. . . . . . . . . . 11

∼      |
95 | | inss2 3477 |
. . . . . . . . . . 11
   |
96 | 94, 95 | eqsstri 3302 |
. . . . . . . . . 10

∼    |
97 | 87, 96 | sstri 3282 |
. . . . . . . . 9
   |
98 | 73, 97 | jctil 523 |
. . . . . . . 8
     
 
 
   ∼    |
99 | | ssin 3478 |
. . . . . . . 8
    
 ∼     ∼
   |
100 | 98, 99 | sylib 188 |
. . . . . . 7
     
 
   ∼    |
101 | | sbthlem1.7 |
. . . . . . . 8
   |
102 | | df-dif 3216 |
. . . . . . . 8
   ∼   |
103 | 101, 102 | eqtri 2373 |
. . . . . . 7
 ∼   |
104 | 100, 68, 103 | 3sstr4g 3313 |
. . . . . 6
     
 
  |
105 | | ssdif 3402 |
. . . . . . . 8
       |
106 | 45, 105 | syl 15 |
. . . . . . 7
     
 
      |
107 | 106, 101,
68 | 3sstr4g 3313 |
. . . . . 6
     
 
  |
108 | 104, 107 | eqssd 3290 |
. . . . 5
     
 
  |
109 | 71, 108 | syl5breq 4675 |
. . . 4
     
 
  |
110 | 10, 68 | ineq12i 3456 |
. . . . . 6
         |
111 | | inindif 4076 |
. . . . . 6
     
 |
112 | 110, 111 | eqtri 2373 |
. . . . 5
   |
113 | 30, 101 | ineq12i 3456 |
. . . . . 6
    
    |
114 | | inindif 4076 |
. . . . . 6
       |
115 | 113, 114 | eqtri 2373 |
. . . . 5
   |
116 | | unen 6049 |
. . . . 5
      
      
   |
117 | 112, 115,
116 | mpanr12 666 |
. . . 4
   
     |
118 | 67, 109, 117 | syl2anc 642 |
. . 3
     
 
  
   |
119 | | ensym 6038 |
. . 3
           |
120 | 118, 119 | sylib 188 |
. 2
     
 
  
   |
121 | 30, 101 | uneq12i 3417 |
. . 3
         |
122 | | inundif 3629 |
. . 3
       |
123 | 121, 122 | eqtri 2373 |
. 2
   |
124 | 10, 68 | uneq12i 3417 |
. . 3
    
    |
125 | | inundif 3629 |
. . 3
       |
126 | 124, 125 | eqtri 2373 |
. 2
   |
127 | 120, 123,
126 | 3brtr3g 4671 |
1
     
 
  |