Step | Hyp | Ref
| Expression |
1 | | prfcl.p |
. . . 4
〈,〉F |
2 | | eqid 2622 |
. . . 4
|
3 | | eqid 2622 |
. . . 4
|
4 | | prfcl.c |
. . . 4
|
5 | | prfcl.d |
. . . 4
|
6 | 1, 2, 3, 4, 5 | prfval 16839 |
. . 3
|
7 | | fvex 6201 |
. . . . . . 7
|
8 | 7 | mptex 6486 |
. . . . . 6
|
9 | 7, 7 | mpt2ex 7247 |
. . . . . 6
|
10 | 8, 9 | op1std 7178 |
. . . . 5
|
11 | 6, 10 | syl 17 |
. . . 4
|
12 | 8, 9 | op2ndd 7179 |
. . . . 5
|
13 | 6, 12 | syl 17 |
. . . 4
|
14 | 11, 13 | opeq12d 4410 |
. . 3
|
15 | 6, 14 | eqtr4d 2659 |
. 2
|
16 | | prfcl.t |
. . . . 5
c |
17 | | eqid 2622 |
. . . . 5
|
18 | | eqid 2622 |
. . . . 5
|
19 | 16, 17, 18 | xpcbas 16818 |
. . . 4
|
20 | | eqid 2622 |
. . . 4
|
21 | | eqid 2622 |
. . . 4
|
22 | | eqid 2622 |
. . . 4
|
23 | | eqid 2622 |
. . . 4
comp comp |
24 | | eqid 2622 |
. . . 4
comp comp |
25 | | funcrcl 16523 |
. . . . . 6
|
26 | 4, 25 | syl 17 |
. . . . 5
|
27 | 26 | simpld 475 |
. . . 4
|
28 | 26 | simprd 479 |
. . . . 5
|
29 | | funcrcl 16523 |
. . . . . . 7
|
30 | 5, 29 | syl 17 |
. . . . . 6
|
31 | 30 | simprd 479 |
. . . . 5
|
32 | 16, 28, 31 | xpccat 16830 |
. . . 4
|
33 | | relfunc 16522 |
. . . . . . . . . 10
|
34 | | 1st2ndbr 7217 |
. . . . . . . . . 10
|
35 | 33, 4, 34 | sylancr 695 |
. . . . . . . . 9
|
36 | 2, 17, 35 | funcf1 16526 |
. . . . . . . 8
|
37 | 36 | ffvelrnda 6359 |
. . . . . . 7
|
38 | | relfunc 16522 |
. . . . . . . . . 10
|
39 | | 1st2ndbr 7217 |
. . . . . . . . . 10
|
40 | 38, 5, 39 | sylancr 695 |
. . . . . . . . 9
|
41 | 2, 18, 40 | funcf1 16526 |
. . . . . . . 8
|
42 | 41 | ffvelrnda 6359 |
. . . . . . 7
|
43 | | opelxpi 5148 |
. . . . . . 7
|
44 | 37, 42, 43 | syl2anc 693 |
. . . . . 6
|
45 | | eqid 2622 |
. . . . . 6
|
46 | 44, 45 | fmptd 6385 |
. . . . 5
|
47 | 11 | feq1d 6030 |
. . . . 5
|
48 | 46, 47 | mpbird 247 |
. . . 4
|
49 | | eqid 2622 |
. . . . . 6
|
50 | | ovex 6678 |
. . . . . . 7
|
51 | 50 | mptex 6486 |
. . . . . 6
|
52 | 49, 51 | fnmpt2i 7239 |
. . . . 5
|
53 | 13 | fneq1d 5981 |
. . . . 5
|
54 | 52, 53 | mpbiri 248 |
. . . 4
|
55 | | eqid 2622 |
. . . . . . . . . 10
|
56 | 35 | adantr 481 |
. . . . . . . . . 10
|
57 | | simprl 794 |
. . . . . . . . . 10
|
58 | | simprr 796 |
. . . . . . . . . 10
|
59 | 2, 3, 55, 56, 57, 58 | funcf2 16528 |
. . . . . . . . 9
|
60 | 59 | ffvelrnda 6359 |
. . . . . . . 8
|
61 | | eqid 2622 |
. . . . . . . . . 10
|
62 | 40 | adantr 481 |
. . . . . . . . . 10
|
63 | 2, 3, 61, 62, 57, 58 | funcf2 16528 |
. . . . . . . . 9
|
64 | 63 | ffvelrnda 6359 |
. . . . . . . 8
|
65 | | opelxpi 5148 |
. . . . . . . 8
|
66 | 60, 64, 65 | syl2anc 693 |
. . . . . . 7
|
67 | 4 | adantr 481 |
. . . . . . . . . . 11
|
68 | 5 | adantr 481 |
. . . . . . . . . . 11
|
69 | 1, 2, 3, 67, 68, 57 | prf1 16840 |
. . . . . . . . . 10
|
70 | 1, 2, 3, 67, 68, 58 | prf1 16840 |
. . . . . . . . . 10
|
71 | 69, 70 | oveq12d 6668 |
. . . . . . . . 9
|
72 | 37 | adantrr 753 |
. . . . . . . . . 10
|
73 | 42 | adantrr 753 |
. . . . . . . . . 10
|
74 | 36 | ffvelrnda 6359 |
. . . . . . . . . . 11
|
75 | 74 | adantrl 752 |
. . . . . . . . . 10
|
76 | 41 | ffvelrnda 6359 |
. . . . . . . . . . 11
|
77 | 76 | adantrl 752 |
. . . . . . . . . 10
|
78 | 16, 17, 18, 55, 61, 72, 73, 75, 77, 20 | xpchom2 16826 |
. . . . . . . . 9
|
79 | 71, 78 | eqtrd 2656 |
. . . . . . . 8
|
80 | 79 | adantr 481 |
. . . . . . 7
|
81 | 66, 80 | eleqtrrd 2704 |
. . . . . 6
|
82 | | eqid 2622 |
. . . . . 6
|
83 | 81, 82 | fmptd 6385 |
. . . . 5
|
84 | 13 | oveqd 6667 |
. . . . . . 7
|
85 | 49 | ovmpt4g 6783 |
. . . . . . . 8
|
86 | 51, 85 | mp3an3 1413 |
. . . . . . 7
|
87 | 84, 86 | sylan9eq 2676 |
. . . . . 6
|
88 | 87 | feq1d 6030 |
. . . . 5
|
89 | 83, 88 | mpbird 247 |
. . . 4
|
90 | | eqid 2622 |
. . . . . . 7
|
91 | 35 | adantr 481 |
. . . . . . 7
|
92 | | simpr 477 |
. . . . . . 7
|
93 | 2, 21, 90, 91, 92 | funcid 16530 |
. . . . . 6
|
94 | | eqid 2622 |
. . . . . . 7
|
95 | 40 | adantr 481 |
. . . . . . 7
|
96 | 2, 21, 94, 95, 92 | funcid 16530 |
. . . . . 6
|
97 | 93, 96 | opeq12d 4410 |
. . . . 5
|
98 | 4 | adantr 481 |
. . . . . 6
|
99 | 5 | adantr 481 |
. . . . . 6
|
100 | 27 | adantr 481 |
. . . . . . 7
|
101 | 2, 3, 21, 100, 92 | catidcl 16343 |
. . . . . 6
|
102 | 1, 2, 3, 98, 99, 92, 92, 101 | prf2 16842 |
. . . . 5
|
103 | 1, 2, 3, 98, 99, 92 | prf1 16840 |
. . . . . . 7
|
104 | 103 | fveq2d 6195 |
. . . . . 6
|
105 | 28 | adantr 481 |
. . . . . . 7
|
106 | 31 | adantr 481 |
. . . . . . 7
|
107 | 16, 105, 106, 17, 18, 90, 94, 22, 37, 42 | xpcid 16829 |
. . . . . 6
|
108 | 104, 107 | eqtrd 2656 |
. . . . 5
|
109 | 97, 102, 108 | 3eqtr4d 2666 |
. . . 4
|
110 | | eqid 2622 |
. . . . . . 7
comp comp |
111 | 35 | 3ad2ant1 1082 |
. . . . . . 7
|
112 | | simp21 1094 |
. . . . . . 7
|
113 | | simp22 1095 |
. . . . . . 7
|
114 | | simp23 1096 |
. . . . . . 7
|
115 | | simp3l 1089 |
. . . . . . 7
|
116 | | simp3r 1090 |
. . . . . . 7
|
117 | 2, 3, 23, 110, 111, 112, 113, 114, 115, 116 | funcco 16531 |
. . . . . 6
comp comp |
118 | | eqid 2622 |
. . . . . . 7
comp comp |
119 | 5 | 3ad2ant1 1082 |
. . . . . . . 8
|
120 | 38, 119, 39 | sylancr 695 |
. . . . . . 7
|
121 | 2, 3, 23, 118, 120, 112, 113, 114, 115, 116 | funcco 16531 |
. . . . . 6
comp comp |
122 | 117, 121 | opeq12d 4410 |
. . . . 5
comp comp
comp comp |
123 | 4 | 3ad2ant1 1082 |
. . . . . 6
|
124 | 27 | 3ad2ant1 1082 |
. . . . . . 7
|
125 | 2, 3, 23, 124, 112, 113, 114, 115, 116 | catcocl 16346 |
. . . . . 6
comp |
126 | 1, 2, 3, 123, 119, 112, 114, 125 | prf2 16842 |
. . . . 5
comp comp comp |
127 | 1, 2, 3, 123, 119, 112 | prf1 16840 |
. . . . . . . . 9
|
128 | 1, 2, 3, 123, 119, 113 | prf1 16840 |
. . . . . . . . 9
|
129 | 127, 128 | opeq12d 4410 |
. . . . . . . 8
|
130 | 1, 2, 3, 123, 119, 114 | prf1 16840 |
. . . . . . . 8
|
131 | 129, 130 | oveq12d 6668 |
. . . . . . 7
comp comp |
132 | 1, 2, 3, 123, 119, 113, 114, 116 | prf2 16842 |
. . . . . . 7
|
133 | 1, 2, 3, 123, 119, 112, 113, 115 | prf2 16842 |
. . . . . . 7
|
134 | 131, 132,
133 | oveq123d 6671 |
. . . . . 6
comp comp |
135 | 36 | 3ad2ant1 1082 |
. . . . . . . 8
|
136 | 135, 112 | ffvelrnd 6360 |
. . . . . . 7
|
137 | 41 | 3ad2ant1 1082 |
. . . . . . . 8
|
138 | 137, 112 | ffvelrnd 6360 |
. . . . . . 7
|
139 | 135, 113 | ffvelrnd 6360 |
. . . . . . 7
|
140 | 137, 113 | ffvelrnd 6360 |
. . . . . . 7
|
141 | 135, 114 | ffvelrnd 6360 |
. . . . . . 7
|
142 | 137, 114 | ffvelrnd 6360 |
. . . . . . 7
|
143 | 2, 3, 55, 111, 112, 113 | funcf2 16528 |
. . . . . . . 8
|
144 | 143, 115 | ffvelrnd 6360 |
. . . . . . 7
|
145 | 2, 3, 61, 120, 112, 113 | funcf2 16528 |
. . . . . . . 8
|
146 | 145, 115 | ffvelrnd 6360 |
. . . . . . 7
|
147 | 2, 3, 55, 111, 113, 114 | funcf2 16528 |
. . . . . . . 8
|
148 | 147, 116 | ffvelrnd 6360 |
. . . . . . 7
|
149 | 2, 3, 61, 120, 113, 114 | funcf2 16528 |
. . . . . . . 8
|
150 | 149, 116 | ffvelrnd 6360 |
. . . . . . 7
|
151 | 16, 17, 18, 55, 61, 136, 138, 139, 140, 110, 118, 24, 141, 142, 144, 146, 148, 150 | xpcco2 16827 |
. . . . . 6
comp comp comp |
152 | 134, 151 | eqtrd 2656 |
. . . . 5
comp comp comp |
153 | 122, 126,
152 | 3eqtr4d 2666 |
. . . 4
comp comp |
154 | 2, 19, 3, 20, 21, 22, 23, 24, 27, 32, 48, 54, 89, 109, 153 | isfuncd 16525 |
. . 3
|
155 | | df-br 4654 |
. . 3
|
156 | 154, 155 | sylib 208 |
. 2
|
157 | 15, 156 | eqeltrd 2701 |
1
|