Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . . 6
|
2 | | eqid 2622 |
. . . . . 6
|
3 | | eqid 2622 |
. . . . . 6
comp comp |
4 | | setcmon.h |
. . . . . 6
Mono |
5 | | setcmon.u |
. . . . . . 7
|
6 | | setcmon.c |
. . . . . . . 8
|
7 | 6 | setccat 16735 |
. . . . . . 7
|
8 | 5, 7 | syl 17 |
. . . . . 6
|
9 | | setcmon.x |
. . . . . . 7
|
10 | 6, 5 | setcbas 16728 |
. . . . . . 7
|
11 | 9, 10 | eleqtrd 2703 |
. . . . . 6
|
12 | | setcmon.y |
. . . . . . 7
|
13 | 12, 10 | eleqtrd 2703 |
. . . . . 6
|
14 | 1, 2, 3, 4, 8, 11,
13 | monhom 16395 |
. . . . 5
|
15 | 14 | sselda 3603 |
. . . 4
|
16 | 6, 5, 2, 9, 12 | elsetchom 16731 |
. . . . 5
|
17 | 16 | biimpa 501 |
. . . 4
|
18 | 15, 17 | syldan 487 |
. . 3
|
19 | | simprr 796 |
. . . . . . . . . . . 12
|
20 | 19 | sneqd 4189 |
. . . . . . . . . . 11
|
21 | 20 | xpeq2d 5139 |
. . . . . . . . . 10
|
22 | 18 | adantr 481 |
. . . . . . . . . . . 12
|
23 | | ffn 6045 |
. . . . . . . . . . . 12
|
24 | 22, 23 | syl 17 |
. . . . . . . . . . 11
|
25 | | simprll 802 |
. . . . . . . . . . 11
|
26 | | fcoconst 6401 |
. . . . . . . . . . 11
|
27 | 24, 25, 26 | syl2anc 693 |
. . . . . . . . . 10
|
28 | | simprlr 803 |
. . . . . . . . . . 11
|
29 | | fcoconst 6401 |
. . . . . . . . . . 11
|
30 | 24, 28, 29 | syl2anc 693 |
. . . . . . . . . 10
|
31 | 21, 27, 30 | 3eqtr4d 2666 |
. . . . . . . . 9
|
32 | 5 | ad2antrr 762 |
. . . . . . . . . 10
|
33 | 9 | ad2antrr 762 |
. . . . . . . . . 10
|
34 | 12 | ad2antrr 762 |
. . . . . . . . . 10
|
35 | | fconst6g 6094 |
. . . . . . . . . . 11
|
36 | 25, 35 | syl 17 |
. . . . . . . . . 10
|
37 | 6, 32, 3, 33, 33, 34, 36, 22 | setcco 16733 |
. . . . . . . . 9
comp |
38 | | fconst6g 6094 |
. . . . . . . . . . 11
|
39 | 28, 38 | syl 17 |
. . . . . . . . . 10
|
40 | 6, 32, 3, 33, 33, 34, 39, 22 | setcco 16733 |
. . . . . . . . 9
comp |
41 | 31, 37, 40 | 3eqtr4d 2666 |
. . . . . . . 8
comp
comp |
42 | 8 | ad2antrr 762 |
. . . . . . . . 9
|
43 | 11 | ad2antrr 762 |
. . . . . . . . 9
|
44 | 13 | ad2antrr 762 |
. . . . . . . . 9
|
45 | | simplr 792 |
. . . . . . . . 9
|
46 | 6, 32, 2, 33, 33 | elsetchom 16731 |
. . . . . . . . . 10
|
47 | 36, 46 | mpbird 247 |
. . . . . . . . 9
|
48 | 6, 32, 2, 33, 33 | elsetchom 16731 |
. . . . . . . . . 10
|
49 | 39, 48 | mpbird 247 |
. . . . . . . . 9
|
50 | 1, 2, 3, 4, 42, 43, 44, 43, 45, 47, 49 | moni 16396 |
. . . . . . . 8
comp comp |
51 | 41, 50 | mpbid 222 |
. . . . . . 7
|
52 | 51 | fveq1d 6193 |
. . . . . 6
|
53 | | vex 3203 |
. . . . . . . 8
|
54 | 53 | fvconst2 6469 |
. . . . . . 7
|
55 | 25, 54 | syl 17 |
. . . . . 6
|
56 | | vex 3203 |
. . . . . . . 8
|
57 | 56 | fvconst2 6469 |
. . . . . . 7
|
58 | 25, 57 | syl 17 |
. . . . . 6
|
59 | 52, 55, 58 | 3eqtr3d 2664 |
. . . . 5
|
60 | 59 | expr 643 |
. . . 4
|
61 | 60 | ralrimivva 2971 |
. . 3
|
62 | | dff13 6512 |
. . 3
|
63 | 18, 61, 62 | sylanbrc 698 |
. 2
|
64 | | f1f 6101 |
. . . 4
|
65 | 16 | biimpar 502 |
. . . 4
|
66 | 64, 65 | sylan2 491 |
. . 3
|
67 | 10 | adantr 481 |
. . . . . 6
|
68 | 67 | eleq2d 2687 |
. . . . 5
|
69 | 5 | ad2antrr 762 |
. . . . . . . . . . 11
|
70 | | simprl 794 |
. . . . . . . . . . 11
|
71 | 9 | ad2antrr 762 |
. . . . . . . . . . 11
|
72 | 12 | ad2antrr 762 |
. . . . . . . . . . 11
|
73 | | simprrl 804 |
. . . . . . . . . . . 12
|
74 | 6, 69, 2, 70, 71 | elsetchom 16731 |
. . . . . . . . . . . 12
|
75 | 73, 74 | mpbid 222 |
. . . . . . . . . . 11
|
76 | 64 | ad2antlr 763 |
. . . . . . . . . . 11
|
77 | 6, 69, 3, 70, 71, 72, 75, 76 | setcco 16733 |
. . . . . . . . . 10
comp |
78 | | simprrr 805 |
. . . . . . . . . . . 12
|
79 | 6, 69, 2, 70, 71 | elsetchom 16731 |
. . . . . . . . . . . 12
|
80 | 78, 79 | mpbid 222 |
. . . . . . . . . . 11
|
81 | 6, 69, 3, 70, 71, 72, 80, 76 | setcco 16733 |
. . . . . . . . . 10
comp |
82 | 77, 81 | eqeq12d 2637 |
. . . . . . . . 9
comp comp |
83 | | simplr 792 |
. . . . . . . . . . 11
|
84 | | cocan1 6546 |
. . . . . . . . . . 11
|
85 | 83, 75, 80, 84 | syl3anc 1326 |
. . . . . . . . . 10
|
86 | 85 | biimpd 219 |
. . . . . . . . 9
|
87 | 82, 86 | sylbid 230 |
. . . . . . . 8
comp comp |
88 | 87 | anassrs 680 |
. . . . . . 7
comp comp |
89 | 88 | ralrimivva 2971 |
. . . . . 6
comp comp |
90 | 89 | ex 450 |
. . . . 5
comp comp |
91 | 68, 90 | sylbird 250 |
. . . 4
comp comp |
92 | 91 | ralrimiv 2965 |
. . 3
comp comp
|
93 | 1, 2, 3, 4, 8, 11,
13 | ismon2 16394 |
. . . 4
comp comp
|
94 | 93 | adantr 481 |
. . 3
comp comp
|
95 | 66, 92, 94 | mpbir2and 957 |
. 2
|
96 | 63, 95 | impbida 877 |
1
|