Step | Hyp | Ref
| Expression |
1 | | fthmon.r |
. 2
|
2 | | eqid 2622 |
. . . . . 6
|
3 | | eqid 2622 |
. . . . . 6
|
4 | | eqid 2622 |
. . . . . 6
comp comp |
5 | | fthmon.n |
. . . . . 6
Mono |
6 | | fthmon.f |
. . . . . . . . . . 11
Faith |
7 | | fthfunc 16567 |
. . . . . . . . . . . 12
Faith |
8 | 7 | ssbri 4697 |
. . . . . . . . . . 11
Faith
|
9 | 6, 8 | syl 17 |
. . . . . . . . . 10
|
10 | | df-br 4654 |
. . . . . . . . . 10
|
11 | 9, 10 | sylib 208 |
. . . . . . . . 9
|
12 | | funcrcl 16523 |
. . . . . . . . 9
|
13 | 11, 12 | syl 17 |
. . . . . . . 8
|
14 | 13 | simprd 479 |
. . . . . . 7
|
15 | 14 | adantr 481 |
. . . . . 6
|
16 | | fthmon.b |
. . . . . . . 8
|
17 | 9 | adantr 481 |
. . . . . . . 8
|
18 | 16, 2, 17 | funcf1 16526 |
. . . . . . 7
|
19 | | fthmon.x |
. . . . . . . 8
|
20 | 19 | adantr 481 |
. . . . . . 7
|
21 | 18, 20 | ffvelrnd 6360 |
. . . . . 6
|
22 | | fthmon.y |
. . . . . . . 8
|
23 | 22 | adantr 481 |
. . . . . . 7
|
24 | 18, 23 | ffvelrnd 6360 |
. . . . . 6
|
25 | | simpr1 1067 |
. . . . . . 7
|
26 | 18, 25 | ffvelrnd 6360 |
. . . . . 6
|
27 | | fthmon.1 |
. . . . . . 7
|
28 | 27 | adantr 481 |
. . . . . 6
|
29 | | fthmon.h |
. . . . . . . 8
|
30 | 16, 29, 3, 17, 25, 20 | funcf2 16528 |
. . . . . . 7
|
31 | | simpr2 1068 |
. . . . . . 7
|
32 | 30, 31 | ffvelrnd 6360 |
. . . . . 6
|
33 | | simpr3 1069 |
. . . . . . 7
|
34 | 30, 33 | ffvelrnd 6360 |
. . . . . 6
|
35 | 2, 3, 4, 5, 15, 21, 24, 26, 28, 32, 34 | moni 16396 |
. . . . 5
comp comp |
36 | | eqid 2622 |
. . . . . . . 8
comp comp |
37 | 1 | adantr 481 |
. . . . . . . 8
|
38 | 16, 29, 36, 4, 17, 25, 20, 23, 31, 37 | funcco 16531 |
. . . . . . 7
comp comp |
39 | 16, 29, 36, 4, 17, 25, 20, 23, 33, 37 | funcco 16531 |
. . . . . . 7
comp comp |
40 | 38, 39 | eqeq12d 2637 |
. . . . . 6
comp comp comp comp |
41 | 6 | adantr 481 |
. . . . . . 7
Faith |
42 | 13 | simpld 475 |
. . . . . . . . 9
|
43 | 42 | adantr 481 |
. . . . . . . 8
|
44 | 16, 29, 36, 43, 25, 20, 23, 31, 37 | catcocl 16346 |
. . . . . . 7
comp |
45 | 16, 29, 36, 43, 25, 20, 23, 33, 37 | catcocl 16346 |
. . . . . . 7
comp |
46 | 16, 29, 3, 41, 25, 23, 44, 45 | fthi 16578 |
. . . . . 6
comp comp comp comp |
47 | 40, 46 | bitr3d 270 |
. . . . 5
comp comp comp comp |
48 | 16, 29, 3, 41, 25, 20, 31, 33 | fthi 16578 |
. . . . 5
|
49 | 35, 47, 48 | 3bitr3d 298 |
. . . 4
comp comp |
50 | 49 | biimpd 219 |
. . 3
comp comp
|
51 | 50 | ralrimivvva 2972 |
. 2
comp comp
|
52 | | fthmon.m |
. . 3
Mono |
53 | 16, 29, 36, 52, 42, 19, 22 | ismon2 16394 |
. 2
comp comp |
54 | 1, 51, 53 | mpbir2and 957 |
1
|