Step | Hyp | Ref
| Expression |
1 | | peano4nninf.s |
. . 3

ℕ∞               |
2 | 1 | nnsf 14407 |
. 2
 ℕ∞ ℕ∞ |
3 | | fveq1 5510 |
. . . . . . . . . . 11
           |
4 | | fveq1 5510 |
. . . . . . . . . . 11
           |
5 | 3, 4 | sseq12d 3186 |
. . . . . . . . . 10
             
       |
6 | 5 | ralbidv 2477 |
. . . . . . . . 9
  
                    |
7 | | df-nninf 7113 |
. . . . . . . . 9
ℕ∞   
           |
8 | 6, 7 | elrab2 2896 |
. . . . . . . 8
 ℕ∞    
           |
9 | 8 | simplbi 274 |
. . . . . . 7
 ℕ∞     |
10 | | elmapfn 6665 |
. . . . . . 7
  
  |
11 | 9, 10 | syl 14 |
. . . . . 6
 ℕ∞   |
12 | 11 | ad2antrr 488 |
. . . . 5
  
ℕ∞
ℕ∞            |
13 | | fveq1 5510 |
. . . . . . . . . . 11
           |
14 | | fveq1 5510 |
. . . . . . . . . . 11
           |
15 | 13, 14 | sseq12d 3186 |
. . . . . . . . . 10
             
       |
16 | 15 | ralbidv 2477 |
. . . . . . . . 9
  
                    |
17 | 16, 7 | elrab2 2896 |
. . . . . . . 8
 ℕ∞    
           |
18 | 17 | simplbi 274 |
. . . . . . 7
 ℕ∞     |
19 | | elmapfn 6665 |
. . . . . . 7
  
  |
20 | 18, 19 | syl 14 |
. . . . . 6
 ℕ∞   |
21 | 20 | ad2antlr 489 |
. . . . 5
  
ℕ∞
ℕ∞            |
22 | | simplr 528 |
. . . . . . 7
    ℕ∞
ℕ∞                     |
23 | 22 | fveq1d 5513 |
. . . . . 6
    ℕ∞
ℕ∞                             |
24 | | fveq1 5510 |
. . . . . . . . . . . 12
             |
25 | 24 | ifeq2d 3552 |
. . . . . . . . . . 11
                       |
26 | 25 | mpteq2dv 4091 |
. . . . . . . . . 10
                           |
27 | | omex 4589 |
. . . . . . . . . . 11
 |
28 | 27 | mptex 5738 |
. . . . . . . . . 10
             |
29 | 26, 1, 28 | fvmpt 5589 |
. . . . . . . . 9
 ℕ∞                   |
30 | 29 | ad3antrrr 492 |
. . . . . . . 8
    ℕ∞
ℕ∞                             |
31 | | simpr 110 |
. . . . . . . . . 10
     ℕ∞
ℕ∞              |
32 | 31 | eqeq1d 2186 |
. . . . . . . . 9
     ℕ∞
ℕ∞            
   |
33 | 31 | unieqd 3818 |
. . . . . . . . . 10
     ℕ∞
ℕ∞            
   |
34 | 33 | fveq2d 5515 |
. . . . . . . . 9
     ℕ∞
ℕ∞                        |
35 | 32, 34 | ifbieq2d 3558 |
. . . . . . . 8
     ℕ∞
ℕ∞                                  |
36 | | peano2 4591 |
. . . . . . . . 9

  |
37 | 36 | adantl 277 |
. . . . . . . 8
    ℕ∞
ℕ∞          
  |
38 | | 1lt2o 6437 |
. . . . . . . . . 10
 |
39 | 38 | a1i 9 |
. . . . . . . . 9
    ℕ∞
ℕ∞             |
40 | | nninff 7115 |
. . . . . . . . . . 11
 ℕ∞       |
41 | 40 | ad3antrrr 492 |
. . . . . . . . . 10
    ℕ∞
ℕ∞                 |
42 | | nnpredcl 4619 |
. . . . . . . . . . 11
    |
43 | 37, 42 | syl 14 |
. . . . . . . . . 10
    ℕ∞
ℕ∞           
  |
44 | 41, 43 | ffvelcdmd 5648 |
. . . . . . . . 9
    ℕ∞
