Step | Hyp | Ref
| Expression |
1 | | ctssdccl.s |
. . . 4
     inl    |
2 | | ssrab2 3241 |
. . . 4
     inl  
 |
3 | 1, 2 | eqsstri 3188 |
. . 3
 |
4 | 3 | a1i 9 |
. 2

  |
5 | | djulf1o 7057 |
. . . . . . 7
inl        |
6 | | f1ocnv 5475 |
. . . . . . 7
inl       inl         |
7 | | f1ofun 5464 |
. . . . . . 7
 inl       inl |
8 | 5, 6, 7 | mp2b 8 |
. . . . . 6
inl |
9 | | ctssdccl.f |
. . . . . . 7
      ⊔    |
10 | | fofun 5440 |
. . . . . . 7
      ⊔ 
  |
11 | 9, 10 | syl 14 |
. . . . . 6
   |
12 | | funco 5257 |
. . . . . . 7
  inl

 inl    |
13 | | ctssdccl.g |
. . . . . . . 8
 inl   |
14 | 13 | funeqi 5238 |
. . . . . . 7
  inl    |
15 | 12, 14 | sylibr 134 |
. . . . . 6
  inl

  |
16 | 8, 11, 15 | sylancr 414 |
. . . . 5
   |
17 | | fof 5439 |
. . . . . . . . . . . 12
      ⊔ 
     ⊔
   |
18 | 9, 17 | syl 14 |
. . . . . . . . . . 11
      ⊔    |
19 | 18 | fdmd 5373 |
. . . . . . . . . 10
   |
20 | 19 | eleq2d 2247 |
. . . . . . . . 9
     |
21 | 20 | anbi1d 465 |
. . . . . . . 8
  
    inl
     inl   |
22 | | dmcoss 4897 |
. . . . . . . . . . . 12
 inl   |
23 | 22 | sseli 3152 |
. . . . . . . . . . 11
  inl 
  |
24 | 23 | pm4.71ri 392 |
. . . . . . . . . 10
  inl 
  inl     |
25 | | dmfco 5585 |
. . . . . . . . . . 11
     inl 
    inl  |
26 | 25 | pm5.32da 452 |
. . . . . . . . . 10

 
 inl        inl   |
27 | 24, 26 | bitrid 192 |
. . . . . . . . 9

  inl 
     inl   |
28 | 11, 27 | syl 14 |
. . . . . . . 8
   inl 
     inl   |
29 | | simpr 110 |
. . . . . . . . . . 11
        inl  
    inl    |
30 | | imassrn 4982 |
. . . . . . . . . . . . . 14
inl  inl |
31 | 30 | sseli 3152 |
. . . . . . . . . . . . 13
     inl 
    inl |
32 | 31 | adantl 277 |
. . . . . . . . . . . 12
        inl  
    inl |
33 | | df-rn 4638 |
. . . . . . . . . . . . 13
inl inl |
34 | 33 | eleq2i 2244 |
. . . . . . . . . . . 12
     inl
    inl |
35 | 32, 34 | sylib 122 |
. . . . . . . . . . 11
        inl  
    inl |
36 | 29, 35 | 2thd 175 |
. . . . . . . . . 10
        inl  
     inl      inl  |
37 | | djuin 7063 |
. . . . . . . . . . . . . 14
 inl  inr    |
38 | | disjel 3478 |
. . . . . . . . . . . . . 14
   inl 
inr       inl       inr    |
39 | 37, 38 | mpan 424 |
. . . . . . . . . . . . 13
     inl 
    inr    |
40 | 39 | con2i 627 |
. . . . . . . . . . . 12
     inr 
    inl    |
41 | 40 | adantl 277 |
. . . . . . . . . . 11
        inr  
    inl    |
42 | | djuin 7063 |
. . . . . . . . . . . . . . . 16
 inl  inr    |
43 | | disjel 3478 |
. . . . . . . . . . . . . . . 16
   inl  inr       inl       inr    |
44 | 42, 43 | mpan 424 |
. . . . . . . . . . . . . . 15
     inl 
    inr    |
45 | | dfrn4 5090 |
. . . . . . . . . . . . . . 15
inl inl   |
46 | 44, 45 | eleq2s 2272 |
. . . . . . . . . . . . . 14
     inl
    inr    |
47 | 46 | con2i 627 |
. . . . . . . . . . . . 13
     inr 
    inl |
48 | 47 | adantl 277 |
. . . . . . . . . . . 12
        inr  
    inl |
49 | 48, 34 | sylnib 676 |
. . . . . . . . . . 11
        inr  
    inl |
50 | 41, 49 | 2falsed 702 |
. . . . . . . . . 10
        inr  
     inl      inl  |
51 | 18 | ffvelcdmda 5652 |
. . . . . . . . . . . 12
 

     ⊔    |
