Proof of Theorem infxpenlem
Step | Hyp | Ref
| Expression |
1 | | sseq2 3454 |
. . . 4
 
   |
2 | | xpeq12 4853 |
. . . . . 6
 
       |
3 | 2 | anidms 651 |
. . . . 5
       |
4 | | id 22 |
. . . . 5
   |
5 | 3, 4 | breq12d 4415 |
. . . 4
   
     |
6 | 1, 5 | imbi12d 322 |
. . 3
    
 
      |
7 | | sseq2 3454 |
. . . 4
 
   |
8 | | xpeq12 4853 |
. . . . . 6
 
       |
9 | 8 | anidms 651 |
. . . . 5
       |
10 | | id 22 |
. . . . 5
   |
11 | 9, 10 | breq12d 4415 |
. . . 4
   
     |
12 | 7, 11 | imbi12d 322 |
. . 3
    
 
      |
13 | | infxpen.2 |
. . . . . . . 8
      
 
 
    |
14 | | vex 3048 |
. . . . . . . . . . . . 13
 |
15 | 14, 14 | xpex 6595 |
. . . . . . . . . . . 12
   |
16 | | simpll 760 |
. . . . . . . . . . . . . . . . . 18
      
 
 
    |
17 | 13, 16 | sylbi 199 |
. . . . . . . . . . . . . . . . 17
   |
18 | | onss 6617 |
. . . . . . . . . . . . . . . . 17
   |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . . 16

  |
20 | | xpss12 4940 |
. . . . . . . . . . . . . . . 16
 
       |
21 | 19, 19, 20 | syl2anc 667 |
. . . . . . . . . . . . . . 15
  
    |
22 | | leweon.1 |
. . . . . . . . . . . . . . . . 17
   
   
                                  |
23 | | r0weon.1 |
. . . . . . . . . . . . . . . . 17
       
                                                    |
24 | 22, 23 | r0weon 8443 |
. . . . . . . . . . . . . . . 16
  
Se     |
25 | 24 | simpli 460 |
. . . . . . . . . . . . . . 15

  |
26 | | wess 4821 |
. . . . . . . . . . . . . . 15
    
  
     |
27 | 21, 25, 26 | mpisyl 21 |
. . . . . . . . . . . . . 14
     |
28 | | weinxp 4902 |
. . . . . . . . . . . . . 14
  
            |
29 | 27, 28 | sylib 200 |
. . . . . . . . . . . . 13
             |
30 | | infxpen.1 |
. . . . . . . . . . . . . 14
         |
31 | | weeq1 4822 |
. . . . . . . . . . . . . 14
         
 
             |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . . . . . 13
  
            |
33 | 29, 32 | sylibr 216 |
. . . . . . . . . . . 12
     |
34 | | infxpen.4 |
. . . . . . . . . . . . 13
OrdIso      |
35 | 34 | oiiso 8052 |
. . . . . . . . . . . 12
   
          |
36 | 15, 33, 35 | sylancr 669 |
. . . . . . . . . . 11

       |
37 | | isof1o 6216 |
. . . . . . . . . . 11

    
        |
38 | | f1ocnv 5826 |
. . . . . . . . . . 11
                |
39 | | f1of1 5813 |
. . . . . . . . . . 11
                 |
40 | 36, 37, 38, 39 | 4syl 19 |
. . . . . . . . . 10
          |
41 | | f1f1orn 5825 |
. . . . . . . . . 10
                  |
42 | 15 | f1oen 7590 |
. . . . . . . . . 10
              |
43 | 40, 41, 42 | 3syl 18 |
. . . . . . . . 9
  
   |
44 | | f1ofn 5815 |
. . . . . . . . . . 11
        
    |
45 | 36, 37, 38, 44 | 4syl 19 |
. . . . . . . . . 10
 
    |
46 | 36 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
          |
47 | 37, 38, 39 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18

    
         |
48 | | cnvimass 5188 |
. . . . . . . . . . . . . . . . . . 19
        |
49 | | inss2 3653 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
50 | 30, 49 | eqsstri 3462 |
. . . . . . . . . . . . . . . . . . . . 21
       |
51 | | dmss 5034 |
. . . . . . . . . . . . . . . . . . . . 21
      
        |
52 | 50, 51 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
       |
53 | | dmxpid 5054 |
. . . . . . . . . . . . . . . . . . . 20
         |
54 | 52, 53 | sseqtri 3464 |
. . . . . . . . . . . . . . . . . . 19
   |
