Step | Hyp | Ref
| Expression |
1 | | efgval.r |
. 2
β’ βΌ = (
~FG βπΌ) |
2 | | vex 3451 |
. . . . . . . . . . . 12
β’ π β V |
3 | | 2on 8430 |
. . . . . . . . . . . . 13
β’
2o β On |
4 | 3 | elexi 3466 |
. . . . . . . . . . . 12
β’
2o β V |
5 | 2, 4 | xpex 7691 |
. . . . . . . . . . 11
β’ (π Γ 2o) β
V |
6 | | wrdexg 14421 |
. . . . . . . . . . 11
β’ ((π Γ 2o) β V
β Word (π Γ
2o) β V) |
7 | | fvi 6921 |
. . . . . . . . . . 11
β’ (Word
(π Γ 2o)
β V β ( I βWord (π Γ 2o)) = Word (π Γ
2o)) |
8 | 5, 6, 7 | mp2b 10 |
. . . . . . . . . 10
β’ ( I
βWord (π Γ
2o)) = Word (π
Γ 2o) |
9 | | xpeq1 5651 |
. . . . . . . . . . . 12
β’ (π = πΌ β (π Γ 2o) = (πΌ Γ 2o)) |
10 | | wrdeq 14433 |
. . . . . . . . . . . 12
β’ ((π Γ 2o) = (πΌ Γ 2o) β
Word (π Γ
2o) = Word (πΌ
Γ 2o)) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . 11
β’ (π = πΌ β Word (π Γ 2o) = Word (πΌ Γ
2o)) |
12 | 11 | fveq2d 6850 |
. . . . . . . . . 10
β’ (π = πΌ β ( I βWord (π Γ 2o)) = ( I βWord
(πΌ Γ
2o))) |
13 | 8, 12 | eqtr3id 2787 |
. . . . . . . . 9
β’ (π = πΌ β Word (π Γ 2o) = ( I βWord
(πΌ Γ
2o))) |
14 | | efgval.w |
. . . . . . . . 9
β’ π = ( I βWord (πΌ Γ
2o)) |
15 | 13, 14 | eqtr4di 2791 |
. . . . . . . 8
β’ (π = πΌ β Word (π Γ 2o) = π) |
16 | | ereq2 8662 |
. . . . . . . 8
β’ (Word
(π Γ 2o) =
π β (π Er Word (π Γ 2o) β π Er π)) |
17 | 15, 16 | syl 17 |
. . . . . . 7
β’ (π = πΌ β (π Er Word (π Γ 2o) β π Er π)) |
18 | | raleq 3308 |
. . . . . . . . 9
β’ (π = πΌ β (βπ¦ β π βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©) β
βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))) |
19 | 18 | ralbidv 3171 |
. . . . . . . 8
β’ (π = πΌ β (βπ β (0...(β―βπ₯))βπ¦ β π βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©) β
βπ β
(0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))) |
20 | 15, 19 | raleqbidv 3318 |
. . . . . . 7
β’ (π = πΌ β (βπ₯ β Word (π Γ 2o)βπ β
(0...(β―βπ₯))βπ¦ β π βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©) β
βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))) |
21 | 17, 20 | anbi12d 632 |
. . . . . 6
β’ (π = πΌ β ((π Er Word (π Γ 2o) β§ βπ₯ β Word (π Γ 2o)βπ β
(0...(β―βπ₯))βπ¦ β π βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©)) β (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©)))) |
22 | 21 | abbidv 2802 |
. . . . 5
β’ (π = πΌ β {π β£ (π Er Word (π Γ 2o) β§ βπ₯ β Word (π Γ 2o)βπ β
(0...(β―βπ₯))βπ¦ β π βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))} = {π β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))}) |
23 | 22 | inteqd 4916 |
. . . 4
β’ (π = πΌ β β© {π β£ (π Er Word (π Γ 2o) β§ βπ₯ β Word (π Γ 2o)βπ β
(0...(β―βπ₯))βπ¦ β π βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))} = β© {π
β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))}) |
24 | | df-efg 19499 |
. . . 4
β’
~FG = (π
β V β¦ β© {π β£ (π Er Word (π Γ 2o) β§ βπ₯ β Word (π Γ 2o)βπ β
(0...(β―βπ₯))βπ¦ β π βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))}) |
25 | 14 | efglem 19506 |
. . . . 5
β’
βπ(π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©)) |
26 | | intexab 5300 |
. . . . 5
β’
(βπ(π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©)) β β© {π
β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))} β
V) |
27 | 25, 26 | mpbi 229 |
. . . 4
β’ β© {π
β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))} β
V |
28 | 23, 24, 27 | fvmpt 6952 |
. . 3
β’ (πΌ β V β (
~FG βπΌ) = β© {π β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))}) |
29 | | fvprc 6838 |
. . . 4
β’ (Β¬
πΌ β V β (
~FG βπΌ) = β
) |
30 | | abn0 4344 |
. . . . . . . 8
β’ ({π β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))} β β
β βπ(π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))) |
31 | 25, 30 | mpbir 230 |
. . . . . . 7
β’ {π β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))} β
β
|
32 | | intssuni 4935 |
. . . . . . 7
β’ ({π β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))} β β
β β© {π β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))} β βͺ {π
β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))}) |
33 | 31, 32 | ax-mp 5 |
. . . . . 6
β’ β© {π
β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))} β βͺ {π
β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))} |
34 | | erssxp 8677 |
. . . . . . . . . . . 12
β’ (π Er π β π β (π Γ π)) |
35 | 14 | efgrcl 19505 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β π β (πΌ β V β§ π = Word (πΌ Γ 2o))) |
36 | 35 | simpld 496 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β π β πΌ β V) |
37 | 36 | con3i 154 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
πΌ β V β Β¬
π₯ β π) |
38 | 37 | eq0rdv 4368 |
. . . . . . . . . . . . . . 15
β’ (Β¬
πΌ β V β π = β
) |
39 | 38 | xpeq2d 5667 |
. . . . . . . . . . . . . 14
β’ (Β¬
πΌ β V β (π Γ π) = (π Γ β
)) |
40 | | xp0 6114 |
. . . . . . . . . . . . . 14
β’ (π Γ β
) =
β
|
41 | 39, 40 | eqtrdi 2789 |
. . . . . . . . . . . . 13
β’ (Β¬
πΌ β V β (π Γ π) = β
) |
42 | | ss0b 4361 |
. . . . . . . . . . . . 13
β’ ((π Γ π) β β
β (π Γ π) = β
) |
43 | 41, 42 | sylibr 233 |
. . . . . . . . . . . 12
β’ (Β¬
πΌ β V β (π Γ π) β β
) |
44 | 34, 43 | sylan9ssr 3962 |
. . . . . . . . . . 11
β’ ((Β¬
πΌ β V β§ π Er π) β π β β
) |
45 | 44 | ex 414 |
. . . . . . . . . 10
β’ (Β¬
πΌ β V β (π Er π β π β β
)) |
46 | 45 | adantrd 493 |
. . . . . . . . 9
β’ (Β¬
πΌ β V β ((π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©)) β π β
β
)) |
47 | 46 | alrimiv 1931 |
. . . . . . . 8
β’ (Β¬
πΌ β V β
βπ((π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©)) β π β
β
)) |
48 | | sseq1 3973 |
. . . . . . . . 9
β’ (π€ = π β (π€ β β
β π β β
)) |
49 | 48 | ralab2 3659 |
. . . . . . . 8
β’
(βπ€ β
{π β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))}π€ β β
β
βπ((π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©)) β π β
β
)) |
50 | 47, 49 | sylibr 233 |
. . . . . . 7
β’ (Β¬
πΌ β V β
βπ€ β {π β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))}π€ β
β
) |
51 | | unissb 4904 |
. . . . . . 7
β’ (βͺ {π
β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))} β β
β βπ€ β
{π β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))}π€ β
β
) |
52 | 50, 51 | sylibr 233 |
. . . . . 6
β’ (Β¬
πΌ β V β βͺ {π
β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))} β
β
) |
53 | 33, 52 | sstrid 3959 |
. . . . 5
β’ (Β¬
πΌ β V β β© {π
β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))} β
β
) |
54 | | ss0 4362 |
. . . . 5
β’ (β© {π
β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))} β β
β β© {π β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))} =
β
) |
55 | 53, 54 | syl 17 |
. . . 4
β’ (Β¬
πΌ β V β β© {π
β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))} =
β
) |
56 | 29, 55 | eqtr4d 2776 |
. . 3
β’ (Β¬
πΌ β V β (
~FG βπΌ) = β© {π β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))}) |
57 | 28, 56 | pm2.61i 182 |
. 2
β’ (
~FG βπΌ) = β© {π β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))} |
58 | 1, 57 | eqtri 2761 |
1
β’ βΌ =
β© {π β£ (π Er π β§ βπ₯ β π βπ β (0...(β―βπ₯))βπ¦ β πΌ βπ§ β 2o π₯π(π₯ splice β¨π, π, β¨ββ¨π¦, π§β©β¨π¦, (1o β π§)β©ββ©β©))} |