Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . . 6
|
2 | | 1st2ndprf.t |
. . . . . . 7
c |
3 | | eqid 2622 |
. . . . . . 7
|
4 | | eqid 2622 |
. . . . . . 7
|
5 | 2, 3, 4 | xpcbas 16818 |
. . . . . 6
|
6 | | relfunc 16522 |
. . . . . . 7
|
7 | | 1st2ndprf.f |
. . . . . . 7
|
8 | | 1st2ndbr 7217 |
. . . . . . 7
|
9 | 6, 7, 8 | sylancr 695 |
. . . . . 6
|
10 | 1, 5, 9 | funcf1 16526 |
. . . . 5
|
11 | 10 | feqmptd 6249 |
. . . 4
|
12 | 10 | ffvelrnda 6359 |
. . . . . . 7
|
13 | | 1st2nd2 7205 |
. . . . . . 7
|
14 | 12, 13 | syl 17 |
. . . . . 6
|
15 | 7 | adantr 481 |
. . . . . . . . 9
|
16 | | 1st2ndprf.d |
. . . . . . . . . . 11
|
17 | | 1st2ndprf.e |
. . . . . . . . . . 11
|
18 | | eqid 2622 |
. . . . . . . . . . 11
F F |
19 | 2, 16, 17, 18 | 1stfcl 16837 |
. . . . . . . . . 10
F
|
20 | 19 | adantr 481 |
. . . . . . . . 9
F |
21 | | simpr 477 |
. . . . . . . . 9
|
22 | 1, 15, 20, 21 | cofu1 16544 |
. . . . . . . 8
F func
F
|
23 | | eqid 2622 |
. . . . . . . . 9
|
24 | 16 | adantr 481 |
. . . . . . . . 9
|
25 | 17 | adantr 481 |
. . . . . . . . 9
|
26 | 2, 5, 23, 24, 25, 18, 12 | 1stf1 16832 |
. . . . . . . 8
F |
27 | 22, 26 | eqtrd 2656 |
. . . . . . 7
F func
|
28 | | eqid 2622 |
. . . . . . . . . . 11
F F |
29 | 2, 16, 17, 28 | 2ndfcl 16838 |
. . . . . . . . . 10
F
|
30 | 29 | adantr 481 |
. . . . . . . . 9
F |
31 | 1, 15, 30, 21 | cofu1 16544 |
. . . . . . . 8
F func
F
|
32 | 2, 5, 23, 24, 25, 28, 12 | 2ndf1 16835 |
. . . . . . . 8
F |
33 | 31, 32 | eqtrd 2656 |
. . . . . . 7
F func
|
34 | 27, 33 | opeq12d 4410 |
. . . . . 6
F func
F func |
35 | 14, 34 | eqtr4d 2659 |
. . . . 5
F
func F func
|
36 | 35 | mpteq2dva 4744 |
. . . 4
F func F
func |
37 | 11, 36 | eqtrd 2656 |
. . 3
F func F
func |
38 | 1, 9 | funcfn2 16529 |
. . . . 5
|
39 | | fnov 6768 |
. . . . 5
|
40 | 38, 39 | sylib 208 |
. . . 4
|
41 | | eqid 2622 |
. . . . . . . . 9
|
42 | 9 | adantr 481 |
. . . . . . . . 9
|
43 | | simprl 794 |
. . . . . . . . 9
|
44 | | simprr 796 |
. . . . . . . . 9
|
45 | 1, 41, 23, 42, 43, 44 | funcf2 16528 |
. . . . . . . 8
|
46 | 45 | feqmptd 6249 |
. . . . . . 7
|
47 | 2, 23 | relxpchom 16821 |
. . . . . . . . . 10
|
48 | 45 | ffvelrnda 6359 |
. . . . . . . . . 10
|
49 | | 1st2nd 7214 |
. . . . . . . . . 10
|
50 | 47, 48, 49 | sylancr 695 |
. . . . . . . . 9
|
51 | 7 | ad2antrr 762 |
. . . . . . . . . . . 12
|
52 | 19 | ad2antrr 762 |
. . . . . . . . . . . 12
F
|
53 | 43 | adantr 481 |
. . . . . . . . . . . 12
|
54 | 44 | adantr 481 |
. . . . . . . . . . . 12
|
55 | | simpr 477 |
. . . . . . . . . . . 12
|
56 | 1, 51, 52, 53, 54, 41, 55 | cofu2 16546 |
. . . . . . . . . . 11
F func
F |
57 | 16 | adantr 481 |
. . . . . . . . . . . . . 14
|
58 | 17 | adantr 481 |
. . . . . . . . . . . . . 14
|
59 | 12 | adantrr 753 |
. . . . . . . . . . . . . 14
|
60 | 10 | ffvelrnda 6359 |
. . . . . . . . . . . . . . 15
|
61 | 60 | adantrl 752 |
. . . . . . . . . . . . . 14
|
62 | 2, 5, 23, 57, 58, 18, 59, 61 | 1stf2 16833 |
. . . . . . . . . . . . 13
F |
63 | 62 | adantr 481 |
. . . . . . . . . . . 12
F |
64 | 63 | fveq1d 6193 |
. . . . . . . . . . 11
F
|
65 | | fvres 6207 |
. . . . . . . . . . . 12
|
66 | 48, 65 | syl 17 |
. . . . . . . . . . 11
|
67 | 56, 64, 66 | 3eqtrd 2660 |
. . . . . . . . . 10
F func
|
68 | 29 | ad2antrr 762 |
. . . . . . . . . . . 12
F
|
69 | 1, 51, 68, 53, 54, 41, 55 | cofu2 16546 |
. . . . . . . . . . 11
F func
F |
70 | 2, 5, 23, 57, 58, 28, 59, 61 | 2ndf2 16836 |
. . . . . . . . . . . . 13
F |
71 | 70 | adantr 481 |
. . . . . . . . . . . 12
F |
72 | 71 | fveq1d 6193 |
. . . . . . . . . . 11
F
|
73 | | fvres 6207 |
. . . . . . . . . . . 12
|
74 | 48, 73 | syl 17 |
. . . . . . . . . . 11
|
75 | 69, 72, 74 | 3eqtrd 2660 |
. . . . . . . . . 10
F func
|
76 | 67, 75 | opeq12d 4410 |
. . . . . . . . 9
F func
F func
|
77 | 50, 76 | eqtr4d 2659 |
. . . . . . . 8
F func F
func |
78 | 77 | mpteq2dva 4744 |
. . . . . . 7
F
func F func
|
79 | 46, 78 | eqtrd 2656 |
. . . . . 6
F func
F func |
80 | 79 | 3impb 1260 |
. . . . 5
F func
F func |
81 | 80 | mpt2eq3dva 6719 |
. . . 4
F
func F func
|
82 | 40, 81 | eqtrd 2656 |
. . 3
F
func F func
|
83 | 37, 82 | opeq12d 4410 |
. 2
F
func F func
F
func F func
|
84 | | 1st2nd 7214 |
. . 3
|
85 | 6, 7, 84 | sylancr 695 |
. 2
|
86 | | eqid 2622 |
. . 3
F
func 〈,〉F F func F func
〈,〉F F func
|
87 | 7, 19 | cofucl 16548 |
. . 3
F func
|
88 | 7, 29 | cofucl 16548 |
. . 3
F func
|
89 | 86, 1, 41, 87, 88 | prfval 16839 |
. 2
F func
〈,〉F F func
F
func F func
F
func F func
|
90 | 83, 85, 89 | 3eqtr4d 2666 |
1
F
func 〈,〉F F func |