55 | 48, 54 | sstri 3441 |
. . . . . . . . . . . . . . . . . 18
          |
56 | | f1ores 5828 |
. . . . . . . . . . . . . . . . . 18
                                                      |
57 | 47, 55, 56 | sylancl 668 |
. . . . . . . . . . . . . . . . 17

    
                                   |
58 | 15, 15 | xpex 6595 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
59 | 58 | inex2 4545 |
. . . . . . . . . . . . . . . . . . . . 21
         |
60 | 30, 59 | eqeltri 2525 |
. . . . . . . . . . . . . . . . . . . 20
 |
61 | 60 | cnvex 6740 |
. . . . . . . . . . . . . . . . . . 19
  |
62 | | imaexg 6730 |
. . . . . . . . . . . . . . . . . . 19
           |
63 | 61, 62 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
        |
64 | 63 | f1oen 7590 |
. . . . . . . . . . . . . . . . 17
  
                                                    |
65 | 46, 57, 64 | 3syl 18 |
. . . . . . . . . . . . . . . 16
 
                        |
66 | | sseqin2 3651 |
. . . . . . . . . . . . . . . . . . 19
                              |
67 | 55, 66 | mpbi 212 |
. . . . . . . . . . . . . . . . . 18
                   |
68 | 67 | imaeq2i 5166 |
. . . . . . . . . . . . . . . . 17
                             |
69 | | isocnv 6221 |
. . . . . . . . . . . . . . . . . . . 20

    
         |
70 | 46, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
 
            |
71 | | simpr 463 |
. . . . . . . . . . . . . . . . . . 19
 
       |
72 | | isoini 6229 |
. . . . . . . . . . . . . . . . . . 19
  
                                       |
73 | 70, 71, 72 | syl2anc 667 |
. . . . . . . . . . . . . . . . . 18
 
                                 |
74 | | fvex 5875 |
. . . . . . . . . . . . . . . . . . . . 21
      |
75 | 74 | epini 5198 |
. . . . . . . . . . . . . . . . . . . 20
                |
76 | 75 | ineq2i 3631 |
. . . . . . . . . . . . . . . . . . 19

                   |
77 | 34 | oicl 8044 |
. . . . . . . . . . . . . . . . . . . . 21
 |
78 | | f1of 5814 |
. . . . . . . . . . . . . . . . . . . . . . 23
                 |
79 | 36, 37, 38, 78 | 4syl 19 |
. . . . . . . . . . . . . . . . . . . . . 22
          |
80 | 79 | ffvelrnda 6022 |
. . . . . . . . . . . . . . . . . . . . 21
 
          |
81 | | ordelss 5439 |
. . . . . . . . . . . . . . . . . . . . 21
 
             |
82 | 77, 80, 81 | sylancr 669 |
. . . . . . . . . . . . . . . . . . . 20
 
       
  |
83 | | dfss1 3637 |
. . . . . . . . . . . . . . . . . . . 20
     
              |
84 | 82, 83 | sylib 200 |
. . . . . . . . . . . . . . . . . . 19
 
                 |
85 | 76, 84 | syl5eq 2497 |
. . . . . . . . . . . . . . . . . 18
 
                      |
86 | 73, 85 | eqtrd 2485 |
. . . . . . . . . . . . . . . . 17
 
                          |
87 | 68, 86 | syl5eqr 2499 |
. . . . . . . . . . . . . . . 16
 
                      |
88 | 65, 87 | breqtrd 4427 |
. . . . . . . . . . . . . . 15
 
                 |
89 | 88 | ensymd 7620 |
. . . . . . . . . . . . . 14
 
                 |
90 | | infxpen.3 |
. . . . . . . . . . . . . . . . . . 19
           |
91 | | fvex 5875 |
. . . . . . . . . . . . . . . . . . . 20
     |
92 | | fvex 5875 |
. . . . . . . . . . . . . . . . . . . 20
     |
93 | 91, 92 | unex 6589 |
. . . . . . . . . . . . . . . . . . 19
           |
94 | 90, 93 | eqeltri 2525 |
. . . . . . . . . . . . . . . . . 18
 |
95 | 94 | sucex 6638 |
. . . . . . . . . . . . . . . . 17
 |
96 | 95, 95 | xpex 6595 |
. . . . . . . . . . . . . . . 16
   |
97 | | xpss 4941 |
. . . . . . . . . . . . . . . . . . . 20
  
  |
98 | | simp3 1010 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 
                 |
99 | | vex 3048 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
100 | | vex 3048 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
101 | 100 | eliniseg 5197 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
     |
