Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. . 3
β’ ((πΆ β (Mooreβπ) β§ π β π« π) β πΆ β (Mooreβπ)) |
2 | | simpll 765 |
. . . . . . 7
β’ (((πΆ β (Mooreβπ) β§ π β π« π) β§ π β π) β πΆ β (Mooreβπ)) |
3 | | ssel2 3976 |
. . . . . . . . 9
β’ ((π β π« π β§ π β π) β π β π« π) |
4 | 3 | elpwid 4610 |
. . . . . . . 8
β’ ((π β π« π β§ π β π) β π β π) |
5 | 4 | adantll 712 |
. . . . . . 7
β’ (((πΆ β (Mooreβπ) β§ π β π« π) β§ π β π) β π β π) |
6 | | mrcfval.f |
. . . . . . . 8
β’ πΉ = (mrClsβπΆ) |
7 | 6 | mrcssid 17557 |
. . . . . . 7
β’ ((πΆ β (Mooreβπ) β§ π β π) β π β (πΉβπ )) |
8 | 2, 5, 7 | syl2anc 584 |
. . . . . 6
β’ (((πΆ β (Mooreβπ) β§ π β π« π) β§ π β π) β π β (πΉβπ )) |
9 | 6 | mrcf 17549 |
. . . . . . . . . . 11
β’ (πΆ β (Mooreβπ) β πΉ:π« πβΆπΆ) |
10 | 9 | ffund 6718 |
. . . . . . . . . 10
β’ (πΆ β (Mooreβπ) β Fun πΉ) |
11 | 10 | adantr 481 |
. . . . . . . . 9
β’ ((πΆ β (Mooreβπ) β§ π β π« π) β Fun πΉ) |
12 | 9 | fdmd 6725 |
. . . . . . . . . . 11
β’ (πΆ β (Mooreβπ) β dom πΉ = π« π) |
13 | 12 | sseq2d 4013 |
. . . . . . . . . 10
β’ (πΆ β (Mooreβπ) β (π β dom πΉ β π β π« π)) |
14 | 13 | biimpar 478 |
. . . . . . . . 9
β’ ((πΆ β (Mooreβπ) β§ π β π« π) β π β dom πΉ) |
15 | | funfvima2 7229 |
. . . . . . . . 9
β’ ((Fun
πΉ β§ π β dom πΉ) β (π β π β (πΉβπ ) β (πΉ β π))) |
16 | 11, 14, 15 | syl2anc 584 |
. . . . . . . 8
β’ ((πΆ β (Mooreβπ) β§ π β π« π) β (π β π β (πΉβπ ) β (πΉ β π))) |
17 | 16 | imp 407 |
. . . . . . 7
β’ (((πΆ β (Mooreβπ) β§ π β π« π) β§ π β π) β (πΉβπ ) β (πΉ β π)) |
18 | | elssuni 4940 |
. . . . . . 7
β’ ((πΉβπ ) β (πΉ β π) β (πΉβπ ) β βͺ (πΉ β π)) |
19 | 17, 18 | syl 17 |
. . . . . 6
β’ (((πΆ β (Mooreβπ) β§ π β π« π) β§ π β π) β (πΉβπ ) β βͺ (πΉ β π)) |
20 | 8, 19 | sstrd 3991 |
. . . . 5
β’ (((πΆ β (Mooreβπ) β§ π β π« π) β§ π β π) β π β βͺ (πΉ β π)) |
21 | 20 | ralrimiva 3146 |
. . . 4
β’ ((πΆ β (Mooreβπ) β§ π β π« π) β βπ β π π β βͺ (πΉ β π)) |
22 | | unissb 4942 |
. . . 4
β’ (βͺ π
β βͺ (πΉ β π) β βπ β π π β βͺ (πΉ β π)) |
23 | 21, 22 | sylibr 233 |
. . 3
β’ ((πΆ β (Mooreβπ) β§ π β π« π) β βͺ π β βͺ (πΉ
β π)) |
24 | 6 | mrcssv 17554 |
. . . . . . 7
β’ (πΆ β (Mooreβπ) β (πΉβπ₯) β π) |
25 | 24 | adantr 481 |
. . . . . 6
β’ ((πΆ β (Mooreβπ) β§ π β π« π) β (πΉβπ₯) β π) |
26 | 25 | ralrimivw 3150 |
. . . . 5
β’ ((πΆ β (Mooreβπ) β§ π β π« π) β βπ₯ β π (πΉβπ₯) β π) |
27 | 9 | ffnd 6715 |
. . . . . 6
β’ (πΆ β (Mooreβπ) β πΉ Fn π« π) |
28 | | sseq1 4006 |
. . . . . . 7
β’ (π = (πΉβπ₯) β (π β π β (πΉβπ₯) β π)) |
29 | 28 | ralima 7236 |
. . . . . 6
β’ ((πΉ Fn π« π β§ π β π« π) β (βπ β (πΉ β π)π β π β βπ₯ β π (πΉβπ₯) β π)) |
30 | 27, 29 | sylan 580 |
. . . . 5
β’ ((πΆ β (Mooreβπ) β§ π β π« π) β (βπ β (πΉ β π)π β π β βπ₯ β π (πΉβπ₯) β π)) |
31 | 26, 30 | mpbird 256 |
. . . 4
β’ ((πΆ β (Mooreβπ) β§ π β π« π) β βπ β (πΉ β π)π β π) |
32 | | unissb 4942 |
. . . 4
β’ (βͺ (πΉ
β π) β π β βπ β (πΉ β π)π β π) |
33 | 31, 32 | sylibr 233 |
. . 3
β’ ((πΆ β (Mooreβπ) β§ π β π« π) β βͺ (πΉ β π) β π) |
34 | 6 | mrcss 17556 |
. . 3
β’ ((πΆ β (Mooreβπ) β§ βͺ π
β βͺ (πΉ β π) β§ βͺ (πΉ β π) β π) β (πΉββͺ π) β (πΉββͺ (πΉ β π))) |
35 | 1, 23, 33, 34 | syl3anc 1371 |
. 2
β’ ((πΆ β (Mooreβπ) β§ π β π« π) β (πΉββͺ π) β (πΉββͺ (πΉ β π))) |
36 | | simpll 765 |
. . . . . . . 8
β’ (((πΆ β (Mooreβπ) β§ π β π« π) β§ π₯ β π) β πΆ β (Mooreβπ)) |
37 | | elssuni 4940 |
. . . . . . . . 9
β’ (π₯ β π β π₯ β βͺ π) |
38 | 37 | adantl 482 |
. . . . . . . 8
β’ (((πΆ β (Mooreβπ) β§ π β π« π) β§ π₯ β π) β π₯ β βͺ π) |
39 | | sspwuni 5102 |
. . . . . . . . . . 11
β’ (π β π« π β βͺ π
β π) |
40 | 39 | biimpi 215 |
. . . . . . . . . 10
β’ (π β π« π β βͺ π
β π) |
41 | 40 | adantl 482 |
. . . . . . . . 9
β’ ((πΆ β (Mooreβπ) β§ π β π« π) β βͺ π β π) |
42 | 41 | adantr 481 |
. . . . . . . 8
β’ (((πΆ β (Mooreβπ) β§ π β π« π) β§ π₯ β π) β βͺ π β π) |
43 | 6 | mrcss 17556 |
. . . . . . . 8
β’ ((πΆ β (Mooreβπ) β§ π₯ β βͺ π β§ βͺ π
β π) β (πΉβπ₯) β (πΉββͺ π)) |
44 | 36, 38, 42, 43 | syl3anc 1371 |
. . . . . . 7
β’ (((πΆ β (Mooreβπ) β§ π β π« π) β§ π₯ β π) β (πΉβπ₯) β (πΉββͺ π)) |
45 | 44 | ralrimiva 3146 |
. . . . . 6
β’ ((πΆ β (Mooreβπ) β§ π β π« π) β βπ₯ β π (πΉβπ₯) β (πΉββͺ π)) |
46 | | sseq1 4006 |
. . . . . . . 8
β’ (π = (πΉβπ₯) β (π β (πΉββͺ π) β (πΉβπ₯) β (πΉββͺ π))) |
47 | 46 | ralima 7236 |
. . . . . . 7
β’ ((πΉ Fn π« π β§ π β π« π) β (βπ β (πΉ β π)π β (πΉββͺ π) β βπ₯ β π (πΉβπ₯) β (πΉββͺ π))) |
48 | 27, 47 | sylan 580 |
. . . . . 6
β’ ((πΆ β (Mooreβπ) β§ π β π« π) β (βπ β (πΉ β π)π β (πΉββͺ π) β βπ₯ β π (πΉβπ₯) β (πΉββͺ π))) |
49 | 45, 48 | mpbird 256 |
. . . . 5
β’ ((πΆ β (Mooreβπ) β§ π β π« π) β βπ β (πΉ β π)π β (πΉββͺ π)) |
50 | | unissb 4942 |
. . . . 5
β’ (βͺ (πΉ
β π) β (πΉββͺ π)
β βπ β
(πΉ β π)π β (πΉββͺ π)) |
51 | 49, 50 | sylibr 233 |
. . . 4
β’ ((πΆ β (Mooreβπ) β§ π β π« π) β βͺ (πΉ β π) β (πΉββͺ π)) |
52 | 6 | mrcssv 17554 |
. . . . 5
β’ (πΆ β (Mooreβπ) β (πΉββͺ π) β π) |
53 | 52 | adantr 481 |
. . . 4
β’ ((πΆ β (Mooreβπ) β§ π β π« π) β (πΉββͺ π) β π) |
54 | 6 | mrcss 17556 |
. . . 4
β’ ((πΆ β (Mooreβπ) β§ βͺ (πΉ
β π) β (πΉββͺ π)
β§ (πΉββͺ π)
β π) β (πΉββͺ (πΉ
β π)) β (πΉβ(πΉββͺ π))) |
55 | 1, 51, 53, 54 | syl3anc 1371 |
. . 3
β’ ((πΆ β (Mooreβπ) β§ π β π« π) β (πΉββͺ (πΉ β π)) β (πΉβ(πΉββͺ π))) |
56 | 6 | mrcidm 17559 |
. . . 4
β’ ((πΆ β (Mooreβπ) β§ βͺ π
β π) β (πΉβ(πΉββͺ π)) = (πΉββͺ π)) |
57 | 1, 41, 56 | syl2anc 584 |
. . 3
β’ ((πΆ β (Mooreβπ) β§ π β π« π) β (πΉβ(πΉββͺ π)) = (πΉββͺ π)) |
58 | 55, 57 | sseqtrd 4021 |
. 2
β’ ((πΆ β (Mooreβπ) β§ π β π« π) β (πΉββͺ (πΉ β π)) β (πΉββͺ π)) |
59 | 35, 58 | eqssd 3998 |
1
β’ ((πΆ β (Mooreβπ) β§ π β π« π) β (πΉββͺ π) = (πΉββͺ (πΉ β π))) |