Step | Hyp | Ref
| Expression |
1 | | simpl 482 |
. . . . . . 7
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → 𝑎 = 〈“𝐴𝐵𝐶”〉) |
2 | | eqidd 2729 |
. . . . . . . 8
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → 𝑥 = 𝑥) |
3 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → 𝑏 = 〈“𝐷𝐸𝐹”〉) |
4 | 3 | fveq1d 6894 |
. . . . . . . 8
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → (𝑏‘1) = (〈“𝐷𝐸𝐹”〉‘1)) |
5 | | eqidd 2729 |
. . . . . . . 8
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → 𝑦 = 𝑦) |
6 | 2, 4, 5 | s3eqd 14842 |
. . . . . . 7
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → 〈“𝑥(𝑏‘1)𝑦”〉 = 〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉) |
7 | 1, 6 | breq12d 5156 |
. . . . . 6
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ↔ 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉)) |
8 | 4 | fveq2d 6896 |
. . . . . . 7
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → (𝐾‘(𝑏‘1)) = (𝐾‘(〈“𝐷𝐸𝐹”〉‘1))) |
9 | 3 | fveq1d 6894 |
. . . . . . 7
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → (𝑏‘0) = (〈“𝐷𝐸𝐹”〉‘0)) |
10 | 2, 8, 9 | breq123d 5157 |
. . . . . 6
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → (𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ↔ 𝑥(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘0))) |
11 | 3 | fveq1d 6894 |
. . . . . . 7
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → (𝑏‘2) = (〈“𝐷𝐸𝐹”〉‘2)) |
12 | 5, 8, 11 | breq123d 5157 |
. . . . . 6
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → (𝑦(𝐾‘(𝑏‘1))(𝑏‘2) ↔ 𝑦(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘2))) |
13 | 7, 10, 12 | 3anbi123d 1433 |
. . . . 5
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → ((𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)) ↔ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉 ∧ 𝑥(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘0) ∧ 𝑦(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘2)))) |
14 | 13 | 2rexbidv 3215 |
. . . 4
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)) ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉 ∧ 𝑥(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘0) ∧ 𝑦(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘2)))) |
15 | | eqid 2728 |
. . . 4
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑃 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))} = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑃 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))} |
16 | 14, 15 | brab2a 5766 |
. . 3
⊢
(〈“𝐴𝐵𝐶”〉{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑃 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))}〈“𝐷𝐸𝐹”〉 ↔ ((〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑m (0..^3)) ∧
〈“𝐷𝐸𝐹”〉 ∈ (𝑃 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉 ∧ 𝑥(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘0) ∧ 𝑦(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘2)))) |
17 | | eqidd 2729 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → 𝑥 = 𝑥) |
18 | | iscgra.e |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ 𝑃) |
19 | | s3fv1 14870 |
. . . . . . . . . 10
⊢ (𝐸 ∈ 𝑃 → (〈“𝐷𝐸𝐹”〉‘1) = 𝐸) |
20 | 18, 19 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (〈“𝐷𝐸𝐹”〉‘1) = 𝐸) |
21 | 20 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (〈“𝐷𝐸𝐹”〉‘1) = 𝐸) |
22 | | eqidd 2729 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → 𝑦 = 𝑦) |
23 | 17, 21, 22 | s3eqd 14842 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → 〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉 = 〈“𝑥𝐸𝑦”〉) |
24 | 23 | breq2d 5155 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉 ↔ 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉)) |
25 | 21 | fveq2d 6896 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (𝐾‘(〈“𝐷𝐸𝐹”〉‘1)) = (𝐾‘𝐸)) |
26 | | iscgra.d |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
27 | | s3fv0 14869 |
. . . . . . . . 9
⊢ (𝐷 ∈ 𝑃 → (〈“𝐷𝐸𝐹”〉‘0) = 𝐷) |
28 | 26, 27 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (〈“𝐷𝐸𝐹”〉‘0) = 𝐷) |
29 | 28 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (〈“𝐷𝐸𝐹”〉‘0) = 𝐷) |
30 | 17, 25, 29 | breq123d 5157 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (𝑥(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘0) ↔ 𝑥(𝐾‘𝐸)𝐷)) |
31 | | iscgra.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ 𝑃) |
32 | | s3fv2 14871 |
. . . . . . . . 9
⊢ (𝐹 ∈ 𝑃 → (〈“𝐷𝐸𝐹”〉‘2) = 𝐹) |
33 | 31, 32 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (〈“𝐷𝐸𝐹”〉‘2) = 𝐹) |
34 | 33 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (〈“𝐷𝐸𝐹”〉‘2) = 𝐹) |
35 | 22, 25, 34 | breq123d 5157 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (𝑦(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘2) ↔ 𝑦(𝐾‘𝐸)𝐹)) |
36 | 24, 30, 35 | 3anbi123d 1433 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉 ∧ 𝑥(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘0) ∧ 𝑦(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘2)) ↔
(〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥(𝐾‘𝐸)𝐷 ∧ 𝑦(𝐾‘𝐸)𝐹))) |
37 | 36 | 2rexbidva 3213 |
. . . 4
⊢ (𝜑 → (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉 ∧ 𝑥(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘0) ∧ 𝑦(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘2)) ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥(𝐾‘𝐸)𝐷 ∧ 𝑦(𝐾‘𝐸)𝐹))) |
38 | 37 | anbi2d 629 |
. . 3
⊢ (𝜑 → (((〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑m (0..^3)) ∧
〈“𝐷𝐸𝐹”〉 ∈ (𝑃 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉 ∧ 𝑥(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘0) ∧ 𝑦(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘2))) ↔
((〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑m (0..^3)) ∧
〈“𝐷𝐸𝐹”〉 ∈ (𝑃 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥(𝐾‘𝐸)𝐷 ∧ 𝑦(𝐾‘𝐸)𝐹)))) |
39 | 16, 38 | bitrid 283 |
. 2
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑃 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))}〈“𝐷𝐸𝐹”〉 ↔ ((〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑m (0..^3)) ∧
〈“𝐷𝐸𝐹”〉 ∈ (𝑃 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥(𝐾‘𝐸)𝐷 ∧ 𝑦(𝐾‘𝐸)𝐹)))) |
40 | | iscgra.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
41 | | elex 3489 |
. . . 4
⊢ (𝐺 ∈ TarskiG → 𝐺 ∈ V) |
42 | | iscgra.p |
. . . . . . . 8
⊢ 𝑃 = (Base‘𝐺) |
43 | | iscgra.k |
. . . . . . . 8
⊢ 𝐾 = (hlG‘𝐺) |
44 | | simpl 482 |
. . . . . . . . . . . 12
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → 𝑝 = 𝑃) |
45 | 44 | oveq1d 7430 |
. . . . . . . . . . 11
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → (𝑝 ↑m (0..^3)) = (𝑃 ↑m
(0..^3))) |
46 | 45 | eleq2d 2815 |
. . . . . . . . . 10
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → (𝑎 ∈ (𝑝 ↑m (0..^3)) ↔ 𝑎 ∈ (𝑃 ↑m
(0..^3)))) |
47 | 45 | eleq2d 2815 |
. . . . . . . . . 10
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → (𝑏 ∈ (𝑝 ↑m (0..^3)) ↔ 𝑏 ∈ (𝑃 ↑m
(0..^3)))) |
48 | 46, 47 | anbi12d 631 |
. . . . . . . . 9
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → ((𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m (0..^3))) ↔ (𝑎 ∈ (𝑃 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑃 ↑m
(0..^3))))) |
49 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → 𝑘 = 𝐾) |
50 | 49 | fveq1d 6894 |
. . . . . . . . . . . . 13
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → (𝑘‘(𝑏‘1)) = (𝐾‘(𝑏‘1))) |
51 | 50 | breqd 5154 |
. . . . . . . . . . . 12
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → (𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ↔ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0))) |
52 | 50 | breqd 5154 |
. . . . . . . . . . . 12
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → (𝑦(𝑘‘(𝑏‘1))(𝑏‘2) ↔ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2))) |
53 | 51, 52 | 3anbi23d 1436 |
. . . . . . . . . . 11
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → ((𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)) ↔ (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))) |
54 | 44, 53 | rexeqbidv 3339 |
. . . . . . . . . 10
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → (∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)) ↔ ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))) |
55 | 44, 54 | rexeqbidv 3339 |
. . . . . . . . 9
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → (∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)) ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))) |
56 | 48, 55 | anbi12d 631 |
. . . . . . . 8
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → (((𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2))) ↔ ((𝑎 ∈ (𝑃 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑃 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2))))) |
57 | 42, 43, 56 | sbcie2s 17124 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → ([(Base‘𝑔) / 𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2))) ↔ ((𝑎 ∈ (𝑃 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑃 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2))))) |
58 | 57 | opabbidv 5209 |
. . . . . 6
⊢ (𝑔 = 𝐺 → {〈𝑎, 𝑏〉 ∣ [(Base‘𝑔) / 𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))} = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑃 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))}) |
59 | | fveq2 6892 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → (cgrG‘𝑔) = (cgrG‘𝐺)) |
60 | 59 | breqd 5154 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ↔ 𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉)) |
61 | 60 | 3anbi1d 1437 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → ((𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)) ↔ (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))) |
62 | 61 | 2rexbidv 3215 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)) ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))) |
63 | 62 | anbi2d 629 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (((𝑎 ∈ (𝑃 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑃 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2))) ↔ ((𝑎 ∈ (𝑃 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑃 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2))))) |
64 | 63 | opabbidv 5209 |
. . . . . 6
⊢ (𝑔 = 𝐺 → {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑃 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))} = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑃 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))}) |
65 | 58, 64 | eqtrd 2768 |
. . . . 5
⊢ (𝑔 = 𝐺 → {〈𝑎, 𝑏〉 ∣ [(Base‘𝑔) / 𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))} = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑃 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))}) |
66 | | df-cgra 28606 |
. . . . 5
⊢ cgrA =
(𝑔 ∈ V ↦
{〈𝑎, 𝑏〉 ∣
[(Base‘𝑔) /
𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))}) |
67 | | ovex 7448 |
. . . . . . 7
⊢ (𝑃 ↑m (0..^3))
∈ V |
68 | 67, 67 | xpex 7750 |
. . . . . 6
⊢ ((𝑃 ↑m (0..^3))
× (𝑃
↑m (0..^3))) ∈ V |
69 | | opabssxp 5765 |
. . . . . 6
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑃 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))} ⊆ ((𝑃 ↑m (0..^3)) × (𝑃 ↑m
(0..^3))) |
70 | 68, 69 | ssexi 5317 |
. . . . 5
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑃 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))} ∈ V |
71 | 65, 66, 70 | fvmpt 7000 |
. . . 4
⊢ (𝐺 ∈ V →
(cgrA‘𝐺) =
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑃 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))}) |
72 | 40, 41, 71 | 3syl 18 |
. . 3
⊢ (𝜑 → (cgrA‘𝐺) = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑃 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))}) |
73 | 72 | breqd 5154 |
. 2
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉 ↔ 〈“𝐴𝐵𝐶”〉{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑃 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))}〈“𝐷𝐸𝐹”〉)) |
74 | | iscgra.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
75 | | iscgra.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
76 | | iscgra.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
77 | 74, 75, 76 | s3cld 14850 |
. . . . 5
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃) |
78 | | s3len 14872 |
. . . . 5
⊢
(♯‘〈“𝐴𝐵𝐶”〉) = 3 |
79 | 42 | fvexi 6906 |
. . . . . 6
⊢ 𝑃 ∈ V |
80 | | 3nn0 12515 |
. . . . . 6
⊢ 3 ∈
ℕ0 |
81 | | wrdmap 14523 |
. . . . . 6
⊢ ((𝑃 ∈ V ∧ 3 ∈
ℕ0) → ((〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃 ∧ (♯‘〈“𝐴𝐵𝐶”〉) = 3) ↔
〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑m
(0..^3)))) |
82 | 79, 80, 81 | mp2an 691 |
. . . . 5
⊢
((〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃 ∧ (♯‘〈“𝐴𝐵𝐶”〉) = 3) ↔
〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑m
(0..^3))) |
83 | 77, 78, 82 | sylanblc 588 |
. . . 4
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑m
(0..^3))) |
84 | 26, 18, 31 | s3cld 14850 |
. . . . 5
⊢ (𝜑 → 〈“𝐷𝐸𝐹”〉 ∈ Word 𝑃) |
85 | | s3len 14872 |
. . . . 5
⊢
(♯‘〈“𝐷𝐸𝐹”〉) = 3 |
86 | | wrdmap 14523 |
. . . . . 6
⊢ ((𝑃 ∈ V ∧ 3 ∈
ℕ0) → ((〈“𝐷𝐸𝐹”〉 ∈ Word 𝑃 ∧ (♯‘〈“𝐷𝐸𝐹”〉) = 3) ↔
〈“𝐷𝐸𝐹”〉 ∈ (𝑃 ↑m
(0..^3)))) |
87 | 79, 80, 86 | mp2an 691 |
. . . . 5
⊢
((〈“𝐷𝐸𝐹”〉 ∈ Word 𝑃 ∧ (♯‘〈“𝐷𝐸𝐹”〉) = 3) ↔
〈“𝐷𝐸𝐹”〉 ∈ (𝑃 ↑m
(0..^3))) |
88 | 84, 85, 87 | sylanblc 588 |
. . . 4
⊢ (𝜑 → 〈“𝐷𝐸𝐹”〉 ∈ (𝑃 ↑m
(0..^3))) |
89 | 83, 88 | jca 511 |
. . 3
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑m (0..^3)) ∧
〈“𝐷𝐸𝐹”〉 ∈ (𝑃 ↑m
(0..^3)))) |
90 | 89 | biantrurd 532 |
. 2
⊢ (𝜑 → (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥(𝐾‘𝐸)𝐷 ∧ 𝑦(𝐾‘𝐸)𝐹) ↔ ((〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑m (0..^3)) ∧
〈“𝐷𝐸𝐹”〉 ∈ (𝑃 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥(𝐾‘𝐸)𝐷 ∧ 𝑦(𝐾‘𝐸)𝐹)))) |
91 | 39, 73, 90 | 3bitr4d 311 |
1
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉 ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥(𝐾‘𝐸)𝐷 ∧ 𝑦(𝐾‘𝐸)𝐹))) |