| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpl 482 | . . . . . . 7
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → 𝑎 = 〈“𝐴𝐵𝐶”〉) | 
| 2 |  | eqidd 2737 | . . . . . . . 8
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → 𝑥 = 𝑥) | 
| 3 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → 𝑏 = 〈“𝐷𝐸𝐹”〉) | 
| 4 | 3 | fveq1d 6907 | . . . . . . . 8
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → (𝑏‘1) = (〈“𝐷𝐸𝐹”〉‘1)) | 
| 5 |  | eqidd 2737 | . . . . . . . 8
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → 𝑦 = 𝑦) | 
| 6 | 2, 4, 5 | s3eqd 14904 | . . . . . . 7
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → 〈“𝑥(𝑏‘1)𝑦”〉 = 〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉) | 
| 7 | 1, 6 | breq12d 5155 | . . . . . 6
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ↔ 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉)) | 
| 8 | 4 | fveq2d 6909 | . . . . . . 7
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → (𝐾‘(𝑏‘1)) = (𝐾‘(〈“𝐷𝐸𝐹”〉‘1))) | 
| 9 | 3 | fveq1d 6907 | . . . . . . 7
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → (𝑏‘0) = (〈“𝐷𝐸𝐹”〉‘0)) | 
| 10 | 2, 8, 9 | breq123d 5156 | . . . . . 6
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → (𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ↔ 𝑥(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘0))) | 
| 11 | 3 | fveq1d 6907 | . . . . . . 7
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → (𝑏‘2) = (〈“𝐷𝐸𝐹”〉‘2)) | 
| 12 | 5, 8, 11 | breq123d 5156 | . . . . . 6
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → (𝑦(𝐾‘(𝑏‘1))(𝑏‘2) ↔ 𝑦(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘2))) | 
| 13 | 7, 10, 12 | 3anbi123d 1437 | . . . . 5
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → ((𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)) ↔ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉 ∧ 𝑥(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘0) ∧ 𝑦(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘2)))) | 
| 14 | 13 | 2rexbidv 3221 | . . . 4
⊢ ((𝑎 = 〈“𝐴𝐵𝐶”〉 ∧ 𝑏 = 〈“𝐷𝐸𝐹”〉) → (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)) ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉 ∧ 𝑥(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘0) ∧ 𝑦(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘2)))) | 
| 15 |  | eqid 2736 | . . . 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 5778 | . . 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 2737 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → 𝑥 = 𝑥) | 
| 18 |  | iscgra.e | . . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ 𝑃) | 
| 19 |  | s3fv1 14932 | . . . . . . . . . 10
⊢ (𝐸 ∈ 𝑃 → (〈“𝐷𝐸𝐹”〉‘1) = 𝐸) | 
| 20 | 18, 19 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (〈“𝐷𝐸𝐹”〉‘1) = 𝐸) | 
| 21 | 20 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (〈“𝐷𝐸𝐹”〉‘1) = 𝐸) | 
| 22 |  | eqidd 2737 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → 𝑦 = 𝑦) | 
| 23 | 17, 21, 22 | s3eqd 14904 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → 〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉 = 〈“𝑥𝐸𝑦”〉) | 
| 24 | 23 | breq2d 5154 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉 ↔ 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉)) | 
| 25 | 21 | fveq2d 6909 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (𝐾‘(〈“𝐷𝐸𝐹”〉‘1)) = (𝐾‘𝐸)) | 
| 26 |  | iscgra.d | . . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ 𝑃) | 
| 27 |  | s3fv0 14931 | . . . . . . . . 9
⊢ (𝐷 ∈ 𝑃 → (〈“𝐷𝐸𝐹”〉‘0) = 𝐷) | 
| 28 | 26, 27 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (〈“𝐷𝐸𝐹”〉‘0) = 𝐷) | 
| 29 | 28 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (〈“𝐷𝐸𝐹”〉‘0) = 𝐷) | 
| 30 | 17, 25, 29 | breq123d 5156 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (𝑥(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘0) ↔ 𝑥(𝐾‘𝐸)𝐷)) | 
| 31 |  | iscgra.f | . . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ 𝑃) | 
| 32 |  | s3fv2 14933 | . . . . . . . . 9
⊢ (𝐹 ∈ 𝑃 → (〈“𝐷𝐸𝐹”〉‘2) = 𝐹) | 
| 33 | 31, 32 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (〈“𝐷𝐸𝐹”〉‘2) = 𝐹) | 
| 34 | 33 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (〈“𝐷𝐸𝐹”〉‘2) = 𝐹) | 
| 35 | 22, 25, 34 | breq123d 5156 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → (𝑦(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘2) ↔ 𝑦(𝐾‘𝐸)𝐹)) | 
| 36 | 24, 30, 35 | 3anbi123d 1437 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝑃)) → ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉 ∧ 𝑥(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘0) ∧ 𝑦(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘2)) ↔
(〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥(𝐾‘𝐸)𝐷 ∧ 𝑦(𝐾‘𝐸)𝐹))) | 
| 37 | 36 | 2rexbidva 3219 | . . . 4
⊢ (𝜑 → (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥(〈“𝐷𝐸𝐹”〉‘1)𝑦”〉 ∧ 𝑥(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘0) ∧ 𝑦(𝐾‘(〈“𝐷𝐸𝐹”〉‘1))(〈“𝐷𝐸𝐹”〉‘2)) ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥(𝐾‘𝐸)𝐷 ∧ 𝑦(𝐾‘𝐸)𝐹))) | 
| 38 | 37 | anbi2d 630 | . . 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 3500 | . . . 4
⊢ (𝐺 ∈ TarskiG → 𝐺 ∈ V) | 
| 42 |  | iscgra.p | . . . . . . . 8
⊢ 𝑃 = (Base‘𝐺) | 
| 43 |  | iscgra.k | . . . . . . . 8
⊢ 𝐾 = (hlG‘𝐺) | 
| 44 |  | simpl 482 | . . . . . . . . . . . 12
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → 𝑝 = 𝑃) | 
| 45 | 44 | oveq1d 7447 | . . . . . . . . . . 11
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → (𝑝 ↑m (0..^3)) = (𝑃 ↑m
(0..^3))) | 
| 46 | 45 | eleq2d 2826 | . . . . . . . . . 10
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → (𝑎 ∈ (𝑝 ↑m (0..^3)) ↔ 𝑎 ∈ (𝑃 ↑m
(0..^3)))) | 
| 47 | 45 | eleq2d 2826 | . . . . . . . . . 10
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → (𝑏 ∈ (𝑝 ↑m (0..^3)) ↔ 𝑏 ∈ (𝑃 ↑m
(0..^3)))) | 
| 48 | 46, 47 | anbi12d 632 | . . . . . . . . 9
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → ((𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m (0..^3))) ↔ (𝑎 ∈ (𝑃 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑃 ↑m
(0..^3))))) | 
| 49 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → 𝑘 = 𝐾) | 
| 50 | 49 | fveq1d 6907 | . . . . . . . . . . . . 13
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → (𝑘‘(𝑏‘1)) = (𝐾‘(𝑏‘1))) | 
| 51 | 50 | breqd 5153 | . . . . . . . . . . . 12
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → (𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ↔ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0))) | 
| 52 | 50 | breqd 5153 | . . . . . . . . . . . 12
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → (𝑦(𝑘‘(𝑏‘1))(𝑏‘2) ↔ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2))) | 
| 53 | 51, 52 | 3anbi23d 1440 | . . . . . . . . . . 11
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → ((𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)) ↔ (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))) | 
| 54 | 44, 53 | rexeqbidv 3346 | . . . . . . . . . 10
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → (∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)) ↔ ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))) | 
| 55 | 44, 54 | rexeqbidv 3346 | . . . . . . . . 9
⊢ ((𝑝 = 𝑃 ∧ 𝑘 = 𝐾) → (∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)) ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))) | 
| 56 | 48, 55 | anbi12d 632 | . . . . . . . 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 17199 | . . . . . . 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 5208 | . . . . . 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 6905 | . . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → (cgrG‘𝑔) = (cgrG‘𝐺)) | 
| 60 | 59 | breqd 5153 | . . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ↔ 𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉)) | 
| 61 | 60 | 3anbi1d 1441 | . . . . . . . . 9
⊢ (𝑔 = 𝐺 → ((𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)) ↔ (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))) | 
| 62 | 61 | 2rexbidv 3221 | . . . . . . . 8
⊢ (𝑔 = 𝐺 → (∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)) ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))) | 
| 63 | 62 | anbi2d 630 | . . . . . . 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 5208 | . . . . . 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 2776 | . . . . 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 28817 | . . . . 5
⊢ cgrA =
(𝑔 ∈ V ↦
{〈𝑎, 𝑏〉 ∣
[(Base‘𝑔) /
𝑝][(hlG‘𝑔) / 𝑘]((𝑎 ∈ (𝑝 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑝 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑝 ∃𝑦 ∈ 𝑝 (𝑎(cgrG‘𝑔)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝑘‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝑘‘(𝑏‘1))(𝑏‘2)))}) | 
| 67 |  | ovex 7465 | . . . . . . 7
⊢ (𝑃 ↑m (0..^3))
∈ V | 
| 68 | 67, 67 | xpex 7774 | . . . . . 6
⊢ ((𝑃 ↑m (0..^3))
× (𝑃
↑m (0..^3))) ∈ V | 
| 69 |  | opabssxp 5777 | . . . . . 6
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑃 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))} ⊆ ((𝑃 ↑m (0..^3)) × (𝑃 ↑m
(0..^3))) | 
| 70 | 68, 69 | ssexi 5321 | . . . . 5
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑m (0..^3)) ∧ 𝑏 ∈ (𝑃 ↑m (0..^3))) ∧
∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (𝑎(cgrG‘𝐺)〈“𝑥(𝑏‘1)𝑦”〉 ∧ 𝑥(𝐾‘(𝑏‘1))(𝑏‘0) ∧ 𝑦(𝐾‘(𝑏‘1))(𝑏‘2)))} ∈ V | 
| 71 | 65, 66, 70 | fvmpt 7015 | . . . 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 5153 | . 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 14912 | . . . . 5
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃) | 
| 78 |  | s3len 14934 | . . . . 5
⊢
(♯‘〈“𝐴𝐵𝐶”〉) = 3 | 
| 79 | 42 | fvexi 6919 | . . . . . 6
⊢ 𝑃 ∈ V | 
| 80 |  | 3nn0 12546 | . . . . . 6
⊢ 3 ∈
ℕ0 | 
| 81 |  | wrdmap 14585 | . . . . . 6
⊢ ((𝑃 ∈ V ∧ 3 ∈
ℕ0) → ((〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃 ∧ (♯‘〈“𝐴𝐵𝐶”〉) = 3) ↔
〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑m
(0..^3)))) | 
| 82 | 79, 80, 81 | mp2an 692 | . . . . 5
⊢
((〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃 ∧ (♯‘〈“𝐴𝐵𝐶”〉) = 3) ↔
〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑m
(0..^3))) | 
| 83 | 77, 78, 82 | sylanblc 589 | . . . 4
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑m
(0..^3))) | 
| 84 | 26, 18, 31 | s3cld 14912 | . . . . 5
⊢ (𝜑 → 〈“𝐷𝐸𝐹”〉 ∈ Word 𝑃) | 
| 85 |  | s3len 14934 | . . . . 5
⊢
(♯‘〈“𝐷𝐸𝐹”〉) = 3 | 
| 86 |  | wrdmap 14585 | . . . . . 6
⊢ ((𝑃 ∈ V ∧ 3 ∈
ℕ0) → ((〈“𝐷𝐸𝐹”〉 ∈ Word 𝑃 ∧ (♯‘〈“𝐷𝐸𝐹”〉) = 3) ↔
〈“𝐷𝐸𝐹”〉 ∈ (𝑃 ↑m
(0..^3)))) | 
| 87 | 79, 80, 86 | mp2an 692 | . . . . 5
⊢
((〈“𝐷𝐸𝐹”〉 ∈ Word 𝑃 ∧ (♯‘〈“𝐷𝐸𝐹”〉) = 3) ↔
〈“𝐷𝐸𝐹”〉 ∈ (𝑃 ↑m
(0..^3))) | 
| 88 | 84, 85, 87 | sylanblc 589 | . . . 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‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥(𝐾‘𝐸)𝐷 ∧ 𝑦(𝐾‘𝐸)𝐹))) |