Step | Hyp | Ref
| Expression |
1 | | simpl 476 |
. . . . . . . 8
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → 𝑎 = 〈“𝐴𝐵𝐶”〉) |
2 | | eqidd 2826 |
. . . . . . . . 9
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → 𝑥 = 𝑥) |
3 | | simpr 479 |
. . . . . . . . . 10
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → 𝑏 = 〈“𝐷𝐸𝐹”〉) |
4 | 3 | fveq1d 6435 |
. . . . . . . . 9
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → (𝑏‘1) = (〈“𝐷𝐸𝐹”〉‘1)) |
5 | | eqidd 2826 |
. . . . . . . . 9
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → 𝑦 = 𝑦) |
6 | 2, 4, 5 | s3eqd 13985 |
. . . . . . . 8
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → 〈“𝑥(𝑏‘1)𝑦”〉 = 〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉) |
7 | 1, 6 | breq12d 4886 |
. . . . . . 7
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ↔ 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉)) |
8 | 4 | fveq2d 6437 |
. . . . . . . 8
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → (𝐾‘(𝑏‘1)) = (𝐾‘(〈“𝐷𝐸𝐹”〉‘1))) |
9 | 3 | fveq1d 6435 |
. . . . . . . 8
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → (𝑏‘0) = (〈“𝐷𝐸𝐹”〉‘0)) |
10 | 2, 8, 9 | breq123d 4887 |
. . . . . . 7
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → (𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ↔ 𝑥(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘0))) |
11 | 3 | fveq1d 6435 |
. . . . . . . 8
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → (𝑏‘2) = (〈“𝐷𝐸𝐹”〉‘2)) |
12 | 5, 8, 11 | breq123d 4887 |
. . . . . . 7
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → (𝑦(𝐾‘(𝑏‘1))(𝑏‘2) ↔ 𝑦(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘2))) |
13 | 7, 10, 12 | 3anbi123d 1566 |
. . . . . 6
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → ((𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)) ↔ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉 ∧ 𝑥(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘0) ∧ 𝑦(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘2)))) |
14 | 13 | 2rexbidv 3267 |
. . . . 5
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)) ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉 ∧ 𝑥(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘0) ∧ 𝑦(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘2)))) |
15 | | eqid 2825 |
. . . . 5
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
𝑏 ∈ (𝑃 ↑𝑚 (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))} = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
𝑏 ∈ (𝑃 ↑𝑚 (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))} |
16 | 14, 15 | brab2a 5429 |
. . . 4
⊢
(〈“𝐴𝐵𝐶”〉{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
𝑏 ∈ (𝑃 ↑𝑚 (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))}〈“𝐷𝐸𝐹”〉 ↔ ((〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
〈“𝐷𝐸𝐹”〉 ∈ (𝑃 ↑𝑚 (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉 ∧ 𝑥(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘0) ∧ 𝑦(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘2)))) |
17 | 16 | a1i 11 |
. . 3
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
𝑏 ∈ (𝑃 ↑𝑚 (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))}〈“𝐷𝐸𝐹”〉 ↔ ((〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
〈“𝐷𝐸𝐹”〉 ∈ (𝑃 ↑𝑚 (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉 ∧ 𝑥(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘0) ∧ 𝑦(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘2))))) |
18 | | eqidd 2826 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → 𝑥 = 𝑥) |
19 | | iscgra.e |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ 𝑃) |
20 | | s3fv1 14013 |
. . . . . . . . . 10
⊢ (𝐸 ∈ 𝑃 → (〈“𝐷𝐸𝐹”〉‘1) = 𝐸) |
21 | 19, 20 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (〈“𝐷𝐸𝐹”〉‘1) = 𝐸) |
22 | 21 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (〈“𝐷𝐸𝐹”〉‘1) = 𝐸) |
23 | | eqidd 2826 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → 𝑦 = 𝑦) |
24 | 18, 22, 23 | s3eqd 13985 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → 〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉 = 〈“𝑥𝐸𝑦”〉) |
25 | 24 | breq2d 4885 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉 ↔ 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉)) |
26 | 22 | fveq2d 6437 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (𝐾‘(〈“𝐷𝐸𝐹”〉‘1)) = (𝐾‘𝐸)) |
27 | | iscgra.d |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
28 | | s3fv0 14012 |
. . . . . . . . 9
⊢ (𝐷 ∈ 𝑃 → (〈“𝐷𝐸𝐹”〉‘0) = 𝐷) |
29 | 27, 28 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (〈“𝐷𝐸𝐹”〉‘0) = 𝐷) |
30 | 29 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (〈“𝐷𝐸𝐹”〉‘0) = 𝐷) |
31 | 18, 26, 30 | breq123d 4887 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (𝑥(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘0) ↔ 𝑥(𝐾‘𝐸)𝐷)) |
32 | | iscgra.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ 𝑃) |
33 | | s3fv2 14014 |
. . . . . . . . 9
⊢ (𝐹 ∈ 𝑃 → (〈“𝐷𝐸𝐹”〉‘2) = 𝐹) |
34 | 32, 33 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (〈“𝐷𝐸𝐹”〉‘2) = 𝐹) |
35 | 34 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (〈“𝐷𝐸𝐹”〉‘2) = 𝐹) |
36 | 23, 26, 35 | breq123d 4887 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (𝑦(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘2) ↔ 𝑦(𝐾‘𝐸)𝐹)) |
37 | 25, 31, 36 | 3anbi123d 1566 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉 ∧ 𝑥(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘0) ∧ 𝑦(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘2)) ↔
(〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥(𝐾‘𝐸)𝐷 ∧ 𝑦(𝐾‘𝐸)𝐹))) |
38 | 37 | 2rexbidva 3266 |
. . . 4
⊢ (𝜑 → (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉 ∧ 𝑥(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘0) ∧ 𝑦(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘2)) ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥(𝐾‘𝐸)𝐷 ∧ 𝑦(𝐾‘𝐸)𝐹))) |
39 | 38 | anbi2d 624 |
. . 3
⊢ (𝜑 → (((〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
〈“𝐷𝐸𝐹”〉 ∈ (𝑃 ↑𝑚 (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉 ∧ 𝑥(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘0) ∧ 𝑦(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘2))) ↔
((〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
〈“𝐷𝐸𝐹”〉 ∈ (𝑃 ↑𝑚 (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥(𝐾‘𝐸)𝐷 ∧ 𝑦(𝐾‘𝐸)𝐹)))) |
40 | 17, 39 | bitrd 271 |
. 2
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
𝑏 ∈ (𝑃 ↑𝑚 (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))}〈“𝐷𝐸𝐹”〉 ↔ ((〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
〈“𝐷𝐸𝐹”〉 ∈ (𝑃 ↑𝑚 (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥(𝐾‘𝐸)𝐷 ∧ 𝑦(𝐾‘𝐸)𝐹)))) |
41 | | iscgra.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
42 | | elex 3429 |
. . . 4
⊢ (𝐺 ∈ TarskiG → 𝐺 ∈ V) |
43 | | iscgra.p |
. . . . . . . 8
⊢ 𝑃 = (Base‘𝐺) |
44 | | iscgra.k |
. . . . . . . 8
⊢ 𝐾 = (hlG‘𝐺) |
45 | | simpl 476 |
. . . . . . . . . . . . 13
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → 𝑝 = 𝑃) |
46 | 45 | eqcomd 2831 |
. . . . . . . . . . . 12
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → 𝑃 = 𝑝) |
47 | 46 | oveq1d 6920 |
. . . . . . . . . . 11
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → (𝑃 ↑𝑚 (0..^3)) =
(𝑝
↑𝑚 (0..^3))) |
48 | 47 | eleq2d 2892 |
. . . . . . . . . 10
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → (𝑎 ∈ (𝑃 ↑𝑚 (0..^3)) ↔
𝑎 ∈ (𝑝 ↑𝑚
(0..^3)))) |
49 | 47 | eleq2d 2892 |
. . . . . . . . . 10
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → (𝑏 ∈ (𝑃 ↑𝑚 (0..^3)) ↔
𝑏 ∈ (𝑝 ↑𝑚
(0..^3)))) |
50 | 48, 49 | anbi12d 626 |
. . . . . . . . 9
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → ((𝑎 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
𝑏 ∈ (𝑃 ↑𝑚 (0..^3))) ↔
(𝑎 ∈ (𝑝 ↑𝑚
(0..^3)) ∧ 𝑏 ∈
(𝑝
↑𝑚 (0..^3))))) |
51 | | simpr 479 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → 𝑘 = 𝐾) |
52 | | eqidd 2826 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → (𝑏‘1) = (𝑏‘1)) |
53 | 51, 52 | fveq12d 6440 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → (𝑘‘(𝑏‘1)) = (𝐾‘(𝑏‘1))) |
54 | 53 | breqd 4884 |
. . . . . . . . . . . . 13
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → (𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ↔ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0))) |
55 | 53 | breqd 4884 |
. . . . . . . . . . . . 13
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → (𝑦(𝑘‘(𝑏‘1))(𝑏‘2) ↔ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2))) |
56 | 54, 55 | 3anbi23d 1569 |
. . . . . . . . . . . 12
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → ((𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)) ↔ (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))) |
57 | 56 | bicomd 215 |
. . . . . . . . . . 11
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → ((𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)) ↔ (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))) |
58 | 46, 57 | rexeqbidv 3365 |
. . . . . . . . . 10
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → (∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)) ↔ ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))) |
59 | 46, 58 | rexeqbidv 3365 |
. . . . . . . . 9
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)) ↔ ∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))) |
60 | 50, 59 | anbi12d 626 |
. . . . . . . 8
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → (((𝑎 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
𝑏 ∈ (𝑃 ↑𝑚 (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2))) ↔ ((𝑎 ∈ (𝑝 ↑𝑚 (0..^3)) ∧
𝑏 ∈ (𝑝 ↑𝑚
(0..^3))) ∧ ∃𝑥
∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2))))) |
61 | 43, 44, 60 | sbcie2s 16279 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → ([(Base‘𝑔) / 𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝 ↑𝑚 (0..^3)) ∧
𝑏 ∈ (𝑝 ↑𝑚
(0..^3))) ∧ ∃𝑥
∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2))) ↔ ((𝑎 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
𝑏 ∈ (𝑃 ↑𝑚 (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2))))) |
62 | 61 | opabbidv 4939 |
. . . . . 6
⊢ (𝑔 = 𝐺 → {〈𝑎, 𝑏〉 ∣ [(Base‘𝑔) / 𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝 ↑𝑚 (0..^3)) ∧
𝑏 ∈ (𝑝 ↑𝑚
(0..^3))) ∧ ∃𝑥
∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))} = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
𝑏 ∈ (𝑃 ↑𝑚 (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))}) |
63 | | fveq2 6433 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝐺 → (cgrG‘𝑔) = (cgrG‘𝐺)) |
64 | 63 | breqd 4884 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ↔ 𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉)) |
65 | 64 | 3anbi1d 1570 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → ((𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)) ↔ (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))) |
66 | 65 | rexbidv 3262 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)) ↔ ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))) |
67 | 66 | rexbidv 3262 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)) ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))) |
68 | 67 | anbi2d 624 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (((𝑎 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
𝑏 ∈ (𝑃 ↑𝑚 (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2))) ↔ ((𝑎 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
𝑏 ∈ (𝑃 ↑𝑚 (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2))))) |
69 | 68 | opabbidv 4939 |
. . . . . 6
⊢ (𝑔 = 𝐺 → {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
𝑏 ∈ (𝑃 ↑𝑚 (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))} = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
𝑏 ∈ (𝑃 ↑𝑚 (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))}) |
70 | 62, 69 | eqtrd 2861 |
. . . . 5
⊢ (𝑔 = 𝐺 → {〈𝑎, 𝑏〉 ∣ [(Base‘𝑔) / 𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝 ↑𝑚 (0..^3)) ∧
𝑏 ∈ (𝑝 ↑𝑚
(0..^3))) ∧ ∃𝑥
∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))} = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
𝑏 ∈ (𝑃 ↑𝑚 (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))}) |
71 | | df-cgra 26117 |
. . . . 5
⊢ cgrA =
(𝑔 ∈ V ↦
{〈𝑎, 𝑏〉 ∣
[(Base‘𝑔) /
𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝 ↑𝑚 (0..^3)) ∧
𝑏 ∈ (𝑝 ↑𝑚
(0..^3))) ∧ ∃𝑥
∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))}) |
72 | | ovex 6937 |
. . . . . . 7
⊢ (𝑃 ↑𝑚
(0..^3)) ∈ V |
73 | 72, 72 | xpex 7223 |
. . . . . 6
⊢ ((𝑃 ↑𝑚
(0..^3)) × (𝑃
↑𝑚 (0..^3))) ∈ V |
74 | | opabssxp 5428 |
. . . . . 6
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
𝑏 ∈ (𝑃 ↑𝑚 (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))} ⊆ ((𝑃 ↑𝑚 (0..^3)) ×
(𝑃
↑𝑚 (0..^3))) |
75 | 73, 74 | ssexi 5028 |
. . . . 5
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
𝑏 ∈ (𝑃 ↑𝑚 (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))} ∈ V |
76 | 70, 71, 75 | fvmpt 6529 |
. . . 4
⊢ (𝐺 ∈ V →
(cgrA‘𝐺) =
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
𝑏 ∈ (𝑃 ↑𝑚 (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))}) |
77 | 41, 42, 76 | 3syl 18 |
. . 3
⊢ (𝜑 → (cgrA‘𝐺) = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
𝑏 ∈ (𝑃 ↑𝑚 (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))}) |
78 | 77 | breqd 4884 |
. 2
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉 ↔ 〈“𝐴𝐵𝐶”〉{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
𝑏 ∈ (𝑃 ↑𝑚 (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))}〈“𝐷𝐸𝐹”〉)) |
79 | | iscgra.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
80 | | iscgra.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
81 | | iscgra.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
82 | 79, 80, 81 | s3cld 13993 |
. . . . . 6
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃) |
83 | | s3len 14015 |
. . . . . . 7
⊢
(♯‘〈“𝐴𝐵𝐶”〉) = 3 |
84 | 83 | a1i 11 |
. . . . . 6
⊢ (𝜑 →
(♯‘〈“𝐴𝐵𝐶”〉) = 3) |
85 | 82, 84 | jca 509 |
. . . . 5
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃 ∧ (♯‘〈“𝐴𝐵𝐶”〉) = 3)) |
86 | 43 | fvexi 6447 |
. . . . . 6
⊢ 𝑃 ∈ V |
87 | | 3nn0 11638 |
. . . . . 6
⊢ 3 ∈
ℕ0 |
88 | | wrdmap 13606 |
. . . . . 6
⊢ ((𝑃 ∈ V ∧ 3 ∈
ℕ0) → ((〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃 ∧ (♯‘〈“𝐴𝐵𝐶”〉) = 3) ↔
〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑𝑚
(0..^3)))) |
89 | 86, 87, 88 | mp2an 685 |
. . . . 5
⊢
((〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃 ∧ (♯‘〈“𝐴𝐵𝐶”〉) = 3) ↔
〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑𝑚
(0..^3))) |
90 | 85, 89 | sylib 210 |
. . . 4
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑𝑚
(0..^3))) |
91 | 27, 19, 32 | s3cld 13993 |
. . . . . 6
⊢ (𝜑 → 〈“𝐷𝐸𝐹”〉 ∈ Word 𝑃) |
92 | | s3len 14015 |
. . . . . . 7
⊢
(♯‘〈“𝐷𝐸𝐹”〉) = 3 |
93 | 92 | a1i 11 |
. . . . . 6
⊢ (𝜑 →
(♯‘〈“𝐷𝐸𝐹”〉) = 3) |
94 | 91, 93 | jca 509 |
. . . . 5
⊢ (𝜑 → (〈“𝐷𝐸𝐹”〉 ∈ Word 𝑃 ∧ (♯‘〈“𝐷𝐸𝐹”〉) = 3)) |
95 | | wrdmap 13606 |
. . . . . 6
⊢ ((𝑃 ∈ V ∧ 3 ∈
ℕ0) → ((〈“𝐷𝐸𝐹”〉 ∈ Word 𝑃 ∧ (♯‘〈“𝐷𝐸𝐹”〉) = 3) ↔
〈“𝐷𝐸𝐹”〉 ∈ (𝑃 ↑𝑚
(0..^3)))) |
96 | 86, 87, 95 | mp2an 685 |
. . . . 5
⊢
((〈“𝐷𝐸𝐹”〉 ∈ Word 𝑃 ∧ (♯‘〈“𝐷𝐸𝐹”〉) = 3) ↔
〈“𝐷𝐸𝐹”〉 ∈ (𝑃 ↑𝑚
(0..^3))) |
97 | 94, 96 | sylib 210 |
. . . 4
⊢ (𝜑 → 〈“𝐷𝐸𝐹”〉 ∈ (𝑃 ↑𝑚
(0..^3))) |
98 | 90, 97 | jca 509 |
. . 3
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
〈“𝐷𝐸𝐹”〉 ∈ (𝑃 ↑𝑚
(0..^3)))) |
99 | 98 | biantrurd 530 |
. 2
⊢ (𝜑 → (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥(𝐾‘𝐸)𝐷 ∧ 𝑦(𝐾‘𝐸)𝐹) ↔ ((〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑𝑚 (0..^3)) ∧
〈“𝐷𝐸𝐹”〉 ∈ (𝑃 ↑𝑚 (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥(𝐾‘𝐸)𝐷 ∧ 𝑦(𝐾‘𝐸)𝐹)))) |
100 | 40, 78, 99 | 3bitr4d 303 |
1
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉 ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥(𝐾‘𝐸)𝐷 ∧ 𝑦(𝐾‘𝐸)𝐹))) |