Step | Hyp | Ref
| Expression |
1 | | simpl 109 |
. . . . . . 7
         
         
   |
2 | | nninfex 7120 |
. . . . . . . . . 10
ℕ∞  |
3 | | fconstmpt 4674 |
. . . . . . . . . . . . . . 15
       |
4 | | 0nninf 14756 |
. . . . . . . . . . . . . . 15
    ℕ∞ |
5 | 3, 4 | eqeltrri 2251 |
. . . . . . . . . . . . . 14
  ℕ∞ |
6 | 5 | fconst6 5416 |
. . . . . . . . . . . . 13
         ℕ∞ |
7 | 6 | a1i 9 |
. . . . . . . . . . . 12
            ℕ∞ |
8 | | ssel 3150 |
. . . . . . . . . . . . . . . . . 18
   
     |
9 | | elsni 3611 |
. . . . . . . . . . . . . . . . . 18
     |
10 | 8, 9 | syl6 33 |
. . . . . . . . . . . . . . . . 17
   
   |
11 | | ssel 3150 |
. . . . . . . . . . . . . . . . . 18
         |
12 | | elsni 3611 |
. . . . . . . . . . . . . . . . . 18
     |
13 | 11, 12 | syl6 33 |
. . . . . . . . . . . . . . . . 17
       |
14 | 10, 13 | anim12d 335 |
. . . . . . . . . . . . . . . 16
     
     |
15 | | eqtr3 2197 |
. . . . . . . . . . . . . . . 16
     |
16 | 14, 15 | syl6 33 |
. . . . . . . . . . . . . . 15
     
   |
17 | 16 | imp 124 |
. . . . . . . . . . . . . 14
 
  
    |
18 | 17 | a1d 22 |
. . . . . . . . . . . . 13
 
  
                      
   |
19 | 18 | ralrimivva 2559 |
. . . . . . . . . . . 12
    
                    
   |
20 | | dff13 5769 |
. . . . . . . . . . . 12
          ℕ∞
          ℕ∞  
                    
    |
21 | 7, 19, 20 | sylanbrc 417 |
. . . . . . . . . . 11
            ℕ∞ |
22 | | exmidsbthrlem.s |
. . . . . . . . . . . . 13

ℕ∞               |
23 | 22 | peano4nninf 14758 |
. . . . . . . . . . . 12
 ℕ∞ ℕ∞ |
24 | 23 | a1i 9 |
. . . . . . . . . . 11
    ℕ∞ ℕ∞ |
25 | | disj 3472 |
. . . . . . . . . . . . 13
       
          |
26 | 22 | peano3nninf 14759 |
. . . . . . . . . . . . . . . . . . 19
 ℕ∞         |
27 | | eqidd 2178 |
. . . . . . . . . . . . . . . . . . . . 21
   |
28 | 27 | cbvmptv 4100 |
. . . . . . . . . . . . . . . . . . . 20
     |
29 | 28 | neeq2i 2363 |
. . . . . . . . . . . . . . . . . . 19
      
        |
30 | 26, 29 | sylib 122 |
. . . . . . . . . . . . . . . . . 18
 ℕ∞         |
31 | 30 | neneqd 2368 |
. . . . . . . . . . . . . . . . 17
 ℕ∞         |
32 | 31 | nrex 2569 |
. . . . . . . . . . . . . . . 16

ℕ∞        |
33 | | f1dm 5427 |
. . . . . . . . . . . . . . . . . 18
  ℕ∞ ℕ∞
ℕ∞ |
34 | 23, 33 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
ℕ∞ |
35 | | eqcom 2179 |
. . . . . . . . . . . . . . . . 17
  
   
        |
36 | 34, 35 | rexeqbii 2490 |
. . . . . . . . . . . . . . . 16
        
 ℕ∞         |
37 | 32, 36 | mtbir 671 |
. . . . . . . . . . . . . . 15

  
     |
38 | 22 | funmpt2 5256 |
. . . . . . . . . . . . . . . 16
 |
39 | | elrnrexdm 5656 |
. . . . . . . . . . . . . . . 16

  

          |
40 | 38, 39 | ax-mp 5 |
. . . . . . . . . . . . . . 15
  

         |
41 | 37, 40 | mto 662 |
. . . . . . . . . . . . . 14
 
 |
42 | | rnxpss 5061 |
. . . . . . . . . . . . . . . . 17
           |
43 | 42 | sseli 3152 |
. . . . . . . . . . . . . . . 16
      
      |
44 | | elsni 3611 |
. . . . . . . . . . . . . . . 16
         |
45 | 43, 44 | syl 14 |
. . . . . . . . . . . . . . 15
      
    |
46 | 45 | eleq1d 2246 |
. . . . . . . . . . . . . 14
      

     |
47 | 41, 46 | mtbiri 675 |
. . . . . . . . . . . . 13
      
  |
48 | 25, 47 | mprgbir 2535 |
. . . . . . . . . . . 12
         |
49 | 48 | a1i 9 |
. . . . . . . . . . 11
         
   |
50 | 21, 24, 49 | casef1 7089 |
. . . . . . . . . 10
   case            ⊔ ℕ∞ ℕ∞ |
51 | | f1domg 6758 |
. . . . . . . . . 10
ℕ∞
case            ⊔
ℕ∞ ℕ∞  ⊔
ℕ∞ ℕ∞  |
52 | 2, 50, 51 | mpsyl 65 |
. . . . . . . . 9
    ⊔ ℕ∞ ℕ∞ |