102 | 99, 101 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
            |
103 | 98, 102 | sylib 200 |
. . . . . . . . . . . . . . . . . . . . 21
 
 
            |
104 | 30 | breqi 4408 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
            |
105 | | brin 4452 |
. . . . . . . . . . . . . . . . . . . . . . 23
          
  
           |
106 | 104, 105 | bitri 253 |
. . . . . . . . . . . . . . . . . . . . . 22
  
  
           |
107 | 106 | simprbi 466 |
. . . . . . . . . . . . . . . . . . . . 21
             |
108 | | brxp 4865 |
. . . . . . . . . . . . . . . . . . . . . 22
        
  
     |
109 | 108 | simplbi 462 |
. . . . . . . . . . . . . . . . . . . . 21
             |
110 | 103, 107,
109 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
 
 
            |
111 | 97, 110 | sseldi 3430 |
. . . . . . . . . . . . . . . . . . 19
 
 
            |
112 | 17 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
 
     |
113 | 112 | 3adant3 1028 |
. . . . . . . . . . . . . . . . . . . . 21
 
 
          |
114 | | xp1st 6823 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
115 | | onelon 5448 |
. . . . . . . . . . . . . . . . . . . . . 22
             |
116 | 114, 115 | sylan2 477 |
. . . . . . . . . . . . . . . . . . . . 21
 
         |
117 | 113, 110,
116 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . 20
 
 
              |
118 | | eloni 5433 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
119 | | elxp7 6826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  
                |
120 | 119 | simprbi 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
               |
121 | | ordunel 6654 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
          
            |
122 | 121 | 3expib 1211 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

                        |
123 | 118, 120,
122 | syl2im 39 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                 |
124 | 112, 71, 123 | sylc 62 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
               |
125 | 90, 124 | syl5eqel 2533 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     |
126 | | simprr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
      
 
 
  
  |
127 | 13, 126 | sylbi 199 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
  |
128 | | simprl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
      
 
 
    |
129 | 13, 128 | sylbi 199 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

  |
130 | | iscard 8409 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    
 
   |
131 | | cardlim 8406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
           |
132 | | sseq2 3454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    
    
   |
133 | | limeq 5435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    
        |
134 | 132, 133 | bibi12d 323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    
 
   
    
     |
135 | 131, 134 | mpbii 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    

   |
136 | 130, 135 | sylbir 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    
   |
137 | 136 | biimpa 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   

   |
138 | 17, 127, 129, 137 | syl21anc 1267 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
139 | 138 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
     |
140 | | limsuc 6676 |
. . . . . . . . . . . . . . . . . . . . . . . 24


   |
141 | 139, 140 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   
   |
142 | 125, 141 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . . 22
 
     |
143 | | onelon 5448 |
. . . . . . . . . . . . . . . . . . . . . 22
  
  |
144 | 112, 142,
143 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . 21
 
     |
145 | 144 | 3adant3 1028 |
. . . . . . . . . . . . . . . . . . . 20
 
 
          |
146 | | ssun1 3597 |
. . . . . . . . . . . . . . . . . . . . 21
               |
147 | 146 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
 
 
           
            |
148 | 106 | simplbi 462 |
. . . . . . . . . . . . . . . . . . . . 21
       |
149 | | df-br 4403 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  
  
  |
150 | 23 | eleq2i 2521 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
          
                                                         |
151 | | opabid 4708 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           
                                                                                                           |
152 | 149, 150,
151 | 3bitri 275 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
   
                                                    |
153 | 152 | simprbi 466 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                                   |
154 | | simpl 459 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                               |
155 | 154 | orim2i 521 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                                                                           |
156 | 153, 155 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                               |
157 | | fvex 5875 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
158 | | fvex 5875 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
159 | 157, 158 | unex 6589 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
160 | 159 | elsuc 5492 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                                                 |
161 | 156, 160 | sylibr 216 |
. . . . . . . . . . . . . . . . . . . . . 22
                         |
162 | | suceq 5488 |
. . . . . . . . . . . . . . . . . . . . . . 23
          
            |
163 | 90, 162 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
164 | 161, 163 | syl6eleqr 2540 |
. . . . . . . . . . . . . . . . . . . . 21
               |
165 | 103, 148,
164 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
 
 
                    |
166 | | ontr2 5470 |
. . . . . . . . . . . . . . . . . . . . 21
                                         |
167 | 166 | imp 431 |
. . . . . . . . . . . . . . . . . . . 20
                                         |
