Step | Hyp | Ref
| Expression |
1 | | updjud.a |
. . . . . 6
   |
2 | | updjud.b |
. . . . . 6
   |
3 | 1, 2 | jca 306 |
. . . . 5
 
   |
4 | | djuex 7042 |
. . . . 5
 
  ⊔
   |
5 | | mptexg 5742 |
. . . . 5
  ⊔    ⊔                              |
6 | 3, 4, 5 | 3syl 17 |
. . . 4
   ⊔                              |
7 | | feq1 5349 |
. . . . . . 7
   ⊔
                               ⊔   
  ⊔
                              ⊔
      |
8 | | coeq1 4785 |
. . . . . . . 8
   ⊔
                            inl      ⊔
                           inl     |
9 | 8 | eqeq1d 2186 |
. . . . . . 7
   ⊔
                             inl  
   ⊔                            inl      |
10 | | coeq1 4785 |
. . . . . . . 8
   ⊔
                            inr      ⊔
                           inr     |
11 | 10 | eqeq1d 2186 |
. . . . . . 7
   ⊔
                             inr  
   ⊔                            inr      |
12 | 7, 9, 11 | 3anbi123d 1312 |
. . . . . 6
   ⊔
                                ⊔
    inl    inr       ⊔
                              ⊔
      ⊔                            inl      ⊔                            inr       |
13 | | eqeq1 2184 |
. . . . . . . 8
   ⊔
                              ⊔                               |
14 | 13 | imbi2d 230 |
. . . . . . 7
   ⊔
                                 ⊔     inl    inr    
     ⊔     inl    inr      ⊔
                               |
15 | 14 | ralbidv 2477 |
. . . . . 6
   ⊔
                                  ⊔     inl    inr    
      ⊔     inl    inr      ⊔                                |
16 | 12, 15 | anbi12d 473 |
. . . . 5
   ⊔
                                 ⊔     inl   
inr    
     ⊔     inl    inr     
    ⊔                               ⊔       ⊔
                           inl      ⊔                            inr    
     ⊔     inl    inr      ⊔
                                |
17 | 16 | adantl 277 |
. . . 4
 

 ⊔                                   ⊔     inl   
inr    
     ⊔     inl    inr     
    ⊔                               ⊔       ⊔
                           inl      ⊔                            inr    
     ⊔     inl    inr      ⊔
                                |
18 | | updjud.f |
. . . . . 6
       |
19 | | updjud.g |
. . . . . 6
       |
20 | | eqid 2177 |
. . . . . 6
  ⊔                              ⊔                             |
21 | 18, 19, 20 | updjudhf 7078 |
. . . . 5
   ⊔                               ⊔      |
22 | 18, 19, 20 | updjudhcoinlf 7079 |
. . . . 5
    ⊔
                           inl     |
23 | 18, 19, 20 | updjudhcoinrg 7080 |
. . . . 5
    ⊔
                           inr     |
24 | | simpr 110 |
. . . . . . 7
 
   ⊔                               ⊔       ⊔
                           inl      ⊔                            inr        ⊔
                              ⊔
      ⊔                            inl      ⊔                            inr      |
25 | | eqeq2 2187 |
. . . . . . . . . . . . . . . . . . . . . 22
    ⊔                            inl  
  inl      ⊔                            inl  
 inl      |
26 | | fvres 5540 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  inl     inl    |
27 | 26 | eqcomd 2183 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 inl   inl       |
28 | 27 | eqeq2d 2189 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  inl 
 inl
       |
29 | 28 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      ⊔                            inl    inl   
  inl 
 inl
       |
30 | | fveq1 5515 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    ⊔                            inl    inl       ⊔                            inl        inl        |
31 | 30 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      ⊔                            inl    inl   
     ⊔                            inl        inl        |
32 | | inlresf1 7060 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
inl       ⊔   |
33 | | f1fn 5424 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 inl       ⊔  inl    |
34 | 32, 33 | mp1i 10 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     ⊔
                           inl    inl    inl    |
35 | | fvco2 5586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  inl       ⊔
                           inl         ⊔
                              inl
       |
