ishpg - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ishpg		Structured version Visualization version GIF version

Theorem ishpg 25651

Description: Value of the half-plane relation for a given line 𝐷. (Contributed by Thierry Arnoux, 4-Mar-2020.)

**Hypotheses**
Ref	Expression
ishpg.p	⊢ 𝑃 = (Base‘𝐺)
ishpg.i	⊢ 𝐼 = (Itv‘𝐺)
ishpg.l	⊢ 𝐿 = (LineG‘𝐺)
ishpg.o	⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))}
ishpg.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
ishpg.d	⊢ (𝜑 → 𝐷 ∈ ran 𝐿)

**Assertion**
Ref	Expression
ishpg	⊢ (𝜑 → ((hpG‘𝐺)‘𝐷) = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (𝑎𝑂𝑐 ∧ 𝑏𝑂𝑐)})

Distinct variable groups: 𝐷,𝑎,𝑏,𝑐,𝑡 𝐺,𝑎,𝑏 𝐼,𝑎,𝑏,𝑐,𝑡 𝑃,𝑎,𝑏,𝑐,𝑡 Allowed substitution hints: 𝜑(𝑡,𝑎,𝑏,𝑐) 𝐺(𝑡,𝑐) 𝐿(𝑡,𝑎,𝑏,𝑐) 𝑂(𝑡,𝑎,𝑏,𝑐)

