Step | Hyp | Ref
| Expression |
1 | | fnmrc 17488 |
. . . . 5
β’ mrCls Fn
βͺ ran Moore |
2 | | fnfun 6603 |
. . . . 5
β’ (mrCls Fn
βͺ ran Moore β Fun mrCls) |
3 | 1, 2 | ax-mp 5 |
. . . 4
β’ Fun
mrCls |
4 | | fvelima 6909 |
. . . 4
β’ ((Fun
mrCls β§ πΉ β (mrCls
β (Mooreβπ΅)))
β βπ§ β
(Mooreβπ΅)(mrClsβπ§) = πΉ) |
5 | 3, 4 | mpan 689 |
. . 3
β’ (πΉ β (mrCls β
(Mooreβπ΅)) β
βπ§ β
(Mooreβπ΅)(mrClsβπ§) = πΉ) |
6 | | elfvex 6881 |
. . . . . 6
β’ (π§ β (Mooreβπ΅) β π΅ β V) |
7 | | eqid 2737 |
. . . . . . . 8
β’
(mrClsβπ§) =
(mrClsβπ§) |
8 | 7 | mrcf 17490 |
. . . . . . 7
β’ (π§ β (Mooreβπ΅) β (mrClsβπ§):π« π΅βΆπ§) |
9 | | mresspw 17473 |
. . . . . . 7
β’ (π§ β (Mooreβπ΅) β π§ β π« π΅) |
10 | 8, 9 | fssd 6687 |
. . . . . 6
β’ (π§ β (Mooreβπ΅) β (mrClsβπ§):π« π΅βΆπ« π΅) |
11 | 7 | mrcssid 17498 |
. . . . . . . . . 10
β’ ((π§ β (Mooreβπ΅) β§ π₯ β π΅) β π₯ β ((mrClsβπ§)βπ₯)) |
12 | 11 | adantrr 716 |
. . . . . . . . 9
β’ ((π§ β (Mooreβπ΅) β§ (π₯ β π΅ β§ π¦ β π₯)) β π₯ β ((mrClsβπ§)βπ₯)) |
13 | 7 | mrcss 17497 |
. . . . . . . . . . 11
β’ ((π§ β (Mooreβπ΅) β§ π¦ β π₯ β§ π₯ β π΅) β ((mrClsβπ§)βπ¦) β ((mrClsβπ§)βπ₯)) |
14 | 13 | 3expb 1121 |
. . . . . . . . . 10
β’ ((π§ β (Mooreβπ΅) β§ (π¦ β π₯ β§ π₯ β π΅)) β ((mrClsβπ§)βπ¦) β ((mrClsβπ§)βπ₯)) |
15 | 14 | ancom2s 649 |
. . . . . . . . 9
β’ ((π§ β (Mooreβπ΅) β§ (π₯ β π΅ β§ π¦ β π₯)) β ((mrClsβπ§)βπ¦) β ((mrClsβπ§)βπ₯)) |
16 | 7 | mrcidm 17500 |
. . . . . . . . . 10
β’ ((π§ β (Mooreβπ΅) β§ π₯ β π΅) β ((mrClsβπ§)β((mrClsβπ§)βπ₯)) = ((mrClsβπ§)βπ₯)) |
17 | 16 | adantrr 716 |
. . . . . . . . 9
β’ ((π§ β (Mooreβπ΅) β§ (π₯ β π΅ β§ π¦ β π₯)) β ((mrClsβπ§)β((mrClsβπ§)βπ₯)) = ((mrClsβπ§)βπ₯)) |
18 | 12, 15, 17 | 3jca 1129 |
. . . . . . . 8
β’ ((π§ β (Mooreβπ΅) β§ (π₯ β π΅ β§ π¦ β π₯)) β (π₯ β ((mrClsβπ§)βπ₯) β§ ((mrClsβπ§)βπ¦) β ((mrClsβπ§)βπ₯) β§ ((mrClsβπ§)β((mrClsβπ§)βπ₯)) = ((mrClsβπ§)βπ₯))) |
19 | 18 | ex 414 |
. . . . . . 7
β’ (π§ β (Mooreβπ΅) β ((π₯ β π΅ β§ π¦ β π₯) β (π₯ β ((mrClsβπ§)βπ₯) β§ ((mrClsβπ§)βπ¦) β ((mrClsβπ§)βπ₯) β§ ((mrClsβπ§)β((mrClsβπ§)βπ₯)) = ((mrClsβπ§)βπ₯)))) |
20 | 19 | alrimivv 1932 |
. . . . . 6
β’ (π§ β (Mooreβπ΅) β βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β ((mrClsβπ§)βπ₯) β§ ((mrClsβπ§)βπ¦) β ((mrClsβπ§)βπ₯) β§ ((mrClsβπ§)β((mrClsβπ§)βπ₯)) = ((mrClsβπ§)βπ₯)))) |
21 | 6, 10, 20 | 3jca 1129 |
. . . . 5
β’ (π§ β (Mooreβπ΅) β (π΅ β V β§ (mrClsβπ§):π« π΅βΆπ« π΅ β§ βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β ((mrClsβπ§)βπ₯) β§ ((mrClsβπ§)βπ¦) β ((mrClsβπ§)βπ₯) β§ ((mrClsβπ§)β((mrClsβπ§)βπ₯)) = ((mrClsβπ§)βπ₯))))) |
22 | | feq1 6650 |
. . . . . 6
β’
((mrClsβπ§) =
πΉ β
((mrClsβπ§):π«
π΅βΆπ« π΅ β πΉ:π« π΅βΆπ« π΅)) |
23 | | fveq1 6842 |
. . . . . . . . . 10
β’
((mrClsβπ§) =
πΉ β
((mrClsβπ§)βπ₯) = (πΉβπ₯)) |
24 | 23 | sseq2d 3977 |
. . . . . . . . 9
β’
((mrClsβπ§) =
πΉ β (π₯ β ((mrClsβπ§)βπ₯) β π₯ β (πΉβπ₯))) |
25 | | fveq1 6842 |
. . . . . . . . . 10
β’
((mrClsβπ§) =
πΉ β
((mrClsβπ§)βπ¦) = (πΉβπ¦)) |
26 | 25, 23 | sseq12d 3978 |
. . . . . . . . 9
β’
((mrClsβπ§) =
πΉ β
(((mrClsβπ§)βπ¦) β ((mrClsβπ§)βπ₯) β (πΉβπ¦) β (πΉβπ₯))) |
27 | | id 22 |
. . . . . . . . . . 11
β’
((mrClsβπ§) =
πΉ β (mrClsβπ§) = πΉ) |
28 | 27, 23 | fveq12d 6850 |
. . . . . . . . . 10
β’
((mrClsβπ§) =
πΉ β
((mrClsβπ§)β((mrClsβπ§)βπ₯)) = (πΉβ(πΉβπ₯))) |
29 | 28, 23 | eqeq12d 2753 |
. . . . . . . . 9
β’
((mrClsβπ§) =
πΉ β
(((mrClsβπ§)β((mrClsβπ§)βπ₯)) = ((mrClsβπ§)βπ₯) β (πΉβ(πΉβπ₯)) = (πΉβπ₯))) |
30 | 24, 26, 29 | 3anbi123d 1437 |
. . . . . . . 8
β’
((mrClsβπ§) =
πΉ β ((π₯ β ((mrClsβπ§)βπ₯) β§ ((mrClsβπ§)βπ¦) β ((mrClsβπ§)βπ₯) β§ ((mrClsβπ§)β((mrClsβπ§)βπ₯)) = ((mrClsβπ§)βπ₯)) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯)))) |
31 | 30 | imbi2d 341 |
. . . . . . 7
β’
((mrClsβπ§) =
πΉ β (((π₯ β π΅ β§ π¦ β π₯) β (π₯ β ((mrClsβπ§)βπ₯) β§ ((mrClsβπ§)βπ¦) β ((mrClsβπ§)βπ₯) β§ ((mrClsβπ§)β((mrClsβπ§)βπ₯)) = ((mrClsβπ§)βπ₯))) β ((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯))))) |
32 | 31 | 2albidv 1927 |
. . . . . 6
β’
((mrClsβπ§) =
πΉ β (βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β ((mrClsβπ§)βπ₯) β§ ((mrClsβπ§)βπ¦) β ((mrClsβπ§)βπ₯) β§ ((mrClsβπ§)β((mrClsβπ§)βπ₯)) = ((mrClsβπ§)βπ₯))) β βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯))))) |
33 | 22, 32 | 3anbi23d 1440 |
. . . . 5
β’
((mrClsβπ§) =
πΉ β ((π΅ β V β§
(mrClsβπ§):π«
π΅βΆπ« π΅ β§ βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β ((mrClsβπ§)βπ₯) β§ ((mrClsβπ§)βπ¦) β ((mrClsβπ§)βπ₯) β§ ((mrClsβπ§)β((mrClsβπ§)βπ₯)) = ((mrClsβπ§)βπ₯)))) β (π΅ β V β§ πΉ:π« π΅βΆπ« π΅ β§ βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯)))))) |
34 | 21, 33 | syl5ibcom 244 |
. . . 4
β’ (π§ β (Mooreβπ΅) β ((mrClsβπ§) = πΉ β (π΅ β V β§ πΉ:π« π΅βΆπ« π΅ β§ βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯)))))) |
35 | 34 | rexlimiv 3146 |
. . 3
β’
(βπ§ β
(Mooreβπ΅)(mrClsβπ§) = πΉ β (π΅ β V β§ πΉ:π« π΅βΆπ« π΅ β§ βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯))))) |
36 | 5, 35 | syl 17 |
. 2
β’ (πΉ β (mrCls β
(Mooreβπ΅)) β
(π΅ β V β§ πΉ:π« π΅βΆπ« π΅ β§ βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯))))) |
37 | | simp1 1137 |
. . . 4
β’ ((π΅ β V β§ πΉ:π« π΅βΆπ« π΅ β§ βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯)))) β π΅ β V) |
38 | | simp2 1138 |
. . . 4
β’ ((π΅ β V β§ πΉ:π« π΅βΆπ« π΅ β§ βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯)))) β πΉ:π« π΅βΆπ« π΅) |
39 | | ssid 3967 |
. . . . . . 7
β’ π§ β π§ |
40 | | 3simpb 1150 |
. . . . . . . . . . 11
β’ ((π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯)) β (π₯ β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯))) |
41 | 40 | imim2i 16 |
. . . . . . . . . 10
β’ (((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯))) β ((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯)))) |
42 | 41 | 2alimi 1815 |
. . . . . . . . 9
β’
(βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯))) β βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯)))) |
43 | | sseq1 3970 |
. . . . . . . . . . . . . 14
β’ (π₯ = π§ β (π₯ β π΅ β π§ β π΅)) |
44 | 43 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π₯ = π§ β§ π¦ = π§) β (π₯ β π΅ β π§ β π΅)) |
45 | | sseq12 3972 |
. . . . . . . . . . . . . 14
β’ ((π¦ = π§ β§ π₯ = π§) β (π¦ β π₯ β π§ β π§)) |
46 | 45 | ancoms 460 |
. . . . . . . . . . . . 13
β’ ((π₯ = π§ β§ π¦ = π§) β (π¦ β π₯ β π§ β π§)) |
47 | 44, 46 | anbi12d 632 |
. . . . . . . . . . . 12
β’ ((π₯ = π§ β§ π¦ = π§) β ((π₯ β π΅ β§ π¦ β π₯) β (π§ β π΅ β§ π§ β π§))) |
48 | | id 22 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π§ β π₯ = π§) |
49 | | fveq2 6843 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π§ β (πΉβπ₯) = (πΉβπ§)) |
50 | 48, 49 | sseq12d 3978 |
. . . . . . . . . . . . . 14
β’ (π₯ = π§ β (π₯ β (πΉβπ₯) β π§ β (πΉβπ§))) |
51 | 50 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π₯ = π§ β§ π¦ = π§) β (π₯ β (πΉβπ₯) β π§ β (πΉβπ§))) |
52 | | 2fveq3 6848 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π§ β (πΉβ(πΉβπ₯)) = (πΉβ(πΉβπ§))) |
53 | 52, 49 | eqeq12d 2753 |
. . . . . . . . . . . . . 14
β’ (π₯ = π§ β ((πΉβ(πΉβπ₯)) = (πΉβπ₯) β (πΉβ(πΉβπ§)) = (πΉβπ§))) |
54 | 53 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π₯ = π§ β§ π¦ = π§) β ((πΉβ(πΉβπ₯)) = (πΉβπ₯) β (πΉβ(πΉβπ§)) = (πΉβπ§))) |
55 | 51, 54 | anbi12d 632 |
. . . . . . . . . . . 12
β’ ((π₯ = π§ β§ π¦ = π§) β ((π₯ β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯)) β (π§ β (πΉβπ§) β§ (πΉβ(πΉβπ§)) = (πΉβπ§)))) |
56 | 47, 55 | imbi12d 345 |
. . . . . . . . . . 11
β’ ((π₯ = π§ β§ π¦ = π§) β (((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯))) β ((π§ β π΅ β§ π§ β π§) β (π§ β (πΉβπ§) β§ (πΉβ(πΉβπ§)) = (πΉβπ§))))) |
57 | 56 | spc2gv 3560 |
. . . . . . . . . 10
β’ ((π§ β V β§ π§ β V) β (βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯))) β ((π§ β π΅ β§ π§ β π§) β (π§ β (πΉβπ§) β§ (πΉβ(πΉβπ§)) = (πΉβπ§))))) |
58 | 57 | el2v 3454 |
. . . . . . . . 9
β’
(βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯))) β ((π§ β π΅ β§ π§ β π§) β (π§ β (πΉβπ§) β§ (πΉβ(πΉβπ§)) = (πΉβπ§)))) |
59 | 42, 58 | syl 17 |
. . . . . . . 8
β’
(βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯))) β ((π§ β π΅ β§ π§ β π§) β (π§ β (πΉβπ§) β§ (πΉβ(πΉβπ§)) = (πΉβπ§)))) |
60 | 59 | 3ad2ant3 1136 |
. . . . . . 7
β’ ((π΅ β V β§ πΉ:π« π΅βΆπ« π΅ β§ βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯)))) β ((π§ β π΅ β§ π§ β π§) β (π§ β (πΉβπ§) β§ (πΉβ(πΉβπ§)) = (πΉβπ§)))) |
61 | 39, 60 | mpan2i 696 |
. . . . . 6
β’ ((π΅ β V β§ πΉ:π« π΅βΆπ« π΅ β§ βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯)))) β (π§ β π΅ β (π§ β (πΉβπ§) β§ (πΉβ(πΉβπ§)) = (πΉβπ§)))) |
62 | 61 | imp 408 |
. . . . 5
β’ (((π΅ β V β§ πΉ:π« π΅βΆπ« π΅ β§ βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯)))) β§ π§ β π΅) β (π§ β (πΉβπ§) β§ (πΉβ(πΉβπ§)) = (πΉβπ§))) |
63 | 62 | simpld 496 |
. . . 4
β’ (((π΅ β V β§ πΉ:π« π΅βΆπ« π΅ β§ βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯)))) β§ π§ β π΅) β π§ β (πΉβπ§)) |
64 | | simp2 1138 |
. . . . . . . . 9
β’ ((π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯)) β (πΉβπ¦) β (πΉβπ₯)) |
65 | 64 | imim2i 16 |
. . . . . . . 8
β’ (((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯))) β ((π₯ β π΅ β§ π¦ β π₯) β (πΉβπ¦) β (πΉβπ₯))) |
66 | 65 | 2alimi 1815 |
. . . . . . 7
β’
(βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯))) β βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (πΉβπ¦) β (πΉβπ₯))) |
67 | 66 | 3ad2ant3 1136 |
. . . . . 6
β’ ((π΅ β V β§ πΉ:π« π΅βΆπ« π΅ β§ βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯)))) β βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (πΉβπ¦) β (πΉβπ₯))) |
68 | 43 | adantr 482 |
. . . . . . . . . 10
β’ ((π₯ = π§ β§ π¦ = π€) β (π₯ β π΅ β π§ β π΅)) |
69 | | sseq12 3972 |
. . . . . . . . . . 11
β’ ((π¦ = π€ β§ π₯ = π§) β (π¦ β π₯ β π€ β π§)) |
70 | 69 | ancoms 460 |
. . . . . . . . . 10
β’ ((π₯ = π§ β§ π¦ = π€) β (π¦ β π₯ β π€ β π§)) |
71 | 68, 70 | anbi12d 632 |
. . . . . . . . 9
β’ ((π₯ = π§ β§ π¦ = π€) β ((π₯ β π΅ β§ π¦ β π₯) β (π§ β π΅ β§ π€ β π§))) |
72 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π¦ = π€ β (πΉβπ¦) = (πΉβπ€)) |
73 | | sseq12 3972 |
. . . . . . . . . 10
β’ (((πΉβπ¦) = (πΉβπ€) β§ (πΉβπ₯) = (πΉβπ§)) β ((πΉβπ¦) β (πΉβπ₯) β (πΉβπ€) β (πΉβπ§))) |
74 | 72, 49, 73 | syl2anr 598 |
. . . . . . . . 9
β’ ((π₯ = π§ β§ π¦ = π€) β ((πΉβπ¦) β (πΉβπ₯) β (πΉβπ€) β (πΉβπ§))) |
75 | 71, 74 | imbi12d 345 |
. . . . . . . 8
β’ ((π₯ = π§ β§ π¦ = π€) β (((π₯ β π΅ β§ π¦ β π₯) β (πΉβπ¦) β (πΉβπ₯)) β ((π§ β π΅ β§ π€ β π§) β (πΉβπ€) β (πΉβπ§)))) |
76 | 75 | spc2gv 3560 |
. . . . . . 7
β’ ((π§ β V β§ π€ β V) β (βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (πΉβπ¦) β (πΉβπ₯)) β ((π§ β π΅ β§ π€ β π§) β (πΉβπ€) β (πΉβπ§)))) |
77 | 76 | el2v 3454 |
. . . . . 6
β’
(βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (πΉβπ¦) β (πΉβπ₯)) β ((π§ β π΅ β§ π€ β π§) β (πΉβπ€) β (πΉβπ§))) |
78 | 67, 77 | syl 17 |
. . . . 5
β’ ((π΅ β V β§ πΉ:π« π΅βΆπ« π΅ β§ βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯)))) β ((π§ β π΅ β§ π€ β π§) β (πΉβπ€) β (πΉβπ§))) |
79 | 78 | 3impib 1117 |
. . . 4
β’ (((π΅ β V β§ πΉ:π« π΅βΆπ« π΅ β§ βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯)))) β§ π§ β π΅ β§ π€ β π§) β (πΉβπ€) β (πΉβπ§)) |
80 | 62 | simprd 497 |
. . . 4
β’ (((π΅ β V β§ πΉ:π« π΅βΆπ« π΅ β§ βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯)))) β§ π§ β π΅) β (πΉβ(πΉβπ§)) = (πΉβπ§)) |
81 | 37, 38, 63, 79, 80 | ismrcd2 41025 |
. . 3
β’ ((π΅ β V β§ πΉ:π« π΅βΆπ« π΅ β§ βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯)))) β πΉ = (mrClsβdom (πΉ β© I ))) |
82 | 37, 38, 63, 79, 80 | ismrcd1 41024 |
. . . 4
β’ ((π΅ β V β§ πΉ:π« π΅βΆπ« π΅ β§ βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯)))) β dom (πΉ β© I ) β (Mooreβπ΅)) |
83 | | fvssunirn 6876 |
. . . . . 6
β’
(Mooreβπ΅)
β βͺ ran Moore |
84 | 1 | fndmi 6607 |
. . . . . 6
β’ dom mrCls
= βͺ ran Moore |
85 | 83, 84 | sseqtrri 3982 |
. . . . 5
β’
(Mooreβπ΅)
β dom mrCls |
86 | | funfvima2 7182 |
. . . . 5
β’ ((Fun
mrCls β§ (Mooreβπ΅)
β dom mrCls) β (dom (πΉ β© I ) β (Mooreβπ΅) β (mrClsβdom (πΉ β© I )) β (mrCls
β (Mooreβπ΅)))) |
87 | 3, 85, 86 | mp2an 691 |
. . . 4
β’ (dom
(πΉ β© I ) β
(Mooreβπ΅) β
(mrClsβdom (πΉ β© I
)) β (mrCls β (Mooreβπ΅))) |
88 | 82, 87 | syl 17 |
. . 3
β’ ((π΅ β V β§ πΉ:π« π΅βΆπ« π΅ β§ βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯)))) β (mrClsβdom (πΉ β© I )) β (mrCls
β (Mooreβπ΅))) |
89 | 81, 88 | eqeltrd 2838 |
. 2
β’ ((π΅ β V β§ πΉ:π« π΅βΆπ« π΅ β§ βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯)))) β πΉ β (mrCls β (Mooreβπ΅))) |
90 | 36, 89 | impbii 208 |
1
β’ (πΉ β (mrCls β
(Mooreβπ΅)) β
(π΅ β V β§ πΉ:π« π΅βΆπ« π΅ β§ βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯))))) |