Step | Hyp | Ref
| Expression |
1 | | xppreima2.3 |
. . . 4
ā¢ š» = (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©) |
2 | 1 | funmpt2 6541 |
. . 3
ā¢ Fun š» |
3 | | xppreima2.1 |
. . . . . . . 8
ā¢ (š ā š¹:š“ā¶šµ) |
4 | 3 | ffvelcdmda 7036 |
. . . . . . 7
ā¢ ((š ā§ š„ ā š“) ā (š¹āš„) ā šµ) |
5 | | xppreima2.2 |
. . . . . . . 8
ā¢ (š ā šŗ:š“ā¶š¶) |
6 | 5 | ffvelcdmda 7036 |
. . . . . . 7
ā¢ ((š ā§ š„ ā š“) ā (šŗāš„) ā š¶) |
7 | | opelxp 5670 |
. . . . . . 7
ā¢
(āØ(š¹āš„), (šŗāš„)ā© ā (šµ Ć š¶) ā ((š¹āš„) ā šµ ā§ (šŗāš„) ā š¶)) |
8 | 4, 6, 7 | sylanbrc 584 |
. . . . . 6
ā¢ ((š ā§ š„ ā š“) ā āØ(š¹āš„), (šŗāš„)ā© ā (šµ Ć š¶)) |
9 | 8, 1 | fmptd 7063 |
. . . . 5
ā¢ (š ā š»:š“ā¶(šµ Ć š¶)) |
10 | 9 | frnd 6677 |
. . . 4
ā¢ (š ā ran š» ā (šµ Ć š¶)) |
11 | | xpss 5650 |
. . . 4
ā¢ (šµ Ć š¶) ā (V Ć V) |
12 | 10, 11 | sstrdi 3957 |
. . 3
ā¢ (š ā ran š» ā (V Ć V)) |
13 | | xppreima 31608 |
. . 3
ā¢ ((Fun
š» ā§ ran š» ā (V Ć V)) ā
(ā”š» ā (š Ć š)) = ((ā”(1st ā š») ā š) ā© (ā”(2nd ā š») ā š))) |
14 | 2, 12, 13 | sylancr 588 |
. 2
ā¢ (š ā (ā”š» ā (š Ć š)) = ((ā”(1st ā š») ā š) ā© (ā”(2nd ā š») ā š))) |
15 | | fo1st 7942 |
. . . . . . . . 9
ā¢
1st :VāontoāV |
16 | | fofn 6759 |
. . . . . . . . 9
ā¢
(1st :VāontoāV ā 1st Fn V) |
17 | 15, 16 | ax-mp 5 |
. . . . . . . 8
ā¢
1st Fn V |
18 | | opex 5422 |
. . . . . . . . 9
ā¢
āØ(š¹āš„), (šŗāš„)ā© ā V |
19 | 18, 1 | fnmpti 6645 |
. . . . . . . 8
ā¢ š» Fn š“ |
20 | | ssv 3969 |
. . . . . . . 8
ā¢ ran š» ā V |
21 | | fnco 6619 |
. . . . . . . 8
ā¢
((1st Fn V ā§ š» Fn š“ ā§ ran š» ā V) ā (1st ā
š») Fn š“) |
22 | 17, 19, 20, 21 | mp3an 1462 |
. . . . . . 7
ā¢
(1st ā š») Fn š“ |
23 | 22 | a1i 11 |
. . . . . 6
ā¢ (š ā (1st ā
š») Fn š“) |
24 | 3 | ffnd 6670 |
. . . . . 6
ā¢ (š ā š¹ Fn š“) |
25 | 2 | a1i 11 |
. . . . . . . . . 10
ā¢ ((š ā§ š„ ā š“) ā Fun š») |
26 | 12 | adantr 482 |
. . . . . . . . . 10
ā¢ ((š ā§ š„ ā š“) ā ran š» ā (V Ć V)) |
27 | | simpr 486 |
. . . . . . . . . . 11
ā¢ ((š ā§ š„ ā š“) ā š„ ā š“) |
28 | 18, 1 | dmmpti 6646 |
. . . . . . . . . . 11
ā¢ dom š» = š“ |
29 | 27, 28 | eleqtrrdi 2845 |
. . . . . . . . . 10
ā¢ ((š ā§ š„ ā š“) ā š„ ā dom š») |
30 | | opfv 31607 |
. . . . . . . . . 10
ā¢ (((Fun
š» ā§ ran š» ā (V Ć V)) ā§
š„ ā dom š») ā (š»āš„) = āØ((1st ā š»)āš„), ((2nd ā š»)āš„)ā©) |
31 | 25, 26, 29, 30 | syl21anc 837 |
. . . . . . . . 9
ā¢ ((š ā§ š„ ā š“) ā (š»āš„) = āØ((1st ā š»)āš„), ((2nd ā š»)āš„)ā©) |
32 | 1 | fvmpt2 6960 |
. . . . . . . . . 10
ā¢ ((š„ ā š“ ā§ āØ(š¹āš„), (šŗāš„)ā© ā (šµ Ć š¶)) ā (š»āš„) = āØ(š¹āš„), (šŗāš„)ā©) |
33 | 27, 8, 32 | syl2anc 585 |
. . . . . . . . 9
ā¢ ((š ā§ š„ ā š“) ā (š»āš„) = āØ(š¹āš„), (šŗāš„)ā©) |
34 | 31, 33 | eqtr3d 2775 |
. . . . . . . 8
ā¢ ((š ā§ š„ ā š“) ā āØ((1st ā
š»)āš„), ((2nd ā š»)āš„)ā© = āØ(š¹āš„), (šŗāš„)ā©) |
35 | | fvex 6856 |
. . . . . . . . 9
ā¢
((1st ā š»)āš„) ā V |
36 | | fvex 6856 |
. . . . . . . . 9
ā¢
((2nd ā š»)āš„) ā V |
37 | 35, 36 | opth 5434 |
. . . . . . . 8
ā¢
(āØ((1st ā š»)āš„), ((2nd ā š»)āš„)ā© = āØ(š¹āš„), (šŗāš„)ā© ā (((1st ā
š»)āš„) = (š¹āš„) ā§ ((2nd ā š»)āš„) = (šŗāš„))) |
38 | 34, 37 | sylib 217 |
. . . . . . 7
ā¢ ((š ā§ š„ ā š“) ā (((1st ā š»)āš„) = (š¹āš„) ā§ ((2nd ā š»)āš„) = (šŗāš„))) |
39 | 38 | simpld 496 |
. . . . . 6
ā¢ ((š ā§ š„ ā š“) ā ((1st ā š»)āš„) = (š¹āš„)) |
40 | 23, 24, 39 | eqfnfvd 6986 |
. . . . 5
ā¢ (š ā (1st ā
š») = š¹) |
41 | 40 | cnveqd 5832 |
. . . 4
ā¢ (š ā ā”(1st ā š») = ā”š¹) |
42 | 41 | imaeq1d 6013 |
. . 3
ā¢ (š ā (ā”(1st ā š») ā š) = (ā”š¹ ā š)) |
43 | | fo2nd 7943 |
. . . . . . . . 9
ā¢
2nd :VāontoāV |
44 | | fofn 6759 |
. . . . . . . . 9
ā¢
(2nd :VāontoāV ā 2nd Fn V) |
45 | 43, 44 | ax-mp 5 |
. . . . . . . 8
ā¢
2nd Fn V |
46 | | fnco 6619 |
. . . . . . . 8
ā¢
((2nd Fn V ā§ š» Fn š“ ā§ ran š» ā V) ā (2nd ā
š») Fn š“) |
47 | 45, 19, 20, 46 | mp3an 1462 |
. . . . . . 7
ā¢
(2nd ā š») Fn š“ |
48 | 47 | a1i 11 |
. . . . . 6
ā¢ (š ā (2nd ā
š») Fn š“) |
49 | 5 | ffnd 6670 |
. . . . . 6
ā¢ (š ā šŗ Fn š“) |
50 | 38 | simprd 497 |
. . . . . 6
ā¢ ((š ā§ š„ ā š“) ā ((2nd ā š»)āš„) = (šŗāš„)) |
51 | 48, 49, 50 | eqfnfvd 6986 |
. . . . 5
ā¢ (š ā (2nd ā
š») = šŗ) |
52 | 51 | cnveqd 5832 |
. . . 4
ā¢ (š ā ā”(2nd ā š») = ā”šŗ) |
53 | 52 | imaeq1d 6013 |
. . 3
ā¢ (š ā (ā”(2nd ā š») ā š) = (ā”šŗ ā š)) |
54 | 42, 53 | ineq12d 4174 |
. 2
ā¢ (š ā ((ā”(1st ā š») ā š) ā© (ā”(2nd ā š») ā š)) = ((ā”š¹ ā š) ā© (ā”šŗ ā š))) |
55 | 14, 54 | eqtrd 2773 |
1
ā¢ (š ā (ā”š» ā (š Ć š)) = ((ā”š¹ ā š) ā© (ā”šŗ ā š))) |