168 | 117, 145,
147, 165, 167 | syl22anc 1269 |
. . . . . . . . . . . . . . . . . . 19
 
 
              |
169 | | xp2nd 6824 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
170 | | onelon 5448 |
. . . . . . . . . . . . . . . . . . . . . 22
             |
171 | 169, 170 | sylan2 477 |
. . . . . . . . . . . . . . . . . . . . 21
 
         |
172 | 113, 110,
171 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . 20
 
 
              |
173 | | ssun2 3598 |
. . . . . . . . . . . . . . . . . . . . 21
               |
174 | 173 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
 
 
           
            |
175 | | ontr2 5470 |
. . . . . . . . . . . . . . . . . . . . 21
                                         |
176 | 175 | imp 431 |
. . . . . . . . . . . . . . . . . . . 20
                                         |
177 | 172, 145,
174, 165, 176 | syl22anc 1269 |
. . . . . . . . . . . . . . . . . . 19
 
 
              |
178 | | elxp7 6826 |
. . . . . . . . . . . . . . . . . . . 20
  
                |
179 | 178 | biimpri 210 |
. . . . . . . . . . . . . . . . . . 19
                   |
180 | 111, 168,
177, 179 | syl12anc 1266 |
. . . . . . . . . . . . . . . . . 18
 
 
            |
181 | 180 | 3expia 1210 |
. . . . . . . . . . . . . . . . 17
 
                |
182 | 181 | ssrdv 3438 |
. . . . . . . . . . . . . . . 16
 
              |
183 | | ssdomg 7615 |
. . . . . . . . . . . . . . . 16
                         |
184 | 96, 182, 183 | mpsyl 65 |
. . . . . . . . . . . . . . 15
 
              |
185 | 129 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
     |
186 | | nnfi 7765 |
. . . . . . . . . . . . . . . . . . . 20
   |
187 | | xpfi 7842 |
. . . . . . . . . . . . . . . . . . . . . 22
 
     |
188 | 187 | anidms 651 |
. . . . . . . . . . . . . . . . . . . . 21
     |
189 | | isfinite 8157 |
. . . . . . . . . . . . . . . . . . . . 21
  
    |
190 | 188, 189 | sylib 200 |
. . . . . . . . . . . . . . . . . . . 20
  
  |
191 | 186, 190 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
  
  |
192 | | ssdomg 7615 |
. . . . . . . . . . . . . . . . . . . 20
     |
193 | 14, 192 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19

  |
194 | | sdomdomtr 7705 |
. . . . . . . . . . . . . . . . . . 19
         |
195 | 191, 193,
194 | syl2an 480 |
. . . . . . . . . . . . . . . . . 18
   
   |
196 | 195 | expcom 437 |
. . . . . . . . . . . . . . . . 17

  
   |
197 | 185, 196 | syl 17 |
. . . . . . . . . . . . . . . 16
 
     
   |
198 | 127 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
   
  |
199 | | breq1 4405 |
. . . . . . . . . . . . . . . . . . 19
     |
200 | 199 | rspccv 3147 |
. . . . . . . . . . . . . . . . . 18
 
    |
201 | 198, 142,
200 | sylc 62 |
. . . . . . . . . . . . . . . . 17
 
     |
202 | | omelon 8151 |
. . . . . . . . . . . . . . . . . . 19
 |
203 | | ontri1 5457 |
. . . . . . . . . . . . . . . . . . 19
       |
204 | 202, 144,
203 | sylancr 669 |
. . . . . . . . . . . . . . . . . 18
 
   
   |
205 | | simplr 762 |
. . . . . . . . . . . . . . . . . . . . 21
      
 
 
  

     |
206 | 13, 205 | sylbi 199 |
. . . . . . . . . . . . . . . . . . . 20
    
   |
207 | 206 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
 
   

     |
208 | | sseq2 3454 |
. . . . . . . . . . . . . . . . . . . . 21
     |
209 | | xpeq12 4853 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

      |
210 | 209 | anidms 651 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
211 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22

  |
212 | 210, 211 | breq12d 4415 |
. . . . . . . . . . . . . . . . . . . . 21
         |
213 | 208, 212 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . 20
    
 

     |
214 | 213 | rspccv 3147 |
. . . . . . . . . . . . . . . . . . 19
 
    
       |
215 | 207, 142,
214 | sylc 62 |
. . . . . . . . . . . . . . . . . 18
 
    
    |
216 | 204, 215 | sylbird 239 |
. . . . . . . . . . . . . . . . 17
 
         |
