Step | Hyp | Ref
| Expression |
1 | | israg.a |
. . . 4
β’ (π β π΄ β π) |
2 | | israg.b |
. . . 4
β’ (π β π΅ β π) |
3 | | israg.c |
. . . 4
β’ (π β πΆ β π) |
4 | 1, 2, 3 | s3cld 14823 |
. . 3
β’ (π β β¨βπ΄π΅πΆββ© β Word π) |
5 | | fveqeq2 6901 |
. . . . 5
β’ (π€ = β¨βπ΄π΅πΆββ© β ((β―βπ€) = 3 β
(β―ββ¨βπ΄π΅πΆββ©) = 3)) |
6 | | fveq1 6891 |
. . . . . . 7
β’ (π€ = β¨βπ΄π΅πΆββ© β (π€β0) = (β¨βπ΄π΅πΆββ©β0)) |
7 | | fveq1 6891 |
. . . . . . 7
β’ (π€ = β¨βπ΄π΅πΆββ© β (π€β2) = (β¨βπ΄π΅πΆββ©β2)) |
8 | 6, 7 | oveq12d 7427 |
. . . . . 6
β’ (π€ = β¨βπ΄π΅πΆββ© β ((π€β0) β (π€β2)) = ((β¨βπ΄π΅πΆββ©β0) β (β¨βπ΄π΅πΆββ©β2))) |
9 | | fveq1 6891 |
. . . . . . . . 9
β’ (π€ = β¨βπ΄π΅πΆββ© β (π€β1) = (β¨βπ΄π΅πΆββ©β1)) |
10 | 9 | fveq2d 6896 |
. . . . . . . 8
β’ (π€ = β¨βπ΄π΅πΆββ© β (πβ(π€β1)) = (πβ(β¨βπ΄π΅πΆββ©β1))) |
11 | 10, 7 | fveq12d 6899 |
. . . . . . 7
β’ (π€ = β¨βπ΄π΅πΆββ© β ((πβ(π€β1))β(π€β2)) = ((πβ(β¨βπ΄π΅πΆββ©β1))β(β¨βπ΄π΅πΆββ©β2))) |
12 | 6, 11 | oveq12d 7427 |
. . . . . 6
β’ (π€ = β¨βπ΄π΅πΆββ© β ((π€β0) β ((πβ(π€β1))β(π€β2))) = ((β¨βπ΄π΅πΆββ©β0) β ((πβ(β¨βπ΄π΅πΆββ©β1))β(β¨βπ΄π΅πΆββ©β2)))) |
13 | 8, 12 | eqeq12d 2749 |
. . . . 5
β’ (π€ = β¨βπ΄π΅πΆββ© β (((π€β0) β (π€β2)) = ((π€β0) β ((πβ(π€β1))β(π€β2))) β ((β¨βπ΄π΅πΆββ©β0) β (β¨βπ΄π΅πΆββ©β2)) =
((β¨βπ΄π΅πΆββ©β0) β ((πβ(β¨βπ΄π΅πΆββ©β1))β(β¨βπ΄π΅πΆββ©β2))))) |
14 | 5, 13 | anbi12d 632 |
. . . 4
β’ (π€ = β¨βπ΄π΅πΆββ© β (((β―βπ€) = 3 β§ ((π€β0) β (π€β2)) = ((π€β0) β ((πβ(π€β1))β(π€β2)))) β
((β―ββ¨βπ΄π΅πΆββ©) = 3 β§
((β¨βπ΄π΅πΆββ©β0) β (β¨βπ΄π΅πΆββ©β2)) =
((β¨βπ΄π΅πΆββ©β0) β ((πβ(β¨βπ΄π΅πΆββ©β1))β(β¨βπ΄π΅πΆββ©β2)))))) |
15 | 14 | elrab3 3685 |
. . 3
β’
(β¨βπ΄π΅πΆββ© β Word π β (β¨βπ΄π΅πΆββ© β {π€ β Word π β£ ((β―βπ€) = 3 β§ ((π€β0) β (π€β2)) = ((π€β0) β ((πβ(π€β1))β(π€β2))))} β
((β―ββ¨βπ΄π΅πΆββ©) = 3 β§
((β¨βπ΄π΅πΆββ©β0) β (β¨βπ΄π΅πΆββ©β2)) =
((β¨βπ΄π΅πΆββ©β0) β ((πβ(β¨βπ΄π΅πΆββ©β1))β(β¨βπ΄π΅πΆββ©β2)))))) |
16 | 4, 15 | syl 17 |
. 2
β’ (π β (β¨βπ΄π΅πΆββ© β {π€ β Word π β£ ((β―βπ€) = 3 β§ ((π€β0) β (π€β2)) = ((π€β0) β ((πβ(π€β1))β(π€β2))))} β
((β―ββ¨βπ΄π΅πΆββ©) = 3 β§
((β¨βπ΄π΅πΆββ©β0) β (β¨βπ΄π΅πΆββ©β2)) =
((β¨βπ΄π΅πΆββ©β0) β ((πβ(β¨βπ΄π΅πΆββ©β1))β(β¨βπ΄π΅πΆββ©β2)))))) |
17 | | df-rag 27945 |
. . . 4
β’ βG
= (π β V β¦
{π€ β Word
(Baseβπ) β£
((β―βπ€) = 3
β§ ((π€β0)(distβπ)(π€β2)) = ((π€β0)(distβπ)(((pInvGβπ)β(π€β1))β(π€β2))))}) |
18 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π = πΊ) β π = πΊ) |
19 | 18 | fveq2d 6896 |
. . . . . . 7
β’ ((π β§ π = πΊ) β (Baseβπ) = (BaseβπΊ)) |
20 | | israg.p |
. . . . . . 7
β’ π = (BaseβπΊ) |
21 | 19, 20 | eqtr4di 2791 |
. . . . . 6
β’ ((π β§ π = πΊ) β (Baseβπ) = π) |
22 | | wrdeq 14486 |
. . . . . 6
β’
((Baseβπ) =
π β Word
(Baseβπ) = Word π) |
23 | 21, 22 | syl 17 |
. . . . 5
β’ ((π β§ π = πΊ) β Word (Baseβπ) = Word π) |
24 | 18 | fveq2d 6896 |
. . . . . . . . 9
β’ ((π β§ π = πΊ) β (distβπ) = (distβπΊ)) |
25 | | israg.d |
. . . . . . . . 9
β’ β =
(distβπΊ) |
26 | 24, 25 | eqtr4di 2791 |
. . . . . . . 8
β’ ((π β§ π = πΊ) β (distβπ) = β ) |
27 | 26 | oveqd 7426 |
. . . . . . 7
β’ ((π β§ π = πΊ) β ((π€β0)(distβπ)(π€β2)) = ((π€β0) β (π€β2))) |
28 | | eqidd 2734 |
. . . . . . . 8
β’ ((π β§ π = πΊ) β (π€β0) = (π€β0)) |
29 | 18 | fveq2d 6896 |
. . . . . . . . . . 11
β’ ((π β§ π = πΊ) β (pInvGβπ) = (pInvGβπΊ)) |
30 | | israg.s |
. . . . . . . . . . 11
β’ π = (pInvGβπΊ) |
31 | 29, 30 | eqtr4di 2791 |
. . . . . . . . . 10
β’ ((π β§ π = πΊ) β (pInvGβπ) = π) |
32 | 31 | fveq1d 6894 |
. . . . . . . . 9
β’ ((π β§ π = πΊ) β ((pInvGβπ)β(π€β1)) = (πβ(π€β1))) |
33 | 32 | fveq1d 6894 |
. . . . . . . 8
β’ ((π β§ π = πΊ) β (((pInvGβπ)β(π€β1))β(π€β2)) = ((πβ(π€β1))β(π€β2))) |
34 | 26, 28, 33 | oveq123d 7430 |
. . . . . . 7
β’ ((π β§ π = πΊ) β ((π€β0)(distβπ)(((pInvGβπ)β(π€β1))β(π€β2))) = ((π€β0) β ((πβ(π€β1))β(π€β2)))) |
35 | 27, 34 | eqeq12d 2749 |
. . . . . 6
β’ ((π β§ π = πΊ) β (((π€β0)(distβπ)(π€β2)) = ((π€β0)(distβπ)(((pInvGβπ)β(π€β1))β(π€β2))) β ((π€β0) β (π€β2)) = ((π€β0) β ((πβ(π€β1))β(π€β2))))) |
36 | 35 | anbi2d 630 |
. . . . 5
β’ ((π β§ π = πΊ) β (((β―βπ€) = 3 β§ ((π€β0)(distβπ)(π€β2)) = ((π€β0)(distβπ)(((pInvGβπ)β(π€β1))β(π€β2)))) β ((β―βπ€) = 3 β§ ((π€β0) β (π€β2)) = ((π€β0) β ((πβ(π€β1))β(π€β2)))))) |
37 | 23, 36 | rabeqbidv 3450 |
. . . 4
β’ ((π β§ π = πΊ) β {π€ β Word (Baseβπ) β£ ((β―βπ€) = 3 β§ ((π€β0)(distβπ)(π€β2)) = ((π€β0)(distβπ)(((pInvGβπ)β(π€β1))β(π€β2))))} = {π€ β Word π β£ ((β―βπ€) = 3 β§ ((π€β0) β (π€β2)) = ((π€β0) β ((πβ(π€β1))β(π€β2))))}) |
38 | | israg.g |
. . . . 5
β’ (π β πΊ β TarskiG) |
39 | 38 | elexd 3495 |
. . . 4
β’ (π β πΊ β V) |
40 | 20 | fvexi 6906 |
. . . . . . 7
β’ π β V |
41 | 40 | wrdexi 14476 |
. . . . . 6
β’ Word
π β V |
42 | 41 | rabex 5333 |
. . . . 5
β’ {π€ β Word π β£ ((β―βπ€) = 3 β§ ((π€β0) β (π€β2)) = ((π€β0) β ((πβ(π€β1))β(π€β2))))} β V |
43 | 42 | a1i 11 |
. . . 4
β’ (π β {π€ β Word π β£ ((β―βπ€) = 3 β§ ((π€β0) β (π€β2)) = ((π€β0) β ((πβ(π€β1))β(π€β2))))} β V) |
44 | 17, 37, 39, 43 | fvmptd2 7007 |
. . 3
β’ (π β (βGβπΊ) = {π€ β Word π β£ ((β―βπ€) = 3 β§ ((π€β0) β (π€β2)) = ((π€β0) β ((πβ(π€β1))β(π€β2))))}) |
45 | 44 | eleq2d 2820 |
. 2
β’ (π β (β¨βπ΄π΅πΆββ© β (βGβπΊ) β β¨βπ΄π΅πΆββ© β {π€ β Word π β£ ((β―βπ€) = 3 β§ ((π€β0) β (π€β2)) = ((π€β0) β ((πβ(π€β1))β(π€β2))))})) |
46 | | s3fv0 14842 |
. . . . . . 7
β’ (π΄ β π β (β¨βπ΄π΅πΆββ©β0) = π΄) |
47 | 1, 46 | syl 17 |
. . . . . 6
β’ (π β (β¨βπ΄π΅πΆββ©β0) = π΄) |
48 | 47 | eqcomd 2739 |
. . . . 5
β’ (π β π΄ = (β¨βπ΄π΅πΆββ©β0)) |
49 | | s3fv2 14844 |
. . . . . . 7
β’ (πΆ β π β (β¨βπ΄π΅πΆββ©β2) = πΆ) |
50 | 3, 49 | syl 17 |
. . . . . 6
β’ (π β (β¨βπ΄π΅πΆββ©β2) = πΆ) |
51 | 50 | eqcomd 2739 |
. . . . 5
β’ (π β πΆ = (β¨βπ΄π΅πΆββ©β2)) |
52 | 48, 51 | oveq12d 7427 |
. . . 4
β’ (π β (π΄ β πΆ) = ((β¨βπ΄π΅πΆββ©β0) β (β¨βπ΄π΅πΆββ©β2))) |
53 | | s3fv1 14843 |
. . . . . . . . 9
β’ (π΅ β π β (β¨βπ΄π΅πΆββ©β1) = π΅) |
54 | 2, 53 | syl 17 |
. . . . . . . 8
β’ (π β (β¨βπ΄π΅πΆββ©β1) = π΅) |
55 | 54 | eqcomd 2739 |
. . . . . . 7
β’ (π β π΅ = (β¨βπ΄π΅πΆββ©β1)) |
56 | 55 | fveq2d 6896 |
. . . . . 6
β’ (π β (πβπ΅) = (πβ(β¨βπ΄π΅πΆββ©β1))) |
57 | 56, 51 | fveq12d 6899 |
. . . . 5
β’ (π β ((πβπ΅)βπΆ) = ((πβ(β¨βπ΄π΅πΆββ©β1))β(β¨βπ΄π΅πΆββ©β2))) |
58 | 48, 57 | oveq12d 7427 |
. . . 4
β’ (π β (π΄ β ((πβπ΅)βπΆ)) = ((β¨βπ΄π΅πΆββ©β0) β ((πβ(β¨βπ΄π΅πΆββ©β1))β(β¨βπ΄π΅πΆββ©β2)))) |
59 | 52, 58 | eqeq12d 2749 |
. . 3
β’ (π β ((π΄ β πΆ) = (π΄ β ((πβπ΅)βπΆ)) β ((β¨βπ΄π΅πΆββ©β0) β (β¨βπ΄π΅πΆββ©β2)) =
((β¨βπ΄π΅πΆββ©β0) β ((πβ(β¨βπ΄π΅πΆββ©β1))β(β¨βπ΄π΅πΆββ©β2))))) |
60 | | s3len 14845 |
. . . . 5
β’
(β―ββ¨βπ΄π΅πΆββ©) = 3 |
61 | 60 | a1i 11 |
. . . 4
β’ (π β
(β―ββ¨βπ΄π΅πΆββ©) = 3) |
62 | 61 | biantrurd 534 |
. . 3
β’ (π β (((β¨βπ΄π΅πΆββ©β0) β (β¨βπ΄π΅πΆββ©β2)) =
((β¨βπ΄π΅πΆββ©β0) β ((πβ(β¨βπ΄π΅πΆββ©β1))β(β¨βπ΄π΅πΆββ©β2))) β
((β―ββ¨βπ΄π΅πΆββ©) = 3 β§ ((β¨βπ΄π΅πΆββ©β0) β (β¨βπ΄π΅πΆββ©β2)) = ((β¨βπ΄π΅πΆββ©β0) β ((πβ(β¨βπ΄π΅πΆββ©β1))β(β¨βπ΄π΅πΆββ©β2)))))) |
63 | 59, 62 | bitrd 279 |
. 2
β’ (π β ((π΄ β πΆ) = (π΄ β ((πβπ΅)βπΆ)) β ((β―ββ¨βπ΄π΅πΆββ©) = 3 β§
((β¨βπ΄π΅πΆββ©β0) β (β¨βπ΄π΅πΆββ©β2)) =
((β¨βπ΄π΅πΆββ©β0) β ((πβ(β¨βπ΄π΅πΆββ©β1))β(β¨βπ΄π΅πΆββ©β2)))))) |
64 | 16, 45, 63 | 3bitr4d 311 |
1
β’ (π β (β¨βπ΄π΅πΆββ© β (βGβπΊ) β (π΄ β πΆ) = (π΄ β ((πβπ΅)βπΆ)))) |