Step | Hyp | Ref
| Expression |
1 | | difinfsnlem.f |
. . . . . . . 8
    ⊔      |
2 | | f1f 5422 |
. . . . . . . 8
    ⊔   
  
⊔      |
3 | 1, 2 | syl 14 |
. . . . . . 7
    ⊔      |
4 | | 0lt1o 6441 |
. . . . . . . 8
 |
5 | | djurcl 7051 |
. . . . . . . 8

inr  
⊔    |
6 | 4, 5 | mp1i 10 |
. . . . . . 7
 inr  
⊔    |
7 | 3, 6 | ffvelcdmd 5653 |
. . . . . 6
    inr     |
8 | | difinfsnlem.fb |
. . . . . . 7
    inr     |
9 | | elsni 3611 |
. . . . . . . 8
    inr    
   inr     |
10 | 9 | necon3ai 2396 |
. . . . . . 7
    inr      inr       |
11 | 8, 10 | syl 14 |
. . . . . 6
    inr       |
12 | 7, 11 | eldifd 3140 |
. . . . 5
    inr         |
13 | 12 | ad2antrr 488 |
. . . 4
       inl   
   inr         |
14 | 3 | adantr 276 |
. . . . . . 7
 

  
⊔      |
15 | | djulcl 7050 |
. . . . . . . 8
 inl   ⊔    |
16 | 15 | adantl 277 |
. . . . . . 7
 

inl   ⊔    |
17 | 14, 16 | ffvelcdmd 5653 |
. . . . . 6
 

   inl     |
18 | 17 | adantr 276 |
. . . . 5
       inl       inl     |
19 | | elsni 3611 |
. . . . . . 7
    inl        inl     |
20 | 19 | con3i 632 |
. . . . . 6
    inl  
   inl       |
21 | 20 | adantl 277 |
. . . . 5
       inl       inl       |
22 | 18, 21 | eldifd 3140 |
. . . 4
       inl       inl         |
23 | | difinfsnlem.dc |
. . . . . 6
  
DECID   |
24 | 23 | adantr 276 |
. . . . 5
 



DECID
  |
25 | | difinfsnlem.b |
. . . . . . 7
   |
26 | 25 | adantr 276 |
. . . . . 6
 

  |
27 | | eqeq12 2190 |
. . . . . . . 8
     inl    
   inl      |
28 | 27 | dcbid 838 |
. . . . . . 7
     inl    DECID
DECID    inl      |
29 | 28 | rspc2gv 2854 |
. . . . . 6
     inl     

DECID
DECID    inl      |
30 | 17, 26, 29 | syl2anc 411 |
. . . . 5
 

 

DECID
DECID    inl      |
31 | 24, 30 | mpd 13 |
. . . 4
 

DECID    inl     |
32 | 13, 22, 31 | ifcldadc 3564 |
. . 3
 

     inl       inr       inl          |
33 | 32 | ralrimiva 2550 |
. 2
       inl       inr       inl          |
34 | | simplr 528 |
. . . . . . . . 9
    
 
   inl       inl       inl     |
35 | | simpr 110 |
. . . . . . . . 9
    
 
   inl       inl       inl     |
36 | 34, 35 | eqtr4d 2213 |
. . . . . . . 8
    
 
   inl       inl       inl      inl     |
37 | 1 | ad3antrrr 492 |
. . . . . . . . 9
    
 
   inl       inl       ⊔      |
38 | 15 | ad2antrl 490 |
. . . . . . . . . 10
 
   inl  
⊔    |
39 | 38 | ad2antrr 488 |
. . . . . . . . 9
    
 
   inl       inl    inl  
⊔    |
40 | | simprr 531 |
. . . . . . . . . . 11
 
  
  |
41 | 40 | ad2antrr 488 |
. . . . . . . . . 10
    
 
   inl       inl   
  |
42 | | djulcl 7050 |
. . . . . . . . . 10
 inl   ⊔    |
43 | 41, 42 | syl 14 |
. . . . . . . . 9
    
 
   inl       inl    inl  
⊔    |
44 | | f1veqaeq 5770 |
. . . . . . . . 9
     ⊔   
 inl  
⊔  inl  
⊔   
    inl      inl   inl  inl     |
45 | 37, 39, 43, 44 | syl12anc 1236 |
. . . . . . . 8
    
 
   inl       inl        inl      inl   inl  inl     |
46 | 36, 45 | mpd 13 |
. . . . . . 7
    
 
   inl       inl    inl  inl    |
47 | | inl11 7064 |
. . . . . . . 8
 
  inl  inl 
   |
48 | 47 | ad3antlr 493 |
. . . . . . 7
    
 
   inl       inl     inl  inl 
   |
