Theorem ishlg 28610

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 3000	. . . . 5 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑎 ≠ 𝐶 ↔ 𝐴 ≠ 𝐶))
3		simpr 484	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵)
4	3	neeq1d 3000	. . . . 5 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑏 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
5	3	oveq2d 7447	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝐶𝐼𝑏) = (𝐶𝐼𝐵))
6	1, 5	eleq12d 2835	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑎 ∈ (𝐶𝐼𝑏) ↔ 𝐴 ∈ (𝐶𝐼𝐵)))
7	1	oveq2d 7447	. . . . . . 7 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝐶𝐼𝑎) = (𝐶𝐼𝐴))
8	3, 7	eleq12d 2835	. . . . . 6 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝑏 ∈ (𝐶𝐼𝑎) ↔ 𝐵 ∈ (𝐶𝐼𝐴)))
9	6, 8	orbi12d 919	. . . . 5 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ((𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎)) ↔ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴))))
10	2, 4, 9	3anbi123d 1438	. . . 4 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ((𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))) ↔ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴)))))
11		eqid 2737	. . . 4 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))}
12	10, 11	brab2a 5779	. . 3 ⊢ (𝐴{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))}𝐵 ↔ ((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴)))))
13	12	a1i 11	. 2 ⊢ (𝜑 → (𝐴{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))}𝐵 ↔ ((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴))))))
14		ishlg.k	. . . . 5 ⊢ 𝐾 = (hlG‘𝐺)
15		ishlg.g	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ 𝑉)
16		elex 3501	. . . . . 6 ⊢ (𝐺 ∈ 𝑉 → 𝐺 ∈ V)
17		fveq2 6906	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺))
18		ishlg.p	. . . . . . . . 9 ⊢ 𝑃 = (Base‘𝐺)
19	17, 18	eqtr4di 2795	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝑃)
20	19	eleq2d 2827	. . . . . . . . . . 11 ⊢ (𝑔 = 𝐺 → (𝑎 ∈ (Base‘𝑔) ↔ 𝑎 ∈ 𝑃))
21	19	eleq2d 2827	. . . . . . . . . . 11 ⊢ (𝑔 = 𝐺 → (𝑏 ∈ (Base‘𝑔) ↔ 𝑏 ∈ 𝑃))
22	20, 21	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → ((𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔)) ↔ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)))
23		fveq2 6906	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝐺 → (Itv‘𝑔) = (Itv‘𝐺))
24		ishlg.i	. . . . . . . . . . . . . . 15 ⊢ 𝐼 = (Itv‘𝐺)
25	23, 24	eqtr4di 2795	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝐺 → (Itv‘𝑔) = 𝐼)
26	25	oveqd 7448	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝐺 → (𝑐(Itv‘𝑔)𝑏) = (𝑐𝐼𝑏))
27	26	eleq2d 2827	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝐺 → (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ↔ 𝑎 ∈ (𝑐𝐼𝑏)))
28	25	oveqd 7448	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝐺 → (𝑐(Itv‘𝑔)𝑎) = (𝑐𝐼𝑎))
29	28	eleq2d 2827	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝐺 → (𝑏 ∈ (𝑐(Itv‘𝑔)𝑎) ↔ 𝑏 ∈ (𝑐𝐼𝑎)))
30	27, 29	orbi12d 919	. . . . . . . . . . 11 ⊢ (𝑔 = 𝐺 → ((𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎)) ↔ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))
31	30	3anbi3d 1444	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → ((𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎))) ↔ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎)))))
32	22, 31	anbi12d 632	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (((𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔)) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎)))) ↔ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))))
33	32	opabbidv 5209	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔)) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎))))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))})
34	19, 33	mpteq12dv 5233	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (𝑐 ∈ (Base‘𝑔) ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔)) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎))))}) = (𝑐 ∈ 𝑃 ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))}))
35		df-hlg 28609	. . . . . . 7 ⊢ hlG = (𝑔 ∈ V ↦ (𝑐 ∈ (Base‘𝑔) ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔)) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎))))}))
36	34, 35, 18	mptfvmpt 7248	. . . . . 6 ⊢ (𝐺 ∈ V → (hlG‘𝐺) = (𝑐 ∈ 𝑃 ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))}))
37	15, 16, 36	3syl 18	. . . . 5 ⊢ (𝜑 → (hlG‘𝐺) = (𝑐 ∈ 𝑃 ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))}))
38	14, 37	eqtrid 2789	. . . 4 ⊢ (𝜑 → 𝐾 = (𝑐 ∈ 𝑃 ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))}))
39		neeq2 3004	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (𝑎 ≠ 𝑐 ↔ 𝑎 ≠ 𝐶))
40		neeq2 3004	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (𝑏 ≠ 𝑐 ↔ 𝑏 ≠ 𝐶))
41		oveq1 7438	. . . . . . . . . 10 ⊢ (𝑐 = 𝐶 → (𝑐𝐼𝑏) = (𝐶𝐼𝑏))
42	41	eleq2d 2827	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → (𝑎 ∈ (𝑐𝐼𝑏) ↔ 𝑎 ∈ (𝐶𝐼𝑏)))
43		oveq1 7438	. . . . . . . . . 10 ⊢ (𝑐 = 𝐶 → (𝑐𝐼𝑎) = (𝐶𝐼𝑎))
44	43	eleq2d 2827	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → (𝑏 ∈ (𝑐𝐼𝑎) ↔ 𝑏 ∈ (𝐶𝐼𝑎)))
45	42, 44	orbi12d 919	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → ((𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎)) ↔ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))
46	39, 40, 45	3anbi123d 1438	. . . . . . 7 ⊢ (𝑐 = 𝐶 → ((𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))) ↔ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎)))))
47	46	anbi2d 630	. . . . . 6 ⊢ (𝑐 = 𝐶 → (((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎)))) ↔ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))))
48	47	opabbidv 5209	. . . . 5 ⊢ (𝑐 = 𝐶 → {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))})
49	48	adantl 481	. . . 4 ⊢ ((𝜑 ∧ 𝑐 = 𝐶) → {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))})
50		ishlg.c	. . . 4 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
51	18	fvexi 6920	. . . . . . 7 ⊢ 𝑃 ∈ V
52	51, 51	xpex 7773	. . . . . 6 ⊢ (𝑃 × 𝑃) ∈ V
53		opabssxp 5778	. . . . . 6 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))} ⊆ (𝑃 × 𝑃)
54	52, 53	ssexi 5322	. . . . 5 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))} ∈ V
55	54	a1i 11	. . . 4 ⊢ (𝜑 → {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))} ∈ V)
56	38, 49, 50, 55	fvmptd 7023	. . 3 ⊢ (𝜑 → (𝐾‘𝐶) = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) ∧ (𝑎 ≠ 𝐶 ∧ 𝑏 ≠ 𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))})
57	56	breqd 5154	. 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 1540   ∈ wcel 2108   ≠ wne 2940  Vcvv 3480   class class class wbr 5143  {copab 5205   ↦ cmpt 5225   × cxp 5683  ‘cfv 6561  (class class class)co 7431  Basecbs 17247  Itvcitv 28441  hlGchlg 28608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-hlg 28609

This theorem is referenced by:  hlcomb  28611  hlne1  28613  hlne2  28614  hlln  28615  hlid  28617  hltr  28618  hlbtwn  28619  btwnhl1  28620  btwnhl2  28621  btwnhl  28622  lnhl  28623  hlcgrex  28624  mirhl  28687  mirbtwnhl  28688  mirhl2  28689  opphllem4  28758  opphl  28762  hlpasch  28764  lnopp2hpgb  28771  cgracgr  28826  cgraswap  28828  flatcgra  28832  cgrahl  28835  cgracol  28836