Theorem ishlg2

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

	Ref	Expression
Hypotheses	ishlg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	ishlg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	ishlg.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
	ishlg2.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
	ishlg2.1	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
Assertion	ishlg2	⊢ ( 𝜑 → ( 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ↔ ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ishlg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		ishlg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		ishlg.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
4		ishlg2.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
5		ishlg2.1	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
6		neeq2	⊢ ( 𝑐 = 𝐶 → ( 𝑎 ≠ 𝑐 ↔ 𝑎 ≠ 𝐶 ) )
7		neeq2	⊢ ( 𝑐 = 𝐶 → ( 𝑏 ≠ 𝑐 ↔ 𝑏 ≠ 𝐶 ) )
8		oveq1	⊢ ( 𝑐 = 𝐶 → ( 𝑐 𝐼 𝑏 ) = ( 𝐶 𝐼 𝑏 ) )
9	8	eleq2d	⊢ ( 𝑐 = 𝐶 → ( 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ↔ 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ) )
10		oveq1	⊢ ( 𝑐 = 𝐶 → ( 𝑐 𝐼 𝑎 ) = ( 𝐶 𝐼 𝑎 ) )
11	10	eleq2d	⊢ ( 𝑐 = 𝐶 → ( 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ↔ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) )
12	9 11	orbi12d	⊢ ( 𝑐 = 𝐶 → ( ( 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ) ↔ ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ) )
13	6 7 12	3anbi123d	⊢ ( 𝑐 = 𝐶 → ( ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ) ) ↔ ( 𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ) ) )
14	13	anbi2d	⊢ ( 𝑐 = 𝐶 → ( ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ) ) ) ↔ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ) ) ) )
15	14	opabbidv	⊢ ( 𝑐 = 𝐶 → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ) ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ) ) } )
16		elex	⊢ ( 𝐺 ∈ 𝑉 → 𝐺 ∈ V )
17		fveq2	⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
18	17 1	eqtr4di	⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = 𝑃 )
19	18	eleq2d	⊢ ( 𝑔 = 𝐺 → ( 𝑎 ∈ ( Base ‘ 𝑔 ) ↔ 𝑎 ∈ 𝑃 ) )
20	18	eleq2d	⊢ ( 𝑔 = 𝐺 → ( 𝑏 ∈ ( Base ‘ 𝑔 ) ↔ 𝑏 ∈ 𝑃 ) )
21	19 20	anbi12d	⊢ ( 𝑔 = 𝐺 → ( ( 𝑎 ∈ ( Base ‘ 𝑔 ) ∧ 𝑏 ∈ ( Base ‘ 𝑔 ) ) ↔ ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ) )
22		fveq2	⊢ ( 𝑔 = 𝐺 → ( Itv ‘ 𝑔 ) = ( Itv ‘ 𝐺 ) )
23	22 2	eqtr4di	⊢ ( 𝑔 = 𝐺 → ( Itv ‘ 𝑔 ) = 𝐼 )
24	23	oveqd	⊢ ( 𝑔 = 𝐺 → ( 𝑐 ( Itv ‘ 𝑔 ) 𝑏 ) = ( 𝑐 𝐼 𝑏 ) )
25	24	eleq2d	⊢ ( 𝑔 = 𝐺 → ( 𝑎 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑏 ) ↔ 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ) )
26	23	oveqd	⊢ ( 𝑔 = 𝐺 → ( 𝑐 ( Itv ‘ 𝑔 ) 𝑎 ) = ( 𝑐 𝐼 𝑎 ) )
27	26	eleq2d	⊢ ( 𝑔 = 𝐺 → ( 𝑏 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑎 ) ↔ 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ) )
28	25 27	orbi12d	⊢ ( 𝑔 = 𝐺 → ( ( 𝑎 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑎 ) ) ↔ ( 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ) ) )
29	28	3anbi3d	⊢ ( 𝑔 = 𝐺 → ( ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) ↔ ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ) ) ) )
30	21 29	anbi12d	⊢ ( 𝑔 = 𝐺 → ( ( ( 𝑎 ∈ ( Base ‘ 𝑔 ) ∧ 𝑏 ∈ ( Base ‘ 𝑔 ) ) ∧ ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) ) ↔ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ) ) ) ) )
31	30	opabbidv	⊢ ( 𝑔 = 𝐺 → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( Base ‘ 𝑔 ) ∧ 𝑏 ∈ ( Base ‘ 𝑔 ) ) ∧ ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ) ) ) } )
32	18 31	mpteq12dv	⊢ ( 𝑔 = 𝐺 → ( 𝑐 ∈ ( Base ‘ 𝑔 ) ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( Base ‘ 𝑔 ) ∧ 𝑏 ∈ ( Base ‘ 𝑔 ) ) ∧ ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) ) } ) = ( 𝑐 ∈ 𝑃 ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ) ) ) } ) )
33		df-hlg	⊢ hlG = ( 𝑔 ∈ V ↦ ( 𝑐 ∈ ( Base ‘ 𝑔 ) ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( Base ‘ 𝑔 ) ∧ 𝑏 ∈ ( Base ‘ 𝑔 ) ) ∧ ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) ) } ) )
34	32 33 1	mptfvmpt	⊢ ( 𝐺 ∈ V → ( hlG ‘ 𝐺 ) = ( 𝑐 ∈ 𝑃 ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ) ) ) } ) )
35	4 16 34	3syl	⊢ ( 𝜑 → ( hlG ‘ 𝐺 ) = ( 𝑐 ∈ 𝑃 ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ) ) ) } ) )
36	3 35	eqtrid	⊢ ( 𝜑 → 𝐾 = ( 𝑐 ∈ 𝑃 ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ ( 𝑎 ∈ ( 𝑐 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝑐 𝐼 𝑎 ) ) ) ) } ) )
37	1	fvexi	⊢ 𝑃 ∈ V
38	37 37	xpex	⊢ ( 𝑃 × 𝑃 ) ∈ V
39		opabssxp	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ) ) } ⊆ ( 𝑃 × 𝑃 )
40	38 39	ssexi	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ) ) } ∈ V
41	40	a1i	⊢ ( 𝜑 → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ) ) } ∈ V )
42	15 36 5 41	fvmptd4	⊢ ( 𝜑 → ( 𝐾 ‘ 𝐶 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ) ) } )
43	42	breqd	⊢ ( 𝜑 → ( 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ↔ 𝐴 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ) ) } 𝐵 ) )
44		simpl	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → 𝑎 = 𝐴 )
45	44	neeq1d	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝑎 ≠ 𝐶 ↔ 𝐴 ≠ 𝐶 ) )
46		simpr	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → 𝑏 = 𝐵 )
47	46	neeq1d	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝑏 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶 ) )
48	46	oveq2d	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝐶 𝐼 𝑏 ) = ( 𝐶 𝐼 𝐵 ) )
49	44 48	eleq12d	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ↔ 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ) )
50	44	oveq2d	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝐶 𝐼 𝑎 ) = ( 𝐶 𝐼 𝐴 ) )
51	46 50	eleq12d	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ↔ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) )
52	49 51	orbi12d	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ↔ ( 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) ) )
53	45 47 52	3anbi123d	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ( 𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ) ↔ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) ) ) )
54		eqid	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ) ) }
55	53 54	brab2a	⊢ ( 𝐴 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ ( 𝑎 ∈ ( 𝐶 𝐼 𝑏 ) ∨ 𝑏 ∈ ( 𝐶 𝐼 𝑎 ) ) ) ) } 𝐵 ↔ ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) ) ) )
56	43 55	bitrdi	⊢ ( 𝜑 → ( 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ↔ ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) ) ) ) ) )