Step | Hyp | Ref
| Expression |
1 | | ismrcd.f |
. . 3
β’ (π β πΉ:π« π΅βΆπ« π΅) |
2 | 1 | ffnd 6673 |
. 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 41068 |
. . 3
β’ (π β dom (πΉ β© I ) β (Mooreβπ΅)) |
8 | | eqid 2733 |
. . . 4
β’
(mrClsβdom (πΉ
β© I )) = (mrClsβdom (πΉ β© I )) |
9 | 8 | mrcf 17497 |
. . 3
β’ (dom
(πΉ β© I ) β
(Mooreβπ΅) β
(mrClsβdom (πΉ β© I
)):π« π΅βΆdom
(πΉ β© I
)) |
10 | | ffn 6672 |
. . 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 17511 |
. . . . . 6
β’ (π β ((mrClsβdom (πΉ β© I ))βπ§) β π΅) |
13 | 12 | adantr 482 |
. . . . 5
β’ ((π β§ π§ β π« π΅) β ((mrClsβdom (πΉ β© I ))βπ§) β π΅) |
14 | | elpwi 4571 |
. . . . . 6
β’ (π§ β π« π΅ β π§ β π΅) |
15 | 8 | mrcssid 17505 |
. . . . . 6
β’ ((dom
(πΉ β© I ) β
(Mooreβπ΅) β§ π§ β π΅) β π§ β ((mrClsβdom (πΉ β© I ))βπ§)) |
16 | 7, 14, 15 | syl2an 597 |
. . . . 5
β’ ((π β§ π§ β π« π΅) β π§ β ((mrClsβdom (πΉ β© I ))βπ§)) |
17 | 5 | 3expib 1123 |
. . . . . . . 8
β’ (π β ((π₯ β π΅ β§ π¦ β π₯) β (πΉβπ¦) β (πΉβπ₯))) |
18 | 17 | alrimivv 1932 |
. . . . . . 7
β’ (π β βπ¦βπ₯((π₯ β π΅ β§ π¦ β π₯) β (πΉβπ¦) β (πΉβπ₯))) |
19 | | vex 3451 |
. . . . . . . 8
β’ π§ β V |
20 | | fvex 6859 |
. . . . . . . 8
β’
((mrClsβdom (πΉ
β© I ))βπ§) β
V |
21 | | sseq1 3973 |
. . . . . . . . . . . 12
β’ (π₯ = ((mrClsβdom (πΉ β© I ))βπ§) β (π₯ β π΅ β ((mrClsβdom (πΉ β© I ))βπ§) β π΅)) |
22 | 21 | adantl 483 |
. . . . . . . . . . 11
β’ ((π¦ = π§ β§ π₯ = ((mrClsβdom (πΉ β© I ))βπ§)) β (π₯ β π΅ β ((mrClsβdom (πΉ β© I ))βπ§) β π΅)) |
23 | | sseq12 3975 |
. . . . . . . . . . 11
β’ ((π¦ = π§ β§ π₯ = ((mrClsβdom (πΉ β© I ))βπ§)) β (π¦ β π₯ β π§ β ((mrClsβdom (πΉ β© I ))βπ§))) |
24 | 22, 23 | anbi12d 632 |
. . . . . . . . . 10
β’ ((π¦ = π§ β§ π₯ = ((mrClsβdom (πΉ β© I ))βπ§)) β ((π₯ β π΅ β§ π¦ β π₯) β (((mrClsβdom (πΉ β© I ))βπ§) β π΅ β§ π§ β ((mrClsβdom (πΉ β© I ))βπ§)))) |
25 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π¦ = π§ β (πΉβπ¦) = (πΉβπ§)) |
26 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π₯ = ((mrClsβdom (πΉ β© I ))βπ§) β (πΉβπ₯) = (πΉβ((mrClsβdom (πΉ β© I ))βπ§))) |
27 | | sseq12 3975 |
. . . . . . . . . . 11
β’ (((πΉβπ¦) = (πΉβπ§) β§ (πΉβπ₯) = (πΉβ((mrClsβdom (πΉ β© I ))βπ§))) β ((πΉβπ¦) β (πΉβπ₯) β (πΉβπ§) β (πΉβ((mrClsβdom (πΉ β© I ))βπ§)))) |
28 | 25, 26, 27 | syl2an 597 |
. . . . . . . . . 10
β’ ((π¦ = π§ β§ π₯ = ((mrClsβdom (πΉ β© I ))βπ§)) β ((πΉβπ¦) β (πΉβπ₯) β (πΉβπ§) β (πΉβ((mrClsβdom (πΉ β© I ))βπ§)))) |
29 | 24, 28 | imbi12d 345 |
. . . . . . . . 9
β’ ((π¦ = π§ β§ π₯ = ((mrClsβdom (πΉ β© I ))βπ§)) β (((π₯ β π΅ β§ π¦ β π₯) β (πΉβπ¦) β (πΉβπ₯)) β ((((mrClsβdom (πΉ β© I ))βπ§) β π΅ β§ π§ β ((mrClsβdom (πΉ β© I ))βπ§)) β (πΉβπ§) β (πΉβ((mrClsβdom (πΉ β© I ))βπ§))))) |
30 | 29 | spc2gv 3561 |
. . . . . . . 8
β’ ((π§ β V β§
((mrClsβdom (πΉ β©
I ))βπ§) β V)
β (βπ¦βπ₯((π₯ β π΅ β§ π¦ β π₯) β (πΉβπ¦) β (πΉβπ₯)) β ((((mrClsβdom (πΉ β© I ))βπ§) β π΅ β§ π§ β ((mrClsβdom (πΉ β© I ))βπ§)) β (πΉβπ§) β (πΉβ((mrClsβdom (πΉ β© I ))βπ§))))) |
31 | 19, 20, 30 | mp2an 691 |
. . . . . . 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 482 |
. . . . 5
β’ ((π β§ π§ β π« π΅) β ((((mrClsβdom (πΉ β© I ))βπ§) β π΅ β§ π§ β ((mrClsβdom (πΉ β© I ))βπ§)) β (πΉβπ§) β (πΉβ((mrClsβdom (πΉ β© I ))βπ§)))) |
34 | 13, 16, 33 | mp2and 698 |
. . . 4
β’ ((π β§ π§ β π« π΅) β (πΉβπ§) β (πΉβ((mrClsβdom (πΉ β© I ))βπ§))) |
35 | 8 | mrccl 17499 |
. . . . . 6
β’ ((dom
(πΉ β© I ) β
(Mooreβπ΅) β§ π§ β π΅) β ((mrClsβdom (πΉ β© I ))βπ§) β dom (πΉ β© I )) |
36 | 7, 14, 35 | syl2an 597 |
. . . . 5
β’ ((π β§ π§ β π« π΅) β ((mrClsβdom (πΉ β© I ))βπ§) β dom (πΉ β© I )) |
37 | 2 | adantr 482 |
. . . . . 6
β’ ((π β§ π§ β π« π΅) β πΉ Fn π« π΅) |
38 | 20 | elpw 4568 |
. . . . . . . 8
β’
(((mrClsβdom (πΉ β© I ))βπ§) β π« π΅ β ((mrClsβdom (πΉ β© I ))βπ§) β π΅) |
39 | 12, 38 | sylibr 233 |
. . . . . . 7
β’ (π β ((mrClsβdom (πΉ β© I ))βπ§) β π« π΅) |
40 | 39 | adantr 482 |
. . . . . 6
β’ ((π β§ π§ β π« π΅) β ((mrClsβdom (πΉ β© I ))βπ§) β π« π΅) |
41 | | fnelfp 7125 |
. . . . . 6
β’ ((πΉ Fn π« π΅ β§ ((mrClsβdom (πΉ β© I ))βπ§) β π« π΅) β (((mrClsβdom (πΉ β© I ))βπ§) β dom (πΉ β© I ) β (πΉβ((mrClsβdom (πΉ β© I ))βπ§)) = ((mrClsβdom (πΉ β© I ))βπ§))) |
42 | 37, 40, 41 | syl2anc 585 |
. . . . 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 3988 |
. . 3
β’ ((π β§ π§ β π« π΅) β (πΉβπ§) β ((mrClsβdom (πΉ β© I ))βπ§)) |
45 | 7 | adantr 482 |
. . . 4
β’ ((π β§ π§ β π« π΅) β dom (πΉ β© I ) β (Mooreβπ΅)) |
46 | | sseq1 3973 |
. . . . . . . 8
β’ (π₯ = π§ β (π₯ β π΅ β π§ β π΅)) |
47 | 46 | anbi2d 630 |
. . . . . . 7
β’ (π₯ = π§ β ((π β§ π₯ β π΅) β (π β§ π§ β π΅))) |
48 | | id 22 |
. . . . . . . 8
β’ (π₯ = π§ β π₯ = π§) |
49 | | fveq2 6846 |
. . . . . . . 8
β’ (π₯ = π§ β (πΉβπ₯) = (πΉβπ§)) |
50 | 48, 49 | sseq12d 3981 |
. . . . . . 7
β’ (π₯ = π§ β (π₯ β (πΉβπ₯) β π§ β (πΉβπ§))) |
51 | 47, 50 | imbi12d 345 |
. . . . . 6
β’ (π₯ = π§ β (((π β§ π₯ β π΅) β π₯ β (πΉβπ₯)) β ((π β§ π§ β π΅) β π§ β (πΉβπ§)))) |
52 | 51, 4 | chvarvv 2003 |
. . . . 5
β’ ((π β§ π§ β π΅) β π§ β (πΉβπ§)) |
53 | 14, 52 | sylan2 594 |
. . . 4
β’ ((π β§ π§ β π« π΅) β π§ β (πΉβπ§)) |
54 | | 2fveq3 6851 |
. . . . . . . . 9
β’ (π₯ = π§ β (πΉβ(πΉβπ₯)) = (πΉβ(πΉβπ§))) |
55 | 54, 49 | eqeq12d 2749 |
. . . . . . . 8
β’ (π₯ = π§ β ((πΉβ(πΉβπ₯)) = (πΉβπ₯) β (πΉβ(πΉβπ§)) = (πΉβπ§))) |
56 | 47, 55 | imbi12d 345 |
. . . . . . 7
β’ (π₯ = π§ β (((π β§ π₯ β π΅) β (πΉβ(πΉβπ₯)) = (πΉβπ₯)) β ((π β§ π§ β π΅) β (πΉβ(πΉβπ§)) = (πΉβπ§)))) |
57 | 56, 6 | chvarvv 2003 |
. . . . . 6
β’ ((π β§ π§ β π΅) β (πΉβ(πΉβπ§)) = (πΉβπ§)) |
58 | 14, 57 | sylan2 594 |
. . . . 5
β’ ((π β§ π§ β π« π΅) β (πΉβ(πΉβπ§)) = (πΉβπ§)) |
59 | 1 | ffvelcdmda 7039 |
. . . . . 6
β’ ((π β§ π§ β π« π΅) β (πΉβπ§) β π« π΅) |
60 | | fnelfp 7125 |
. . . . . 6
β’ ((πΉ Fn π« π΅ β§ (πΉβπ§) β π« π΅) β ((πΉβπ§) β dom (πΉ β© I ) β (πΉβ(πΉβπ§)) = (πΉβπ§))) |
61 | 37, 59, 60 | syl2anc 585 |
. . . . 5
β’ ((π β§ π§ β π« π΅) β ((πΉβπ§) β dom (πΉ β© I ) β (πΉβ(πΉβπ§)) = (πΉβπ§))) |
62 | 58, 61 | mpbird 257 |
. . . 4
β’ ((π β§ π§ β π« π΅) β (πΉβπ§) β dom (πΉ β© I )) |
63 | 8 | mrcsscl 17508 |
. . . 4
β’ ((dom
(πΉ β© I ) β
(Mooreβπ΅) β§ π§ β (πΉβπ§) β§ (πΉβπ§) β dom (πΉ β© I )) β ((mrClsβdom (πΉ β© I ))βπ§) β (πΉβπ§)) |
64 | 45, 53, 62, 63 | syl3anc 1372 |
. . 3
β’ ((π β§ π§ β π« π΅) β ((mrClsβdom (πΉ β© I ))βπ§) β (πΉβπ§)) |
65 | 44, 64 | eqssd 3965 |
. 2
β’ ((π β§ π§ β π« π΅) β (πΉβπ§) = ((mrClsβdom (πΉ β© I ))βπ§)) |
66 | 2, 11, 65 | eqfnfvd 6989 |
1
β’ (π β πΉ = (mrClsβdom (πΉ β© I ))) |