Proof of Theorem funcestrcsetclem9
Step | Hyp | Ref
| Expression |
1 | | funcestrcsetc.e |
. . . . . 6
ExtStrCat |
2 | | funcestrcsetc.u |
. . . . . . 7
WUni |
3 | 2 | adantr 481 |
. . . . . 6
WUni |
4 | | eqid 2622 |
. . . . . 6
|
5 | 1, 2 | estrcbas 16765 |
. . . . . . . . . . 11
|
6 | | funcestrcsetc.b |
. . . . . . . . . . 11
|
7 | 5, 6 | syl6reqr 2675 |
. . . . . . . . . 10
|
8 | 7 | eleq2d 2687 |
. . . . . . . . 9
|
9 | 8 | biimpcd 239 |
. . . . . . . 8
|
10 | 9 | 3ad2ant1 1082 |
. . . . . . 7
|
11 | 10 | impcom 446 |
. . . . . 6
|
12 | 7 | eleq2d 2687 |
. . . . . . . . 9
|
13 | 12 | biimpcd 239 |
. . . . . . . 8
|
14 | 13 | 3ad2ant2 1083 |
. . . . . . 7
|
15 | 14 | impcom 446 |
. . . . . 6
|
16 | | eqid 2622 |
. . . . . 6
|
17 | | eqid 2622 |
. . . . . 6
|
18 | 1, 3, 4, 11, 15, 16, 17 | estrchom 16767 |
. . . . 5
|
19 | 18 | eleq2d 2687 |
. . . 4
|
20 | 7 | eleq2d 2687 |
. . . . . . . . 9
|
21 | 20 | biimpcd 239 |
. . . . . . . 8
|
22 | 21 | 3ad2ant3 1084 |
. . . . . . 7
|
23 | 22 | impcom 446 |
. . . . . 6
|
24 | | eqid 2622 |
. . . . . 6
|
25 | 1, 3, 4, 15, 23, 17, 24 | estrchom 16767 |
. . . . 5
|
26 | 25 | eleq2d 2687 |
. . . 4
|
27 | 19, 26 | anbi12d 747 |
. . 3
|
28 | | elmapi 7879 |
. . . . . . . . . 10
|
29 | | elmapi 7879 |
. . . . . . . . . 10
|
30 | | fco 6058 |
. . . . . . . . . 10
|
31 | 28, 29, 30 | syl2an 494 |
. . . . . . . . 9
|
32 | | fvex 6201 |
. . . . . . . . . 10
|
33 | | fvex 6201 |
. . . . . . . . . 10
|
34 | 32, 33 | elmap 7886 |
. . . . . . . . 9
|
35 | 31, 34 | sylibr 224 |
. . . . . . . 8
|
36 | 35 | ancoms 469 |
. . . . . . 7
|
37 | 36 | adantl 482 |
. . . . . 6
|
38 | | fvresi 6439 |
. . . . . 6
|
39 | 37, 38 | syl 17 |
. . . . 5
|
40 | | funcestrcsetc.s |
. . . . . . . . 9
|
41 | | funcestrcsetc.c |
. . . . . . . . 9
|
42 | | funcestrcsetc.f |
. . . . . . . . 9
|
43 | | funcestrcsetc.g |
. . . . . . . . 9
|
44 | 1, 40, 6, 41, 2, 42, 43, 16, 24 | funcestrcsetclem5 16784 |
. . . . . . . 8
|
45 | 44 | 3adantr2 1221 |
. . . . . . 7
|
46 | 45 | adantr 481 |
. . . . . 6
|
47 | 3 | adantr 481 |
. . . . . . 7
WUni |
48 | | eqid 2622 |
. . . . . . 7
comp comp |
49 | 11 | adantr 481 |
. . . . . . 7
|
50 | 15 | adantr 481 |
. . . . . . 7
|
51 | 23 | adantr 481 |
. . . . . . 7
|
52 | 29 | ad2antrl 764 |
. . . . . . 7
|
53 | 28 | ad2antll 765 |
. . . . . . 7
|
54 | 1, 47, 48, 49, 50, 51, 16, 17, 24, 52, 53 | estrcco 16770 |
. . . . . 6
comp |
55 | 46, 54 | fveq12d 6197 |
. . . . 5
comp
|
56 | | eqid 2622 |
. . . . . . 7
comp comp |
57 | 1, 40, 6, 41, 2, 42 | funcestrcsetclem2 16781 |
. . . . . . . . 9
|
58 | 57 | 3ad2antr1 1226 |
. . . . . . . 8
|
59 | 58 | adantr 481 |
. . . . . . 7
|
60 | 1, 40, 6, 41, 2, 42 | funcestrcsetclem2 16781 |
. . . . . . . . 9
|
61 | 60 | 3ad2antr2 1227 |
. . . . . . . 8
|
62 | 61 | adantr 481 |
. . . . . . 7
|
63 | 1, 40, 6, 41, 2, 42 | funcestrcsetclem2 16781 |
. . . . . . . . 9
|
64 | 63 | 3ad2antr3 1228 |
. . . . . . . 8
|
65 | 64 | adantr 481 |
. . . . . . 7
|
66 | 1, 40, 6, 41, 2, 42 | funcestrcsetclem1 16780 |
. . . . . . . . . . . 12
|
67 | 66 | 3ad2antr1 1226 |
. . . . . . . . . . 11
|
68 | 1, 40, 6, 41, 2, 42 | funcestrcsetclem1 16780 |
. . . . . . . . . . . 12
|
69 | 68 | 3ad2antr2 1227 |
. . . . . . . . . . 11
|
70 | 67, 69 | feq23d 6040 |
. . . . . . . . . 10
|
71 | 70 | adantr 481 |
. . . . . . . . 9
|
72 | 52, 71 | mpbird 247 |
. . . . . . . 8
|
73 | | simpll 790 |
. . . . . . . . . 10
|
74 | | 3simpa 1058 |
. . . . . . . . . . 11
|
75 | 74 | ad2antlr 763 |
. . . . . . . . . 10
|
76 | | simprl 794 |
. . . . . . . . . 10
|
77 | 1, 40, 6, 41, 2, 42, 43, 16, 17 | funcestrcsetclem6 16785 |
. . . . . . . . . 10
|
78 | 73, 75, 76, 77 | syl3anc 1326 |
. . . . . . . . 9
|
79 | 78 | feq1d 6030 |
. . . . . . . 8
|
80 | 72, 79 | mpbird 247 |
. . . . . . 7
|
81 | 1, 40, 6, 41, 2, 42 | funcestrcsetclem1 16780 |
. . . . . . . . . . . 12
|
82 | 81 | 3ad2antr3 1228 |
. . . . . . . . . . 11
|
83 | 69, 82 | feq23d 6040 |
. . . . . . . . . 10
|
84 | 83 | adantr 481 |
. . . . . . . . 9
|
85 | 53, 84 | mpbird 247 |
. . . . . . . 8
|
86 | | 3simpc 1060 |
. . . . . . . . . . 11
|
87 | 86 | ad2antlr 763 |
. . . . . . . . . 10
|
88 | | simprr 796 |
. . . . . . . . . 10
|
89 | 1, 40, 6, 41, 2, 42, 43, 17, 24 | funcestrcsetclem6 16785 |
. . . . . . . . . 10
|
90 | 73, 87, 88, 89 | syl3anc 1326 |
. . . . . . . . 9
|
91 | 90 | feq1d 6030 |
. . . . . . . 8
|
92 | 85, 91 | mpbird 247 |
. . . . . . 7
|
93 | 40, 47, 56, 59, 62, 65, 80, 92 | setcco 16733 |
. . . . . 6
comp |
94 | 90, 78 | coeq12d 5286 |
. . . . . 6
|
95 | 93, 94 | eqtrd 2656 |
. . . . 5
comp |
96 | 39, 55, 95 | 3eqtr4d 2666 |
. . . 4
comp comp |
97 | 96 | ex 450 |
. . 3
comp comp |
98 | 27, 97 | sylbid 230 |
. 2
comp comp |
99 | 98 | 3impia 1261 |
1
comp comp |