Step | Hyp | Ref
| Expression |
1 | | iseqlg.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
2 | | elex 3212 |
. . . 4
⊢ (𝐺 ∈ TarskiG → 𝐺 ∈ V) |
3 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺)) |
4 | | iseqlg.p |
. . . . . . . 8
⊢ 𝑃 = (Base‘𝐺) |
5 | 3, 4 | syl6eqr 2674 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝑃) |
6 | 5 | oveq1d 6665 |
. . . . . 6
⊢ (𝑔 = 𝐺 → ((Base‘𝑔) ↑𝑚 (0..^3)) =
(𝑃
↑𝑚 (0..^3))) |
7 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (cgrG‘𝑔) = (cgrG‘𝐺)) |
8 | 7 | breqd 4664 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (𝑥(cgrG‘𝑔)〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉 ↔ 𝑥(cgrG‘𝐺)〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉)) |
9 | 6, 8 | rabeqbidv 3195 |
. . . . 5
⊢ (𝑔 = 𝐺 → {𝑥 ∈ ((Base‘𝑔) ↑𝑚 (0..^3)) ∣
𝑥(cgrG‘𝑔)〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉} = {𝑥 ∈ (𝑃 ↑𝑚 (0..^3)) ∣
𝑥(cgrG‘𝐺)〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉}) |
10 | | df-eqlg 25746 |
. . . . 5
⊢ eqltrG =
(𝑔 ∈ V ↦ {𝑥 ∈ ((Base‘𝑔) ↑𝑚
(0..^3)) ∣ 𝑥(cgrG‘𝑔)〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉}) |
11 | | ovex 6678 |
. . . . . 6
⊢ (𝑃 ↑𝑚
(0..^3)) ∈ V |
12 | 11 | rabex 4813 |
. . . . 5
⊢ {𝑥 ∈ (𝑃 ↑𝑚 (0..^3)) ∣
𝑥(cgrG‘𝐺)〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉} ∈
V |
13 | 9, 10, 12 | fvmpt 6282 |
. . . 4
⊢ (𝐺 ∈ V →
(eqltrG‘𝐺) = {𝑥 ∈ (𝑃 ↑𝑚 (0..^3)) ∣
𝑥(cgrG‘𝐺)〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉}) |
14 | 1, 2, 13 | 3syl 18 |
. . 3
⊢ (𝜑 → (eqltrG‘𝐺) = {𝑥 ∈ (𝑃 ↑𝑚 (0..^3)) ∣
𝑥(cgrG‘𝐺)〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉}) |
15 | 14 | eleq2d 2687 |
. 2
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉 ∈ (eqltrG‘𝐺) ↔ 〈“𝐴𝐵𝐶”〉 ∈ {𝑥 ∈ (𝑃 ↑𝑚 (0..^3)) ∣
𝑥(cgrG‘𝐺)〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉})) |
16 | | id 22 |
. . . . 5
⊢ (𝑥 = 〈“𝐴𝐵𝐶”〉 → 𝑥 = 〈“𝐴𝐵𝐶”〉) |
17 | | fveq1 6190 |
. . . . . 6
⊢ (𝑥 = 〈“𝐴𝐵𝐶”〉 → (𝑥‘1) = (〈“𝐴𝐵𝐶”〉‘1)) |
18 | | fveq1 6190 |
. . . . . 6
⊢ (𝑥 = 〈“𝐴𝐵𝐶”〉 → (𝑥‘2) = (〈“𝐴𝐵𝐶”〉‘2)) |
19 | | fveq1 6190 |
. . . . . 6
⊢ (𝑥 = 〈“𝐴𝐵𝐶”〉 → (𝑥‘0) = (〈“𝐴𝐵𝐶”〉‘0)) |
20 | 17, 18, 19 | s3eqd 13609 |
. . . . 5
⊢ (𝑥 = 〈“𝐴𝐵𝐶”〉 → 〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉 =
〈“(〈“𝐴𝐵𝐶”〉‘1)(〈“𝐴𝐵𝐶”〉‘2)(〈“𝐴𝐵𝐶”〉‘0)”〉) |
21 | 16, 20 | breq12d 4666 |
. . . 4
⊢ (𝑥 = 〈“𝐴𝐵𝐶”〉 → (𝑥(cgrG‘𝐺)〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉 ↔
〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“(〈“𝐴𝐵𝐶”〉‘1)(〈“𝐴𝐵𝐶”〉‘2)(〈“𝐴𝐵𝐶”〉‘0)”〉)) |
22 | 21 | elrab 3363 |
. . 3
⊢
(〈“𝐴𝐵𝐶”〉 ∈ {𝑥 ∈ (𝑃 ↑𝑚 (0..^3)) ∣
𝑥(cgrG‘𝐺)〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉} ↔
(〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“(〈“𝐴𝐵𝐶”〉‘1)(〈“𝐴𝐵𝐶”〉‘2)(〈“𝐴𝐵𝐶”〉‘0)”〉)) |
23 | 22 | a1i 11 |
. 2
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉 ∈ {𝑥 ∈ (𝑃 ↑𝑚 (0..^3)) ∣
𝑥(cgrG‘𝐺)〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉} ↔
(〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“(〈“𝐴𝐵𝐶”〉‘1)(〈“𝐴𝐵𝐶”〉‘2)(〈“𝐴𝐵𝐶”〉‘0)”〉))) |
24 | | iseqlg.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
25 | | iseqlg.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
26 | | iseqlg.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
27 | 24, 25, 26 | s3cld 13617 |
. . . . . 6
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃) |
28 | | s3len 13639 |
. . . . . . 7
⊢
(#‘〈“𝐴𝐵𝐶”〉) = 3 |
29 | 28 | a1i 11 |
. . . . . 6
⊢ (𝜑 →
(#‘〈“𝐴𝐵𝐶”〉) = 3) |
30 | 27, 29 | jca 554 |
. . . . 5
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃 ∧ (#‘〈“𝐴𝐵𝐶”〉) = 3)) |
31 | | fvex 6201 |
. . . . . . 7
⊢
(Base‘𝐺)
∈ V |
32 | 4, 31 | eqeltri 2697 |
. . . . . 6
⊢ 𝑃 ∈ V |
33 | | 3nn0 11310 |
. . . . . 6
⊢ 3 ∈
ℕ0 |
34 | | wrdmap 13336 |
. . . . . 6
⊢ ((𝑃 ∈ V ∧ 3 ∈
ℕ0) → ((〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃 ∧ (#‘〈“𝐴𝐵𝐶”〉) = 3) ↔
〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑𝑚
(0..^3)))) |
35 | 32, 33, 34 | mp2an 708 |
. . . . 5
⊢
((〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃 ∧ (#‘〈“𝐴𝐵𝐶”〉) = 3) ↔
〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑𝑚
(0..^3))) |
36 | 30, 35 | sylib 208 |
. . . 4
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑𝑚
(0..^3))) |
37 | 36 | biantrurd 529 |
. . 3
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“(〈“𝐴𝐵𝐶”〉‘1)(〈“𝐴𝐵𝐶”〉‘2)(〈“𝐴𝐵𝐶”〉‘0)”〉 ↔
(〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“(〈“𝐴𝐵𝐶”〉‘1)(〈“𝐴𝐵𝐶”〉‘2)(〈“𝐴𝐵𝐶”〉‘0)”〉))) |
38 | | s3fv1 13637 |
. . . . . 6
⊢ (𝐵 ∈ 𝑃 → (〈“𝐴𝐵𝐶”〉‘1) = 𝐵) |
39 | 25, 38 | syl 17 |
. . . . 5
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉‘1) = 𝐵) |
40 | | s3fv2 13638 |
. . . . . 6
⊢ (𝐶 ∈ 𝑃 → (〈“𝐴𝐵𝐶”〉‘2) = 𝐶) |
41 | 26, 40 | syl 17 |
. . . . 5
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉‘2) = 𝐶) |
42 | | s3fv0 13636 |
. . . . . 6
⊢ (𝐴 ∈ 𝑃 → (〈“𝐴𝐵𝐶”〉‘0) = 𝐴) |
43 | 24, 42 | syl 17 |
. . . . 5
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉‘0) = 𝐴) |
44 | 39, 41, 43 | s3eqd 13609 |
. . . 4
⊢ (𝜑 →
〈“(〈“𝐴𝐵𝐶”〉‘1)(〈“𝐴𝐵𝐶”〉‘2)(〈“𝐴𝐵𝐶”〉‘0)”〉 =
〈“𝐵𝐶𝐴”〉) |
45 | 44 | breq2d 4665 |
. . 3
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“(〈“𝐴𝐵𝐶”〉‘1)(〈“𝐴𝐵𝐶”〉‘2)(〈“𝐴𝐵𝐶”〉‘0)”〉 ↔
〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐵𝐶𝐴”〉)) |
46 | 37, 45 | bitr3d 270 |
. 2
⊢ (𝜑 → ((〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“(〈“𝐴𝐵𝐶”〉‘1)(〈“𝐴𝐵𝐶”〉‘2)(〈“𝐴𝐵𝐶”〉‘0)”〉) ↔
〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐵𝐶𝐴”〉)) |
47 | 15, 23, 46 | 3bitrd 294 |
1
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉 ∈ (eqltrG‘𝐺) ↔ 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐵𝐶𝐴”〉)) |