49 | 46, 48 | mpbid 147 |
. . . . . 6
    
 
   inl       inl   
  |
50 | 49 | a1d 22 |
. . . . 5
    
 
   inl       inl          inl       inr       inl         inl       inr       inl   
   |
51 | 40 | ad2antrr 488 |
. . . . . . . . . 10
    
 
   inl       inl   
  |
52 | | djune 7077 |
. . . . . . . . . . 11
   inl  inr    |
53 | 52 | necomd 2433 |
. . . . . . . . . 10
   inr  inl    |
54 | 51, 4, 53 | sylancl 413 |
. . . . . . . . 9
    
 
   inl       inl   
inr  inl    |
55 | 54 | neneqd 2368 |
. . . . . . . 8
    
 
   inl       inl   
inr 
inl    |
56 | 1 | ad3antrrr 492 |
. . . . . . . . 9
    
 
   inl       inl   
  
⊔      |
57 | 4, 5 | mp1i 10 |
. . . . . . . . 9
    
 
   inl       inl   
inr  
⊔    |
58 | 40, 42 | syl 14 |
. . . . . . . . . 10
 
   inl  
⊔    |
59 | 58 | ad2antrr 488 |
. . . . . . . . 9
    
 
   inl       inl   
inl   ⊔    |
60 | | f1veqaeq 5770 |
. . . . . . . . 9
     ⊔   
 inr  
⊔  inl  
⊔   
    inr      inl   inr  inl     |
61 | 56, 57, 59, 60 | syl12anc 1236 |
. . . . . . . 8
    
 
   inl       inl   
    inr      inl   inr  inl     |
62 | 55, 61 | mtod 663 |
. . . . . . 7
    
 
   inl       inl   
   inr      inl     |
63 | | simplr 528 |
. . . . . . . . 9
    
 
   inl       inl   
   inl     |
64 | 63 | iftrued 3542 |
. . . . . . . 8
    
 
   inl       inl   
     inl       inr       inl       inr     |
65 | | simpr 110 |
. . . . . . . . 9
    
 
   inl       inl   
   inl     |
66 | 65 | iffalsed 3545 |
. . . . . . . 8
    
 
   inl       inl   
     inl       inr       inl       inl     |
67 | 64, 66 | eqeq12d 2192 |
. . . . . . 7
    
 
   inl       inl   
      inl       inr       inl         inl       inr       inl       inr      inl      |
68 | 62, 67 | mtbird 673 |
. . . . . 6
    
 
   inl       inl   
     inl       inr       inl         inl       inr       inl      |
69 | 68 | pm2.21d 619 |
. . . . 5
    
 
   inl       inl   
      inl       inr       inl         inl       inr       inl   
   |
70 | 23 | adantr 276 |
. . . . . . . 8
 
   

DECID   |
71 | 3 | adantr 276 |
. . . . . . . . . 10
 
      ⊔      |
72 | 71, 58 | ffvelcdmd 5653 |
. . . . . . . . 9
 
      inl     |
73 | 25 | adantr 276 |
. . . . . . . . 9
 
  
  |
74 | | eqeq12 2190 |
. . . . . . . . . . 11
     inl    
   inl      |
75 | 74 | dcbid 838 |
. . . . . . . . . 10
     inl    DECID
DECID    inl      |
76 | 75 | rspc2gv 2854 |
. . . . . . . . 9
     inl     

DECID
DECID    inl      |
77 | 72, 73, 76 | syl2anc 411 |
. . . . . . . 8
 
      DECID DECID    inl      |
78 | 70, 77 | mpd 13 |
. . . . . . 7
 
   DECID    inl     |
79 | | exmiddc 836 |
. . . . . . 7
DECID    inl       inl      inl      |
80 | 78, 79 | syl 14 |
. . . . . 6
 
       inl      inl      |
81 | 80 | adantr 276 |
. . . . 5
   
 
   inl        inl      inl      |
82 | 50, 69, 81 | mpjaodan 798 |
. . . 4
   
 
   inl          inl       inr       inl         inl       inr       inl   
   |
83 | | simprl 529 |
. . . . . . . . . . 11
 
  
  |
84 | 83 | ad2antrr 488 |
. . . . . . . . . 10
    
 
   inl       inl   
  |
85 | | djune 7077 |
. . . . . . . . . 10
   inl  inr    |
86 | 84, 4, 85 | sylancl 413 |
. . . . . . . . 9
    
 
   inl       inl   
inl  inr    |
87 | 86 | neneqd 2368 |
. . . . . . . 8
    
 
   inl       inl   
inl  inr    |
88 | 1 | ad3antrrr 492 |
. . . . . . . . 9
    
 
   inl       inl   
  
