| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpr 484 | . . . . . . . 8
⊢ ((𝑝 = 𝑋 ∧ 𝑡 = 〈“𝐴𝐵𝐶”〉) → 𝑡 = 〈“𝐴𝐵𝐶”〉) | 
| 2 | 1 | fveq1d 6908 | . . . . . . 7
⊢ ((𝑝 = 𝑋 ∧ 𝑡 = 〈“𝐴𝐵𝐶”〉) → (𝑡‘0) = (〈“𝐴𝐵𝐶”〉‘0)) | 
| 3 | 1 | fveq1d 6908 | . . . . . . 7
⊢ ((𝑝 = 𝑋 ∧ 𝑡 = 〈“𝐴𝐵𝐶”〉) → (𝑡‘1) = (〈“𝐴𝐵𝐶”〉‘1)) | 
| 4 | 2, 3 | neeq12d 3002 | . . . . . 6
⊢ ((𝑝 = 𝑋 ∧ 𝑡 = 〈“𝐴𝐵𝐶”〉) → ((𝑡‘0) ≠ (𝑡‘1) ↔ (〈“𝐴𝐵𝐶”〉‘0) ≠
(〈“𝐴𝐵𝐶”〉‘1))) | 
| 5 | 1 | fveq1d 6908 | . . . . . . 7
⊢ ((𝑝 = 𝑋 ∧ 𝑡 = 〈“𝐴𝐵𝐶”〉) → (𝑡‘2) = (〈“𝐴𝐵𝐶”〉‘2)) | 
| 6 | 5, 3 | neeq12d 3002 | . . . . . 6
⊢ ((𝑝 = 𝑋 ∧ 𝑡 = 〈“𝐴𝐵𝐶”〉) → ((𝑡‘2) ≠ (𝑡‘1) ↔ (〈“𝐴𝐵𝐶”〉‘2) ≠
(〈“𝐴𝐵𝐶”〉‘1))) | 
| 7 |  | simpl 482 | . . . . . . 7
⊢ ((𝑝 = 𝑋 ∧ 𝑡 = 〈“𝐴𝐵𝐶”〉) → 𝑝 = 𝑋) | 
| 8 | 7, 3 | neeq12d 3002 | . . . . . 6
⊢ ((𝑝 = 𝑋 ∧ 𝑡 = 〈“𝐴𝐵𝐶”〉) → (𝑝 ≠ (𝑡‘1) ↔ 𝑋 ≠ (〈“𝐴𝐵𝐶”〉‘1))) | 
| 9 | 4, 6, 8 | 3anbi123d 1438 | . . . . 5
⊢ ((𝑝 = 𝑋 ∧ 𝑡 = 〈“𝐴𝐵𝐶”〉) → (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ↔ ((〈“𝐴𝐵𝐶”〉‘0) ≠
(〈“𝐴𝐵𝐶”〉‘1) ∧
(〈“𝐴𝐵𝐶”〉‘2) ≠
(〈“𝐴𝐵𝐶”〉‘1) ∧ 𝑋 ≠ (〈“𝐴𝐵𝐶”〉‘1)))) | 
| 10 | 2, 5 | oveq12d 7449 | . . . . . . . 8
⊢ ((𝑝 = 𝑋 ∧ 𝑡 = 〈“𝐴𝐵𝐶”〉) → ((𝑡‘0)𝐼(𝑡‘2)) = ((〈“𝐴𝐵𝐶”〉‘0)𝐼(〈“𝐴𝐵𝐶”〉‘2))) | 
| 11 | 10 | eleq2d 2827 | . . . . . . 7
⊢ ((𝑝 = 𝑋 ∧ 𝑡 = 〈“𝐴𝐵𝐶”〉) → (𝑥 ∈ ((𝑡‘0)𝐼(𝑡‘2)) ↔ 𝑥 ∈ ((〈“𝐴𝐵𝐶”〉‘0)𝐼(〈“𝐴𝐵𝐶”〉‘2)))) | 
| 12 | 3 | eqeq2d 2748 | . . . . . . . 8
⊢ ((𝑝 = 𝑋 ∧ 𝑡 = 〈“𝐴𝐵𝐶”〉) → (𝑥 = (𝑡‘1) ↔ 𝑥 = (〈“𝐴𝐵𝐶”〉‘1))) | 
| 13 |  | eqidd 2738 | . . . . . . . . 9
⊢ ((𝑝 = 𝑋 ∧ 𝑡 = 〈“𝐴𝐵𝐶”〉) → 𝑥 = 𝑥) | 
| 14 | 3 | fveq2d 6910 | . . . . . . . . 9
⊢ ((𝑝 = 𝑋 ∧ 𝑡 = 〈“𝐴𝐵𝐶”〉) → (𝐾‘(𝑡‘1)) = (𝐾‘(〈“𝐴𝐵𝐶”〉‘1))) | 
| 15 | 13, 14, 7 | breq123d 5157 | . . . . . . . 8
⊢ ((𝑝 = 𝑋 ∧ 𝑡 = 〈“𝐴𝐵𝐶”〉) → (𝑥(𝐾‘(𝑡‘1))𝑝 ↔ 𝑥(𝐾‘(〈“𝐴𝐵𝐶”〉‘1))𝑋)) | 
| 16 | 12, 15 | orbi12d 919 | . . . . . . 7
⊢ ((𝑝 = 𝑋 ∧ 𝑡 = 〈“𝐴𝐵𝐶”〉) → ((𝑥 = (𝑡‘1) ∨ 𝑥(𝐾‘(𝑡‘1))𝑝) ↔ (𝑥 = (〈“𝐴𝐵𝐶”〉‘1) ∨ 𝑥(𝐾‘(〈“𝐴𝐵𝐶”〉‘1))𝑋))) | 
| 17 | 11, 16 | anbi12d 632 | . . . . . 6
⊢ ((𝑝 = 𝑋 ∧ 𝑡 = 〈“𝐴𝐵𝐶”〉) → ((𝑥 ∈ ((𝑡‘0)𝐼(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥(𝐾‘(𝑡‘1))𝑝)) ↔ (𝑥 ∈ ((〈“𝐴𝐵𝐶”〉‘0)𝐼(〈“𝐴𝐵𝐶”〉‘2)) ∧ (𝑥 = (〈“𝐴𝐵𝐶”〉‘1) ∨ 𝑥(𝐾‘(〈“𝐴𝐵𝐶”〉‘1))𝑋)))) | 
| 18 | 17 | rexbidv 3179 | . . . . 5
⊢ ((𝑝 = 𝑋 ∧ 𝑡 = 〈“𝐴𝐵𝐶”〉) → (∃𝑥 ∈ 𝑃 (𝑥 ∈ ((𝑡‘0)𝐼(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥(𝐾‘(𝑡‘1))𝑝)) ↔ ∃𝑥 ∈ 𝑃 (𝑥 ∈ ((〈“𝐴𝐵𝐶”〉‘0)𝐼(〈“𝐴𝐵𝐶”〉‘2)) ∧ (𝑥 = (〈“𝐴𝐵𝐶”〉‘1) ∨ 𝑥(𝐾‘(〈“𝐴𝐵𝐶”〉‘1))𝑋)))) | 
| 19 | 9, 18 | anbi12d 632 | . . . 4
⊢ ((𝑝 = 𝑋 ∧ 𝑡 = 〈“𝐴𝐵𝐶”〉) → ((((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ 𝑃 (𝑥 ∈ ((𝑡‘0)𝐼(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥(𝐾‘(𝑡‘1))𝑝))) ↔ (((〈“𝐴𝐵𝐶”〉‘0) ≠
(〈“𝐴𝐵𝐶”〉‘1) ∧
(〈“𝐴𝐵𝐶”〉‘2) ≠
(〈“𝐴𝐵𝐶”〉‘1) ∧ 𝑋 ≠ (〈“𝐴𝐵𝐶”〉‘1)) ∧ ∃𝑥 ∈ 𝑃 (𝑥 ∈ ((〈“𝐴𝐵𝐶”〉‘0)𝐼(〈“𝐴𝐵𝐶”〉‘2)) ∧ (𝑥 = (〈“𝐴𝐵𝐶”〉‘1) ∨ 𝑥(𝐾‘(〈“𝐴𝐵𝐶”〉‘1))𝑋))))) | 
| 20 |  | eqid 2737 | . . . 4
⊢
{〈𝑝, 𝑡〉 ∣ ((𝑝 ∈ 𝑃 ∧ 𝑡 ∈ (𝑃 ↑m (0..^3))) ∧ (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ 𝑃 (𝑥 ∈ ((𝑡‘0)𝐼(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥(𝐾‘(𝑡‘1))𝑝))))} = {〈𝑝, 𝑡〉 ∣ ((𝑝 ∈ 𝑃 ∧ 𝑡 ∈ (𝑃 ↑m (0..^3))) ∧ (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ 𝑃 (𝑥 ∈ ((𝑡‘0)𝐼(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥(𝐾‘(𝑡‘1))𝑝))))} | 
| 21 | 19, 20 | brab2a 5779 | . . 3
⊢ (𝑋{〈𝑝, 𝑡〉 ∣ ((𝑝 ∈ 𝑃 ∧ 𝑡 ∈ (𝑃 ↑m (0..^3))) ∧ (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ 𝑃 (𝑥 ∈ ((𝑡‘0)𝐼(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥(𝐾‘(𝑡‘1))𝑝))))}〈“𝐴𝐵𝐶”〉 ↔ ((𝑋 ∈ 𝑃 ∧ 〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑m (0..^3))) ∧
(((〈“𝐴𝐵𝐶”〉‘0) ≠
(〈“𝐴𝐵𝐶”〉‘1) ∧
(〈“𝐴𝐵𝐶”〉‘2) ≠
(〈“𝐴𝐵𝐶”〉‘1) ∧ 𝑋 ≠ (〈“𝐴𝐵𝐶”〉‘1)) ∧ ∃𝑥 ∈ 𝑃 (𝑥 ∈ ((〈“𝐴𝐵𝐶”〉‘0)𝐼(〈“𝐴𝐵𝐶”〉‘2)) ∧ (𝑥 = (〈“𝐴𝐵𝐶”〉‘1) ∨ 𝑥(𝐾‘(〈“𝐴𝐵𝐶”〉‘1))𝑋))))) | 
| 22 |  | isinag.a | . . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑃) | 
| 23 |  | s3fv0 14930 | . . . . . . . 8
⊢ (𝐴 ∈ 𝑃 → (〈“𝐴𝐵𝐶”〉‘0) = 𝐴) | 
| 24 | 22, 23 | syl 17 | . . . . . . 7
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉‘0) = 𝐴) | 
| 25 |  | isinag.b | . . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ 𝑃) | 
| 26 |  | s3fv1 14931 | . . . . . . . 8
⊢ (𝐵 ∈ 𝑃 → (〈“𝐴𝐵𝐶”〉‘1) = 𝐵) | 
| 27 | 25, 26 | syl 17 | . . . . . . 7
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉‘1) = 𝐵) | 
| 28 | 24, 27 | neeq12d 3002 | . . . . . 6
⊢ (𝜑 → ((〈“𝐴𝐵𝐶”〉‘0) ≠
(〈“𝐴𝐵𝐶”〉‘1) ↔ 𝐴 ≠ 𝐵)) | 
| 29 |  | isinag.c | . . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ 𝑃) | 
| 30 |  | s3fv2 14932 | . . . . . . . 8
⊢ (𝐶 ∈ 𝑃 → (〈“𝐴𝐵𝐶”〉‘2) = 𝐶) | 
| 31 | 29, 30 | syl 17 | . . . . . . 7
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉‘2) = 𝐶) | 
| 32 | 31, 27 | neeq12d 3002 | . . . . . 6
⊢ (𝜑 → ((〈“𝐴𝐵𝐶”〉‘2) ≠
(〈“𝐴𝐵𝐶”〉‘1) ↔ 𝐶 ≠ 𝐵)) | 
| 33 | 27 | neeq2d 3001 | . . . . . 6
⊢ (𝜑 → (𝑋 ≠ (〈“𝐴𝐵𝐶”〉‘1) ↔ 𝑋 ≠ 𝐵)) | 
| 34 | 28, 32, 33 | 3anbi123d 1438 | . . . . 5
⊢ (𝜑 → (((〈“𝐴𝐵𝐶”〉‘0) ≠
(〈“𝐴𝐵𝐶”〉‘1) ∧
(〈“𝐴𝐵𝐶”〉‘2) ≠
(〈“𝐴𝐵𝐶”〉‘1) ∧ 𝑋 ≠ (〈“𝐴𝐵𝐶”〉‘1)) ↔ (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵))) | 
| 35 | 24, 31 | oveq12d 7449 | . . . . . . . 8
⊢ (𝜑 → ((〈“𝐴𝐵𝐶”〉‘0)𝐼(〈“𝐴𝐵𝐶”〉‘2)) = (𝐴𝐼𝐶)) | 
| 36 | 35 | eleq2d 2827 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ((〈“𝐴𝐵𝐶”〉‘0)𝐼(〈“𝐴𝐵𝐶”〉‘2)) ↔ 𝑥 ∈ (𝐴𝐼𝐶))) | 
| 37 | 27 | eqeq2d 2748 | . . . . . . . 8
⊢ (𝜑 → (𝑥 = (〈“𝐴𝐵𝐶”〉‘1) ↔ 𝑥 = 𝐵)) | 
| 38 | 27 | fveq2d 6910 | . . . . . . . . 9
⊢ (𝜑 → (𝐾‘(〈“𝐴𝐵𝐶”〉‘1)) = (𝐾‘𝐵)) | 
| 39 | 38 | breqd 5154 | . . . . . . . 8
⊢ (𝜑 → (𝑥(𝐾‘(〈“𝐴𝐵𝐶”〉‘1))𝑋 ↔ 𝑥(𝐾‘𝐵)𝑋)) | 
| 40 | 37, 39 | orbi12d 919 | . . . . . . 7
⊢ (𝜑 → ((𝑥 = (〈“𝐴𝐵𝐶”〉‘1) ∨ 𝑥(𝐾‘(〈“𝐴𝐵𝐶”〉‘1))𝑋) ↔ (𝑥 = 𝐵 ∨ 𝑥(𝐾‘𝐵)𝑋))) | 
| 41 | 36, 40 | anbi12d 632 | . . . . . 6
⊢ (𝜑 → ((𝑥 ∈ ((〈“𝐴𝐵𝐶”〉‘0)𝐼(〈“𝐴𝐵𝐶”〉‘2)) ∧ (𝑥 = (〈“𝐴𝐵𝐶”〉‘1) ∨ 𝑥(𝐾‘(〈“𝐴𝐵𝐶”〉‘1))𝑋)) ↔ (𝑥 ∈ (𝐴𝐼𝐶) ∧ (𝑥 = 𝐵 ∨ 𝑥(𝐾‘𝐵)𝑋)))) | 
| 42 | 41 | rexbidv 3179 | . . . . 5
⊢ (𝜑 → (∃𝑥 ∈ 𝑃 (𝑥 ∈ ((〈“𝐴𝐵𝐶”〉‘0)𝐼(〈“𝐴𝐵𝐶”〉‘2)) ∧ (𝑥 = (〈“𝐴𝐵𝐶”〉‘1) ∨ 𝑥(𝐾‘(〈“𝐴𝐵𝐶”〉‘1))𝑋)) ↔ ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐶) ∧ (𝑥 = 𝐵 ∨ 𝑥(𝐾‘𝐵)𝑋)))) | 
| 43 | 34, 42 | anbi12d 632 | . . . 4
⊢ (𝜑 → ((((〈“𝐴𝐵𝐶”〉‘0) ≠
(〈“𝐴𝐵𝐶”〉‘1) ∧
(〈“𝐴𝐵𝐶”〉‘2) ≠
(〈“𝐴𝐵𝐶”〉‘1) ∧ 𝑋 ≠ (〈“𝐴𝐵𝐶”〉‘1)) ∧ ∃𝑥 ∈ 𝑃 (𝑥 ∈ ((〈“𝐴𝐵𝐶”〉‘0)𝐼(〈“𝐴𝐵𝐶”〉‘2)) ∧ (𝑥 = (〈“𝐴𝐵𝐶”〉‘1) ∨ 𝑥(𝐾‘(〈“𝐴𝐵𝐶”〉‘1))𝑋))) ↔ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵) ∧ ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐶) ∧ (𝑥 = 𝐵 ∨ 𝑥(𝐾‘𝐵)𝑋))))) | 
| 44 | 43 | anbi2d 630 | . . 3
⊢ (𝜑 → (((𝑋 ∈ 𝑃 ∧ 〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑m (0..^3))) ∧
(((〈“𝐴𝐵𝐶”〉‘0) ≠
(〈“𝐴𝐵𝐶”〉‘1) ∧
(〈“𝐴𝐵𝐶”〉‘2) ≠
(〈“𝐴𝐵𝐶”〉‘1) ∧ 𝑋 ≠ (〈“𝐴𝐵𝐶”〉‘1)) ∧ ∃𝑥 ∈ 𝑃 (𝑥 ∈ ((〈“𝐴𝐵𝐶”〉‘0)𝐼(〈“𝐴𝐵𝐶”〉‘2)) ∧ (𝑥 = (〈“𝐴𝐵𝐶”〉‘1) ∨ 𝑥(𝐾‘(〈“𝐴𝐵𝐶”〉‘1))𝑋)))) ↔ ((𝑋 ∈ 𝑃 ∧ 〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑m (0..^3))) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵) ∧ ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐶) ∧ (𝑥 = 𝐵 ∨ 𝑥(𝐾‘𝐵)𝑋)))))) | 
| 45 | 21, 44 | bitrid 283 | . 2
⊢ (𝜑 → (𝑋{〈𝑝, 𝑡〉 ∣ ((𝑝 ∈ 𝑃 ∧ 𝑡 ∈ (𝑃 ↑m (0..^3))) ∧ (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ 𝑃 (𝑥 ∈ ((𝑡‘0)𝐼(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥(𝐾‘(𝑡‘1))𝑝))))}〈“𝐴𝐵𝐶”〉 ↔ ((𝑋 ∈ 𝑃 ∧ 〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑m (0..^3))) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵) ∧ ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐶) ∧ (𝑥 = 𝐵 ∨ 𝑥(𝐾‘𝐵)𝑋)))))) | 
| 46 |  | isinag.g | . . . 4
⊢ (𝜑 → 𝐺 ∈ 𝑉) | 
| 47 |  | elex 3501 | . . . 4
⊢ (𝐺 ∈ 𝑉 → 𝐺 ∈ V) | 
| 48 |  | fveq2 6906 | . . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺)) | 
| 49 |  | isinag.p | . . . . . . . . . 10
⊢ 𝑃 = (Base‘𝐺) | 
| 50 | 48, 49 | eqtr4di 2795 | . . . . . . . . 9
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝑃) | 
| 51 | 50 | eleq2d 2827 | . . . . . . . 8
⊢ (𝑔 = 𝐺 → (𝑝 ∈ (Base‘𝑔) ↔ 𝑝 ∈ 𝑃)) | 
| 52 | 50 | oveq1d 7446 | . . . . . . . . 9
⊢ (𝑔 = 𝐺 → ((Base‘𝑔) ↑m (0..^3)) = (𝑃 ↑m
(0..^3))) | 
| 53 | 52 | eleq2d 2827 | . . . . . . . 8
⊢ (𝑔 = 𝐺 → (𝑡 ∈ ((Base‘𝑔) ↑m (0..^3)) ↔ 𝑡 ∈ (𝑃 ↑m
(0..^3)))) | 
| 54 | 51, 53 | anbi12d 632 | . . . . . . 7
⊢ (𝑔 = 𝐺 → ((𝑝 ∈ (Base‘𝑔) ∧ 𝑡 ∈ ((Base‘𝑔) ↑m (0..^3))) ↔ (𝑝 ∈ 𝑃 ∧ 𝑡 ∈ (𝑃 ↑m
(0..^3))))) | 
| 55 |  | fveq2 6906 | . . . . . . . . . . . . 13
⊢ (𝑔 = 𝐺 → (Itv‘𝑔) = (Itv‘𝐺)) | 
| 56 |  | isinag.i | . . . . . . . . . . . . 13
⊢ 𝐼 = (Itv‘𝐺) | 
| 57 | 55, 56 | eqtr4di 2795 | . . . . . . . . . . . 12
⊢ (𝑔 = 𝐺 → (Itv‘𝑔) = 𝐼) | 
| 58 | 57 | oveqd 7448 | . . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → ((𝑡‘0)(Itv‘𝑔)(𝑡‘2)) = ((𝑡‘0)𝐼(𝑡‘2))) | 
| 59 | 58 | eleq2d 2827 | . . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (𝑥 ∈ ((𝑡‘0)(Itv‘𝑔)(𝑡‘2)) ↔ 𝑥 ∈ ((𝑡‘0)𝐼(𝑡‘2)))) | 
| 60 |  | fveq2 6906 | . . . . . . . . . . . . . 14
⊢ (𝑔 = 𝐺 → (hlG‘𝑔) = (hlG‘𝐺)) | 
| 61 |  | isinag.k | . . . . . . . . . . . . . 14
⊢ 𝐾 = (hlG‘𝐺) | 
| 62 | 60, 61 | eqtr4di 2795 | . . . . . . . . . . . . 13
⊢ (𝑔 = 𝐺 → (hlG‘𝑔) = 𝐾) | 
| 63 | 62 | fveq1d 6908 | . . . . . . . . . . . 12
⊢ (𝑔 = 𝐺 → ((hlG‘𝑔)‘(𝑡‘1)) = (𝐾‘(𝑡‘1))) | 
| 64 | 63 | breqd 5154 | . . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → (𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝 ↔ 𝑥(𝐾‘(𝑡‘1))𝑝)) | 
| 65 | 64 | orbi2d 916 | . . . . . . . . . 10
⊢ (𝑔 = 𝐺 → ((𝑥 = (𝑡‘1) ∨ 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝) ↔ (𝑥 = (𝑡‘1) ∨ 𝑥(𝐾‘(𝑡‘1))𝑝))) | 
| 66 | 59, 65 | anbi12d 632 | . . . . . . . . 9
⊢ (𝑔 = 𝐺 → ((𝑥 ∈ ((𝑡‘0)(Itv‘𝑔)(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝)) ↔ (𝑥 ∈ ((𝑡‘0)𝐼(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥(𝐾‘(𝑡‘1))𝑝)))) | 
| 67 | 50, 66 | rexeqbidv 3347 | . . . . . . . 8
⊢ (𝑔 = 𝐺 → (∃𝑥 ∈ (Base‘𝑔)(𝑥 ∈ ((𝑡‘0)(Itv‘𝑔)(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝)) ↔ ∃𝑥 ∈ 𝑃 (𝑥 ∈ ((𝑡‘0)𝐼(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥(𝐾‘(𝑡‘1))𝑝)))) | 
| 68 | 67 | anbi2d 630 | . . . . . . 7
⊢ (𝑔 = 𝐺 → ((((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥 ∈ ((𝑡‘0)(Itv‘𝑔)(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝))) ↔ (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ 𝑃 (𝑥 ∈ ((𝑡‘0)𝐼(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥(𝐾‘(𝑡‘1))𝑝))))) | 
| 69 | 54, 68 | anbi12d 632 | . . . . . 6
⊢ (𝑔 = 𝐺 → (((𝑝 ∈ (Base‘𝑔) ∧ 𝑡 ∈ ((Base‘𝑔) ↑m (0..^3))) ∧ (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥 ∈ ((𝑡‘0)(Itv‘𝑔)(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝)))) ↔ ((𝑝 ∈ 𝑃 ∧ 𝑡 ∈ (𝑃 ↑m (0..^3))) ∧ (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ 𝑃 (𝑥 ∈ ((𝑡‘0)𝐼(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥(𝐾‘(𝑡‘1))𝑝)))))) | 
| 70 | 69 | opabbidv 5209 | . . . . 5
⊢ (𝑔 = 𝐺 → {〈𝑝, 𝑡〉 ∣ ((𝑝 ∈ (Base‘𝑔) ∧ 𝑡 ∈ ((Base‘𝑔) ↑m (0..^3))) ∧ (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥 ∈ ((𝑡‘0)(Itv‘𝑔)(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝))))} = {〈𝑝, 𝑡〉 ∣ ((𝑝 ∈ 𝑃 ∧ 𝑡 ∈ (𝑃 ↑m (0..^3))) ∧ (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ 𝑃 (𝑥 ∈ ((𝑡‘0)𝐼(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥(𝐾‘(𝑡‘1))𝑝))))}) | 
| 71 |  | df-inag 28845 | . . . . 5
⊢ inA =
(𝑔 ∈ V ↦
{〈𝑝, 𝑡〉 ∣ ((𝑝 ∈ (Base‘𝑔) ∧ 𝑡 ∈ ((Base‘𝑔) ↑m (0..^3))) ∧ (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ (Base‘𝑔)(𝑥 ∈ ((𝑡‘0)(Itv‘𝑔)(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥((hlG‘𝑔)‘(𝑡‘1))𝑝))))}) | 
| 72 | 49 | fvexi 6920 | . . . . . . 7
⊢ 𝑃 ∈ V | 
| 73 |  | ovex 7464 | . . . . . . 7
⊢ (𝑃 ↑m (0..^3))
∈ V | 
| 74 | 72, 73 | xpex 7773 | . . . . . 6
⊢ (𝑃 × (𝑃 ↑m (0..^3))) ∈
V | 
| 75 |  | opabssxp 5778 | . . . . . 6
⊢
{〈𝑝, 𝑡〉 ∣ ((𝑝 ∈ 𝑃 ∧ 𝑡 ∈ (𝑃 ↑m (0..^3))) ∧ (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ 𝑃 (𝑥 ∈ ((𝑡‘0)𝐼(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥(𝐾‘(𝑡‘1))𝑝))))} ⊆ (𝑃 × (𝑃 ↑m
(0..^3))) | 
| 76 | 74, 75 | ssexi 5322 | . . . . 5
⊢
{〈𝑝, 𝑡〉 ∣ ((𝑝 ∈ 𝑃 ∧ 𝑡 ∈ (𝑃 ↑m (0..^3))) ∧ (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ 𝑃 (𝑥 ∈ ((𝑡‘0)𝐼(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥(𝐾‘(𝑡‘1))𝑝))))} ∈ V | 
| 77 | 70, 71, 76 | fvmpt 7016 | . . . 4
⊢ (𝐺 ∈ V →
(inA‘𝐺) =
{〈𝑝, 𝑡〉 ∣ ((𝑝 ∈ 𝑃 ∧ 𝑡 ∈ (𝑃 ↑m (0..^3))) ∧ (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ 𝑃 (𝑥 ∈ ((𝑡‘0)𝐼(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥(𝐾‘(𝑡‘1))𝑝))))}) | 
| 78 | 46, 47, 77 | 3syl 18 | . . 3
⊢ (𝜑 → (inA‘𝐺) = {〈𝑝, 𝑡〉 ∣ ((𝑝 ∈ 𝑃 ∧ 𝑡 ∈ (𝑃 ↑m (0..^3))) ∧ (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ 𝑃 (𝑥 ∈ ((𝑡‘0)𝐼(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥(𝐾‘(𝑡‘1))𝑝))))}) | 
| 79 | 78 | breqd 5154 | . 2
⊢ (𝜑 → (𝑋(inA‘𝐺)〈“𝐴𝐵𝐶”〉 ↔ 𝑋{〈𝑝, 𝑡〉 ∣ ((𝑝 ∈ 𝑃 ∧ 𝑡 ∈ (𝑃 ↑m (0..^3))) ∧ (((𝑡‘0) ≠ (𝑡‘1) ∧ (𝑡‘2) ≠ (𝑡‘1) ∧ 𝑝 ≠ (𝑡‘1)) ∧ ∃𝑥 ∈ 𝑃 (𝑥 ∈ ((𝑡‘0)𝐼(𝑡‘2)) ∧ (𝑥 = (𝑡‘1) ∨ 𝑥(𝐾‘(𝑡‘1))𝑝))))}〈“𝐴𝐵𝐶”〉)) | 
| 80 |  | isinag.x | . . . 4
⊢ (𝜑 → 𝑋 ∈ 𝑃) | 
| 81 | 22, 25, 29 | s3cld 14911 | . . . . 5
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃) | 
| 82 |  | s3len 14933 | . . . . 5
⊢
(♯‘〈“𝐴𝐵𝐶”〉) = 3 | 
| 83 |  | 3nn0 12544 | . . . . . 6
⊢ 3 ∈
ℕ0 | 
| 84 |  | wrdmap 14584 | . . . . . 6
⊢ ((𝑃 ∈ V ∧ 3 ∈
ℕ0) → ((〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃 ∧ (♯‘〈“𝐴𝐵𝐶”〉) = 3) ↔
〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑m
(0..^3)))) | 
| 85 | 72, 83, 84 | mp2an 692 | . . . . 5
⊢
((〈“𝐴𝐵𝐶”〉 ∈ Word 𝑃 ∧ (♯‘〈“𝐴𝐵𝐶”〉) = 3) ↔
〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑m
(0..^3))) | 
| 86 | 81, 82, 85 | sylanblc 589 | . . . 4
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑m
(0..^3))) | 
| 87 | 80, 86 | jca 511 | . . 3
⊢ (𝜑 → (𝑋 ∈ 𝑃 ∧ 〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑m
(0..^3)))) | 
| 88 | 87 | biantrurd 532 | . 2
⊢ (𝜑 → (((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵) ∧ ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐶) ∧ (𝑥 = 𝐵 ∨ 𝑥(𝐾‘𝐵)𝑋))) ↔ ((𝑋 ∈ 𝑃 ∧ 〈“𝐴𝐵𝐶”〉 ∈ (𝑃 ↑m (0..^3))) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵) ∧ ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐶) ∧ (𝑥 = 𝐵 ∨ 𝑥(𝐾‘𝐵)𝑋)))))) | 
| 89 | 45, 79, 88 | 3bitr4d 311 | 1
⊢ (𝜑 → (𝑋(inA‘𝐺)〈“𝐴𝐵𝐶”〉 ↔ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵) ∧ ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐶) ∧ (𝑥 = 𝐵 ∨ 𝑥(𝐾‘𝐵)𝑋))))) |