Step | Hyp | Ref
| Expression |
1 | | ismrcd.f |
. . 3
β’ (π β πΉ:π« π΅βΆπ« π΅) |
2 | 1 | ffnd 6718 |
. 2
β’ (π β πΉ Fn π« π΅) |
3 | | ismrcd.b |
. . . 4
β’ (π β π΅ β π) |
4 | | ismrcd.e |
. . . 4
β’ ((π β§ π₯ β π΅) β π₯ β (πΉβπ₯)) |
5 | | ismrcd.m |
. . . 4
β’ ((π β§ π₯ β π΅ β§ π¦ β π₯) β (πΉβπ¦) β (πΉβπ₯)) |
6 | | ismrcd.i |
. . . 4
β’ ((π β§ π₯ β π΅) β (πΉβ(πΉβπ₯)) = (πΉβπ₯)) |
7 | 3, 1, 4, 5, 6 | ismrcd1 41426 |
. . 3
β’ (π β dom (πΉ β© I ) β (Mooreβπ΅)) |
8 | | eqid 2732 |
. . . 4
β’
(mrClsβdom (πΉ
β© I )) = (mrClsβdom (πΉ β© I )) |
9 | 8 | mrcf 17552 |
. . 3
β’ (dom
(πΉ β© I ) β
(Mooreβπ΅) β
(mrClsβdom (πΉ β© I
)):π« π΅βΆdom
(πΉ β© I
)) |
10 | | ffn 6717 |
. . 3
β’
((mrClsβdom (πΉ
β© I )):π« π΅βΆdom (πΉ β© I ) β (mrClsβdom (πΉ β© I )) Fn π« π΅) |
11 | 7, 9, 10 | 3syl 18 |
. 2
β’ (π β (mrClsβdom (πΉ β© I )) Fn π« π΅) |
12 | 7, 8 | mrcssvd 17566 |
. . . . . 6
β’ (π β ((mrClsβdom (πΉ β© I ))βπ§) β π΅) |
13 | 12 | adantr 481 |
. . . . 5
β’ ((π β§ π§ β π« π΅) β ((mrClsβdom (πΉ β© I ))βπ§) β π΅) |
14 | | elpwi 4609 |
. . . . . 6
β’ (π§ β π« π΅ β π§ β π΅) |
15 | 8 | mrcssid 17560 |
. . . . . 6
β’ ((dom
(πΉ β© I ) β
(Mooreβπ΅) β§ π§ β π΅) β π§ β ((mrClsβdom (πΉ β© I ))βπ§)) |
16 | 7, 14, 15 | syl2an 596 |
. . . . 5
β’ ((π β§ π§ β π« π΅) β π§ β ((mrClsβdom (πΉ β© I ))βπ§)) |
17 | 5 | 3expib 1122 |
. . . . . . . 8
β’ (π β ((π₯ β π΅ β§ π¦ β π₯) β (πΉβπ¦) β (πΉβπ₯))) |
18 | 17 | alrimivv 1931 |
. . . . . . 7
β’ (π β βπ¦βπ₯((π₯ β π΅ β§ π¦ β π₯) β (πΉβπ¦) β (πΉβπ₯))) |
19 | | vex 3478 |
. . . . . . . 8
β’ π§ β V |
20 | | fvex 6904 |
. . . . . . . 8
β’
((mrClsβdom (πΉ
β© I ))βπ§) β
V |
21 | | sseq1 4007 |
. . . . . . . . . . . 12
β’ (π₯ = ((mrClsβdom (πΉ β© I ))βπ§) β (π₯ β π΅ β ((mrClsβdom (πΉ β© I ))βπ§) β π΅)) |
22 | 21 | adantl 482 |
. . . . . . . . . . 11
β’ ((π¦ = π§ β§ π₯ = ((mrClsβdom (πΉ β© I ))βπ§)) β (π₯ β π΅ β ((mrClsβdom (πΉ β© I ))βπ§) β π΅)) |
23 | | sseq12 4009 |
. . . . . . . . . . 11
β’ ((π¦ = π§ β§ π₯ = ((mrClsβdom (πΉ β© I ))βπ§)) β (π¦ β π₯ β π§ β ((mrClsβdom (πΉ β© I ))βπ§))) |
24 | 22, 23 | anbi12d 631 |
. . . . . . . . . 10
β’ ((π¦ = π§ β§ π₯ = ((mrClsβdom (πΉ β© I ))βπ§)) β ((π₯ β π΅ β§ π¦ β π₯) β (((mrClsβdom (πΉ β© I ))βπ§) β π΅ β§ π§ β ((mrClsβdom (πΉ β© I ))βπ§)))) |
25 | | fveq2 6891 |
. . . . . . . . . . 11
β’ (π¦ = π§ β (πΉβπ¦) = (πΉβπ§)) |
26 | | fveq2 6891 |
. . . . . . . . . . 11
β’ (π₯ = ((mrClsβdom (πΉ β© I ))βπ§) β (πΉβπ₯) = (πΉβ((mrClsβdom (πΉ β© I ))βπ§))) |
27 | | sseq12 4009 |
. . . . . . . . . . 11
β’ (((πΉβπ¦) = (πΉβπ§) β§ (πΉβπ₯) = (πΉβ((mrClsβdom (πΉ β© I ))βπ§))) β ((πΉβπ¦) β (πΉβπ₯) β (πΉβπ§) β (πΉβ((mrClsβdom (πΉ β© I ))βπ§)))) |
28 | 25, 26, 27 | syl2an 596 |
. . . . . . . . . 10
β’ ((π¦ = π§ β§ π₯ = ((mrClsβdom (πΉ β© I ))βπ§)) β ((πΉβπ¦) β (πΉβπ₯) β (πΉβπ§) β (πΉβ((mrClsβdom (πΉ β© I ))βπ§)))) |
29 | 24, 28 | imbi12d 344 |
. . . . . . . . 9
β’ ((π¦ = π§ β§ π₯ = ((mrClsβdom (πΉ β© I ))βπ§)) β (((π₯ β π΅ β§ π¦ β π₯) β (πΉβπ¦) β (πΉβπ₯)) β ((((mrClsβdom (πΉ β© I ))βπ§) β π΅ β§ π§ β ((mrClsβdom (πΉ β© I ))βπ§)) β (πΉβπ§) β (πΉβ((mrClsβdom (πΉ β© I ))βπ§))))) |
30 | 29 | spc2gv 3590 |
. . . . . . . 8
β’ ((π§ β V β§
((mrClsβdom (πΉ β©
I ))βπ§) β V)
β (βπ¦βπ₯((π₯ β π΅ β§ π¦ β π₯) β (πΉβπ¦) β (πΉβπ₯)) β ((((mrClsβdom (πΉ β© I ))βπ§) β π΅ β§ π§ β ((mrClsβdom (πΉ β© I ))βπ§)) β (πΉβπ§) β (πΉβ((mrClsβdom (πΉ β© I ))βπ§))))) |
31 | 19, 20, 30 | mp2an 690 |
. . . . . . 7
β’
(βπ¦βπ₯((π₯ β π΅ β§ π¦ β π₯) β (πΉβπ¦) β (πΉβπ₯)) β ((((mrClsβdom (πΉ β© I ))βπ§) β π΅ β§ π§ β ((mrClsβdom (πΉ β© I ))βπ§)) β (πΉβπ§) β (πΉβ((mrClsβdom (πΉ β© I ))βπ§)))) |
32 | 18, 31 | syl 17 |
. . . . . 6
β’ (π β ((((mrClsβdom (πΉ β© I ))βπ§) β π΅ β§ π§ β ((mrClsβdom (πΉ β© I ))βπ§)) β (πΉβπ§) β (πΉβ((mrClsβdom (πΉ β© I ))βπ§)))) |
33 | 32 | adantr 481 |
. . . . 5
β’ ((π β§ π§ β π« π΅) β ((((mrClsβdom (πΉ β© I ))βπ§) β π΅ β§ π§ β ((mrClsβdom (πΉ β© I ))βπ§)) β (πΉβπ§) β (πΉβ((mrClsβdom (πΉ β© I ))βπ§)))) |
34 | 13, 16, 33 | mp2and 697 |
. . . 4
β’ ((π β§ π§ β π« π΅) β (πΉβπ§) β (πΉβ((mrClsβdom (πΉ β© I ))βπ§))) |
35 | 8 | mrccl 17554 |
. . . . . 6
β’ ((dom
(πΉ β© I ) β
(Mooreβπ΅) β§ π§ β π΅) β ((mrClsβdom (πΉ β© I ))βπ§) β dom (πΉ β© I )) |
36 | 7, 14, 35 | syl2an 596 |
. . . . 5
β’ ((π β§ π§ β π« π΅) β ((mrClsβdom (πΉ β© I ))βπ§) β dom (πΉ β© I )) |
37 | 2 | adantr 481 |
. . . . . 6
β’ ((π β§ π§ β π« π΅) β πΉ Fn π« π΅) |
38 | 20 | elpw 4606 |
. . . . . . . 8
β’
(((mrClsβdom (πΉ β© I ))βπ§) β π« π΅ β ((mrClsβdom (πΉ β© I ))βπ§) β π΅) |
39 | 12, 38 | sylibr 233 |
. . . . . . 7
β’ (π β ((mrClsβdom (πΉ β© I ))βπ§) β π« π΅) |
40 | 39 | adantr 481 |
. . . . . 6
β’ ((π β§ π§ β π« π΅) β ((mrClsβdom (πΉ β© I ))βπ§) β π« π΅) |
41 | | fnelfp 7172 |
. . . . . 6
β’ ((πΉ Fn π« π΅ β§ ((mrClsβdom (πΉ β© I ))βπ§) β π« π΅) β (((mrClsβdom (πΉ β© I ))βπ§) β dom (πΉ β© I ) β (πΉβ((mrClsβdom (πΉ β© I ))βπ§)) = ((mrClsβdom (πΉ β© I ))βπ§))) |
42 | 37, 40, 41 | syl2anc 584 |
. . . . 5
β’ ((π β§ π§ β π« π΅) β (((mrClsβdom (πΉ β© I ))βπ§) β dom (πΉ β© I ) β (πΉβ((mrClsβdom (πΉ β© I ))βπ§)) = ((mrClsβdom (πΉ β© I ))βπ§))) |
43 | 36, 42 | mpbid 231 |
. . . 4
β’ ((π β§ π§ β π« π΅) β (πΉβ((mrClsβdom (πΉ β© I ))βπ§)) = ((mrClsβdom (πΉ β© I ))βπ§)) |
44 | 34, 43 | sseqtrd 4022 |
. . 3
β’ ((π β§ π§ β π« π΅) β (πΉβπ§) β ((mrClsβdom (πΉ β© I ))βπ§)) |
45 | 7 | adantr 481 |
. . . 4
β’ ((π β§ π§ β π« π΅) β dom (πΉ β© I ) β (Mooreβπ΅)) |
46 | | sseq1 4007 |
. . . . . . . 8
β’ (π₯ = π§ β (π₯ β π΅ β π§ β π΅)) |
47 | 46 | anbi2d 629 |
. . . . . . 7
β’ (π₯ = π§ β ((π β§ π₯ β π΅) β (π β§ π§ β π΅))) |
48 | | id 22 |
. . . . . . . 8
β’ (π₯ = π§ β π₯ = π§) |
49 | | fveq2 6891 |
. . . . . . . 8
β’ (π₯ = π§ β (πΉβπ₯) = (πΉβπ§)) |
50 | 48, 49 | sseq12d 4015 |
. . . . . . 7
β’ (π₯ = π§ β (π₯ β (πΉβπ₯) β π§ β (πΉβπ§))) |
51 | 47, 50 | imbi12d 344 |
. . . . . 6
β’ (π₯ = π§ β (((π β§ π₯ β π΅) β π₯ β (πΉβπ₯)) β ((π β§ π§ β π΅) β π§ β (πΉβπ§)))) |
52 | 51, 4 | chvarvv 2002 |
. . . . 5
β’ ((π β§ π§ β π΅) β π§ β (πΉβπ§)) |
53 | 14, 52 | sylan2 593 |
. . . 4
β’ ((π β§ π§ β π« π΅) β π§ β (πΉβπ§)) |
54 | | 2fveq3 6896 |
. . . . . . . . 9
β’ (π₯ = π§ β (πΉβ(πΉβπ₯)) = (πΉβ(πΉβπ§))) |
55 | 54, 49 | eqeq12d 2748 |
. . . . . . . 8
β’ (π₯ = π§ β ((πΉβ(πΉβπ₯)) = (πΉβπ₯) β (πΉβ(πΉβπ§)) = (πΉβπ§))) |
56 | 47, 55 | imbi12d 344 |
. . . . . . 7
β’ (π₯ = π§ β (((π β§ π₯ β π΅) β (πΉβ(πΉβπ₯)) = (πΉβπ₯)) β ((π β§ π§ β π΅) β (πΉβ(πΉβπ§)) = (πΉβπ§)))) |
57 | 56, 6 | chvarvv 2002 |
. . . . . 6
β’ ((π β§ π§ β π΅) β (πΉβ(πΉβπ§)) = (πΉβπ§)) |
58 | 14, 57 | sylan2 593 |
. . . . 5
β’ ((π β§ π§ β π« π΅) β (πΉβ(πΉβπ§)) = (πΉβπ§)) |
59 | 1 | ffvelcdmda 7086 |
. . . . . 6
β’ ((π β§ π§ β π« π΅) β (πΉβπ§) β π« π΅) |
60 | | fnelfp 7172 |
. . . . . 6
β’ ((πΉ Fn π« π΅ β§ (πΉβπ§) β π« π΅) β ((πΉβπ§) β dom (πΉ β© I ) β (πΉβ(πΉβπ§)) = (πΉβπ§))) |
61 | 37, 59, 60 | syl2anc 584 |
. . . . 5
β’ ((π β§ π§ β π« π΅) β ((πΉβπ§) β dom (πΉ β© I ) β (πΉβ(πΉβπ§)) = (πΉβπ§))) |
62 | 58, 61 | mpbird 256 |
. . . 4
β’ ((π β§ π§ β π« π΅) β (πΉβπ§) β dom (πΉ β© I )) |
63 | 8 | mrcsscl 17563 |
. . . 4
β’ ((dom
(πΉ β© I ) β
(Mooreβπ΅) β§ π§ β (πΉβπ§) β§ (πΉβπ§) β dom (πΉ β© I )) β ((mrClsβdom (πΉ β© I ))βπ§) β (πΉβπ§)) |
64 | 45, 53, 62, 63 | syl3anc 1371 |
. . 3
β’ ((π β§ π§ β π« π΅) β ((mrClsβdom (πΉ β© I ))βπ§) β (πΉβπ§)) |
65 | 44, 64 | eqssd 3999 |
. 2
β’ ((π β§ π§ β π« π΅) β (πΉβπ§) = ((mrClsβdom (πΉ β© I ))βπ§)) |
66 | 2, 11, 65 | eqfnfvd 7035 |
1
β’ (π β πΉ = (mrClsβdom (πΉ β© I ))) |