⊔      |
89 | 38 | ad2antrr 488 |
. . . . . . . . 9
    
 
   inl       inl   
inl   ⊔    |
90 | 4, 5 | mp1i 10 |
. . . . . . . . 9
    
 
   inl       inl   
inr  
⊔    |
91 | | f1veqaeq 5770 |
. . . . . . . . 9
     ⊔   
 inl  
⊔  inr   ⊔        inl      inr   inl  inr     |
92 | 88, 89, 90, 91 | syl12anc 1236 |
. . . . . . . 8
    
 
   inl       inl   
    inl      inr   inl  inr     |
93 | 87, 92 | mtod 663 |
. . . . . . 7
    
 
   inl       inl   
   inl      inr     |
94 | | simplr 528 |
. . . . . . . . 9
    
 
   inl       inl   
   inl     |
95 | 94 | iffalsed 3545 |
. . . . . . . 8
    
 
   inl       inl   
     inl       inr       inl       inl     |
96 | | simpr 110 |
. . . . . . . . 9
    
 
   inl       inl   
   inl     |
97 | 96 | iftrued 3542 |
. . . . . . . 8
    
 
   inl       inl   
     inl       inr       inl       inr     |
98 | 95, 97 | eqeq12d 2192 |
. . . . . . 7
    
 
   inl       inl   
      inl       inr       inl         inl       inr       inl       inl      inr      |
99 | 93, 98 | mtbird 673 |
. . . . . 6
    
 
   inl       inl   
     inl       inr       inl         inl       inr       inl      |
100 | 99 | pm2.21d 619 |
. . . . 5
    
 
   inl       inl   
      inl       inr       inl         inl       inr       inl   
   |
101 | | simplr 528 |
. . . . . . . . 9
    
 
   inl       inl   
   inl     |
102 | 101 | iffalsed 3545 |
. . . . . . . 8
    
 
   inl       inl   
     inl       inr       inl       inl     |
103 | | simpr 110 |
. . . . . . . . 9
    
 
   inl       inl   
   inl     |
104 | 103 | iffalsed 3545 |
. . . . . . . 8
    
 
   inl       inl   
     inl       inr       inl       inl     |
105 | 102, 104 | eqeq12d 2192 |
. . . . . . 7
    
 
   inl       inl   
      inl       inr       inl         inl       inr       inl       inl      inl      |
106 | 1 | ad3antrrr 492 |
. . . . . . . 8
    
 
   inl       inl   
  
⊔      |
107 | 38 | ad2antrr 488 |
. . . . . . . 8
    
 
   inl       inl   
inl   ⊔    |
108 | 58 | ad2antrr 488 |
. . . . . . . 8
    
 
   inl       inl   
inl   ⊔    |
109 | 106, 107,
108, 44 | syl12anc 1236 |
. . . . . . 7
    
 
   inl       inl   
    inl      inl   inl  inl     |
110 | 105, 109 | sylbid 150 |
. . . . . 6
    
 
   inl       inl   
      inl       inr       inl         inl       inr       inl   
inl  inl     |
111 | 47 | ad3antlr 493 |
. . . . . 6
    
 
   inl       inl   
 inl  inl 
   |
112 | 110, 111 | sylibd 149 |
. . . . 5
    
 
   inl       inl   
      inl       inr       inl         inl       inr       inl   
   |
113 | 80 | adantr 276 |
. . . . 5
   
 
   inl   
    inl      inl      |
114 | 100, 112,
113 | mpjaodan 798 |
. . . 4
   
 
   inl   
      inl       inr       inl         inl       inr       inl   
   |
115 | | exmiddc 836 |
. . . . . 6
DECID    inl       inl      inl      |
116 | 31, 115 | syl 14 |
. . . . 5
 

    inl      inl      |
117 | 116 | adantrr 479 |
. . . 4
 
       inl      inl      |
118 | 82, 114, 117 | mpjaodan 798 |
. . 3
 
         inl       inr       inl         inl       inr       inl   
   |
119 | 118 | ralrimivva 2559 |
. 2
         inl       inr       inl         inl       inr       inl   
   |
120 | | difinfsnlem.g |
. . 3
      inl       inr       inl      |
121 | | 2fveq3 5521 |
. . . . 5
    inl      inl     |
122 | 121 | eqeq1d 2186 |
. . . 4
     inl      inl      |
123 | 122, 121 | ifbieq2d 3559 |
. . 3
      inl       inr       inl         inl       inr       inl      |
124 | 120, 123 | f1mpt 5772 |
. 2
                inl       inr       inl       
        inl       inr       inl         inl       inr       inl   
    |
125 | 33, 119, 124 | sylanbrc 417 |
1
           |