53 | 52 | adantl 277 |
. . . . . . . 8
         
    ⊔ ℕ∞ ℕ∞ |
54 | | inrresf1 7061 |
. . . . . . . . 9
inr
ℕ∞ ℕ∞  ⊔
ℕ∞ |
55 | | vex 2741 |
. . . . . . . . . . 11
 |
56 | | djuex 7042 |
. . . . . . . . . . 11
  ℕ∞   ⊔
ℕ∞   |
57 | 55, 2, 56 | mp2an 426 |
. . . . . . . . . 10
 ⊔ ℕ∞  |
58 | 57 | f1dom 6760 |
. . . . . . . . 9
 inr ℕ∞ ℕ∞  ⊔
ℕ∞
ℕ∞  ⊔
ℕ∞  |
59 | 54, 58 | ax-mp 5 |
. . . . . . . 8
ℕ∞  ⊔
ℕ∞ |
60 | 53, 59 | jctir 313 |
. . . . . . 7
         
     ⊔
ℕ∞ ℕ∞ ℕ∞  ⊔ ℕ∞   |
61 | | breq12 4009 |
. . . . . . . . . . 11
   ⊔ ℕ∞
ℕ∞
  ⊔
ℕ∞ ℕ∞  |
62 | | breq12 4009 |
. . . . . . . . . . . 12
 
ℕ∞  ⊔ ℕ∞
 ℕ∞  ⊔ ℕ∞   |
63 | 62 | ancoms 268 |
. . . . . . . . . . 11
   ⊔ ℕ∞
ℕ∞
 ℕ∞  ⊔ ℕ∞   |
64 | 61, 63 | anbi12d 473 |
. . . . . . . . . 10
   ⊔ ℕ∞
ℕ∞
  
  ⊔ ℕ∞ ℕ∞ ℕ∞  ⊔ ℕ∞    |
65 | | breq12 4009 |
. . . . . . . . . 10
   ⊔ ℕ∞
ℕ∞

 ⊔
ℕ∞
ℕ∞  |
66 | 64, 65 | imbi12d 234 |
. . . . . . . . 9
   ⊔ ℕ∞
ℕ∞
    
   ⊔
ℕ∞ ℕ∞ ℕ∞  ⊔ ℕ∞  ⊔
ℕ∞
ℕ∞   |
67 | 66 | spc2gv 2829 |
. . . . . . . 8
   ⊔
ℕ∞ ℕ∞         
    ⊔
ℕ∞ ℕ∞ ℕ∞  ⊔ ℕ∞  ⊔
ℕ∞
ℕ∞   |
68 | 57, 2, 67 | mp2an 426 |
. . . . . . 7
            ⊔
ℕ∞ ℕ∞ ℕ∞  ⊔ ℕ∞  ⊔
ℕ∞
ℕ∞  |
69 | 1, 60, 68 | sylc 62 |
. . . . . 6
         
    ⊔ ℕ∞ ℕ∞ |
70 | | bren 6747 |
. . . . . 6
  ⊔ ℕ∞ ℕ∞     ⊔ ℕ∞ ℕ∞ |
71 | 69, 70 | sylib 122 |
. . . . 5
         
       ⊔ ℕ∞ ℕ∞ |
72 | | nninfomni 14771 |
. . . . . . . . 9
ℕ∞ Omni |
73 | 72 | a1i 9 |
. . . . . . . 8
         
       ⊔
ℕ∞ ℕ∞ ℕ∞ Omni |
74 | | f1ocnv 5475 |
. . . . . . . . . 10
    ⊔
ℕ∞ ℕ∞   ℕ∞  ⊔ ℕ∞  |
75 | | f1ofo 5469 |
. . . . . . . . . 10
   ℕ∞  ⊔ ℕ∞   ℕ∞  ⊔ ℕ∞  |
76 | 74, 75 | syl 14 |
. . . . . . . . 9
    ⊔
ℕ∞ ℕ∞   ℕ∞  ⊔
ℕ∞  |
77 | 76 | adantl 277 |
. . . . . . . 8
         
       ⊔
ℕ∞ ℕ∞   ℕ∞  ⊔ ℕ∞  |
78 | 73, 77 | fodjuomni 7147 |
. . . . . . 7
         
       ⊔
ℕ∞ ℕ∞  
   |
79 | | sssnm 3755 |
. . . . . . . . . 10
    
     |
80 | 79 | biimpcd 159 |
. . . . . . . . 9
    
     |
81 | 80 | ad2antlr 489 |
. . . . . . . 8
         
       ⊔
ℕ∞ ℕ∞  
     |
82 | 81 | orim1d 787 |
. . . . . . 7
         
       ⊔
ℕ∞ ℕ∞            |
83 | 78, 82 | mpd 13 |
. . . . . 6
         
       ⊔
ℕ∞ ℕ∞       |
84 | 83 | orcomd 729 |
. . . . 5
         
       ⊔
ℕ∞ ℕ∞       |
85 | 71, 84 | exlimddv 1898 |
. . . 4
         
         |
86 | 85 | ex 115 |
. . 3
         
         |
87 | 86 | alrimiv 1874 |
. 2
                     |
88 | | exmid01 4199 |
. 2
EXMID
            |
89 | 87, 88 | sylibr 134 |
1
        
EXMID |