36 | 34, 35 | sylan 283 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      ⊔                            inl    inl   
     ⊔                            inl         ⊔
                              inl
       |
37 | | fvco2 5586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  inl     inl          inl        |
38 | 34, 37 | sylan 283 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      ⊔                            inl    inl   
   inl          inl        |
39 | 31, 36, 38 | 3eqtr3d 2218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
      ⊔                            inl    inl   
    ⊔
                              inl
         inl
       |
40 | | fveq2 5516 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  inl        ⊔
                                 ⊔                               inl        |
41 | | fveq2 5516 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  inl             inl        |
42 | 40, 41 | eqeq12d 2192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  inl         ⊔                                      ⊔
                              inl
         inl
        |
43 | 39, 42 | syl5ibrcom 157 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      ⊔                            inl    inl   
   inl        ⊔                                      |
44 | 29, 43 | sylbid 150 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      ⊔                            inl    inl   
  inl     ⊔
                                     |
45 | 44 | expimpd 363 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     ⊔
                           inl    inl      inl  
   ⊔                                      |
46 | 45 | ex 115 |
. . . . . . . . . . . . . . . . . . . . . . 23
    ⊔                            inl    inl   
 
inl      ⊔                                       |
47 | 46 | eqcoms 2180 |
. . . . . . . . . . . . . . . . . . . . . 22
  inl      ⊔                            inl   
 
inl      ⊔                                       |
48 | 25, 47 | syl6bir 164 |
. . . . . . . . . . . . . . . . . . . . 21
    ⊔                            inl  
  inl   
 
inl      ⊔                                        |
49 | 48 | com23 78 |
. . . . . . . . . . . . . . . . . . . 20
    ⊔                            inl  
   inl    
inl      ⊔
                                       |
50 | 49 | 3ad2ant2 1019 |
. . . . . . . . . . . . . . . . . . 19
    ⊔                               ⊔       ⊔
                           inl      ⊔                            inr       inl     inl  
   ⊔                                        |
51 | 50 | impcom 125 |
. . . . . . . . . . . . . . . . . 18
 
   ⊔                               ⊔       ⊔
                           inl      ⊔                            inr       inl    
inl      ⊔
                                      |
52 | 51 | com12 30 |
. . . . . . . . . . . . . . . . 17
  inl        ⊔
                              ⊔
      ⊔                            inl      ⊔                            inr       inl  
   ⊔                                       |
53 | 52 | 3ad2ant2 1019 |
. . . . . . . . . . . . . . . 16
     ⊔     inl    inr         ⊔
                              ⊔
      ⊔                            inl      ⊔                            inr       inl  
   ⊔                                       |
54 | 53 | impcom 125 |
. . . . . . . . . . . . . . 15
      ⊔                               ⊔       ⊔
                           inl      ⊔                            inr         ⊔     inl    inr    
 
inl      ⊔                                      |
55 | 54 | com12 30 |
. . . . . . . . . . . . . 14
 
inl         ⊔
                              ⊔
      ⊔                            inl      ⊔                            inr         ⊔     inl    inr    
   ⊔                                      |
56 | 55 | rexlimiva 2589 |
. . . . . . . . . . . . 13
  inl 
  
   ⊔                               ⊔       ⊔
                           inl      ⊔                            inr         ⊔     inl    inr    
   ⊔                                      |
57 | | eqeq2 2187 |
. . . . . . . . . . . . . . . . . . . . . 22
    ⊔                            inr  
  inr      ⊔                            inr  
 inr      |
58 | | fvres 5540 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  inr     inr    |
59 | 58 | eqcomd 2183 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 inr   inr       |
60 | 59 | eqeq2d 2189 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  inr 
 inr
       |
61 | 60 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      ⊔                            inr    inr   
  inr 
 inr
       |
62 | | fveq1 5515 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    ⊔                            inr    inr       ⊔                            inr        inr        |
63 | 62 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      ⊔                            inr    inr   
     ⊔                            inr        inr        |
