Metamath Proof Explorer

Theorem ishlg2

Description: Alternate version of ishlg , including closure. (Contributed by Thierry Arnoux, 13-Jul-2026)

Ref Expression
Hypotheses ishlg.p ⊢ P = Base G
ishlg.i ⊢ I = Itv ⁡ G
ishlg.k ⊢ K = hl 𝒢 ⁡ G
ishlg2.g ⊢ φ → G ∈ V
ishlg2.1 ⊢ φ → C ∈ P
Assertion ishlg2 ⊢ φ → A K ⁡ C B ↔ A ∈ P ∧ B ∈ P ∧ A ≠ C ∧ B ≠ C ∧ A ∈ C I B ∨ B ∈ C I A

Proof

Step Hyp Ref Expression
1 ishlg.p ⊢ P = Base G
2 ishlg.i ⊢ I = Itv ⁡ G
3 ishlg.k ⊢ K = hl 𝒢 ⁡ G
4 ishlg2.g ⊢ φ → G ∈ V
5 ishlg2.1 ⊢ φ → C ∈ P
6 neeq2 ⊢ c = C → a ≠ c ↔ a ≠ C
7 neeq2 ⊢ c = C → b ≠ c ↔ b ≠ C
8 oveq1 ⊢ c = C → c I b = C I b
9 8 eleq2d ⊢ c = C → a ∈ c I b ↔ a ∈ C I b
10 oveq1 ⊢ c = C → c I a = C I a
11 10 eleq2d ⊢ c = C → b ∈ c I a ↔ b ∈ C I a
12 9 11 orbi12d ⊢ c = C → a ∈ c I b ∨ b ∈ c I a ↔ a ∈ C I b ∨ b ∈ C I a
13 6 7 12 3anbi123d ⊢ c = C → a ≠ c ∧ b ≠ c ∧ a ∈ c I b ∨ b ∈ c I a ↔ a ≠ C ∧ b ≠ C ∧ a ∈ C I b ∨ b ∈ C I a
14 13 anbi2d ⊢ c = C → a ∈ P ∧ b ∈ P ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c I b ∨ b ∈ c I a ↔ a ∈ P ∧ b ∈ P ∧ a ≠ C ∧ b ≠ C ∧ a ∈ C I b ∨ b ∈ C I a
15 14 opabbidv ⊢ c = C → a b | a ∈ P ∧ b ∈ P ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c I b ∨ b ∈ c I a = a b | a ∈ P ∧ b ∈ P ∧ a ≠ C ∧ b ≠ C ∧ a ∈ C I b ∨ b ∈ C I a
16 elex ⊢ G ∈ V → G ∈ V
17 fveq2 ⊢ g = G → Base g = Base G
18 17 1 eqtr4di ⊢ g = G → Base g = P
19 18 eleq2d ⊢ g = G → a ∈ Base g ↔ a ∈ P
20 18 eleq2d ⊢ g = G → b ∈ Base g ↔ b ∈ P
21 19 20 anbi12d ⊢ g = G → a ∈ Base g ∧ b ∈ Base g ↔ a ∈ P ∧ b ∈ P
22 fveq2 ⊢ g = G → Itv ⁡ g = Itv ⁡ G
23 22 2 eqtr4di ⊢ g = G → Itv ⁡ g = I
24 23 oveqd ⊢ g = G → c Itv ⁡ g b = c I b
25 24 eleq2d ⊢ g = G → a ∈ c Itv ⁡ g b ↔ a ∈ c I b
26 23 oveqd ⊢ g = G → c Itv ⁡ g a = c I a
27 26 eleq2d ⊢ g = G → b ∈ c Itv ⁡ g a ↔ b ∈ c I a
28 25 27 orbi12d ⊢ g = G → a ∈ c Itv ⁡ g b ∨ b ∈ c Itv ⁡ g a ↔ a ∈ c I b ∨ b ∈ c I a
29 28 3anbi3d ⊢ g = G → a ≠ c ∧ b ≠ c ∧ a ∈ c Itv ⁡ g b ∨ b ∈ c Itv ⁡ g a ↔ a ≠ c ∧ b ≠ c ∧ a ∈ c I b ∨ b ∈ c I a
30 21 29 anbi12d ⊢ g = G → a ∈ Base g ∧ b ∈ Base g ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c Itv ⁡ g b ∨ b ∈ c Itv ⁡ g a ↔ a ∈ P ∧ b ∈ P ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c I b ∨ b ∈ c I a
31 30 opabbidv ⊢ g = G → a b | a ∈ Base g ∧ b ∈ Base g ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c Itv ⁡ g b ∨ b ∈ c Itv ⁡ g a = a b | a ∈ P ∧ b ∈ P ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c I b ∨ b ∈ c I a
32 18 31 mpteq12dv ⊢ g = G → c ∈ Base g ⟼ a b | a ∈ Base g ∧ b ∈ Base g ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c Itv ⁡ g b ∨ b ∈ c Itv ⁡ g a = c ∈ P ⟼ a b | a ∈ P ∧ b ∈ P ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c I b ∨ b ∈ c I a
33 df-hlg ⊢ hl 𝒢 = g ∈ V ⟼ c ∈ Base g ⟼ a b | a ∈ Base g ∧ b ∈ Base g ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c Itv ⁡ g b ∨ b ∈ c Itv ⁡ g a
34 32 33 1 mptfvmpt ⊢ G ∈ V → hl 𝒢 ⁡ G = c ∈ P ⟼ a b | a ∈ P ∧ b ∈ P ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c I b ∨ b ∈ c I a
35 4 16 34 3syl ⊢ φ → hl 𝒢 ⁡ G = c ∈ P ⟼ a b | a ∈ P ∧ b ∈ P ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c I b ∨ b ∈ c I a
36 3 35 eqtrid ⊢ φ → K = c ∈ P ⟼ a b | a ∈ P ∧ b ∈ P ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c I b ∨ b ∈ c I a
37 1 fvexi ⊢ P ∈ V
38 37 37 xpex ⊢ P × P ∈ V
39 opabssxp ⊢ a b | a ∈ P ∧ b ∈ P ∧ a ≠ C ∧ b ≠ C ∧ a ∈ C I b ∨ b ∈ C I a ⊆ P × P
40 38 39 ssexi ⊢ a b | a ∈ P ∧ b ∈ P ∧ a ≠ C ∧ b ≠ C ∧ a ∈ C I b ∨ b ∈ C I a ∈ V
41 40 a1i ⊢ φ → a b | a ∈ P ∧ b ∈ P ∧ a ≠ C ∧ b ≠ C ∧ a ∈ C I b ∨ b ∈ C I a ∈ V
42 15 36 5 41 fvmptd4 ⊢ φ → K ⁡ C = a b | a ∈ P ∧ b ∈ P ∧ a ≠ C ∧ b ≠ C ∧ a ∈ C I b ∨ b ∈ C I a
43 42 breqd ⊢ φ → A K ⁡ C B ↔ A a b | a ∈ P ∧ b ∈ P ∧ a ≠ C ∧ b ≠ C ∧ a ∈ C I b ∨ b ∈ C I a B
44 simpl ⊢ a = A ∧ b = B → a = A
45 44 neeq1d ⊢ a = A ∧ b = B → a ≠ C ↔ A ≠ C
46 simpr ⊢ a = A ∧ b = B → b = B
47 46 neeq1d ⊢ a = A ∧ b = B → b ≠ C ↔ B ≠ C
48 46 oveq2d ⊢ a = A ∧ b = B → C I b = C I B
49 44 48 eleq12d ⊢ a = A ∧ b = B → a ∈ C I b ↔ A ∈ C I B
50 44 oveq2d ⊢ a = A ∧ b = B → C I a = C I A
51 46 50 eleq12d ⊢ a = A ∧ b = B → b ∈ C I a ↔ B ∈ C I A
52 49 51 orbi12d ⊢ a = A ∧ b = B → a ∈ C I b ∨ b ∈ C I a ↔ A ∈ C I B ∨ B ∈ C I A
53 45 47 52 3anbi123d ⊢ a = A ∧ b = B → a ≠ C ∧ b ≠ C ∧ a ∈ C I b ∨ b ∈ C I a ↔ A ≠ C ∧ B ≠ C ∧ A ∈ C I B ∨ B ∈ C I A
54 eqid ⊢ a b | a ∈ P ∧ b ∈ P ∧ a ≠ C ∧ b ≠ C ∧ a ∈ C I b ∨ b ∈ C I a = a b | a ∈ P ∧ b ∈ P ∧ a ≠ C ∧ b ≠ C ∧ a ∈ C I b ∨ b ∈ C I a
55 53 54 brab2a ⊢ A a b | a ∈ P ∧ b ∈ P ∧ a ≠ C ∧ b ≠ C ∧ a ∈ C I b ∨ b ∈ C I a B ↔ A ∈ P ∧ B ∈ P ∧ A ≠ C ∧ B ≠ C ∧ A ∈ C I B ∨ B ∈ C I A
56 43 55 bitrdi ⊢ φ → A K ⁡ C B ↔ A ∈ P ∧ B ∈ P ∧ A ≠ C ∧ B ≠ C ∧ A ∈ C I B ∨ B ∈ C I A