ℕ∞                  |
45 | | nndceq0 4614 |
. . . . . . . . . 10
 DECID   |
46 | 37, 45 | syl 14 |
. . . . . . . . 9
    ℕ∞
ℕ∞          
DECID   |
47 | 39, 44, 46 | ifcldcd 3569 |
. . . . . . . 8
    ℕ∞
ℕ∞                       |
48 | 30, 35, 37, 47 | fvmptd 5593 |
. . . . . . 7
    ℕ∞
ℕ∞                               |
49 | | peano3 4592 |
. . . . . . . . . 10
   |
50 | 49 | adantl 277 |
. . . . . . . . 9
    ℕ∞
ℕ∞             |
51 | 50 | neneqd 2368 |
. . . . . . . 8
    ℕ∞
ℕ∞          
  |
52 | 51 | iffalsed 3544 |
. . . . . . 7
    ℕ∞
ℕ∞                            |
53 | | nnord 4608 |
. . . . . . . . . . 11
   |
54 | | ordtr 4375 |
. . . . . . . . . . 11

  |
55 | 53, 54 | syl 14 |
. . . . . . . . . 10
   |
56 | | unisucg 4411 |
. . . . . . . . . 10
 
    |
57 | 55, 56 | mpbid 147 |
. . . . . . . . 9
 
  |
58 | 57 | fveq2d 5515 |
. . . . . . . 8
            |
59 | 58 | adantl 277 |
. . . . . . 7
    ℕ∞
ℕ∞                      |
60 | 48, 52, 59 | 3eqtrd 2214 |
. . . . . 6
    ℕ∞
ℕ∞                         |
61 | | fveq1 5510 |
. . . . . . . . . . . 12
             |
62 | 61 | ifeq2d 3552 |
. . . . . . . . . . 11
                       |
63 | 62 | mpteq2dv 4091 |
. . . . . . . . . 10
                           |
64 | 27 | mptex 5738 |
. . . . . . . . . 10
             |
65 | 63, 1, 64 | fvmpt 5589 |
. . . . . . . . 9
 ℕ∞                   |
66 | 65 | ad3antlr 493 |
. . . . . . . 8
    ℕ∞
ℕ∞                             |
67 | 33 | fveq2d 5515 |
. . . . . . . . 9
     ℕ∞
ℕ∞                        |
68 | 32, 67 | ifbieq2d 3558 |
. . . . . . . 8
     ℕ∞
ℕ∞                                  |
69 | | nninff 7115 |
. . . . . . . . . . 11
 ℕ∞       |
70 | 69 | ad3antlr 493 |
. . . . . . . . . 10
    ℕ∞
ℕ∞                 |
71 | 70, 43 | ffvelcdmd 5648 |
. . . . . . . . 9
    ℕ∞
ℕ∞                  |
72 | 39, 71, 46 | ifcldcd 3569 |
. . . . . . . 8
    ℕ∞
ℕ∞                       |
73 | 66, 68, 37, 72 | fvmptd 5593 |
. . . . . . 7
    ℕ∞
ℕ∞                               |
74 | 51 | iffalsed 3544 |
. . . . . . 7
    ℕ∞
ℕ∞                            |
75 | 57 | fveq2d 5515 |
. . . . . . . 8
            |
76 | 75 | adantl 277 |
. . . . . . 7
    ℕ∞
ℕ∞                      |
77 | 73, 74, 76 | 3eqtrd 2214 |
. . . . . 6
    ℕ∞
ℕ∞                         |
78 | 23, 60, 77 | 3eqtr3d 2218 |
. . . . 5
    ℕ∞
ℕ∞                     |
79 | 12, 21, 78 | eqfnfvd 5612 |
. . . 4
  
ℕ∞
ℕ∞            |
80 | 79 | ex 115 |
. . 3
 
ℕ∞
ℕ∞
            |
81 | 80 | rgen2a 2531 |
. 2
 ℕ∞ 
ℕ∞            |
82 | | dff13 5763 |
. 2
  ℕ∞ ℕ∞
  ℕ∞ ℕ∞ 
ℕ∞ 
ℕ∞              |
83 | 2, 81, 82 | mpbir2an 942 |
1
 ℕ∞ ℕ∞ |