Step | Hyp | Ref
| Expression |
1 | | simp1 1136 |
. . 3
β’ ((πΆ β (Mooreβπ) β§ π β π β§ π β π) β πΆ β (Mooreβπ)) |
2 | | mre1cl 17503 |
. . . . . . 7
β’ (πΆ β (Mooreβπ) β π β πΆ) |
3 | | elpw2g 5321 |
. . . . . . 7
β’ (π β πΆ β (π β π« π β π β π)) |
4 | 2, 3 | syl 17 |
. . . . . 6
β’ (πΆ β (Mooreβπ) β (π β π« π β π β π)) |
5 | 4 | biimpar 478 |
. . . . 5
β’ ((πΆ β (Mooreβπ) β§ π β π) β π β π« π) |
6 | 5 | 3adant3 1132 |
. . . 4
β’ ((πΆ β (Mooreβπ) β§ π β π β§ π β π) β π β π« π) |
7 | | elpw2g 5321 |
. . . . . . 7
β’ (π β πΆ β (π β π« π β π β π)) |
8 | 2, 7 | syl 17 |
. . . . . 6
β’ (πΆ β (Mooreβπ) β (π β π« π β π β π)) |
9 | 8 | biimpar 478 |
. . . . 5
β’ ((πΆ β (Mooreβπ) β§ π β π) β π β π« π) |
10 | 9 | 3adant2 1131 |
. . . 4
β’ ((πΆ β (Mooreβπ) β§ π β π β§ π β π) β π β π« π) |
11 | 6, 10 | prssd 4802 |
. . 3
β’ ((πΆ β (Mooreβπ) β§ π β π β§ π β π) β {π, π} β π« π) |
12 | | mrcfval.f |
. . . 4
β’ πΉ = (mrClsβπΆ) |
13 | 12 | mrcuni 17530 |
. . 3
β’ ((πΆ β (Mooreβπ) β§ {π, π} β π« π) β (πΉββͺ {π, π}) = (πΉββͺ (πΉ β {π, π}))) |
14 | 1, 11, 13 | syl2anc 584 |
. 2
β’ ((πΆ β (Mooreβπ) β§ π β π β§ π β π) β (πΉββͺ {π, π}) = (πΉββͺ (πΉ β {π, π}))) |
15 | | uniprg 4902 |
. . . 4
β’ ((π β π« π β§ π β π« π) β βͺ {π, π} = (π βͺ π)) |
16 | 6, 10, 15 | syl2anc 584 |
. . 3
β’ ((πΆ β (Mooreβπ) β§ π β π β§ π β π) β βͺ {π, π} = (π βͺ π)) |
17 | 16 | fveq2d 6866 |
. 2
β’ ((πΆ β (Mooreβπ) β§ π β π β§ π β π) β (πΉββͺ {π, π}) = (πΉβ(π βͺ π))) |
18 | 12 | mrcf 17518 |
. . . . . . . 8
β’ (πΆ β (Mooreβπ) β πΉ:π« πβΆπΆ) |
19 | 18 | ffnd 6689 |
. . . . . . 7
β’ (πΆ β (Mooreβπ) β πΉ Fn π« π) |
20 | 19 | 3ad2ant1 1133 |
. . . . . 6
β’ ((πΆ β (Mooreβπ) β§ π β π β§ π β π) β πΉ Fn π« π) |
21 | | fnimapr 6945 |
. . . . . 6
β’ ((πΉ Fn π« π β§ π β π« π β§ π β π« π) β (πΉ β {π, π}) = {(πΉβπ), (πΉβπ)}) |
22 | 20, 6, 10, 21 | syl3anc 1371 |
. . . . 5
β’ ((πΆ β (Mooreβπ) β§ π β π β§ π β π) β (πΉ β {π, π}) = {(πΉβπ), (πΉβπ)}) |
23 | 22 | unieqd 4899 |
. . . 4
β’ ((πΆ β (Mooreβπ) β§ π β π β§ π β π) β βͺ (πΉ β {π, π}) = βͺ {(πΉβπ), (πΉβπ)}) |
24 | | fvex 6875 |
. . . . 5
β’ (πΉβπ) β V |
25 | | fvex 6875 |
. . . . 5
β’ (πΉβπ) β V |
26 | 24, 25 | unipr 4903 |
. . . 4
β’ βͺ {(πΉβπ), (πΉβπ)} = ((πΉβπ) βͺ (πΉβπ)) |
27 | 23, 26 | eqtrdi 2787 |
. . 3
β’ ((πΆ β (Mooreβπ) β§ π β π β§ π β π) β βͺ (πΉ β {π, π}) = ((πΉβπ) βͺ (πΉβπ))) |
28 | 27 | fveq2d 6866 |
. 2
β’ ((πΆ β (Mooreβπ) β§ π β π β§ π β π) β (πΉββͺ (πΉ β {π, π})) = (πΉβ((πΉβπ) βͺ (πΉβπ)))) |
29 | 14, 17, 28 | 3eqtr3d 2779 |
1
β’ ((πΆ β (Mooreβπ) β§ π β π β§ π β π) β (πΉβ(π βͺ π)) = (πΉβ((πΉβπ) βͺ (πΉβπ)))) |