52 | | djuun 7066 |
. . . . . . . . . . . . 13
 inl  inr    ⊔
  |
53 | 52 | eleq2i 2244 |
. . . . . . . . . . . 12
      inl  inr  
     ⊔    |
54 | 51, 53 | sylibr 134 |
. . . . . . . . . . 11
 

     inl  inr     |
55 | | elun 3277 |
. . . . . . . . . . 11
      inl  inr  
     inl      inr     |
56 | 54, 55 | sylib 122 |
. . . . . . . . . 10
 

     inl      inr     |
57 | 36, 50, 56 | mpjaodan 798 |
. . . . . . . . 9
 

     inl      inl  |
58 | 57 | pm5.32da 452 |
. . . . . . . 8
  
    inl  
     inl   |
59 | 21, 28, 58 | 3bitr4d 220 |
. . . . . . 7
   inl 
     inl      |
60 | 13 | dmeqi 4829 |
. . . . . . . 8
 inl   |
61 | 60 | eleq2i 2244 |
. . . . . . 7

 inl    |
62 | | fveq2 5516 |
. . . . . . . . 9
           |
63 | 62 | eleq1d 2246 |
. . . . . . . 8
      inl 
    inl     |
64 | 63, 1 | elrab2 2897 |
. . . . . . 7

     inl     |
65 | 59, 61, 64 | 3bitr4g 223 |
. . . . . 6
     |
66 | 65 | eqrdv 2175 |
. . . . 5
   |
67 | | df-fn 5220 |
. . . . 5

    |
68 | 16, 66, 67 | sylanbrc 417 |
. . . 4
   |
69 | 13 | fveq1i 5517 |
. . . . . . 7
      inl      |
70 | 18 | adantr 276 |
. . . . . . . 8
 
      ⊔    |
71 | | fveq2 5516 |
. . . . . . . . . . . . 13
           |
72 | 71 | eleq1d 2246 |
. . . . . . . . . . . 12
      inl 
    inl     |
73 | 72, 1 | elrab2 2897 |
. . . . . . . . . . 11

     inl     |
74 | 73 | biimpi 120 |
. . . . . . . . . 10
      inl     |
75 | 74 | adantl 277 |
. . . . . . . . 9
 
      inl     |
76 | 75 | simpld 112 |
. . . . . . . 8
 
   |
77 | | fvco3 5588 |
. . . . . . . 8
       ⊔ 
   inl
     inl        |
78 | 70, 76, 77 | syl2anc 411 |
. . . . . . 7
 
   inl
     inl        |
79 | 69, 78 | eqtrid 2222 |
. . . . . 6
 
      inl        |
80 | | f1ofun 5464 |
. . . . . . . . . 10
inl      
inl |
81 | 5, 80 | ax-mp 5 |
. . . . . . . . 9
inl |
82 | | fvelima 5568 |
. . . . . . . . 9
  inl
    inl   
inl        |
83 | 81, 82 | mpan 424 |
. . . . . . . 8
     inl 

inl        |
84 | 75, 83 | simpl2im 386 |
. . . . . . 7
 
 
inl        |
85 | | simprr 531 |
. . . . . . . . 9
     inl        inl        |
86 | 85 | fveq2d 5520 |
. . . . . . . 8
     inl         inl inl    inl        |
87 | | vex 2741 |
. . . . . . . . . 10
 |
88 | | f1ocnvfv1 5778 |
. . . . . . . . . 10
 inl      
  inl inl     |
89 | 5, 87, 88 | mp2an 426 |
. . . . . . . . 9
 inl inl    |
90 | | simprl 529 |
. . . . . . . . 9
     inl          |
91 | 89, 90 | eqeltrid 2264 |
. . . . . . . 8
     inl         inl inl     |
92 | 86, 91 | eqeltrrd 2255 |
. . . . . . 7
     inl         inl        |
93 | 84, 92 | rexlimddv 2599 |
. . . . . 6
 
  inl        |
94 | 79, 93 | eqeltrd 2254 |
. . . . 5
 
       |
95 | 94 | ralrimiva 2550 |
. . . 4
        |
96 | | ffnfv 5675 |
. . . 4
    


       |
97 | 68, 95, 96 | sylanbrc 417 |
. . 3
       |
98 | | djulcl 7050 |
. . . . . . . 8
 inl   ⊔    |
99 | | foelrn 5754 |
. . . . . . . . . 10
       ⊔  inl   ⊔   
inl        |
100 | 9, 99 | sylan 283 |
. . . . . . . . 9
 
inl   ⊔    inl        |
101 | | df-rex 2461 |
. . . . . . . . 9
  inl        
inl         |
102 | 100, 101 | sylib 122 |
. . . . . . . 8
 
inl   ⊔      inl         |
103 | 98, 102 | sylan2 286 |
. . . . . . 7
 
    inl         |
104 | | fveq2 5516 |
. . . . . . . . . . . . 13
           |