64 | | inrresf1 7061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
inr       ⊔   |
65 | | f1fn 5424 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 inr       ⊔  inr    |
66 | 64, 65 | mp1i 10 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     ⊔
                           inr    inr    inr    |
67 | | fvco2 5586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  inr       ⊔
                           inr         ⊔
                              inr
       |
68 | 66, 67 | sylan 283 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      ⊔                            inr    inr   
     ⊔                            inr         ⊔
                              inr
       |
69 | | fvco2 5586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  inr     inr          inr        |
70 | 66, 69 | sylan 283 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      ⊔                            inr    inr   
   inr          inr        |
71 | 63, 68, 70 | 3eqtr3d 2218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
      ⊔                            inr    inr   
    ⊔
                              inr
         inr
       |
72 | | fveq2 5516 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  inr        ⊔
                                 ⊔                               inr        |
73 | | fveq2 5516 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  inr             inr        |
74 | 72, 73 | eqeq12d 2192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  inr         ⊔                                      ⊔
                              inr
         inr
        |
75 | 71, 74 | syl5ibrcom 157 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      ⊔                            inr    inr   
   inr        ⊔                                      |
76 | 61, 75 | sylbid 150 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      ⊔                            inr    inr   
  inr     ⊔
                                     |
77 | 76 | expimpd 363 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     ⊔
                           inr    inr      inr  
   ⊔                                      |
78 | 77 | ex 115 |
. . . . . . . . . . . . . . . . . . . . . . 23
    ⊔                            inr    inr   
 
inr      ⊔                                       |
79 | 78 | eqcoms 2180 |
. . . . . . . . . . . . . . . . . . . . . 22
  inr      ⊔                            inr   
 
inr      ⊔                                       |
80 | 57, 79 | syl6bir 164 |
. . . . . . . . . . . . . . . . . . . . 21
    ⊔                            inr  
  inr   
 
inr      ⊔                                        |
81 | 80 | com23 78 |
. . . . . . . . . . . . . . . . . . . 20
    ⊔                            inr  
   inr    
inr      ⊔
                                       |
82 | 81 | 3ad2ant3 1020 |
. . . . . . . . . . . . . . . . . . 19
    ⊔                               ⊔       ⊔
                           inl      ⊔                            inr       inr     inr  
   ⊔                                        |
83 | 82 | impcom 125 |
. . . . . . . . . . . . . . . . . 18
 
   ⊔                               ⊔       ⊔
                           inl      ⊔                            inr       inr    
inr      ⊔
                                      |
84 | 83 | com12 30 |
. . . . . . . . . . . . . . . . 17
  inr        ⊔
                              ⊔
      ⊔                            inl      ⊔                            inr       inr  
   ⊔                                       |
85 | 84 | 3ad2ant3 1020 |
. . . . . . . . . . . . . . . 16
     ⊔     inl    inr         ⊔
                              ⊔
      ⊔                            inl      ⊔                            inr       inr  
   ⊔                                       |
86 | 85 | impcom 125 |
. . . . . . . . . . . . . . 15
      ⊔                               ⊔       ⊔
                           inl      ⊔                            inr         ⊔     inl    inr    
 
inr      ⊔                                      |
87 | 86 | com12 30 |
. . . . . . . . . . . . . 14
 
inr         ⊔
                              ⊔
      ⊔                            inl      ⊔                            inr         ⊔     inl    inr    
   ⊔                                      |
88 | 87 | rexlimiva 2589 |
. . . . . . . . . . . . 13
  inr 
  
   ⊔                               ⊔       ⊔
                           inl      ⊔                            inr         ⊔     inl    inr    
   ⊔                                      |
89 | 56, 88 | jaoi 716 |
. . . . . . . . . . . 12
  
inl  
inr     
   ⊔                               ⊔       ⊔
                           inl      ⊔                            inr         ⊔     inl    inr    
   ⊔                                      |
90 | | djur 7068 |
. . . . . . . . . . . . 13
  ⊔    inl  
inr     |
91 | 90 | biimpi 120 |
. . . . . . . . . . . 12
  ⊔   
