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 28743

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 3485	. . . 4 ⊢ (𝐺 ∈ TarskiG → 𝐺 ∈ V)
3		fveq2 6881	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → (LineG‘𝑔) = (LineG‘𝐺))
4		ishpg.l	. . . . . . . 8 ⊢ 𝐿 = (LineG‘𝐺)
5	3, 4	eqtr4di 2789	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (LineG‘𝑔) = 𝐿)
6	5	rneqd 5923	. . . . . 6 ⊢ (𝑔 = 𝐺 → ran (LineG‘𝑔) = ran 𝐿)
7		ishpg.p	. . . . . . . 8 ⊢ 𝑃 = (Base‘𝐺)
8		ishpg.i	. . . . . . . 8 ⊢ 𝐼 = (Itv‘𝐺)
9		simpl 482	. . . . . . . . 9 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → 𝑝 = 𝑃)
10	9	difeq1d 4105	. . . . . . . . . . . . 13 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑝 ∖ 𝑑) = (𝑃 ∖ 𝑑))
11	10	eleq2d 2821	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑎 ∈ (𝑝 ∖ 𝑑) ↔ 𝑎 ∈ (𝑃 ∖ 𝑑)))
12	10	eleq2d 2821	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑐 ∈ (𝑝 ∖ 𝑑) ↔ 𝑐 ∈ (𝑃 ∖ 𝑑)))
13	11, 12	anbi12d 632	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → ((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ↔ (𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑))))
14		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → 𝑖 = 𝐼)
15	14	oveqd 7427	. . . . . . . . . . . . 13 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑎𝑖𝑐) = (𝑎𝐼𝑐))
16	15	eleq2d 2821	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑡 ∈ (𝑎𝑖𝑐) ↔ 𝑡 ∈ (𝑎𝐼𝑐)))
17	16	rexbidv 3165	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐) ↔ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)))
18	13, 17	anbi12d 632	. . . . . . . . . 10 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ↔ ((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐))))
19	10	eleq2d 2821	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑏 ∈ (𝑝 ∖ 𝑑) ↔ 𝑏 ∈ (𝑃 ∖ 𝑑)))
20	19, 12	anbi12d 632	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ↔ (𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑))))
21	14	oveqd 7427	. . . . . . . . . . . . 13 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑏𝑖𝑐) = (𝑏𝐼𝑐))
22	21	eleq2d 2821	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑡 ∈ (𝑏𝑖𝑐) ↔ 𝑡 ∈ (𝑏𝐼𝑐)))
23	22	rexbidv 3165	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐) ↔ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))
24	20, 23	anbi12d 632	. . . . . . . . . 10 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)) ↔ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐))))
25	18, 24	anbi12d 632	. . . . . . . . 9 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → ((((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐))) ↔ (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))))
26	9, 25	rexeqbidv 3330	. . . . . . . 8 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐))) ↔ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))))
27	7, 8, 26	sbcie2s 17185	. . . . . . 7 ⊢ (𝑔 = 𝐺 → ([(Base‘𝑔) / 𝑝][(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐))) ↔ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))))
28	27	opabbidv 5190	. . . . . 6 ⊢ (𝑔 = 𝐺 → {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))})
29	6, 28	mpteq12dv 5212	. . . . 5 ⊢ (𝑔 = 𝐺 → (𝑑 ∈ ran (LineG‘𝑔) ↦ {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))}) = (𝑑 ∈ ran 𝐿 ↦ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))}))
30		df-hpg 28742	. . . . 5 ⊢ hpG = (𝑔 ∈ V ↦ (𝑑 ∈ ran (LineG‘𝑔) ↦ {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))}))
31	4	fvexi 6895	. . . . . . 7 ⊢ 𝐿 ∈ V
32	31	rnex 7911	. . . . . 6 ⊢ ran 𝐿 ∈ V
33	32	mptex 7220	. . . . 5 ⊢ (𝑑 ∈ ran 𝐿 ↦ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))}) ∈ V
34	29, 30, 33	fvmpt 6991	. . . 4 ⊢ (𝐺 ∈ V → (hpG‘𝐺) = (𝑑 ∈ ran 𝐿 ↦ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))}))
35	1, 2, 34	3syl 18	. . 3 ⊢ (𝜑 → (hpG‘𝐺) = (𝑑 ∈ ran 𝐿 ↦ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))}))
36		difeq2 4100	. . . . . . . . . 10 ⊢ (𝑑 = 𝐷 → (𝑃 ∖ 𝑑) = (𝑃 ∖ 𝐷))
37	36	eleq2d 2821	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → (𝑎 ∈ (𝑃 ∖ 𝑑) ↔ 𝑎 ∈ (𝑃 ∖ 𝐷)))
38	36	eleq2d 2821	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → (𝑐 ∈ (𝑃 ∖ 𝑑) ↔ 𝑐 ∈ (𝑃 ∖ 𝐷)))
39	37, 38	anbi12d 632	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → ((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ↔ (𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷))))
40		rexeq 3305	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → (∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)))
41	39, 40	anbi12d 632	. . . . . . 7 ⊢ (𝑑 = 𝐷 → (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ↔ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐))))
42	36	eleq2d 2821	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → (𝑏 ∈ (𝑃 ∖ 𝑑) ↔ 𝑏 ∈ (𝑃 ∖ 𝐷)))
43	42, 38	anbi12d 632	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ↔ (𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷))))
44		rexeq 3305	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → (∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))
45	43, 44	anbi12d 632	. . . . . . 7 ⊢ (𝑑 = 𝐷 → (((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)) ↔ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))))
46	41, 45	anbi12d 632	. . . . . 6 ⊢ (𝑑 = 𝐷 → ((((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐))) ↔ (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))))
47	46	rexbidv 3165	. . . . 5 ⊢ (𝑑 = 𝐷 → (∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐))) ↔ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))))
48	47	opabbidv 5190	. . . 4 ⊢ (𝑑 = 𝐷 → {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))})
49	48	adantl 481	. . 3 ⊢ ((𝜑 ∧ 𝑑 = 𝐷) → {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))})
50		ishpg.d	. . 3 ⊢ (𝜑 → 𝐷 ∈ ran 𝐿)
51		df-xp 5665	. . . . . 6 ⊢ (𝑃 × 𝑃) = {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)}
52	7	fvexi 6895	. . . . . . 7 ⊢ 𝑃 ∈ V
53	52, 52	xpex 7752	. . . . . 6 ⊢ (𝑃 × 𝑃) ∈ V
54	51, 53	eqeltrri 2832	. . . . 5 ⊢ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)} ∈ V
55		eldifi 4111	. . . . . . . . . 10 ⊢ (𝑎 ∈ (𝑃 ∖ 𝐷) → 𝑎 ∈ 𝑃)
56		eldifi 4111	. . . . . . . . . 10 ⊢ (𝑏 ∈ (𝑃 ∖ 𝐷) → 𝑏 ∈ 𝑃)
57	55, 56	anim12i 613	. . . . . . . . 9 ⊢ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) → (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃))
58	57	ad2ant2r 747	. . . . . . . 8 ⊢ (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ (𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷))) → (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃))
59	58	ad2ant2r 747	. . . . . . 7 ⊢ ((((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))) → (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃))
60	59	rexlimivw 3138	. . . . . 6 ⊢ (∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))) → (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃))
61	60	ssopab2i 5530	. . . . 5 ⊢ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))} ⊆ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)}
62	54, 61	ssexi 5297	. . . 4 ⊢ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))} ∈ V
63	62	a1i 11	. . 3 ⊢ (𝜑 → {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))} ∈ V)
64	35, 49, 50, 63	fvmptd 6998	. 2 ⊢ (𝜑 → ((hpG‘𝐺)‘𝐷) = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))})
65		vex 3468	. . . . . 6 ⊢ 𝑎 ∈ V
66		vex 3468	. . . . . 6 ⊢ 𝑐 ∈ V
67		eleq1w 2818	. . . . . . . 8 ⊢ (𝑒 = 𝑎 → (𝑒 ∈ (𝑃 ∖ 𝐷) ↔ 𝑎 ∈ (𝑃 ∖ 𝐷)))
68	67	anbi1d 631	. . . . . . 7 ⊢ (𝑒 = 𝑎 → ((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ↔ (𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷))))
69		oveq1 7417	. . . . . . . . 9 ⊢ (𝑒 = 𝑎 → (𝑒𝐼𝑓) = (𝑎𝐼𝑓))
70	69	eleq2d 2821	. . . . . . . 8 ⊢ (𝑒 = 𝑎 → (𝑡 ∈ (𝑒𝐼𝑓) ↔ 𝑡 ∈ (𝑎𝐼𝑓)))
71	70	rexbidv 3165	. . . . . . 7 ⊢ (𝑒 = 𝑎 → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑓)))
72	68, 71	anbi12d 632	. . . . . 6 ⊢ (𝑒 = 𝑎 → (((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓)) ↔ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑓))))
73		eleq1w 2818	. . . . . . . 8 ⊢ (𝑓 = 𝑐 → (𝑓 ∈ (𝑃 ∖ 𝐷) ↔ 𝑐 ∈ (𝑃 ∖ 𝐷)))
74	73	anbi2d 630	. . . . . . 7 ⊢ (𝑓 = 𝑐 → ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ↔ (𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷))))
75		oveq2 7418	. . . . . . . . 9 ⊢ (𝑓 = 𝑐 → (𝑎𝐼𝑓) = (𝑎𝐼𝑐))
76	75	eleq2d 2821	. . . . . . . 8 ⊢ (𝑓 = 𝑐 → (𝑡 ∈ (𝑎𝐼𝑓) ↔ 𝑡 ∈ (𝑎𝐼𝑐)))
77	76	rexbidv 3165	. . . . . . 7 ⊢ (𝑓 = 𝑐 → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑓) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)))
78	74, 77	anbi12d 632	. . . . . 6 ⊢ (𝑓 = 𝑐 → (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑓)) ↔ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐))))
79		ishpg.o	. . . . . . 7 ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))}
80		simpl 482	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → 𝑎 = 𝑒)
81	80	eleq1d 2820	. . . . . . . . . 10 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (𝑎 ∈ (𝑃 ∖ 𝐷) ↔ 𝑒 ∈ (𝑃 ∖ 𝐷)))
82		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → 𝑏 = 𝑓)
83	82	eleq1d 2820	. . . . . . . . . 10 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (𝑏 ∈ (𝑃 ∖ 𝐷) ↔ 𝑓 ∈ (𝑃 ∖ 𝐷)))
84	81, 83	anbi12d 632	. . . . . . . . 9 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ↔ (𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷))))
85		oveq12 7419	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (𝑎𝐼𝑏) = (𝑒𝐼𝑓))
86	85	eleq2d 2821	. . . . . . . . . 10 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (𝑡 ∈ (𝑎𝐼𝑏) ↔ 𝑡 ∈ (𝑒𝐼𝑓)))
87	86	rexbidv 3165	. . . . . . . . 9 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓)))
88	84, 87	anbi12d 632	. . . . . . . 8 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏)) ↔ ((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓))))
89	88	cbvopabv 5197	. . . . . . 7 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} = {⟨𝑒, 𝑓⟩ ∣ ((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓))}
90	79, 89	eqtri 2759	. . . . . 6 ⊢ 𝑂 = {⟨𝑒, 𝑓⟩ ∣ ((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓))}
91	65, 66, 72, 78, 90	brab 5523	. . . . 5 ⊢ (𝑎𝑂𝑐 ↔ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)))
92		vex 3468	. . . . . 6 ⊢ 𝑏 ∈ V
93		eleq1w 2818	. . . . . . . 8 ⊢ (𝑒 = 𝑏 → (𝑒 ∈ (𝑃 ∖ 𝐷) ↔ 𝑏 ∈ (𝑃 ∖ 𝐷)))
94	93	anbi1d 631	. . . . . . 7 ⊢ (𝑒 = 𝑏 → ((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ↔ (𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷))))
95		oveq1 7417	. . . . . . . . 9 ⊢ (𝑒 = 𝑏 → (𝑒𝐼𝑓) = (𝑏𝐼𝑓))
96	95	eleq2d 2821	. . . . . . . 8 ⊢ (𝑒 = 𝑏 → (𝑡 ∈ (𝑒𝐼𝑓) ↔ 𝑡 ∈ (𝑏𝐼𝑓)))
97	96	rexbidv 3165	. . . . . . 7 ⊢ (𝑒 = 𝑏 → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑓)))
98	94, 97	anbi12d 632	. . . . . 6 ⊢ (𝑒 = 𝑏 → (((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓)) ↔ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑓))))
99	73	anbi2d 630	. . . . . . 7 ⊢ (𝑓 = 𝑐 → ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ↔ (𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷))))
100		oveq2 7418	. . . . . . . . 9 ⊢ (𝑓 = 𝑐 → (𝑏𝐼𝑓) = (𝑏𝐼𝑐))
101	100	eleq2d 2821	. . . . . . . 8 ⊢ (𝑓 = 𝑐 → (𝑡 ∈ (𝑏𝐼𝑓) ↔ 𝑡 ∈ (𝑏𝐼𝑐)))
102	101	rexbidv 3165	. . . . . . 7 ⊢ (𝑓 = 𝑐 → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑓) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))
103	99, 102	anbi12d 632	. . . . . 6 ⊢ (𝑓 = 𝑐 → (((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑓)) ↔ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))))
104	92, 66, 98, 103, 90	brab 5523	. . . . 5 ⊢ (𝑏𝑂𝑐 ↔ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))
105	91, 104	anbi12i 628	. . . 4 ⊢ ((𝑎𝑂𝑐 ∧ 𝑏𝑂𝑐) ↔ (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))))
106	105	rexbii 3084	. . 3 ⊢ (∃𝑐 ∈ 𝑃 (𝑎𝑂𝑐 ∧ 𝑏𝑂𝑐) ↔ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))))
107	106	opabbii 5191	. 2 ⊢ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (𝑎𝑂𝑐 ∧ 𝑏𝑂𝑐)} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))}
108	64, 107	eqtr4di 2789	1 ⊢ (𝜑 → ((hpG‘𝐺)‘𝐷) = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (𝑎𝑂𝑐 ∧ 𝑏𝑂𝑐)})

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ∃wrex 3061 Vcvv 3464 [wsbc 3770 ∖ cdif 3928 class class class wbr 5124 {copab 5186 ↦ cmpt 5206 × cxp 5657 ran crn 5660 ‘cfv 6536 (class class class)co 7410 Basecbs 17233 TarskiGcstrkg 28411 Itvcitv 28417 LineGclng 28418 hpGchpg 28741

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 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-rep 5254 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3062 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4889 df-iun 4974 df-br 5125 df-opab 5187 df-mpt 5207 df-id 5553 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-ov 7413 df-hpg 28742

This theorem is referenced by: hpgbr 28744

W3C validator