105 | 104 | eleq1d 2246 |
. . . . . . . . . . . 12
      inl 
    inl     |
106 | | simprl 529 |
. . . . . . . . . . . 12
     inl          |
107 | | simprr 531 |
. . . . . . . . . . . . 13
     inl        inl        |
108 | | vex 2741 |
. . . . . . . . . . . . . . . 16
 |
109 | | f1odm 5466 |
. . . . . . . . . . . . . . . . 17
inl      
inl   |
110 | 5, 109 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
inl  |
111 | 108, 110 | eleqtrri 2253 |
. . . . . . . . . . . . . . 15
inl |
112 | | funfvima 5749 |
. . . . . . . . . . . . . . 15
  inl
inl

inl  inl     |
113 | 81, 111, 112 | mp2an 426 |
. . . . . . . . . . . . . 14
 inl  inl    |
114 | 113 | ad2antlr 489 |
. . . . . . . . . . . . 13
     inl        inl  inl    |
115 | 107, 114 | eqeltrrd 2255 |
. . . . . . . . . . . 12
     inl            inl    |
116 | 105, 106,
115 | elrabd 2896 |
. . . . . . . . . . 11
     inl             inl     |
117 | 116, 1 | eleqtrrdi 2271 |
. . . . . . . . . 10
     inl          |
118 | 117, 107 | jca 306 |
. . . . . . . . 9
     inl         inl         |
119 | 118 | ex 115 |
. . . . . . . 8
 
   inl        inl          |
120 | 119 | eximdv 1880 |
. . . . . . 7
 
    
inl          inl          |
121 | 103, 120 | mpd 13 |
. . . . . 6
 
    inl         |
122 | | df-rex 2461 |
. . . . . 6
  inl         inl         |
123 | 121, 122 | sylibr 134 |
. . . . 5
 
 
inl        |
124 | | f1ocnvfv1 5778 |
. . . . . . . . . 10
 inl      
  inl inl     |
125 | 5, 108, 124 | mp2an 426 |
. . . . . . . . 9
 inl inl    |
126 | | simpr 110 |
. . . . . . . . . 10
   


inl       inl        |
127 | 126 | fveq2d 5520 |
. . . . . . . . 9
   


inl        inl inl    inl        |
128 | 125, 127 | eqtr3id 2224 |
. . . . . . . 8
   


inl        inl        |
129 | 13 | fveq1i 5517 |
. . . . . . . . . 10
      inl      |
130 | 18 | ad2antrr 488 |
. . . . . . . . . . 11
          ⊔    |
131 | 3 | sseli 3152 |
. . . . . . . . . . . 12
   |
132 | 131 | adantl 277 |
. . . . . . . . . . 11
       |
133 | | fvco3 5588 |
. . . . . . . . . . 11
       ⊔ 
   inl
     inl        |
134 | 130, 132,
133 | syl2anc 411 |
. . . . . . . . . 10
       inl
     inl        |
135 | 129, 134 | eqtrid 2222 |
. . . . . . . . 9
          inl        |
136 | 135 | adantr 276 |
. . . . . . . 8
   


inl            inl        |
137 | 128, 136 | eqtr4d 2213 |
. . . . . . 7
   


inl             |
138 | 137 | ex 115 |
. . . . . 6
      inl             |
139 | 138 | reximdva 2579 |
. . . . 5
 
  
inl     

       |
140 | 123, 139 | mpd 13 |
. . . 4
 
 
      |
141 | 140 | ralrimiva 2550 |
. . 3
  
      |
142 | | dffo3 5664 |
. . 3
    
     

       |
143 | 97, 141, 142 | sylanbrc 417 |
. 2
       |
144 | 53, 55 | bitr3i 186 |
. . . . . . 7
      ⊔       inl      inr     |
145 | 51, 144 | sylib 122 |
. . . . . 6
 

     inl      inr     |
146 | 40 | orim2i 761 |
. . . . . 6
      inl      inr  
     inl      inl     |
147 | 145, 146 | syl 14 |
. . . . 5
 

     inl      inl     |
148 | | df-dc 835 |
. . . . 5
DECID     inl       inl      inl     |
149 | 147, 148 | sylibr 134 |
. . . 4
 

DECID     inl    |
150 | | ibar 301 |
. . . . . . 7
      inl 
     inl      |
151 | 150 | adantl 277 |
. . . . . 6
 

     inl       inl      |
152 | 151, 64 | bitr4di 198 |
. . . . 5
 

     inl     |
153 | 152 | dcbid 838 |
. . . 4
 

DECID
    inl 
DECID
   |
154 | 149, 153 | mpbid 147 |
. . 3
 

DECID
  |
155 | 154 | ralrimiva 2550 |
. 2
  DECID   |
156 | 4, 143, 155 | 3jca 1177 |
1
       DECID
   |