Proof of Theorem caseinr
Step | Hyp | Ref
| Expression |
1 | | df-case 7077 |
. . . 4
case     inl

inr  |
2 | 1 | fveq1i 5512 |
. . 3
case     inr      inl

inr   inr    |
3 | | caseinr.f |
. . . . . 6
   |
4 | | djulf1o 7051 |
. . . . . . . 8
inl        |
5 | | f1ocnv 5470 |
. . . . . . . 8
inl       inl         |
6 | 4, 5 | ax-mp 5 |
. . . . . . 7
inl        |
7 | | f1ofun 5459 |
. . . . . . 7
 inl       inl |
8 | 6, 7 | ax-mp 5 |
. . . . . 6
inl |
9 | | funco 5252 |
. . . . . 6
  inl
 inl  |
10 | 3, 8, 9 | sylancl 413 |
. . . . 5
  inl  |
11 | | dmco 5133 |
. . . . . . 7

inl   inl   |
12 | | imacnvcnv 5089 |
. . . . . . 7
  inl  inl   |
13 | 11, 12 | eqtri 2198 |
. . . . . 6

inl inl   |
14 | 13 | a1i 9 |
. . . . 5
  inl
inl    |
15 | | df-fn 5215 |
. . . . 5
  inl inl   
inl  inl
inl     |
16 | 10, 14, 15 | sylanbrc 417 |
. . . 4
  inl
inl    |
17 | | caseinr.g |
. . . . . . 7
   |
18 | | fnfun 5309 |
. . . . . . 7
   |
19 | 17, 18 | syl 14 |
. . . . . 6
   |
20 | | djurf1o 7052 |
. . . . . . . 8
inr        |
21 | | f1ocnv 5470 |
. . . . . . . 8
inr      
inr         |
22 | 20, 21 | ax-mp 5 |
. . . . . . 7
inr        |
23 | | f1ofun 5459 |
. . . . . . 7
 inr       inr |
24 | 22, 23 | ax-mp 5 |
. . . . . 6
inr |
25 | | funco 5252 |
. . . . . 6
  inr
 inr  |
26 | 19, 24, 25 | sylancl 413 |
. . . . 5
  inr  |
27 | | dmco 5133 |
. . . . . 6

inr   inr   |
28 | | df-inr 7041 |
. . . . . . . . . . 11
inr   
   |
29 | 28 | funmpt2 5251 |
. . . . . . . . . 10
inr |
30 | | funrel 5229 |
. . . . . . . . . 10
 inr inr |
31 | 29, 30 | ax-mp 5 |
. . . . . . . . 9
inr |
32 | | dfrel2 5075 |
. . . . . . . . 9
 inr  inr inr |
33 | 31, 32 | mpbi 145 |
. . . . . . . 8
 inr inr |
34 | 33 | a1i 9 |
. . . . . . 7
  inr inr |
35 | | fndm 5311 |
. . . . . . . 8
   |
36 | 17, 35 | syl 14 |
. . . . . . 7
   |
37 | 34, 36 | imaeq12d 4967 |
. . . . . 6
   inr  inr    |
38 | 27, 37 | eqtrid 2222 |
. . . . 5
  inr
inr    |
39 | | df-fn 5215 |
. . . . 5
  inr inr  
 inr

inr inr     |
40 | 26, 38, 39 | sylanbrc 417 |
. . . 4
  inr
inr    |
41 | | djuin 7057 |
. . . . 5
 inl  inr    |
42 | 41 | a1i 9 |
. . . 4
  inl  inr     |
43 | | caseinr.a |
. . . . . . . 8
   |
44 | 43 | elexd 2750 |
. . . . . . 7
   |
45 | | f1odm 5461 |
. . . . . . . 8
inr      
inr   |
46 | 20, 45 | ax-mp 5 |
. . . . . . 7
inr  |
47 | 44, 46 | eleqtrrdi 2271 |
. . . . . 6
 inr |
48 | 47, 29 | jctil 312 |
. . . . 5
  inr
inr  |
49 | | funfvima 5743 |
. . . . 5
  inr
inr

inr  inr     |
50 | 48, 43, 49 | sylc 62 |
. . . 4
 inr  inr    |
51 | | fvun2 5579 |
. . . 4
   inl
inl   inr inr    inl  inr   inr  inr       inl  inr   inr     inr  inr     |
52 | 16, 40, 42, 50, 51 | syl112anc 1242 |
. . 3
    inl  inr   inr     inr  inr     |
53 | 2, 52 | eqtrid 2222 |
. 2
 case     inr     inr  inr     |
54 | | f1ofn 5458 |
. . . 4
 inr       inr       |
55 | 22, 54 | ax-mp 5 |
. . 3
inr      |
56 | | f1of 5457 |
. . . . . 6
inr      
inr         |
57 | 20, 56 | ax-mp 5 |
. . . . 5
inr        |
58 | 57 | a1i 9 |
. . . 4
 inr         |
59 | 58, 44 | ffvelcdmd 5648 |
. . 3
 inr        |
60 | | fvco2 5581 |
. . 3
  inr     inr         inr  inr       inr inr      |
61 | 55, 59, 60 | sylancr 414 |
. 2
   inr  inr       inr inr      |
62 | | f1ocnvfv1 5772 |
. . . 4
 inr         inr inr     |
63 | 20, 44, 62 | sylancr 414 |
. . 3
  inr inr     |
64 | 63 | fveq2d 5515 |
. 2
     inr inr          |
65 | 53, 61, 64 | 3eqtrd 2214 |
1
 case     inr         |