Step | Hyp | Ref
| Expression |
1 | | df-ima 4449 |
. . . 4
inl  inl   |
2 | | inlresf1 6743 |
. . . . 5
inl       ⊔   |
3 | | f1rn 5211 |
. . . . 5
 inl       ⊔  inl  
⊔    |
4 | 2, 3 | ax-mp 7 |
. . . 4
inl   ⊔   |
5 | 1, 4 | eqsstri 3056 |
. . 3
inl   ⊔   |
6 | | df-ima 4449 |
. . . 4
inr  inr   |
7 | | inrresf1 6744 |
. . . . 5
inr       ⊔   |
8 | | f1rn 5211 |
. . . . 5
 inr       ⊔  inr  
⊔    |
9 | 7, 8 | ax-mp 7 |
. . . 4
inr   ⊔   |
10 | 6, 9 | eqsstri 3056 |
. . 3
inr   ⊔   |
11 | 5, 10 | unssi 3175 |
. 2
 inl  inr   
⊔   |
12 | | djur 6747 |
. . . . 5
  ⊔   
inl  
inr     |
13 | | vex 2622 |
. . . . . . . . . 10
 |
14 | | djulf1o 6740 |
. . . . . . . . . . 11
inl        |
15 | | f1odm 5251 |
. . . . . . . . . . 11
inl      
inl   |
16 | 14, 15 | ax-mp 7 |
. . . . . . . . . 10
inl  |
17 | 13, 16 | eleqtrri 2163 |
. . . . . . . . 9
inl |
18 | | simpl 107 |
. . . . . . . . 9
 
inl     |
19 | | df-inl 6729 |
. . . . . . . . . . 11
inl       |
20 | 19 | funmpt2 5047 |
. . . . . . . . . 10
inl |
21 | | funfvima 5518 |
. . . . . . . . . 10
  inl
inl

inl  inl     |
22 | 20, 21 | mpan 415 |
. . . . . . . . 9
 inl
 inl  inl     |
23 | 17, 18, 22 | mpsyl 64 |
. . . . . . . 8
 
inl   inl  inl    |
24 | | eleq1 2150 |
. . . . . . . . 9
 inl 
 inl  inl  inl     |
25 | 24 | adantl 271 |
. . . . . . . 8
 
inl    inl 
inl  inl     |
26 | 23, 25 | mpbird 165 |
. . . . . . 7
 
inl   inl    |
27 | 26 | rexlimiva 2484 |
. . . . . 6
  inl 
inl    |
28 | | djurf1o 6741 |
. . . . . . . . . . 11
inr        |
29 | | f1odm 5251 |
. . . . . . . . . . 11
inr      
inr   |
30 | 28, 29 | ax-mp 7 |
. . . . . . . . . 10
inr  |
31 | 13, 30 | eleqtrri 2163 |
. . . . . . . . 9
inr |
32 | | simpl 107 |
. . . . . . . . 9
 
inr     |
33 | | f1ofun 5249 |
. . . . . . . . . . 11
inr      
inr |
34 | 28, 33 | ax-mp 7 |
. . . . . . . . . 10
inr |
35 | | funfvima 5518 |
. . . . . . . . . 10
  inr
inr

inr  inr     |
36 | 34, 35 | mpan 415 |
. . . . . . . . 9
 inr
 inr  inr     |
37 | 31, 32, 36 | mpsyl 64 |
. . . . . . . 8
 
inr   inr  inr    |
38 | | eleq1 2150 |
. . . . . . . . 9
 inr 
 inr  inr  inr     |
39 | 38 | adantl 271 |
. . . . . . . 8
 
inr    inr 
inr  inr     |
40 | 37, 39 | mpbird 165 |
. . . . . . 7
 
inr   inr    |
41 | 40 | rexlimiva 2484 |
. . . . . 6
  inr 
inr    |
42 | 27, 41 | orim12i 711 |
. . . . 5
  
inl  
inr    inl  inr     |
43 | 12, 42 | syl 14 |
. . . 4
  ⊔   inl  inr     |
44 | | elun 3141 |
. . . 4
  inl  inr  
 inl  inr     |
45 | 43, 44 | sylibr 132 |
. . 3
  ⊔   inl  inr     |
46 | 45 | ssriv 3029 |
. 2
 ⊔   inl  inr    |
47 | 11, 46 | eqssi 3041 |
1
 inl  inr    ⊔
  |