inl  
inr     |
92 | 89, 91 | syl11 31 |
. . . . . . . . . . 11
      ⊔                               ⊔       ⊔
                           inl      ⊔                            inr         ⊔     inl    inr    
  ⊔
    ⊔
                                     |
93 | 92 | ralrimiv 2549 |
. . . . . . . . . 10
      ⊔                               ⊔       ⊔
                           inl      ⊔                            inr         ⊔     inl    inr    
  ⊔
     ⊔
                                    |
94 | | ffn 5366 |
. . . . . . . . . . . . 13
   ⊔                               ⊔      ⊔                             ⊔    |
95 | 94 | 3ad2ant1 1018 |
. . . . . . . . . . . 12
    ⊔                               ⊔       ⊔
                           inl      ⊔                            inr      ⊔                             ⊔    |
96 | 95 | adantl 277 |
. . . . . . . . . . 11
 
   ⊔                               ⊔       ⊔
                           inl      ⊔                            inr       ⊔                             ⊔    |
97 | | ffn 5366 |
. . . . . . . . . . . 12
    ⊔   

⊔    |
98 | 97 | 3ad2ant1 1018 |
. . . . . . . . . . 11
     ⊔     inl    inr     ⊔    |
99 | | eqfnfv 5614 |
. . . . . . . . . . 11
    ⊔                             ⊔   ⊔
 
   ⊔                            
 ⊔      ⊔                                      |
100 | 96, 98, 99 | syl2an 289 |
. . . . . . . . . 10
      ⊔                               ⊔       ⊔
                           inl      ⊔                            inr         ⊔     inl    inr    
   ⊔                            
 ⊔      ⊔                                      |
101 | 93, 100 | mpbird 167 |
. . . . . . . . 9
      ⊔                               ⊔       ⊔
                           inl      ⊔                            inr         ⊔     inl    inr    
  ⊔
                             |
102 | 101 | ex 115 |
. . . . . . . 8
 
   ⊔                               ⊔       ⊔
                           inl      ⊔                            inr          ⊔
    inl    inr      ⊔
                              |
103 | 102 | ralrimivw 2551 |
. . . . . . 7
 
   ⊔                               ⊔       ⊔
                           inl      ⊔                            inr     
     ⊔
    inl    inr      ⊔
                              |
104 | 24, 103 | jca 306 |
. . . . . 6
 
   ⊔                               ⊔       ⊔
                           inl      ⊔                            inr         ⊔                               ⊔
      ⊔                            inl      ⊔                            inr    
     ⊔     inl    inr      ⊔
                               |
105 | 104 | ex 115 |
. . . . 5
     ⊔                               ⊔
      ⊔                            inl      ⊔                            inr        ⊔
                              ⊔
      ⊔                            inl      ⊔                            inr    
     ⊔     inl    inr      ⊔
                                |
106 | 21, 22, 23, 105 | mp3and 1340 |
. . . 4
     ⊔                               ⊔
      ⊔                            inl      ⊔                            inr    
     ⊔     inl    inr      ⊔
                               |
107 | 6, 17, 106 | rspcedvd 2848 |
. . 3
       ⊔
    inl    inr          ⊔     inl    inr        |
108 | | feq1 5349 |
. . . . 5
     ⊔   
   ⊔
      |
109 | | coeq1 4785 |
. . . . . 6
  inl    inl     |
110 | 109 | eqeq1d 2186 |
. . . . 5
   inl    inl      |
111 | | coeq1 4785 |
. . . . . 6
  inr    inr     |
112 | 111 | eqeq1d 2186 |
. . . . 5
   inr    inr      |
113 | 108, 110,
112 | 3anbi123d 1312 |
. . . 4
      ⊔    
inl    inr        ⊔     inl    inr       |
114 | 113 | reu8 2934 |
. . 3
      ⊔    
inl    inr    
     ⊔
    inl    inr          ⊔     inl    inr        |
115 | 107, 114 | sylibr 134 |
. 2
      ⊔    
inl    inr      |
116 | | reuv 2757 |
. 2
      ⊔    
inl    inr          ⊔     inl   
inr      |
117 | 115, 116 | sylib 122 |
1
       ⊔     inl   
inr      |