Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . 6
 Subcat 
Subcat    |
2 | | eqid 2471 |
. . . . . 6
 f    f    |
3 | 1, 2 | subcssc 15823 |
. . . . 5
 Subcat 
cat  f     |
4 | | subsubc.d |
. . . . . . 7
 cat
  |
5 | | eqid 2471 |
. . . . . . 7
         |
6 | | subcrcl 15799 |
. . . . . . 7
 Subcat 
  |
7 | | id 22 |
. . . . . . . 8
 Subcat 
Subcat    |
8 | | eqidd 2472 |
. . . . . . . 8
 Subcat 
  |
9 | 7, 8 | subcfn 15824 |
. . . . . . 7
 Subcat 

   |
10 | 7, 9, 5 | subcss1 15825 |
. . . . . . 7
 Subcat 
      |
11 | 4, 5, 6, 9, 10 | reschomf 15814 |
. . . . . 6
 Subcat 
 f     |
12 | 11 | breq2d 4407 |
. . . . 5
 Subcat 
 cat cat 
f      |
13 | 3, 12 | syl5ibr 229 |
. . . 4
 Subcat 
 Subcat  cat    |
14 | 13 | pm4.71rd 647 |
. . 3
 Subcat 
 Subcat   cat Subcat      |
15 | | simpr 468 |
. . . . . . . 8
  Subcat  cat 
cat   |
16 | | simpl 464 |
. . . . . . . . 9
  Subcat  cat 
Subcat    |
17 | | eqid 2471 |
. . . . . . . . 9
 f    f    |
18 | 16, 17 | subcssc 15823 |
. . . . . . . 8
  Subcat  cat 
cat  f     |
19 | | ssctr 15808 |
. . . . . . . 8
  cat cat  f    cat 
f     |
20 | 15, 18, 19 | syl2anc 673 |
. . . . . . 7
  Subcat  cat 
cat  f     |
21 | 12 | biimpa 492 |
. . . . . . 7
  Subcat  cat 
cat  f     |
22 | 20, 21 | 2thd 248 |
. . . . . 6
  Subcat  cat 
 cat  f  
cat  f      |
23 | 16 | adantr 472 |
. . . . . . . . 9
   Subcat  cat  
Subcat    |
24 | 9 | adantr 472 |
. . . . . . . . . 10
  Subcat  cat 

   |
25 | 24 | adantr 472 |
. . . . . . . . 9
   Subcat  cat  
    |
26 | | eqid 2471 |
. . . . . . . . 9
         |
27 | | eqidd 2472 |
. . . . . . . . . . . 12
  Subcat  cat 
  |
28 | 15, 27 | sscfn1 15800 |
. . . . . . . . . . 11
  Subcat  cat 

   |
29 | 28, 24, 15 | ssc1 15804 |
. . . . . . . . . 10
  Subcat  cat 
  |
30 | 29 | sselda 3418 |
. . . . . . . . 9
   Subcat  cat  
  |
31 | 4, 23, 25, 26, 30 | subcid 15830 |
. . . . . . . 8
   Subcat  cat                     |
32 | 31 | eleq1d 2533 |
. . . . . . 7
   Subcat  cat                               |
33 | 32 | ralbidva 2828 |
. . . . . 6
  Subcat  cat 
 
            

                |
34 | 4 | oveq1i 6318 |
. . . . . . . 8
 cat    cat
 cat   |
35 | 6 | adantr 472 |
. . . . . . . . 9
  Subcat  cat 
  |
36 | | dmexg 6743 |
. . . . . . . . . . 11
 Subcat 
  |
37 | | dmexg 6743 |
. . . . . . . . . . 11

  |
38 | 36, 37 | syl 17 |
. . . . . . . . . 10
 Subcat 
  |
39 | 38 | adantr 472 |
. . . . . . . . 9
  Subcat  cat 
  |
40 | 35, 24, 28, 39, 29 | rescabs 15816 |
. . . . . . . 8
  Subcat  cat 
  cat  cat
  cat    |
41 | 34, 40 | syl5req 2518 |
. . . . . . 7
  Subcat  cat 
 cat   cat    |
42 | 41 | eleq1d 2533 |
. . . . . 6
  Subcat  cat 
  cat   cat     |
43 | 22, 33, 42 | 3anbi123d 1365 |
. . . . 5
  Subcat  cat 
  cat 
f                 
cat    cat  f   
             
cat      |
44 | | eqid 2471 |
. . . . . 6
 cat   cat   |
45 | 17, 26, 44, 35, 28 | issubc3 15832 |
. . . . 5
  Subcat  cat 
 Subcat   cat 
f                 
cat      |
46 | | eqid 2471 |
. . . . . 6
         |
47 | | eqid 2471 |
. . . . . 6
 cat   cat   |
48 | 4, 7 | subccat 15831 |
. . . . . . 7
 Subcat 
  |
49 | 48 | adantr 472 |
. . . . . 6
  Subcat  cat 
  |
50 | 2, 46, 47, 49, 28 | issubc3 15832 |
. . . . 5
  Subcat  cat 
 Subcat   cat 
f                 
cat      |
51 | 43, 45, 50 | 3bitr4rd 294 |
. . . 4
  Subcat  cat 
 Subcat  Subcat     |
52 | 51 | pm5.32da 653 |
. . 3
 Subcat 
  cat Subcat    cat
Subcat      |
53 | 14, 52 | bitrd 261 |
. 2
 Subcat 
 Subcat   cat Subcat      |
54 | | ancom 457 |
. 2
  cat Subcat    Subcat 
cat
   |
55 | 53, 54 | syl6bb 269 |
1
 Subcat 
 Subcat   Subcat  cat     |