Step | Hyp | Ref
| Expression |
1 | | fveq2 6819 |
. . . . . . . . . . 11
β’ (π = π΄ β (πβπ) = (πβπ΄)) |
2 | 1 | rneqd 5873 |
. . . . . . . . . 10
β’ (π = π΄ β ran (πβπ) = ran (πβπ΄)) |
3 | | eceq1 8599 |
. . . . . . . . . 10
β’ (π = π΄ β [π]π = [π΄]π) |
4 | 2, 3 | sseq12d 3964 |
. . . . . . . . 9
β’ (π = π΄ β (ran (πβπ) β [π]π β ran (πβπ΄) β [π΄]π)) |
5 | 4 | rspcv 3566 |
. . . . . . . 8
β’ (π΄ β π β (βπ β π ran (πβπ) β [π]π β ran (πβπ΄) β [π΄]π)) |
6 | 5 | adantr 481 |
. . . . . . 7
β’ ((π΄ β π β§ π΅ β ran (πβπ΄)) β (βπ β π ran (πβπ) β [π]π β ran (πβπ΄) β [π΄]π)) |
7 | | ssel 3924 |
. . . . . . . . 9
β’ (ran
(πβπ΄) β [π΄]π β (π΅ β ran (πβπ΄) β π΅ β [π΄]π)) |
8 | 7 | com12 32 |
. . . . . . . 8
β’ (π΅ β ran (πβπ΄) β (ran (πβπ΄) β [π΄]π β π΅ β [π΄]π)) |
9 | | simpl 483 |
. . . . . . . . . . 11
β’ ((π΅ β [π΄]π β§ π΄ β π) β π΅ β [π΄]π) |
10 | | elecg 8604 |
. . . . . . . . . . 11
β’ ((π΅ β [π΄]π β§ π΄ β π) β (π΅ β [π΄]π β π΄ππ΅)) |
11 | 9, 10 | mpbid 231 |
. . . . . . . . . 10
β’ ((π΅ β [π΄]π β§ π΄ β π) β π΄ππ΅) |
12 | | df-br 5090 |
. . . . . . . . . 10
β’ (π΄ππ΅ β β¨π΄, π΅β© β π) |
13 | 11, 12 | sylib 217 |
. . . . . . . . 9
β’ ((π΅ β [π΄]π β§ π΄ β π) β β¨π΄, π΅β© β π) |
14 | 13 | expcom 414 |
. . . . . . . 8
β’ (π΄ β π β (π΅ β [π΄]π β β¨π΄, π΅β© β π)) |
15 | 8, 14 | sylan9r 509 |
. . . . . . 7
β’ ((π΄ β π β§ π΅ β ran (πβπ΄)) β (ran (πβπ΄) β [π΄]π β β¨π΄, π΅β© β π)) |
16 | 6, 15 | syld 47 |
. . . . . 6
β’ ((π΄ β π β§ π΅ β ran (πβπ΄)) β (βπ β π ran (πβπ) β [π]π β β¨π΄, π΅β© β π)) |
17 | 16 | adantld 491 |
. . . . 5
β’ ((π΄ β π β§ π΅ β ran (πβπ΄)) β ((π Er π β§ βπ β π ran (πβπ) β [π]π) β β¨π΄, π΅β© β π)) |
18 | 17 | alrimiv 1929 |
. . . 4
β’ ((π΄ β π β§ π΅ β ran (πβπ΄)) β βπ((π Er π β§ βπ β π ran (πβπ) β [π]π) β β¨π΄, π΅β© β π)) |
19 | | opex 5403 |
. . . . 5
β’
β¨π΄, π΅β© β V |
20 | 19 | elintab 4904 |
. . . 4
β’
(β¨π΄, π΅β© β β© {π
β£ (π Er π β§ βπ β π ran (πβπ) β [π]π)} β βπ((π Er π β§ βπ β π ran (πβπ) β [π]π) β β¨π΄, π΅β© β π)) |
21 | 18, 20 | sylibr 233 |
. . 3
β’ ((π΄ β π β§ π΅ β ran (πβπ΄)) β β¨π΄, π΅β© β β©
{π β£ (π Er π β§ βπ β π ran (πβπ) β [π]π)}) |
22 | | efgval.w |
. . . 4
β’ π = ( I βWord (πΌ Γ
2o)) |
23 | | efgval.r |
. . . 4
β’ βΌ = (
~FG βπΌ) |
24 | | efgval2.m |
. . . 4
β’ π = (π¦ β πΌ, π§ β 2o β¦ β¨π¦, (1o β π§)β©) |
25 | | efgval2.t |
. . . 4
β’ π = (π£ β π β¦ (π β (0...(β―βπ£)), π€ β (πΌ Γ 2o) β¦ (π£ splice β¨π, π, β¨βπ€(πβπ€)ββ©β©))) |
26 | 22, 23, 24, 25 | efgval2 19417 |
. . 3
β’ βΌ =
β© {π β£ (π Er π β§ βπ β π ran (πβπ) β [π]π)} |
27 | 21, 26 | eleqtrrdi 2848 |
. 2
β’ ((π΄ β π β§ π΅ β ran (πβπ΄)) β β¨π΄, π΅β© β βΌ ) |
28 | | df-br 5090 |
. 2
β’ (π΄ βΌ π΅ β β¨π΄, π΅β© β βΌ ) |
29 | 27, 28 | sylibr 233 |
1
β’ ((π΄ β π β§ π΅ β ran (πβπ΄)) β π΄ βΌ π΅) |