217 | | ensdomtr 7708 |
. . . . . . . . . . . . . . . . . 18
    
    |
218 | 217 | expcom 437 |
. . . . . . . . . . . . . . . . 17
  
      |
219 | 201, 216,
218 | sylsyld 58 |
. . . . . . . . . . . . . . . 16
 
         |
220 | 197, 219 | pm2.61d 162 |
. . . . . . . . . . . . . . 15
 
       |
221 | | domsdomtr 7707 |
. . . . . . . . . . . . . . 15
                       |
222 | 184, 220,
221 | syl2anc 667 |
. . . . . . . . . . . . . 14
 
            |
223 | | ensdomtr 7708 |
. . . . . . . . . . . . . 14
                     
       |
224 | 89, 222, 223 | syl2anc 667 |
. . . . . . . . . . . . 13
 
          |
225 | | ordelon 5447 |
. . . . . . . . . . . . . . 15
 
             |
226 | 77, 80, 225 | sylancr 669 |
. . . . . . . . . . . . . 14
 
          |
227 | | onenon 8383 |
. . . . . . . . . . . . . . 15
   |
228 | 112, 227 | syl 17 |
. . . . . . . . . . . . . 14
 
     |
229 | | cardsdomel 8408 |
. . . . . . . . . . . . . 14
             
            |
230 | 226, 228,
229 | syl2anc 667 |
. . . . . . . . . . . . 13
 
                     |
231 | 224, 230 | mpbid 214 |
. . . . . . . . . . . 12
 
              |
232 | | eleq2 2518 |
. . . . . . . . . . . . . 14
    
                  |
233 | 130, 232 | sylbir 217 |
. . . . . . . . . . . . 13
                      |
234 | 112, 198,
233 | syl2anc 667 |
. . . . . . . . . . . 12
 
                     |
235 | 231, 234 | mpbid 214 |
. . . . . . . . . . 11
 
          |
236 | 235 | ralrimiva 2802 |
. . . . . . . . . 10
            |
237 | | fnfvrnss 6051 |
. . . . . . . . . . 11
  
           
   |
238 | | ssdomg 7615 |
. . . . . . . . . . 11
  

   |
239 | 14, 237, 238 | mpsyl 65 |
. . . . . . . . . 10
  
           
   |
240 | 45, 236, 239 | syl2anc 667 |
. . . . . . . . 9
    |
241 | | endomtr 7627 |
. . . . . . . . 9
   
  
    |
242 | 43, 240, 241 | syl2anc 667 |
. . . . . . . 8
     |
243 | 13, 242 | sylbir 217 |
. . . . . . 7
      
 
 
      |
244 | | df1o2 7194 |
. . . . . . . . . . . 12
   |
245 | | 1onn 7340 |
. . . . . . . . . . . 12
 |
246 | 244, 245 | eqeltrri 2526 |
. . . . . . . . . . 11
   |
247 | | nnsdom 8159 |
. . . . . . . . . . 11
  
    |
248 | | sdomdom 7597 |
. . . . . . . . . . 11
  
 
  |
249 | 246, 247,
248 | mp2b 10 |
. . . . . . . . . 10
   |
250 | | domtr 7622 |
. . . . . . . . . 10
         |
251 | 249, 193,
250 | sylancr 669 |
. . . . . . . . 9

    |
252 | | 0ex 4535 |
. . . . . . . . . . . 12
 |
253 | 14, 252 | xpsnen 7656 |
. . . . . . . . . . 11
     |
254 | 253 | ensymi 7619 |
. . . . . . . . . 10
     |
255 | 14 | xpdom2 7667 |
. . . . . . . . . 10
  
        |
256 | | endomtr 7627 |
. . . . . . . . . 10
            
    |
257 | 254, 255,
256 | sylancr 669 |
. . . . . . . . 9
  
    |
258 | 251, 257 | syl 17 |
. . . . . . . 8

    |
259 | 258 | ad2antrl 734 |
. . . . . . 7
      
 
 
      |
260 | | sbth 7692 |
. . . . . . 7
           |
261 | 243, 259,
260 | syl2anc 667 |
. . . . . 6
      
 
 
      |
262 | 261 | expr 620 |
. . . . 5
      
 

 
     |
263 | | simplr 762 |
. . . . . . . 8
      
 
 
  
  
   |
264 | | simpll 760 |
. . . . . . . . 9
      
 
 
    |
265 | | simprr 766 |
. . . . . . . . 9
      
 
 
  
  |
