Step | Hyp | Ref
| Expression |
1 | | df-ov 7361 |
. . . . . 6
ā¢ (š(š¹ ā 1st )š
) = ((š¹ ā 1st )āāØš, š
ā©) |
2 | | fo1st 7942 |
. . . . . . . 8
ā¢
1st :VāontoāV |
3 | | fofn 6759 |
. . . . . . . 8
ā¢
(1st :VāontoāV ā 1st Fn V) |
4 | 2, 3 | ax-mp 5 |
. . . . . . 7
ā¢
1st Fn V |
5 | | opex 5422 |
. . . . . . 7
ā¢
āØš, š
ā© ā V |
6 | | fvco2 6939 |
. . . . . . 7
ā¢
((1st Fn V ā§ āØš, š
ā© ā V) ā ((š¹ ā 1st )āāØš, š
ā©) = (š¹ā(1st āāØš, š
ā©))) |
7 | 4, 5, 6 | mp2an 691 |
. . . . . 6
ā¢ ((š¹ ā 1st
)āāØš, š
ā©) = (š¹ā(1st āāØš, š
ā©)) |
8 | 1, 7 | eqtri 2761 |
. . . . 5
ā¢ (š(š¹ ā 1st )š
) = (š¹ā(1st āāØš, š
ā©)) |
9 | | fpwwe.1 |
. . . . . . . 8
ā¢ š = {āØš„, šā© ā£ ((š„ ā š“ ā§ š ā (š„ Ć š„)) ā§ (š We š„ ā§ āš¦ ā š„ (š¹ā(ā”š ā {š¦})) = š¦))} |
10 | 9 | bropaex12 5724 |
. . . . . . 7
ā¢ (ššš
ā (š ā V ā§ š
ā V)) |
11 | | op1stg 7934 |
. . . . . . 7
ā¢ ((š ā V ā§ š
ā V) ā
(1st āāØš, š
ā©) = š) |
12 | 10, 11 | syl 17 |
. . . . . 6
ā¢ (ššš
ā (1st āāØš, š
ā©) = š) |
13 | 12 | fveq2d 6847 |
. . . . 5
ā¢ (ššš
ā (š¹ā(1st āāØš, š
ā©)) = (š¹āš)) |
14 | 8, 13 | eqtrid 2785 |
. . . 4
ā¢ (ššš
ā (š(š¹ ā 1st )š
) = (š¹āš)) |
15 | 14 | eleq1d 2819 |
. . 3
ā¢ (ššš
ā ((š(š¹ ā 1st )š
) ā š ā (š¹āš) ā š)) |
16 | 15 | pm5.32i 576 |
. 2
ā¢ ((ššš
ā§ (š(š¹ ā 1st )š
) ā š) ā (ššš
ā§ (š¹āš) ā š)) |
17 | | vex 3448 |
. . . . . . . . . . 11
ā¢ š ā V |
18 | 17 | cnvex 7863 |
. . . . . . . . . 10
ā¢ ā”š ā V |
19 | 18 | imaex 7854 |
. . . . . . . . 9
ā¢ (ā”š ā {š¦}) ā V |
20 | | vex 3448 |
. . . . . . . . . . . 12
ā¢ š¢ ā V |
21 | 17 | inex1 5275 |
. . . . . . . . . . . 12
ā¢ (š ā© (š¢ Ć š¢)) ā V |
22 | 20, 21 | opco1i 8058 |
. . . . . . . . . . 11
ā¢ (š¢(š¹ ā 1st )(š ā© (š¢ Ć š¢))) = (š¹āš¢) |
23 | | fveq2 6843 |
. . . . . . . . . . 11
ā¢ (š¢ = (ā”š ā {š¦}) ā (š¹āš¢) = (š¹ā(ā”š ā {š¦}))) |
24 | 22, 23 | eqtrid 2785 |
. . . . . . . . . 10
ā¢ (š¢ = (ā”š ā {š¦}) ā (š¢(š¹ ā 1st )(š ā© (š¢ Ć š¢))) = (š¹ā(ā”š ā {š¦}))) |
25 | 24 | eqeq1d 2735 |
. . . . . . . . 9
ā¢ (š¢ = (ā”š ā {š¦}) ā ((š¢(š¹ ā 1st )(š ā© (š¢ Ć š¢))) = š¦ ā (š¹ā(ā”š ā {š¦})) = š¦)) |
26 | 19, 25 | sbcie 3783 |
. . . . . . . 8
ā¢
([(ā”š ā {š¦}) / š¢](š¢(š¹ ā 1st )(š ā© (š¢ Ć š¢))) = š¦ ā (š¹ā(ā”š ā {š¦})) = š¦) |
27 | 26 | ralbii 3093 |
. . . . . . 7
ā¢
(āš¦ ā
š„ [(ā”š ā {š¦}) / š¢](š¢(š¹ ā 1st )(š ā© (š¢ Ć š¢))) = š¦ ā āš¦ ā š„ (š¹ā(ā”š ā {š¦})) = š¦) |
28 | 27 | anbi2i 624 |
. . . . . 6
ā¢ ((š We š„ ā§ āš¦ ā š„ [(ā”š ā {š¦}) / š¢](š¢(š¹ ā 1st )(š ā© (š¢ Ć š¢))) = š¦) ā (š We š„ ā§ āš¦ ā š„ (š¹ā(ā”š ā {š¦})) = š¦)) |
29 | 28 | anbi2i 624 |
. . . . 5
ā¢ (((š„ ā š“ ā§ š ā (š„ Ć š„)) ā§ (š We š„ ā§ āš¦ ā š„ [(ā”š ā {š¦}) / š¢](š¢(š¹ ā 1st )(š ā© (š¢ Ć š¢))) = š¦)) ā ((š„ ā š“ ā§ š ā (š„ Ć š„)) ā§ (š We š„ ā§ āš¦ ā š„ (š¹ā(ā”š ā {š¦})) = š¦))) |
30 | 29 | opabbii 5173 |
. . . 4
ā¢
{āØš„, šā© ā£ ((š„ ā š“ ā§ š ā (š„ Ć š„)) ā§ (š We š„ ā§ āš¦ ā š„ [(ā”š ā {š¦}) / š¢](š¢(š¹ ā 1st )(š ā© (š¢ Ć š¢))) = š¦))} = {āØš„, šā© ā£ ((š„ ā š“ ā§ š ā (š„ Ć š„)) ā§ (š We š„ ā§ āš¦ ā š„ (š¹ā(ā”š ā {š¦})) = š¦))} |
31 | 9, 30 | eqtr4i 2764 |
. . 3
ā¢ š = {āØš„, šā© ā£ ((š„ ā š“ ā§ š ā (š„ Ć š„)) ā§ (š We š„ ā§ āš¦ ā š„ [(ā”š ā {š¦}) / š¢](š¢(š¹ ā 1st )(š ā© (š¢ Ć š¢))) = š¦))} |
32 | | fpwwe.2 |
. . 3
ā¢ (š ā š“ ā š) |
33 | | vex 3448 |
. . . . 5
ā¢ š„ ā V |
34 | 33, 17 | opco1i 8058 |
. . . 4
ā¢ (š„(š¹ ā 1st )š) = (š¹āš„) |
35 | | simp1 1137 |
. . . . . . 7
ā¢ ((š„ ā š“ ā§ š ā (š„ Ć š„) ā§ š We š„) ā š„ ā š“) |
36 | | velpw 4566 |
. . . . . . 7
ā¢ (š„ ā š« š“ ā š„ ā š“) |
37 | 35, 36 | sylibr 233 |
. . . . . 6
ā¢ ((š„ ā š“ ā§ š ā (š„ Ć š„) ā§ š We š„) ā š„ ā š« š“) |
38 | | 19.8a 2175 |
. . . . . . . 8
ā¢ (š We š„ ā āš š We š„) |
39 | 38 | 3ad2ant3 1136 |
. . . . . . 7
ā¢ ((š„ ā š“ ā§ š ā (š„ Ć š„) ā§ š We š„) ā āš š We š„) |
40 | | ween 9976 |
. . . . . . 7
ā¢ (š„ ā dom card ā
āš š We š„) |
41 | 39, 40 | sylibr 233 |
. . . . . 6
ā¢ ((š„ ā š“ ā§ š ā (š„ Ć š„) ā§ š We š„) ā š„ ā dom card) |
42 | 37, 41 | elind 4155 |
. . . . 5
ā¢ ((š„ ā š“ ā§ š ā (š„ Ć š„) ā§ š We š„) ā š„ ā (š« š“ ā© dom card)) |
43 | | fpwwe.3 |
. . . . 5
ā¢ ((š ā§ š„ ā (š« š“ ā© dom card)) ā (š¹āš„) ā š“) |
44 | 42, 43 | sylan2 594 |
. . . 4
ā¢ ((š ā§ (š„ ā š“ ā§ š ā (š„ Ć š„) ā§ š We š„)) ā (š¹āš„) ā š“) |
45 | 34, 44 | eqeltrid 2838 |
. . 3
ā¢ ((š ā§ (š„ ā š“ ā§ š ā (š„ Ć š„) ā§ š We š„)) ā (š„(š¹ ā 1st )š) ā š“) |
46 | | fpwwe.4 |
. . 3
ā¢ š = āŖ
dom š |
47 | 31, 32, 45, 46 | fpwwe2 10584 |
. 2
ā¢ (š ā ((ššš
ā§ (š(š¹ ā 1st )š
) ā š) ā (š = š ā§ š
= (šāš)))) |
48 | 16, 47 | bitr3id 285 |
1
ā¢ (š ā ((ššš
ā§ (š¹āš) ā š) ā (š = š ā§ š
= (šāš)))) |