Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . 6
 Subcat 
Subcat    |
2 | | eqid 2450 |
. . . . . 6
 f    f    |
3 | 1, 2 | subcssc 15738 |
. . . . 5
 Subcat 
cat  f     |
4 | | subsubc.d |
. . . . . . 7
 cat
  |
5 | | eqid 2450 |
. . . . . . 7
         |
6 | | subcrcl 15714 |
. . . . . . 7
 Subcat 
  |
7 | | id 22 |
. . . . . . . 8
 Subcat 
Subcat    |
8 | | eqidd 2451 |
. . . . . . . 8
 Subcat 
  |
9 | 7, 8 | subcfn 15739 |
. . . . . . 7
 Subcat 

   |
10 | 7, 9, 5 | subcss1 15740 |
. . . . . . 7
 Subcat 
      |
11 | 4, 5, 6, 9, 10 | reschomf 15729 |
. . . . . 6
 Subcat 
 f     |
12 | 11 | breq2d 4413 |
. . . . 5
 Subcat 
 cat cat 
f      |
13 | 3, 12 | syl5ibr 225 |
. . . 4
 Subcat 
 Subcat  cat    |
14 | 13 | pm4.71rd 640 |
. . 3
 Subcat 
 Subcat   cat Subcat      |
15 | | simpr 463 |
. . . . . . . 8
  Subcat  cat 
cat   |
16 | | simpl 459 |
. . . . . . . . 9
  Subcat  cat 
Subcat    |
17 | | eqid 2450 |
. . . . . . . . 9
 f    f    |
18 | 16, 17 | subcssc 15738 |
. . . . . . . 8
  Subcat  cat 
cat  f     |
19 | | ssctr 15723 |
. . . . . . . 8
  cat cat  f    cat 
f     |
20 | 15, 18, 19 | syl2anc 666 |
. . . . . . 7
  Subcat  cat 
cat  f     |
21 | 12 | biimpa 487 |
. . . . . . 7
  Subcat  cat 
cat  f     |
22 | 20, 21 | 2thd 244 |
. . . . . 6
  Subcat  cat 
 cat  f  
cat  f      |
23 | 16 | adantr 467 |
. . . . . . . . 9
   Subcat  cat  
Subcat    |
24 | 9 | adantr 467 |
. . . . . . . . . 10
  Subcat  cat 

   |
25 | 24 | adantr 467 |
. . . . . . . . 9
   Subcat  cat  
    |
26 | | eqid 2450 |
. . . . . . . . 9
         |
27 | | eqidd 2451 |
. . . . . . . . . . . 12
  Subcat  cat 
  |
28 | 15, 27 | sscfn1 15715 |
. . . . . . . . . . 11
  Subcat  cat 

   |
29 | 28, 24, 15 | ssc1 15719 |
. . . . . . . . . 10
  Subcat  cat 
  |
30 | 29 | sselda 3431 |
. . . . . . . . 9
   Subcat  cat  
  |
31 | 4, 23, 25, 26, 30 | subcid 15745 |
. . . . . . . 8
   Subcat  cat                     |
32 | 31 | eleq1d 2512 |
. . . . . . 7
   Subcat  cat                               |
33 | 32 | ralbidva 2823 |
. . . . . 6
  Subcat  cat 
 
            

                |
34 | 4 | oveq1i 6298 |
. . . . . . . 8
 cat    cat
 cat   |
35 | 6 | adantr 467 |
. . . . . . . . 9
  Subcat  cat 
  |
36 | | dmexg 6721 |
. . . . . . . . . . 11
 Subcat 
  |
37 | | dmexg 6721 |
. . . . . . . . . . 11

  |
38 | 36, 37 | syl 17 |
. . . . . . . . . 10
 Subcat 
  |
39 | 38 | adantr 467 |
. . . . . . . . 9
  Subcat  cat 
  |
40 | 35, 24, 28, 39, 29 | rescabs 15731 |
. . . . . . . 8
  Subcat  cat 
  cat  cat
  cat    |
41 | 34, 40 | syl5req 2497 |
. . . . . . 7
  Subcat  cat 
 cat   cat    |
42 | 41 | eleq1d 2512 |
. . . . . 6
  Subcat  cat 
  cat   cat     |
43 | 22, 33, 42 | 3anbi123d 1338 |
. . . . 5
  Subcat  cat 
  cat 
f                 
cat    cat  f   
             
cat      |
44 | | eqid 2450 |
. . . . . 6
 cat   cat   |
45 | 17, 26, 44, 35, 28 | issubc3 15747 |
. . . . 5
  Subcat  cat 
 Subcat   cat 
f                 
cat      |
46 | | eqid 2450 |
. . . . . 6
         |
47 | | eqid 2450 |
. . . . . 6
 cat   cat   |
48 | 4, 7 | subccat 15746 |
. . . . . . 7
 Subcat 
  |
49 | 48 | adantr 467 |
. . . . . 6
  Subcat  cat 
  |
50 | 2, 46, 47, 49, 28 | issubc3 15747 |
. . . . 5
  Subcat  cat 
 Subcat   cat 
f                 
cat      |
51 | 43, 45, 50 | 3bitr4rd 290 |
. . . 4
  Subcat  cat 
 Subcat  Subcat     |
52 | 51 | pm5.32da 646 |
. . 3
 Subcat 
  cat Subcat    cat
Subcat      |
53 | 14, 52 | bitrd 257 |
. 2
 Subcat 
 Subcat   cat Subcat      |
54 | | ancom 452 |
. 2
  cat Subcat    Subcat 
cat
   |
55 | 53, 54 | syl6bb 265 |
1
 Subcat 
 Subcat   Subcat  cat     |