266 | | rexnal 2836 |
. . . . . . . . . 10
 

  |
267 | | onelss 5465 |
. . . . . . . . . . . . 13
     |
268 | | ssdomg 7615 |
. . . . . . . . . . . . 13
 
   |
269 | 267, 268 | syld 45 |
. . . . . . . . . . . 12
     |
270 | | bren2 7600 |
. . . . . . . . . . . . 13

    |
271 | 270 | simplbi2 631 |
. . . . . . . . . . . 12

    |
272 | 269, 271 | syl6 34 |
. . . . . . . . . . 11
       |
273 | 272 | reximdvai 2859 |
. . . . . . . . . 10
  

   |
274 | 266, 273 | syl5bir 222 |
. . . . . . . . 9
  
    |
275 | 264, 265,
274 | sylc 62 |
. . . . . . . 8
      
 
 
  
  |
276 | | r19.29 2925 |
. . . . . . . 8
     
       

   |
277 | 263, 275,
276 | syl2anc 667 |
. . . . . . 7
      
 
 
  
   

   |
278 | | simprl 764 |
. . . . . . . 8
      
 
 
    |
279 | | onelon 5448 |
. . . . . . . . . . . . . . . . 17
 
   |
280 | | ensym 7618 |
. . . . . . . . . . . . . . . . . 18
   |
281 | | domentr 7628 |
. . . . . . . . . . . . . . . . . 18
     |
282 | 193, 280,
281 | syl2an 480 |
. . . . . . . . . . . . . . . . 17
 
   |
283 | | domnsym 7698 |
. . . . . . . . . . . . . . . . . . 19

  |
284 | | nnsdom 8159 |
. . . . . . . . . . . . . . . . . . 19
   |
285 | 283, 284 | nsyl 125 |
. . . . . . . . . . . . . . . . . 18

  |
286 | | ontri1 5457 |
. . . . . . . . . . . . . . . . . . 19
 
     |
287 | 202, 286 | mpan 676 |
. . . . . . . . . . . . . . . . . 18
 
   |
288 | 285, 287 | syl5ibr 225 |
. . . . . . . . . . . . . . . . 17
 
   |
289 | 279, 282,
288 | syl2im 39 |
. . . . . . . . . . . . . . . 16
 
  

   |
290 | 289 | expd 438 |
. . . . . . . . . . . . . . 15
 
  
    |
291 | 290 | impcom 432 |
. . . . . . . . . . . . . 14
 
  

   |
292 | 291 | imim1d 78 |
. . . . . . . . . . . . 13
 
  
       
    |
293 | 292 | imp32 435 |
. . . . . . . . . . . 12
       
         |
294 | | entr 7621 |
. . . . . . . . . . . . . . . 16
   
  
  |
295 | 294 | ancoms 455 |
. . . . . . . . . . . . . . 15
  

  
  |
296 | | xpen 7735 |
. . . . . . . . . . . . . . . . . 18
    
    |
297 | 296 | anidms 651 |
. . . . . . . . . . . . . . . . 17
       |
298 | | entr 7621 |
. . . . . . . . . . . . . . . . 17
   
      
  |
299 | 297, 298 | sylan 474 |
. . . . . . . . . . . . . . . 16
  

  
  |
300 | 280, 299 | sylan 474 |
. . . . . . . . . . . . . . 15
  

  
  |
301 | 295, 300 | syldan 473 |
. . . . . . . . . . . . . 14
  

  
  |
302 | 301 | ex 436 |
. . . . . . . . . . . . 13
   
     |
303 | 302 | ad2antll 735 |
. . . . . . . . . . . 12
       
             |
304 | 293, 303 | mpd 15 |
. . . . . . . . . . 11
       
         |
305 | 304 | ex 436 |
. . . . . . . . . 10
 
  
    

      |
306 | 305 | expr 620 |
. . . . . . . . 9
 
    
     
    |
307 | 306 | rexlimdv 2877 |
. . . . . . . 8
 
    
         |
308 | 278, 264,
307 | syl2anc 667 |
. . . . . . 7
      
 
 
     
         |
309 | 277, 308 | mpd 15 |
. . . . . 6
      
 
 
   
  |
310 | 309 | expr 620 |
. . . . 5
      
 

 
     |
311 | 262, 310 | pm2.61d 162 |
. . . 4
      
 

    |
312 | 311 | exp31 609 |
. . 3
  
  
   
    |
313 | 6, 12, 312 | tfis3 6684 |
. 2
       |
314 | 313 | imp 431 |
1
       |