Proof of Theorem ishpg Dummy variables 𝑑 𝑒 𝑓 𝑔 𝑖 𝑝 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ishpg.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
2		elex 3212	. . . 4 ⊢ (𝐺 ∈ TarskiG → 𝐺 ∈ V)
3		fveq2 6191	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → (LineG‘𝑔) = (LineG‘𝐺))
4		ishpg.l	. . . . . . . 8 ⊢ 𝐿 = (LineG‘𝐺)
5	3, 4	syl6eqr 2674	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (LineG‘𝑔) = 𝐿)
6	5	rneqd 5353	. . . . . 6 ⊢ (𝑔 = 𝐺 → ran (LineG‘𝑔) = ran 𝐿)
7		ishpg.p	. . . . . . . 8 ⊢ 𝑃 = (Base‘𝐺)
8		ishpg.i	. . . . . . . 8 ⊢ 𝐼 = (Itv‘𝐺)
9		simpl 473	. . . . . . . . . 10 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → 𝑝 = 𝑃)
10	9	eqcomd 2628	. . . . . . . . 9 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → 𝑃 = 𝑝)
11	10	difeq1d 3727	. . . . . . . . . . . . 13 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑃 ∖ 𝑑) = (𝑝 ∖ 𝑑))
12	11	eleq2d 2687	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑎 ∈ (𝑃 ∖ 𝑑) ↔ 𝑎 ∈ (𝑝 ∖ 𝑑)))
13	11	eleq2d 2687	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑐 ∈ (𝑃 ∖ 𝑑) ↔ 𝑐 ∈ (𝑝 ∖ 𝑑)))
14	12, 13	anbi12d 747	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → ((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ↔ (𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑))))
15		simpr 477	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → 𝑖 = 𝐼)
16	15	eqcomd 2628	. . . . . . . . . . . . . 14 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → 𝐼 = 𝑖)
17	16	oveqd 6667	. . . . . . . . . . . . 13 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑎𝐼𝑐) = (𝑎𝑖𝑐))
18	17	eleq2d 2687	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑡 ∈ (𝑎𝐼𝑐) ↔ 𝑡 ∈ (𝑎𝑖𝑐)))
19	18	rexbidv 3052	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐) ↔ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)))
20	14, 19	anbi12d 747	. . . . . . . . . 10 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ↔ ((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐))))
21	11	eleq2d 2687	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑏 ∈ (𝑃 ∖ 𝑑) ↔ 𝑏 ∈ (𝑝 ∖ 𝑑)))
22	21, 13	anbi12d 747	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ↔ (𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑))))
23	16	oveqd 6667	. . . . . . . . . . . . 13 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑏𝐼𝑐) = (𝑏𝑖𝑐))
24	23	eleq2d 2687	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑡 ∈ (𝑏𝐼𝑐) ↔ 𝑡 ∈ (𝑏𝑖𝑐)))
25	24	rexbidv 3052	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐) ↔ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))
26	22, 25	anbi12d 747	. . . . . . . . . 10 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)) ↔ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐))))
27	20, 26	anbi12d 747	. . . . . . . . 9 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → ((((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐))) ↔ (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))))
28	10, 27	rexeqbidv 3153	. . . . . . . 8 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐))) ↔ ∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))))
29	7, 8, 28	sbcie2s 15916	. . . . . . 7 ⊢ (𝑔 = 𝐺 → ([(Base‘𝑔) / 𝑝][(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐))) ↔ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))))
30	29	opabbidv 4716	. . . . . 6 ⊢ (𝑔 = 𝐺 → {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))})
31	6, 30	mpteq12dv 4733	. . . . 5 ⊢ (𝑔 = 𝐺 → (𝑑 ∈ ran (LineG‘𝑔) ↦ {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))}) = (𝑑 ∈ ran 𝐿 ↦ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))}))
32		df-hpg 25650	. . . . 5 ⊢ hpG = (𝑔 ∈ V ↦ (𝑑 ∈ ran (LineG‘𝑔) ↦ {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))}))
33		fvex 6201	. . . . . . . 8 ⊢ (LineG‘𝐺) ∈ V
34	4, 33	eqeltri 2697	. . . . . . 7 ⊢ 𝐿 ∈ V
35	34	rnex 7100	. . . . . 6 ⊢ ran 𝐿 ∈ V
36	35	mptex 6486	. . . . 5 ⊢ (𝑑 ∈ ran 𝐿 ↦ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))}) ∈ V
37	31, 32, 36	fvmpt 6282	. . . 4 ⊢ (𝐺 ∈ V → (hpG‘𝐺) = (𝑑 ∈ ran 𝐿 ↦ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))}))
38	1, 2, 37	3syl 18	. . 3 ⊢ (𝜑 → (hpG‘𝐺) = (𝑑 ∈ ran 𝐿 ↦ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))}))
39		difeq2 3722	. . . . . . . . . 10 ⊢ (𝑑 = 𝐷 → (𝑃 ∖ 𝑑) = (𝑃 ∖ 𝐷))
40	39	eleq2d 2687	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → (𝑎 ∈ (𝑃 ∖ 𝑑) ↔ 𝑎 ∈ (𝑃 ∖ 𝐷)))
41	39	eleq2d 2687	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → (𝑐 ∈ (𝑃 ∖ 𝑑) ↔ 𝑐 ∈ (𝑃 ∖ 𝐷)))
42	40, 41	anbi12d 747	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → ((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ↔ (𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷))))
43		id 22	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → 𝑑 = 𝐷)
44	43	rexeqdv 3145	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → (∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)))
45	42, 44	anbi12d 747	. . . . . . 7 ⊢ (𝑑 = 𝐷 → (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ↔ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐))))
46	39	eleq2d 2687	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → (𝑏 ∈ (𝑃 ∖ 𝑑) ↔ 𝑏 ∈ (𝑃 ∖ 𝐷)))
47	46, 41	anbi12d 747	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ↔ (𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷))))
48	43	rexeqdv 3145	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → (∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))
49	47, 48	anbi12d 747	. . . . . . 7 ⊢ (𝑑 = 𝐷 → (((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)) ↔ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))))
50	45, 49	anbi12d 747	. . . . . 6 ⊢ (𝑑 = 𝐷 → ((((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐))) ↔ (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))))
51	50	rexbidv 3052	. . . . 5 ⊢ (𝑑 = 𝐷 → (∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐))) ↔ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))))
52	51	opabbidv 4716	. . . 4 ⊢ (𝑑 = 𝐷 → {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))})
53	52	adantl 482	. . 3 ⊢ ((𝜑 ∧ 𝑑 = 𝐷) → {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))})
54		ishpg.d	. . 3 ⊢ (𝜑 → 𝐷 ∈ ran 𝐿)
55		df-xp 5120	. . . . . 6 ⊢ (𝑃 × 𝑃) = {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)}
56		fvex 6201	. . . . . . . 8 ⊢ (Base‘𝐺) ∈ V
57	7, 56	eqeltri 2697	. . . . . . 7 ⊢ 𝑃 ∈ V
58	57, 57	xpex 6962	. . . . . 6 ⊢ (𝑃 × 𝑃) ∈ V
59	55, 58	eqeltrri 2698	. . . . 5 ⊢ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)} ∈ V
60		eldifi 3732	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ (𝑃 ∖ 𝐷) → 𝑎 ∈ 𝑃)
61		eldifi 3732	. . . . . . . . . . . 12 ⊢ (𝑏 ∈ (𝑃 ∖ 𝐷) → 𝑏 ∈ 𝑃)
62	60, 61	anim12i 590	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) → (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃))
63	62	adantrr 753	. . . . . . . . . 10 ⊢ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ (𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷))) → (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃))
64	63	adantlr 751	. . . . . . . . 9 ⊢ (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ (𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷))) → (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃))
65	64	adantlr 751	. . . . . . . 8 ⊢ ((((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ (𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷))) → (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃))
66	65	adantrr 753	. . . . . . 7 ⊢ ((((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))) → (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃))
67	66	rexlimivw 3029	. . . . . 6 ⊢ (∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))) → (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃))
68	67	ssopab2i 5003	. . . . 5 ⊢ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))} ⊆ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)}
69	59, 68	ssexi 4803	. . . 4 ⊢ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))} ∈ V
70	69	a1i 11	. . 3 ⊢ (𝜑 → {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))} ∈ V)
71	38, 53, 54, 70	fvmptd 6288	. 2 ⊢ (𝜑 → ((hpG‘𝐺)‘𝐷) = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))})
72		vex 3203	. . . . . . 7 ⊢ 𝑎 ∈ V
73		vex 3203	. . . . . . 7 ⊢ 𝑐 ∈ V
74		eleq1 2689	. . . . . . . . 9 ⊢ (𝑒 = 𝑎 → (𝑒 ∈ (𝑃 ∖ 𝐷) ↔ 𝑎 ∈ (𝑃 ∖ 𝐷)))
75	74	anbi1d 741	. . . . . . . 8 ⊢ (𝑒 = 𝑎 → ((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ↔ (𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷))))
76		oveq1 6657	. . . . . . . . . 10 ⊢ (𝑒 = 𝑎 → (𝑒𝐼𝑓) = (𝑎𝐼𝑓))
77	76	eleq2d 2687	. . . . . . . . 9 ⊢ (𝑒 = 𝑎 → (𝑡 ∈ (𝑒𝐼𝑓) ↔ 𝑡 ∈ (𝑎𝐼𝑓)))
78	77	rexbidv 3052	. . . . . . . 8 ⊢ (𝑒 = 𝑎 → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑓)))
79	75, 78	anbi12d 747	. . . . . . 7 ⊢ (𝑒 = 𝑎 → (((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓)) ↔ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑓))))
80		eleq1 2689	. . . . . . . . 9 ⊢ (𝑓 = 𝑐 → (𝑓 ∈ (𝑃 ∖ 𝐷) ↔ 𝑐 ∈ (𝑃 ∖ 𝐷)))
81	80	anbi2d 740	. . . . . . . 8 ⊢ (𝑓 = 𝑐 → ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ↔ (𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷))))
82		oveq2 6658	. . . . . . . . . 10 ⊢ (𝑓 = 𝑐 → (𝑎𝐼𝑓) = (𝑎𝐼𝑐))
83	82	eleq2d 2687	. . . . . . . . 9 ⊢ (𝑓 = 𝑐 → (𝑡 ∈ (𝑎𝐼𝑓) ↔ 𝑡 ∈ (𝑎𝐼𝑐)))
84	83	rexbidv 3052	. . . . . . . 8 ⊢ (𝑓 = 𝑐 → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑓) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)))
85	81, 84	anbi12d 747	. . . . . . 7 ⊢ (𝑓 = 𝑐 → (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑓)) ↔ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐))))
86		ishpg.o	. . . . . . . 8 ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))}
87		simpl 473	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → 𝑎 = 𝑒)
88	87	eleq1d 2686	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (𝑎 ∈ (𝑃 ∖ 𝐷) ↔ 𝑒 ∈ (𝑃 ∖ 𝐷)))
89		simpr 477	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → 𝑏 = 𝑓)
90	89	eleq1d 2686	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (𝑏 ∈ (𝑃 ∖ 𝐷) ↔ 𝑓 ∈ (𝑃 ∖ 𝐷)))
91	88, 90	anbi12d 747	. . . . . . . . . 10 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ↔ (𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷))))
92		oveq12 6659	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (𝑎𝐼𝑏) = (𝑒𝐼𝑓))
93	92	eleq2d 2687	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (𝑡 ∈ (𝑎𝐼𝑏) ↔ 𝑡 ∈ (𝑒𝐼𝑓)))
94	93	rexbidv 3052	. . . . . . . . . 10 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓)))
95	91, 94	anbi12d 747	. . . . . . . . 9 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏)) ↔ ((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓))))
96	95	cbvopabv 4722	. . . . . . . 8 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} = {⟨𝑒, 𝑓⟩ ∣ ((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓))}
97	86, 96	eqtri 2644	. . . . . . 7 ⊢ 𝑂 = {⟨𝑒, 𝑓⟩ ∣ ((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓))}
98	72, 73, 79, 85, 97	brab 4998	. . . . . 6 ⊢ (𝑎𝑂𝑐 ↔ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)))
99		vex 3203	. . . . . . 7 ⊢ 𝑏 ∈ V
100		eleq1 2689	. . . . . . . . 9 ⊢ (𝑒 = 𝑏 → (𝑒 ∈ (𝑃 ∖ 𝐷) ↔ 𝑏 ∈ (𝑃 ∖ 𝐷)))
101	100	anbi1d 741	. . . . . . . 8 ⊢ (𝑒 = 𝑏 → ((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ↔ (𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷))))
102		oveq1 6657	. . . . . . . . . 10 ⊢ (𝑒 = 𝑏 → (𝑒𝐼𝑓) = (𝑏𝐼𝑓))
103	102	eleq2d 2687	. . . . . . . . 9 ⊢ (𝑒 = 𝑏 → (𝑡 ∈ (𝑒𝐼𝑓) ↔ 𝑡 ∈ (𝑏𝐼𝑓)))
104	103	rexbidv 3052	. . . . . . . 8 ⊢ (𝑒 = 𝑏 → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑓)))
105	101, 104	anbi12d 747	. . . . . . 7 ⊢ (𝑒 = 𝑏 → (((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓)) ↔ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑓))))
106	80	anbi2d 740	. . . . . . . 8 ⊢ (𝑓 = 𝑐 → ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ↔ (𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷))))
107		oveq2 6658	. . . . . . . . . 10 ⊢ (𝑓 = 𝑐 → (𝑏𝐼𝑓) = (𝑏𝐼𝑐))
108	107	eleq2d 2687	. . . . . . . . 9 ⊢ (𝑓 = 𝑐 → (𝑡 ∈ (𝑏𝐼𝑓) ↔ 𝑡 ∈ (𝑏𝐼𝑐)))
109	108	rexbidv 3052	. . . . . . . 8 ⊢ (𝑓 = 𝑐 → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑓) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))
110	106, 109	anbi12d 747	. . . . . . 7 ⊢ (𝑓 = 𝑐 → (((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑓)) ↔ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))))
111	99, 73, 105, 110, 97	brab 4998	. . . . . 6 ⊢ (𝑏𝑂𝑐 ↔ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))
112	98, 111	anbi12i 733	. . . . 5 ⊢ ((𝑎𝑂𝑐 ∧ 𝑏𝑂𝑐) ↔ (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))))
113	112	rexbii 3041	. . . 4 ⊢ (∃𝑐 ∈ 𝑃 (𝑎𝑂𝑐 ∧ 𝑏𝑂𝑐) ↔ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))))
114	113	opabbii 4717	. . 3 ⊢ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (𝑎𝑂𝑐 ∧ 𝑏𝑂𝑐)} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))}
115	114	a1i 11	. 2 ⊢ (𝜑 → {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (𝑎𝑂𝑐 ∧ 𝑏𝑂𝑐)} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))})
116	71, 115	eqtr4d 2659	1 ⊢ (𝜑 → ((hpG‘𝐺)‘𝐷) = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (𝑎𝑂𝑐 ∧ 𝑏𝑂𝑐)})

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ∃wrex 2913 Vcvv 3200 [wsbc 3435 ∖ cdif 3571 class class class wbr 4653 {copab 4712 ↦ cmpt 4729 × cxp 5112 ran crn 5115 ‘cfv 5888 (class class class)co 6650 Basecbs 15857 TarskiGcstrkg 25329 Itvcitv 25335 LineGclng 25336 hpGchpg 25649

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-id 5024 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-ov 6653 df-hpg 25650

This theorem is referenced by: hpgbr 25652

W3C validator