Theorem ishlg 28688

Description: Rays : Definition 6.1 of [Schwabhauser] p. 43. With this definition, 𝐴(𝐾‘𝐶)𝐵 means that 𝐴 and 𝐵 are on the same ray with initial point 𝐶. This follows the same notation as Schwabhauser where rays are first defined as a relation. It is possible to recover the ray itself using e.g., ((𝐾‘𝐶) “ {𝐴}). (Contributed by Thierry Arnoux, 21-Dec-2019.)

Hypotheses

Ref	Expression
ishlg.p	⊢ 𝑃 = (Base‘𝐺)
ishlg.i	⊢ 𝐼 = (Itv‘𝐺)
ishlg.k	⊢ 𝐾 = (hlG‘𝐺)
ishlg.a	⊢ (𝜑 → 𝐴 ∈ 𝑃)
ishlg.b	⊢ (𝜑 → 𝐵 ∈ 𝑃)
ishlg.c	⊢ (𝜑 → 𝐶 ∈ 𝑃)
ishlg.g	⊢ (𝜑 → 𝐺 ∈ 𝑉)

Assertion

Ref	Expression
ishlg	⊢ (𝜑 → (𝐴(𝐾‘𝐶)𝐵 ↔ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴)))))

Proof of Theorem ishlg

Dummy variables 𝑎 𝑏 𝑐 𝑔 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl 482	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → 𝑎 = 𝐴)
2	1	neeq1d 2992	. . . . 5 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑎 ≠ 𝐶 ↔ 𝐴 ≠ 𝐶))
3		simpr 484	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵)
4	3	neeq1d 2992	. . . . 5 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑏 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
5	3	oveq2d 7378	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝐶𝐼𝑏) = (𝐶𝐼𝐵))
6	1, 5	eleq12d 2831	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑎 ∈ (𝐶𝐼𝑏) ↔ 𝐴 ∈ (𝐶𝐼𝐵)))
7	1	oveq2d 7378	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝐶𝐼𝑎) = (𝐶𝐼𝐴))
8	3, 7	eleq12d 2831	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑏 ∈ (𝐶𝐼𝑎) ↔ 𝐵 ∈ (𝐶𝐼𝐴)))
9	6, 8	orbi12d 919	. . . . 5 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ((𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎)) ↔ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴))))
10	2, 4, 9	3anbi123d 1439	. . . 4 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ((𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))) ↔ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴)))))
11		eqid 2737	. . . 4 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))}
12	10, 11	brab2a 5719	. . 3 ⊢ (𝐴{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))}𝐵 ↔ ((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴)))))
13	12	a1i 11	. 2 ⊢ (𝜑 → (𝐴{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))}𝐵 ↔ ((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴))))))
14		ishlg.k	. . . . 5 ⊢ 𝐾 = (hlG‘𝐺)
15		ishlg.g	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ 𝑉)
16		elex 3451	. . . . . 6 ⊢ (𝐺 ∈ 𝑉 → 𝐺 ∈ V)
17		fveq2 6836	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺))
18		ishlg.p	. . . . . . . . 9 ⊢ 𝑃 = (Base‘𝐺)
19	17, 18	eqtr4di 2790	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝑃)
20	19	eleq2d 2823	. . . . . . . . . . 11 ⊢ (𝑔 = 𝐺 → (𝑎 ∈ (Base‘𝑔) ↔ 𝑎 ∈ 𝑃))
21	19	eleq2d 2823	. . . . . . . . . . 11 ⊢ (𝑔 = 𝐺 → (𝑏 ∈ (Base‘𝑔) ↔ 𝑏 ∈ 𝑃))
22	20, 21	anbi12d 633	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → ((𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔)) ↔ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)))
23		fveq2 6836	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝐺 → (Itv‘𝑔) = (Itv‘𝐺))
24		ishlg.i	. . . . . . . . . . . . . . 15 ⊢ 𝐼 = (Itv‘𝐺)
25	23, 24	eqtr4di 2790	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝐺 → (Itv‘𝑔) = 𝐼)
26	25	oveqd 7379	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝐺 → (𝑐(Itv‘𝑔)𝑏) = (𝑐𝐼𝑏))
27	26	eleq2d 2823	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝐺 → (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ↔ 𝑎 ∈ (𝑐𝐼𝑏)))
28	25	oveqd 7379	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝐺 → (𝑐(Itv‘𝑔)𝑎) = (𝑐𝐼𝑎))
29	28	eleq2d 2823	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝐺 → (𝑏 ∈ (𝑐(Itv‘𝑔)𝑎) ↔ 𝑏 ∈ (𝑐𝐼𝑎)))
30	27, 29	orbi12d 919	. . . . . . . . . . 11 ⊢ (𝑔 = 𝐺 → ((𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎)) ↔ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))
31	30	3anbi3d 1445	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → ((𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎))) ↔ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎)))))
32	22, 31	anbi12d 633	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (((𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔)) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎)))) ↔ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))))
33	32	opabbidv 5152	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔)) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎))))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))})
34	19, 33	mpteq12dv 5173	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (𝑐 ∈ (Base‘𝑔) ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔)) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎))))}) = (𝑐 ∈ 𝑃 ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))}))
35		df-hlg 28687	. . . . . . 7 ⊢ hlG = (𝑔 ∈ V ↦ (𝑐 ∈ (Base‘𝑔) ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔)) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎))))}))
36	34, 35, 18	mptfvmpt 7178	. . . . . 6 ⊢ (𝐺 ∈ V → (hlG‘𝐺) = (𝑐 ∈ 𝑃 ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))}))
37	15, 16, 36	3syl 18	. . . . 5 ⊢ (𝜑 → (hlG‘𝐺) = (𝑐 ∈ 𝑃 ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))}))
38	14, 37	eqtrid 2784	. . . 4 ⊢ (𝜑 → 𝐾 = (𝑐 ∈ 𝑃 ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))}))
39		neeq2 2996	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (𝑎 ≠ 𝑐 ↔ 𝑎 ≠ 𝐶))
40		neeq2 2996	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (𝑏 ≠ 𝑐 ↔ 𝑏 ≠ 𝐶))
41		oveq1 7369	. . . . . . . . . 10 ⊢ (𝑐 = 𝐶 → (𝑐𝐼𝑏) = (𝐶𝐼𝑏))
42	41	eleq2d 2823	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → (𝑎 ∈ (𝑐𝐼𝑏) ↔ 𝑎 ∈ (𝐶𝐼𝑏)))
43		oveq1 7369	. . . . . . . . . 10 ⊢ (𝑐 = 𝐶 → (𝑐𝐼𝑎) = (𝐶𝐼𝑎))
44	43	eleq2d 2823	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → (𝑏 ∈ (𝑐𝐼𝑎) ↔ 𝑏 ∈ (𝐶𝐼𝑎)))
45	42, 44	orbi12d 919	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → ((𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎)) ↔ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))
46	39, 40, 45	3anbi123d 1439	. . . . . . 7 ⊢ (𝑐 = 𝐶 → ((𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))) ↔ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎)))))
47	46	anbi2d 631	. . . . . 6 ⊢ (𝑐 = 𝐶 → (((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎)))) ↔ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))))
48	47	opabbidv 5152	. . . . 5 ⊢ (𝑐 = 𝐶 → {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))})
49	48	adantl 481	. . . 4 ⊢ ((𝜑 ∧ 𝑐 = 𝐶) → {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))})
50		ishlg.c	. . . 4 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
51	18	fvexi 6850	. . . . . . 7 ⊢ 𝑃 ∈ V
52	51, 51	xpex 7702	. . . . . 6 ⊢ (𝑃 × 𝑃) ∈ V
53		opabssxp 5718	. . . . . 6 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))} ⊆ (𝑃 × 𝑃)
54	52, 53	ssexi 5260	. . . . 5 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))} ∈ V
55	54	a1i 11	. . . 4 ⊢ (𝜑 → {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))} ∈ V)
56	38, 49, 50, 55	fvmptd 6951	. . 3 ⊢ (𝜑 → (𝐾‘𝐶) = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))})
57	56	breqd 5097	. 2 ⊢ (𝜑 → (𝐴(𝐾‘𝐶)𝐵 ↔ 𝐴{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))}𝐵))
58		ishlg.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
59		ishlg.b	. . . 4 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
60	58, 59	jca 511	. . 3 ⊢ (𝜑 → (𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃))
61	60	biantrurd 532	. 2 ⊢ (𝜑 → ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴))) ↔ ((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴))))))
62	13, 57, 61	3bitr4d 311	1 ⊢ (𝜑 → (𝐴(𝐾‘𝐶)𝐵 ↔ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴)))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  Vcvv 3430   class class class wbr 5086  {copab 5148   ↦ cmpt 5167   × cxp 5624  ‘cfv 6494  (class class class)co 7362  Basecbs 17174  Itvcitv 28519  hlGchlg 28686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5304  ax-pr 5372  ax-un 7684

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5521  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-rn 5637  df-res 5638  df-ima 5639  df-iota 6450  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-ov 7365  df-hlg 28687

This theorem is referenced by:  hlcomb  28689  hlne1  28691  hlne2  28692  hlln  28693  hlid  28695  hltr  28696  hlbtwn  28697  btwnhl1  28698  btwnhl2  28699  btwnhl  28700  lnhl  28701  hlcgrex  28702  mirhl  28765  mirbtwnhl  28766  mirhl2  28767  opphllem4  28836  opphl  28840  hlpasch  28842  lnopp2hpgb  28849  cgracgr  28904  cgraswap  28906  flatcgra  28910  cgrahl  28913  cgracol  28914