Step | Hyp | Ref
| Expression |
1 | | issubc.c |
. 2
|
2 | | issubc.s |
. 2
|
3 | | simpl 473 |
. . . . 5
|
4 | | sscpwex 16475 |
. . . . . . . 8
cat f |
5 | | simpl 473 |
. . . . . . . . 9
cat
f comp cat f |
6 | 5 | ss2abi 3674 |
. . . . . . . 8
cat f
comp
cat
f |
7 | 4, 6 | ssexi 4803 |
. . . . . . 7
cat f
comp |
8 | 7 | csbex 4793 |
. . . . . 6
cat
f comp |
9 | 8 | a1i 11 |
. . . . 5
cat f
comp |
10 | | df-subc 16472 |
. . . . . 6
Subcat cat
f comp |
11 | 10 | fvmpts 6285 |
. . . . 5
cat
f comp Subcat cat
f comp |
12 | 3, 9, 11 | syl2anc 693 |
. . . 4
Subcat cat
f comp |
13 | 12 | eleq2d 2687 |
. . 3
Subcat cat f
comp |
14 | | sbcel2 3989 |
. . . 4
cat
f comp
cat
f comp |
15 | 14 | a1i 11 |
. . 3
cat
f comp
cat
f comp |
16 | | elex 3212 |
. . . . . 6
cat f
comp
|
17 | 16 | a1i 11 |
. . . . 5
cat f
comp
|
18 | | sscrel 16473 |
. . . . . . . 8
cat |
19 | 18 | brrelexi 5158 |
. . . . . . 7
cat
|
20 | 19 | adantr 481 |
. . . . . 6
cat
|
21 | 20 | a1i 11 |
. . . . 5
cat
|
22 | | df-sbc 3436 |
. . . . . . 7
cat
f comp cat f
comp |
23 | | simpr 477 |
. . . . . . . 8
|
24 | | simpr 477 |
. . . . . . . . . . 11
|
25 | | simpr 477 |
. . . . . . . . . . . . . 14
|
26 | 25 | fveq2d 6195 |
. . . . . . . . . . . . 13
f f |
27 | | issubc.h |
. . . . . . . . . . . . 13
f |
28 | 26, 27 | syl6eqr 2674 |
. . . . . . . . . . . 12
f |
29 | 28 | adantr 481 |
. . . . . . . . . . 11
f |
30 | 24, 29 | breq12d 4666 |
. . . . . . . . . 10
cat f
cat |
31 | | vex 3203 |
. . . . . . . . . . . . . 14
|
32 | 31 | dmex 7099 |
. . . . . . . . . . . . 13
|
33 | 32 | dmex 7099 |
. . . . . . . . . . . 12
|
34 | 33 | a1i 11 |
. . . . . . . . . . 11
|
35 | 24 | dmeqd 5326 |
. . . . . . . . . . . . 13
|
36 | 35 | dmeqd 5326 |
. . . . . . . . . . . 12
|
37 | | simpllr 799 |
. . . . . . . . . . . 12
|
38 | 36, 37 | eqtr4d 2659 |
. . . . . . . . . . 11
|
39 | | simpr 477 |
. . . . . . . . . . . 12
|
40 | | simpllr 799 |
. . . . . . . . . . . . . . . . 17
|
41 | 40 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
42 | | issubc.i |
. . . . . . . . . . . . . . . 16
|
43 | 41, 42 | syl6eqr 2674 |
. . . . . . . . . . . . . . 15
|
44 | 43 | fveq1d 6193 |
. . . . . . . . . . . . . 14
|
45 | | simplr 792 |
. . . . . . . . . . . . . . 15
|
46 | 45 | oveqd 6667 |
. . . . . . . . . . . . . 14
|
47 | 44, 46 | eleq12d 2695 |
. . . . . . . . . . . . 13
|
48 | 45 | oveqd 6667 |
. . . . . . . . . . . . . . . 16
|
49 | 45 | oveqd 6667 |
. . . . . . . . . . . . . . . . 17
|
50 | 40 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
comp comp |
51 | | issubc.o |
. . . . . . . . . . . . . . . . . . . . 21
comp |
52 | 50, 51 | syl6eqr 2674 |
. . . . . . . . . . . . . . . . . . . 20
comp |
53 | 52 | oveqd 6667 |
. . . . . . . . . . . . . . . . . . 19
comp |
54 | 53 | oveqd 6667 |
. . . . . . . . . . . . . . . . . 18
comp |
55 | 45 | oveqd 6667 |
. . . . . . . . . . . . . . . . . 18
|
56 | 54, 55 | eleq12d 2695 |
. . . . . . . . . . . . . . . . 17
comp
|
57 | 49, 56 | raleqbidv 3152 |
. . . . . . . . . . . . . . . 16
comp
|
58 | 48, 57 | raleqbidv 3152 |
. . . . . . . . . . . . . . 15
comp
|
59 | 39, 58 | raleqbidv 3152 |
. . . . . . . . . . . . . 14
comp
|
60 | 39, 59 | raleqbidv 3152 |
. . . . . . . . . . . . 13
comp
|
61 | 47, 60 | anbi12d 747 |
. . . . . . . . . . . 12
comp
|
62 | 39, 61 | raleqbidv 3152 |
. . . . . . . . . . 11
comp
|
63 | 34, 38, 62 | sbcied2 3473 |
. . . . . . . . . 10
comp
|
64 | 30, 63 | anbi12d 747 |
. . . . . . . . 9
cat
f comp cat
|
65 | 64 | adantlr 751 |
. . . . . . . 8
cat f
comp cat
|
66 | 23, 65 | sbcied 3472 |
. . . . . . 7
cat
f comp cat
|
67 | 22, 66 | syl5bbr 274 |
. . . . . 6
cat
f comp cat |
68 | 67 | ex 450 |
. . . . 5
cat f
comp cat |
69 | 17, 21, 68 | pm5.21ndd 369 |
. . . 4
cat f
comp cat |
70 | 3, 69 | sbcied 3472 |
. . 3
cat
f comp cat |
71 | 13, 15, 70 | 3bitr2d 296 |
. 2
Subcat cat
|
72 | 1, 2, 71 | syl2anc 693 |
1
Subcat
cat |