Step | Hyp | Ref
| Expression |
1 | | n0i 4298 |
. . . . . 6
β’ (πΉ β ran π β Β¬ ran π = β
) |
2 | | mrsubco.s |
. . . . . . 7
β’ π = (mRSubstβπ) |
3 | 2 | rnfvprc 6841 |
. . . . . 6
β’ (Β¬
π β V β ran π = β
) |
4 | 1, 3 | nsyl2 141 |
. . . . 5
β’ (πΉ β ran π β π β V) |
5 | | eqid 2737 |
. . . . . 6
β’
(mCNβπ) =
(mCNβπ) |
6 | | mrsubvrs.v |
. . . . . 6
β’ π = (mVRβπ) |
7 | | mrsubvrs.r |
. . . . . 6
β’ π
= (mRExβπ) |
8 | 5, 6, 7 | mrexval 34135 |
. . . . 5
β’ (π β V β π
= Word ((mCNβπ) βͺ π)) |
9 | 4, 8 | syl 17 |
. . . 4
β’ (πΉ β ran π β π
= Word ((mCNβπ) βͺ π)) |
10 | 9 | eleq2d 2824 |
. . 3
β’ (πΉ β ran π β (π β π
β π β Word ((mCNβπ) βͺ π))) |
11 | | fveq2 6847 |
. . . . . . . . 9
β’ (π£ = β
β (πΉβπ£) = (πΉββ
)) |
12 | 11 | rneqd 5898 |
. . . . . . . 8
β’ (π£ = β
β ran (πΉβπ£) = ran (πΉββ
)) |
13 | 12 | ineq1d 4176 |
. . . . . . 7
β’ (π£ = β
β (ran (πΉβπ£) β© π) = (ran (πΉββ
) β© π)) |
14 | | rneq 5896 |
. . . . . . . . . . . 12
β’ (π£ = β
β ran π£ = ran β
) |
15 | | rn0 5886 |
. . . . . . . . . . . 12
β’ ran
β
= β
|
16 | 14, 15 | eqtrdi 2793 |
. . . . . . . . . . 11
β’ (π£ = β
β ran π£ = β
) |
17 | 16 | ineq1d 4176 |
. . . . . . . . . 10
β’ (π£ = β
β (ran π£ β© π) = (β
β© π)) |
18 | | 0in 4358 |
. . . . . . . . . 10
β’ (β
β© π) =
β
|
19 | 17, 18 | eqtrdi 2793 |
. . . . . . . . 9
β’ (π£ = β
β (ran π£ β© π) = β
) |
20 | 19 | iuneq1d 4986 |
. . . . . . . 8
β’ (π£ = β
β βͺ π₯ β (ran π£ β© π)(ran (πΉββ¨βπ₯ββ©) β© π) = βͺ
π₯ β β
(ran
(πΉββ¨βπ₯ββ©) β© π)) |
21 | | 0iun 5028 |
. . . . . . . 8
β’ βͺ π₯ β β
(ran (πΉββ¨βπ₯ββ©) β© π) = β
|
22 | 20, 21 | eqtrdi 2793 |
. . . . . . 7
β’ (π£ = β
β βͺ π₯ β (ran π£ β© π)(ran (πΉββ¨βπ₯ββ©) β© π) = β
) |
23 | 13, 22 | eqeq12d 2753 |
. . . . . 6
β’ (π£ = β
β ((ran (πΉβπ£) β© π) = βͺ
π₯ β (ran π£ β© π)(ran (πΉββ¨βπ₯ββ©) β© π) β (ran (πΉββ
) β© π) = β
)) |
24 | 23 | imbi2d 341 |
. . . . 5
β’ (π£ = β
β ((πΉ β ran π β (ran (πΉβπ£) β© π) = βͺ
π₯ β (ran π£ β© π)(ran (πΉββ¨βπ₯ββ©) β© π)) β (πΉ β ran π β (ran (πΉββ
) β© π) = β
))) |
25 | | fveq2 6847 |
. . . . . . . . 9
β’ (π£ = π¦ β (πΉβπ£) = (πΉβπ¦)) |
26 | 25 | rneqd 5898 |
. . . . . . . 8
β’ (π£ = π¦ β ran (πΉβπ£) = ran (πΉβπ¦)) |
27 | 26 | ineq1d 4176 |
. . . . . . 7
β’ (π£ = π¦ β (ran (πΉβπ£) β© π) = (ran (πΉβπ¦) β© π)) |
28 | | rneq 5896 |
. . . . . . . . 9
β’ (π£ = π¦ β ran π£ = ran π¦) |
29 | 28 | ineq1d 4176 |
. . . . . . . 8
β’ (π£ = π¦ β (ran π£ β© π) = (ran π¦ β© π)) |
30 | 29 | iuneq1d 4986 |
. . . . . . 7
β’ (π£ = π¦ β βͺ
π₯ β (ran π£ β© π)(ran (πΉββ¨βπ₯ββ©) β© π) = βͺ
π₯ β (ran π¦ β© π)(ran (πΉββ¨βπ₯ββ©) β© π)) |
31 | 27, 30 | eqeq12d 2753 |
. . . . . 6
β’ (π£ = π¦ β ((ran (πΉβπ£) β© π) = βͺ
π₯ β (ran π£ β© π)(ran (πΉββ¨βπ₯ββ©) β© π) β (ran (πΉβπ¦) β© π) = βͺ
π₯ β (ran π¦ β© π)(ran (πΉββ¨βπ₯ββ©) β© π))) |
32 | 31 | imbi2d 341 |
. . . . 5
β’ (π£ = π¦ β ((πΉ β ran π β (ran (πΉβπ£) β© π) = βͺ
π₯ β (ran π£ β© π)(ran (πΉββ¨βπ₯ββ©) β© π)) β (πΉ β ran π β (ran (πΉβπ¦) β© π) = βͺ
π₯ β (ran π¦ β© π)(ran (πΉββ¨βπ₯ββ©) β© π)))) |
33 | | fveq2 6847 |
. . . . . . . . 9
β’ (π£ = (π¦ ++ β¨βπ§ββ©) β (πΉβπ£) = (πΉβ(π¦ ++ β¨βπ§ββ©))) |
34 | 33 | rneqd 5898 |
. . . . . . . 8
β’ (π£ = (π¦ ++ β¨βπ§ββ©) β ran (πΉβπ£) = ran (πΉβ(π¦ ++ β¨βπ§ββ©))) |
35 | 34 | ineq1d 4176 |
. . . . . . 7
β’ (π£ = (π¦ ++ β¨βπ§ββ©) β (ran (πΉβπ£) β© π) = (ran (πΉβ(π¦ ++ β¨βπ§ββ©)) β© π)) |
36 | | rneq 5896 |
. . . . . . . . 9
β’ (π£ = (π¦ ++ β¨βπ§ββ©) β ran π£ = ran (π¦ ++ β¨βπ§ββ©)) |
37 | 36 | ineq1d 4176 |
. . . . . . . 8
β’ (π£ = (π¦ ++ β¨βπ§ββ©) β (ran π£ β© π) = (ran (π¦ ++ β¨βπ§ββ©) β© π)) |
38 | 37 | iuneq1d 4986 |
. . . . . . 7
β’ (π£ = (π¦ ++ β¨βπ§ββ©) β βͺ π₯ β (ran π£ β© π)(ran (πΉββ¨βπ₯ββ©) β© π) = βͺ
π₯ β (ran (π¦ ++ β¨βπ§ββ©) β© π)(ran (πΉββ¨βπ₯ββ©) β© π)) |
39 | 35, 38 | eqeq12d 2753 |
. . . . . 6
β’ (π£ = (π¦ ++ β¨βπ§ββ©) β ((ran (πΉβπ£) β© π) = βͺ
π₯ β (ran π£ β© π)(ran (πΉββ¨βπ₯ββ©) β© π) β (ran (πΉβ(π¦ ++ β¨βπ§ββ©)) β© π) = βͺ
π₯ β (ran (π¦ ++ β¨βπ§ββ©) β© π)(ran (πΉββ¨βπ₯ββ©) β© π))) |
40 | 39 | imbi2d 341 |
. . . . 5
β’ (π£ = (π¦ ++ β¨βπ§ββ©) β ((πΉ β ran π β (ran (πΉβπ£) β© π) = βͺ
π₯ β (ran π£ β© π)(ran (πΉββ¨βπ₯ββ©) β© π)) β (πΉ β ran π β (ran (πΉβ(π¦ ++ β¨βπ§ββ©)) β© π) = βͺ
π₯ β (ran (π¦ ++ β¨βπ§ββ©) β© π)(ran (πΉββ¨βπ₯ββ©) β© π)))) |
41 | | fveq2 6847 |
. . . . . . . . 9
β’ (π£ = π β (πΉβπ£) = (πΉβπ)) |
42 | 41 | rneqd 5898 |
. . . . . . . 8
β’ (π£ = π β ran (πΉβπ£) = ran (πΉβπ)) |
43 | 42 | ineq1d 4176 |
. . . . . . 7
β’ (π£ = π β (ran (πΉβπ£) β© π) = (ran (πΉβπ) β© π)) |
44 | | rneq 5896 |
. . . . . . . . 9
β’ (π£ = π β ran π£ = ran π) |
45 | 44 | ineq1d 4176 |
. . . . . . . 8
β’ (π£ = π β (ran π£ β© π) = (ran π β© π)) |
46 | 45 | iuneq1d 4986 |
. . . . . . 7
β’ (π£ = π β βͺ
π₯ β (ran π£ β© π)(ran (πΉββ¨βπ₯ββ©) β© π) = βͺ
π₯ β (ran π β© π)(ran (πΉββ¨βπ₯ββ©) β© π)) |
47 | 43, 46 | eqeq12d 2753 |
. . . . . 6
β’ (π£ = π β ((ran (πΉβπ£) β© π) = βͺ
π₯ β (ran π£ β© π)(ran (πΉββ¨βπ₯ββ©) β© π) β (ran (πΉβπ) β© π) = βͺ
π₯ β (ran π β© π)(ran (πΉββ¨βπ₯ββ©) β© π))) |
48 | 47 | imbi2d 341 |
. . . . 5
β’ (π£ = π β ((πΉ β ran π β (ran (πΉβπ£) β© π) = βͺ
π₯ β (ran π£ β© π)(ran (πΉββ¨βπ₯ββ©) β© π)) β (πΉ β ran π β (ran (πΉβπ) β© π) = βͺ
π₯ β (ran π β© π)(ran (πΉββ¨βπ₯ββ©) β© π)))) |
49 | 2 | mrsub0 34150 |
. . . . . . . . 9
β’ (πΉ β ran π β (πΉββ
) = β
) |
50 | 49 | rneqd 5898 |
. . . . . . . 8
β’ (πΉ β ran π β ran (πΉββ
) = ran
β
) |
51 | 50, 15 | eqtrdi 2793 |
. . . . . . 7
β’ (πΉ β ran π β ran (πΉββ
) = β
) |
52 | 51 | ineq1d 4176 |
. . . . . 6
β’ (πΉ β ran π β (ran (πΉββ
) β© π) = (β
β© π)) |
53 | 52, 18 | eqtrdi 2793 |
. . . . 5
β’ (πΉ β ran π β (ran (πΉββ
) β© π) = β
) |
54 | | uneq1 4121 |
. . . . . . . 8
β’ ((ran
(πΉβπ¦) β© π) = βͺ
π₯ β (ran π¦ β© π)(ran (πΉββ¨βπ₯ββ©) β© π) β ((ran (πΉβπ¦) β© π) βͺ (ran (πΉββ¨βπ§ββ©) β© π)) = (βͺ
π₯ β (ran π¦ β© π)(ran (πΉββ¨βπ₯ββ©) β© π) βͺ (ran (πΉββ¨βπ§ββ©) β© π))) |
55 | | simpl 484 |
. . . . . . . . . . . . . 14
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β πΉ β ran π) |
56 | | simprl 770 |
. . . . . . . . . . . . . . 15
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β π¦ β Word ((mCNβπ) βͺ π)) |
57 | 9 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β π
= Word ((mCNβπ) βͺ π)) |
58 | 56, 57 | eleqtrrd 2841 |
. . . . . . . . . . . . . 14
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β π¦ β π
) |
59 | | simprr 772 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β π§ β ((mCNβπ) βͺ π)) |
60 | 59 | s1cld 14498 |
. . . . . . . . . . . . . . 15
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β β¨βπ§ββ© β Word ((mCNβπ) βͺ π)) |
61 | 60, 57 | eleqtrrd 2841 |
. . . . . . . . . . . . . 14
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β β¨βπ§ββ© β π
) |
62 | 2, 7 | mrsubccat 34152 |
. . . . . . . . . . . . . 14
β’ ((πΉ β ran π β§ π¦ β π
β§ β¨βπ§ββ© β π
) β (πΉβ(π¦ ++ β¨βπ§ββ©)) = ((πΉβπ¦) ++ (πΉββ¨βπ§ββ©))) |
63 | 55, 58, 61, 62 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β (πΉβ(π¦ ++ β¨βπ§ββ©)) = ((πΉβπ¦) ++ (πΉββ¨βπ§ββ©))) |
64 | 63 | rneqd 5898 |
. . . . . . . . . . . 12
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β ran (πΉβ(π¦ ++ β¨βπ§ββ©)) = ran ((πΉβπ¦) ++ (πΉββ¨βπ§ββ©))) |
65 | 2, 7 | mrsubf 34151 |
. . . . . . . . . . . . . . . 16
β’ (πΉ β ran π β πΉ:π
βΆπ
) |
66 | 65 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β πΉ:π
βΆπ
) |
67 | 66, 58 | ffvelcdmd 7041 |
. . . . . . . . . . . . . 14
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β (πΉβπ¦) β π
) |
68 | 67, 57 | eleqtrd 2840 |
. . . . . . . . . . . . 13
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β (πΉβπ¦) β Word ((mCNβπ) βͺ π)) |
69 | 66, 61 | ffvelcdmd 7041 |
. . . . . . . . . . . . . 14
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β (πΉββ¨βπ§ββ©) β π
) |
70 | 69, 57 | eleqtrd 2840 |
. . . . . . . . . . . . 13
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β (πΉββ¨βπ§ββ©) β Word ((mCNβπ) βͺ π)) |
71 | | ccatrn 14484 |
. . . . . . . . . . . . 13
β’ (((πΉβπ¦) β Word ((mCNβπ) βͺ π) β§ (πΉββ¨βπ§ββ©) β Word ((mCNβπ) βͺ π)) β ran ((πΉβπ¦) ++ (πΉββ¨βπ§ββ©)) = (ran (πΉβπ¦) βͺ ran (πΉββ¨βπ§ββ©))) |
72 | 68, 70, 71 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β ran ((πΉβπ¦) ++ (πΉββ¨βπ§ββ©)) = (ran (πΉβπ¦) βͺ ran (πΉββ¨βπ§ββ©))) |
73 | 64, 72 | eqtrd 2777 |
. . . . . . . . . . 11
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β ran (πΉβ(π¦ ++ β¨βπ§ββ©)) = (ran (πΉβπ¦) βͺ ran (πΉββ¨βπ§ββ©))) |
74 | 73 | ineq1d 4176 |
. . . . . . . . . 10
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β (ran (πΉβ(π¦ ++ β¨βπ§ββ©)) β© π) = ((ran (πΉβπ¦) βͺ ran (πΉββ¨βπ§ββ©)) β© π)) |
75 | | indir 4240 |
. . . . . . . . . 10
β’ ((ran
(πΉβπ¦) βͺ ran (πΉββ¨βπ§ββ©)) β© π) = ((ran (πΉβπ¦) β© π) βͺ (ran (πΉββ¨βπ§ββ©) β© π)) |
76 | 74, 75 | eqtrdi 2793 |
. . . . . . . . 9
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β (ran (πΉβ(π¦ ++ β¨βπ§ββ©)) β© π) = ((ran (πΉβπ¦) β© π) βͺ (ran (πΉββ¨βπ§ββ©) β© π))) |
77 | | ccatrn 14484 |
. . . . . . . . . . . . . . . 16
β’ ((π¦ β Word ((mCNβπ) βͺ π) β§ β¨βπ§ββ© β Word ((mCNβπ) βͺ π)) β ran (π¦ ++ β¨βπ§ββ©) = (ran π¦ βͺ ran β¨βπ§ββ©)) |
78 | 56, 60, 77 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β ran (π¦ ++ β¨βπ§ββ©) = (ran π¦ βͺ ran β¨βπ§ββ©)) |
79 | | s1rn 14494 |
. . . . . . . . . . . . . . . . 17
β’ (π§ β ((mCNβπ) βͺ π) β ran β¨βπ§ββ© = {π§}) |
80 | 79 | ad2antll 728 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β ran β¨βπ§ββ© = {π§}) |
81 | 80 | uneq2d 4128 |
. . . . . . . . . . . . . . 15
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β (ran π¦ βͺ ran β¨βπ§ββ©) = (ran π¦ βͺ {π§})) |
82 | 78, 81 | eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β ran (π¦ ++ β¨βπ§ββ©) = (ran π¦ βͺ {π§})) |
83 | 82 | ineq1d 4176 |
. . . . . . . . . . . . 13
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β (ran (π¦ ++ β¨βπ§ββ©) β© π) = ((ran π¦ βͺ {π§}) β© π)) |
84 | | indir 4240 |
. . . . . . . . . . . . 13
β’ ((ran
π¦ βͺ {π§}) β© π) = ((ran π¦ β© π) βͺ ({π§} β© π)) |
85 | 83, 84 | eqtrdi 2793 |
. . . . . . . . . . . 12
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β (ran (π¦ ++ β¨βπ§ββ©) β© π) = ((ran π¦ β© π) βͺ ({π§} β© π))) |
86 | 85 | iuneq1d 4986 |
. . . . . . . . . . 11
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β βͺ π₯ β (ran (π¦ ++ β¨βπ§ββ©) β© π)(ran (πΉββ¨βπ₯ββ©) β© π) = βͺ
π₯ β ((ran π¦ β© π) βͺ ({π§} β© π))(ran (πΉββ¨βπ₯ββ©) β© π)) |
87 | | iunxun 5059 |
. . . . . . . . . . 11
β’ βͺ π₯ β ((ran π¦ β© π) βͺ ({π§} β© π))(ran (πΉββ¨βπ₯ββ©) β© π) = (βͺ
π₯ β (ran π¦ β© π)(ran (πΉββ¨βπ₯ββ©) β© π) βͺ βͺ
π₯ β ({π§} β© π)(ran (πΉββ¨βπ₯ββ©) β© π)) |
88 | 86, 87 | eqtrdi 2793 |
. . . . . . . . . 10
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β βͺ π₯ β (ran (π¦ ++ β¨βπ§ββ©) β© π)(ran (πΉββ¨βπ₯ββ©) β© π) = (βͺ
π₯ β (ran π¦ β© π)(ran (πΉββ¨βπ₯ββ©) β© π) βͺ βͺ
π₯ β ({π§} β© π)(ran (πΉββ¨βπ₯ββ©) β© π))) |
89 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ (((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β§ π§ β π) β π§ β π) |
90 | 89 | snssd 4774 |
. . . . . . . . . . . . . . 15
β’ (((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β§ π§ β π) β {π§} β π) |
91 | | df-ss 3932 |
. . . . . . . . . . . . . . 15
β’ ({π§} β π β ({π§} β© π) = {π§}) |
92 | 90, 91 | sylib 217 |
. . . . . . . . . . . . . 14
β’ (((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β§ π§ β π) β ({π§} β© π) = {π§}) |
93 | 92 | iuneq1d 4986 |
. . . . . . . . . . . . 13
β’ (((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β§ π§ β π) β βͺ
π₯ β ({π§} β© π)(ran (πΉββ¨βπ₯ββ©) β© π) = βͺ
π₯ β {π§} (ran (πΉββ¨βπ₯ββ©) β© π)) |
94 | | vex 3452 |
. . . . . . . . . . . . . 14
β’ π§ β V |
95 | | s1eq 14495 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π§ β β¨βπ₯ββ© = β¨βπ§ββ©) |
96 | 95 | fveq2d 6851 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π§ β (πΉββ¨βπ₯ββ©) = (πΉββ¨βπ§ββ©)) |
97 | 96 | rneqd 5898 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π§ β ran (πΉββ¨βπ₯ββ©) = ran (πΉββ¨βπ§ββ©)) |
98 | 97 | ineq1d 4176 |
. . . . . . . . . . . . . 14
β’ (π₯ = π§ β (ran (πΉββ¨βπ₯ββ©) β© π) = (ran (πΉββ¨βπ§ββ©) β© π)) |
99 | 94, 98 | iunxsn 5056 |
. . . . . . . . . . . . 13
β’ βͺ π₯ β {π§} (ran (πΉββ¨βπ₯ββ©) β© π) = (ran (πΉββ¨βπ§ββ©) β© π) |
100 | 93, 99 | eqtrdi 2793 |
. . . . . . . . . . . 12
β’ (((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β§ π§ β π) β βͺ
π₯ β ({π§} β© π)(ran (πΉββ¨βπ₯ββ©) β© π) = (ran (πΉββ¨βπ§ββ©) β© π)) |
101 | | incom 4166 |
. . . . . . . . . . . . . . 15
β’ ({π§} β© π) = (π β© {π§}) |
102 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ (((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β§ Β¬ π§ β π) β Β¬ π§ β π) |
103 | | disjsn 4677 |
. . . . . . . . . . . . . . . 16
β’ ((π β© {π§}) = β
β Β¬ π§ β π) |
104 | 102, 103 | sylibr 233 |
. . . . . . . . . . . . . . 15
β’ (((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β§ Β¬ π§ β π) β (π β© {π§}) = β
) |
105 | 101, 104 | eqtrid 2789 |
. . . . . . . . . . . . . 14
β’ (((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β§ Β¬ π§ β π) β ({π§} β© π) = β
) |
106 | 105 | iuneq1d 4986 |
. . . . . . . . . . . . 13
β’ (((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β§ Β¬ π§ β π) β βͺ
π₯ β ({π§} β© π)(ran (πΉββ¨βπ₯ββ©) β© π) = βͺ
π₯ β β
(ran
(πΉββ¨βπ₯ββ©) β© π)) |
107 | 55 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β§ Β¬ π§ β π) β πΉ β ran π) |
108 | | eldif 3925 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π§ β (((mCNβπ) βͺ π) β π) β (π§ β ((mCNβπ) βͺ π) β§ Β¬ π§ β π)) |
109 | 108 | biimpri 227 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π§ β ((mCNβπ) βͺ π) β§ Β¬ π§ β π) β π§ β (((mCNβπ) βͺ π) β π)) |
110 | 59, 109 | sylan 581 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β§ Β¬ π§ β π) β π§ β (((mCNβπ) βͺ π) β π)) |
111 | | difun2 4445 |
. . . . . . . . . . . . . . . . . . 19
β’
(((mCNβπ)
βͺ π) β π) = ((mCNβπ) β π) |
112 | 110, 111 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β§ Β¬ π§ β π) β π§ β ((mCNβπ) β π)) |
113 | 2, 7, 6, 5 | mrsubcn 34153 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉ β ran π β§ π§ β ((mCNβπ) β π)) β (πΉββ¨βπ§ββ©) = β¨βπ§ββ©) |
114 | 107, 112,
113 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ (((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β§ Β¬ π§ β π) β (πΉββ¨βπ§ββ©) = β¨βπ§ββ©) |
115 | 114 | rneqd 5898 |
. . . . . . . . . . . . . . . 16
β’ (((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β§ Β¬ π§ β π) β ran (πΉββ¨βπ§ββ©) = ran β¨βπ§ββ©) |
116 | 80 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β§ Β¬ π§ β π) β ran β¨βπ§ββ© = {π§}) |
117 | 115, 116 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
β’ (((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β§ Β¬ π§ β π) β ran (πΉββ¨βπ§ββ©) = {π§}) |
118 | 117 | ineq1d 4176 |
. . . . . . . . . . . . . 14
β’ (((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β§ Β¬ π§ β π) β (ran (πΉββ¨βπ§ββ©) β© π) = ({π§} β© π)) |
119 | 118, 105 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β§ Β¬ π§ β π) β (ran (πΉββ¨βπ§ββ©) β© π) = β
) |
120 | 21, 106, 119 | 3eqtr4a 2803 |
. . . . . . . . . . . 12
β’ (((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β§ Β¬ π§ β π) β βͺ
π₯ β ({π§} β© π)(ran (πΉββ¨βπ₯ββ©) β© π) = (ran (πΉββ¨βπ§ββ©) β© π)) |
121 | 100, 120 | pm2.61dan 812 |
. . . . . . . . . . 11
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β βͺ π₯ β ({π§} β© π)(ran (πΉββ¨βπ₯ββ©) β© π) = (ran (πΉββ¨βπ§ββ©) β© π)) |
122 | 121 | uneq2d 4128 |
. . . . . . . . . 10
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β (βͺ π₯ β (ran π¦ β© π)(ran (πΉββ¨βπ₯ββ©) β© π) βͺ βͺ
π₯ β ({π§} β© π)(ran (πΉββ¨βπ₯ββ©) β© π)) = (βͺ
π₯ β (ran π¦ β© π)(ran (πΉββ¨βπ₯ββ©) β© π) βͺ (ran (πΉββ¨βπ§ββ©) β© π))) |
123 | 88, 122 | eqtrd 2777 |
. . . . . . . . 9
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β βͺ π₯ β (ran (π¦ ++ β¨βπ§ββ©) β© π)(ran (πΉββ¨βπ₯ββ©) β© π) = (βͺ
π₯ β (ran π¦ β© π)(ran (πΉββ¨βπ₯ββ©) β© π) βͺ (ran (πΉββ¨βπ§ββ©) β© π))) |
124 | 76, 123 | eqeq12d 2753 |
. . . . . . . 8
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β ((ran (πΉβ(π¦ ++ β¨βπ§ββ©)) β© π) = βͺ
π₯ β (ran (π¦ ++ β¨βπ§ββ©) β© π)(ran (πΉββ¨βπ₯ββ©) β© π) β ((ran (πΉβπ¦) β© π) βͺ (ran (πΉββ¨βπ§ββ©) β© π)) = (βͺ
π₯ β (ran π¦ β© π)(ran (πΉββ¨βπ₯ββ©) β© π) βͺ (ran (πΉββ¨βπ§ββ©) β© π)))) |
125 | 54, 124 | syl5ibr 246 |
. . . . . . 7
β’ ((πΉ β ran π β§ (π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π))) β ((ran (πΉβπ¦) β© π) = βͺ
π₯ β (ran π¦ β© π)(ran (πΉββ¨βπ₯ββ©) β© π) β (ran (πΉβ(π¦ ++ β¨βπ§ββ©)) β© π) = βͺ
π₯ β (ran (π¦ ++ β¨βπ§ββ©) β© π)(ran (πΉββ¨βπ₯ββ©) β© π))) |
126 | 125 | expcom 415 |
. . . . . 6
β’ ((π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π)) β (πΉ β ran π β ((ran (πΉβπ¦) β© π) = βͺ
π₯ β (ran π¦ β© π)(ran (πΉββ¨βπ₯ββ©) β© π) β (ran (πΉβ(π¦ ++ β¨βπ§ββ©)) β© π) = βͺ
π₯ β (ran (π¦ ++ β¨βπ§ββ©) β© π)(ran (πΉββ¨βπ₯ββ©) β© π)))) |
127 | 126 | a2d 29 |
. . . . 5
β’ ((π¦ β Word ((mCNβπ) βͺ π) β§ π§ β ((mCNβπ) βͺ π)) β ((πΉ β ran π β (ran (πΉβπ¦) β© π) = βͺ
π₯ β (ran π¦ β© π)(ran (πΉββ¨βπ₯ββ©) β© π)) β (πΉ β ran π β (ran (πΉβ(π¦ ++ β¨βπ§ββ©)) β© π) = βͺ
π₯ β (ran (π¦ ++ β¨βπ§ββ©) β© π)(ran (πΉββ¨βπ₯ββ©) β© π)))) |
128 | 24, 32, 40, 48, 53, 127 | wrdind 14617 |
. . . 4
β’ (π β Word ((mCNβπ) βͺ π) β (πΉ β ran π β (ran (πΉβπ) β© π) = βͺ
π₯ β (ran π β© π)(ran (πΉββ¨βπ₯ββ©) β© π))) |
129 | 128 | com12 32 |
. . 3
β’ (πΉ β ran π β (π β Word ((mCNβπ) βͺ π) β (ran (πΉβπ) β© π) = βͺ
π₯ β (ran π β© π)(ran (πΉββ¨βπ₯ββ©) β© π))) |
130 | 10, 129 | sylbid 239 |
. 2
β’ (πΉ β ran π β (π β π
β (ran (πΉβπ) β© π) = βͺ
π₯ β (ran π β© π)(ran (πΉββ¨βπ₯ββ©) β© π))) |
131 | 130 | imp 408 |
1
β’ ((πΉ β ran π β§ π β π
) β (ran (πΉβπ) β© π) = βͺ
π₯ β (ran π β© π)(ran (πΉββ¨βπ₯ββ©) β© π)) |