Step | Hyp | Ref
| Expression |
1 | | iseqlg.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
2 | | elex 3418 |
. . . 4
⊢ (𝐺 ∈ TarskiG → 𝐺 ∈ V) |
3 | | fveq2 6687 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺)) |
4 | | iseqlg.p |
. . . . . . . 8
⊢ 𝑃 = (Base‘𝐺) |
5 | 3, 4 | eqtr4di 2792 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝑃) |
6 | 5 | oveq1d 7198 |
. . . . . 6
⊢ (𝑔 = 𝐺 → ((Base‘𝑔) ↑m (0..^3)) = (𝑃 ↑m
(0..^3))) |
7 | | fveq2 6687 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (cgrG‘𝑔) = (cgrG‘𝐺)) |
8 | 7 | breqd 5051 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (𝑥(cgrG‘𝑔)〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉 ↔ 𝑥(cgrG‘𝐺)〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉)) |
9 | 6, 8 | rabeqbidv 3388 |
. . . . 5
⊢ (𝑔 = 𝐺 → {𝑥 ∈ ((Base‘𝑔) ↑m (0..^3)) ∣ 𝑥(cgrG‘𝑔)〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉} = {𝑥 ∈ (𝑃 ↑m (0..^3)) ∣ 𝑥(cgrG‘𝐺)〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉}) |
10 | | df-eqlg 26825 |
. . . . 5
⊢ eqltrG =
(𝑔 ∈ V ↦ {𝑥 ∈ ((Base‘𝑔) ↑m (0..^3))
∣ 𝑥(cgrG‘𝑔)〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉}) |
11 | | ovex 7216 |
. . . . . 6
⊢ (𝑃 ↑m (0..^3))
∈ V |
12 | 11 | rabex 5210 |
. . . . 5
⊢ {𝑥 ∈ (𝑃 ↑m (0..^3)) ∣ 𝑥(cgrG‘𝐺)〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉} ∈
V |
13 | 9, 10, 12 | fvmpt 6788 |
. . . 4
⊢ (𝐺 ∈ V →
(eqltrG‘𝐺) = {𝑥 ∈ (𝑃 ↑m (0..^3)) ∣ 𝑥(cgrG‘𝐺)〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉}) |
14 | 1, 2, 13 | 3syl 18 |
. . 3
⊢ (𝜑 → (eqltrG‘𝐺) = {𝑥 ∈ (𝑃 ↑m (0..^3)) ∣ 𝑥(cgrG‘𝐺)〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉}) |
15 | 14 | eleq2d 2819 |
. 2
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉 ∈ (eqltrG‘𝐺) ↔ 〈“𝐴𝐵𝐶”〉 ∈ {𝑥 ∈ (𝑃 ↑m (0..^3)) ∣ 𝑥(cgrG‘𝐺)〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉})) |
16 | | id 22 |
. . . . 5
⊢ (𝑥 = 〈“𝐴𝐵𝐶”〉 → 𝑥 = 〈“𝐴𝐵𝐶”〉) |
17 | | fveq1 6686 |
. . . . . 6
⊢ (𝑥 = 〈“𝐴𝐵𝐶”〉 → (𝑥‘1) = (〈“𝐴𝐵𝐶”〉‘1)) |
18 | | fveq1 6686 |
. . . . . 6
⊢ (𝑥 = 〈“𝐴𝐵𝐶”〉 → (𝑥‘2) = (〈“𝐴𝐵𝐶”〉‘2)) |
19 | | fveq1 6686 |
. . . . . 6
⊢ (𝑥 = 〈“𝐴𝐵𝐶”〉 → (𝑥‘0) = (〈“𝐴𝐵𝐶”〉‘0)) |
20 | 17, 18, 19 | s3eqd 14328 |
. . . . 5
⊢ (𝑥 = 〈“𝐴𝐵𝐶”〉 → 〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉 =
〈“(〈“𝐴𝐵𝐶”〉‘1)(〈“𝐴𝐵𝐶”〉‘2)(〈“𝐴𝐵𝐶”〉‘0)”〉) |
21 | 16, 20 | breq12d 5053 |
. . . 4
⊢ (𝑥 = 〈“𝐴𝐵𝐶”〉 → (𝑥(cgrG‘𝐺)〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉 ↔
〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“(〈“𝐴𝐵𝐶”〉‘1)(〈“𝐴𝐵𝐶”〉‘2)(〈“𝐴𝐵𝐶”〉‘0)”〉)) |
22 | 21 | elrab 3593 |
. . 3
⊢
(〈“𝐴𝐵𝐶”〉 ∈ {𝑥 ∈ (𝑃 ↑m (0..^3)) ∣ 𝑥(cgrG‘𝐺)〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉} ↔
(〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑m (0..^3)) ∧
〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“(〈“𝐴𝐵𝐶”〉‘1)(〈“𝐴𝐵𝐶”〉‘2)(〈“𝐴𝐵𝐶”〉‘0)”〉)) |
23 | 22 | a1i 11 |
. 2
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉 ∈ {𝑥 ∈ (𝑃 ↑m (0..^3)) ∣ 𝑥(cgrG‘𝐺)〈“(𝑥‘1)(𝑥‘2)(𝑥‘0)”〉} ↔
(〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑m (0..^3)) ∧
〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“(〈“𝐴𝐵𝐶”〉‘1)(〈“𝐴𝐵𝐶”〉‘2)(〈“𝐴𝐵𝐶”〉‘0)”〉))) |
24 | | iseqlg.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
25 | | iseqlg.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
26 | | iseqlg.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
27 | 24, 25, 26 | s3cld 14336 |
. . . . 5
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃) |
28 | | s3len 14358 |
. . . . 5
⊢
(♯‘〈“𝐴𝐵𝐶”〉) = 3 |
29 | 4 | fvexi 6701 |
. . . . . 6
⊢ 𝑃 ∈ V |
30 | | 3nn0 12007 |
. . . . . 6
⊢ 3 ∈
ℕ0 |
31 | | wrdmap 14000 |
. . . . . 6
⊢ ((𝑃 ∈ V ∧ 3 ∈
ℕ0) → ((〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃 ∧ (♯‘〈“𝐴𝐵𝐶”〉) = 3) ↔
〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑m
(0..^3)))) |
32 | 29, 30, 31 | mp2an 692 |
. . . . 5
⊢
((〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃 ∧ (♯‘〈“𝐴𝐵𝐶”〉) = 3) ↔
〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑m
(0..^3))) |
33 | 27, 28, 32 | sylanblc 592 |
. . . 4
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑m
(0..^3))) |
34 | 33 | biantrurd 536 |
. . 3
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“(〈“𝐴𝐵𝐶”〉‘1)(〈“𝐴𝐵𝐶”〉‘2)(〈“𝐴𝐵𝐶”〉‘0)”〉 ↔
(〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑m (0..^3)) ∧
〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“(〈“𝐴𝐵𝐶”〉‘1)(〈“𝐴𝐵𝐶”〉‘2)(〈“𝐴𝐵𝐶”〉‘0)”〉))) |
35 | | s3fv1 14356 |
. . . . . 6
⊢ (𝐵 ∈ 𝑃 → (〈“𝐴𝐵𝐶”〉‘1) = 𝐵) |
36 | 25, 35 | syl 17 |
. . . . 5
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉‘1) = 𝐵) |
37 | | s3fv2 14357 |
. . . . . 6
⊢ (𝐶 ∈ 𝑃 → (〈“𝐴𝐵𝐶”〉‘2) = 𝐶) |
38 | 26, 37 | syl 17 |
. . . . 5
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉‘2) = 𝐶) |
39 | | s3fv0 14355 |
. . . . . 6
⊢ (𝐴 ∈ 𝑃 → (〈“𝐴𝐵𝐶”〉‘0) = 𝐴) |
40 | 24, 39 | syl 17 |
. . . . 5
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉‘0) = 𝐴) |
41 | 36, 38, 40 | s3eqd 14328 |
. . . 4
⊢ (𝜑 →
〈“(〈“𝐴𝐵𝐶”〉‘1)(〈“𝐴𝐵𝐶”〉‘2)(〈“𝐴𝐵𝐶”〉‘0)”〉 =
〈“𝐵𝐶𝐴”〉) |
42 | 41 | breq2d 5052 |
. . 3
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“(〈“𝐴𝐵𝐶”〉‘1)(〈“𝐴𝐵𝐶”〉‘2)(〈“𝐴𝐵𝐶”〉‘0)”〉 ↔
〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐵𝐶𝐴”〉)) |
43 | 34, 42 | bitr3d 284 |
. 2
⊢ (𝜑 → ((〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑m (0..^3)) ∧
〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“(〈“𝐴𝐵𝐶”〉‘1)(〈“𝐴𝐵𝐶”〉‘2)(〈“𝐴𝐵𝐶”〉‘0)”〉) ↔
〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐵𝐶𝐴”〉)) |
44 | 15, 23, 43 | 3bitrd 308 |
1
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉 ∈ (eqltrG‘𝐺) ↔ 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐵𝐶𝐴”〉)) |