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 29243

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 3471	. . . 4 ⊢ (𝐺 ∈ TarskiG → 𝐺 ∈ V)
3		fveq2 6886	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → (LineG‘𝑔) = (LineG‘𝐺))
4		ishpg.l	. . . . . . . 8 ⊢ 𝐿 = (LineG‘𝐺)
5	3, 4	eqtr4di 2813	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (LineG‘𝑔) = 𝐿)
6	5	rneqd 5919	. . . . . 6 ⊢ (𝑔 = 𝐺 → ran (LineG‘𝑔) = ran 𝐿)
7		ishpg.p	. . . . . . . 8 ⊢ 𝑃 = (Base‘𝐺)
8		ishpg.i	. . . . . . . 8 ⊢ 𝐼 = (Itv‘𝐺)
9		simpl 488	. . . . . . . . 9 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → 𝑝 = 𝑃)
10	9	difeq1d 4062	. . . . . . . . . . . . 13 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑝 ∖ 𝑑) = (𝑃 ∖ 𝑑))
11	10	eleq2d 2846	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑎 ∈ (𝑝 ∖ 𝑑) ↔ 𝑎 ∈ (𝑃 ∖ 𝑑)))
12	10	eleq2d 2846	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑐 ∈ (𝑝 ∖ 𝑑) ↔ 𝑐 ∈ (𝑃 ∖ 𝑑)))
13	11, 12	anbi12d 644	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → ((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ↔ (𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑))))
14		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → 𝑖 = 𝐼)
15	14	oveqd 7438	. . . . . . . . . . . . 13 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑎𝑖𝑐) = (𝑎𝐼𝑐))
16	15	eleq2d 2846	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑡 ∈ (𝑎𝑖𝑐) ↔ 𝑡 ∈ (𝑎𝐼𝑐)))
17	16	rexbidv 3186	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐) ↔ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)))
18	13, 17	anbi12d 644	. . . . . . . . . 10 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ↔ ((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐))))
19	10	eleq2d 2846	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑏 ∈ (𝑝 ∖ 𝑑) ↔ 𝑏 ∈ (𝑃 ∖ 𝑑)))
20	19, 12	anbi12d 644	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ↔ (𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑))))
21	14	oveqd 7438	. . . . . . . . . . . . 13 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑏𝑖𝑐) = (𝑏𝐼𝑐))
22	21	eleq2d 2846	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑡 ∈ (𝑏𝑖𝑐) ↔ 𝑡 ∈ (𝑏𝐼𝑐)))
23	22	rexbidv 3186	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐) ↔ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))
24	20, 23	anbi12d 644	. . . . . . . . . 10 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)) ↔ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐))))
25	18, 24	anbi12d 644	. . . . . . . . 9 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → ((((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐))) ↔ (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))))
26	9, 25	rexeqbidv 3335	. . . . . . . 8 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐))) ↔ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))))
27	7, 8, 26	sbcie2s 17345	. . . . . . 7 ⊢ (𝑔 = 𝐺 → ([(Base‘𝑔) / 𝑝][(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐))) ↔ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))))
28	27	opabbidv 5170	. . . . . 6 ⊢ (𝑔 = 𝐺 → {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))})
29	6, 28	mpteq12dv 5191	. . . . 5 ⊢ (𝑔 = 𝐺 → (𝑑 ∈ ran (LineG‘𝑔) ↦ {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))}) = (𝑑 ∈ ran 𝐿 ↦ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))}))
30		df-hpg 29242	. . . . 5 ⊢ hpG = (𝑔 ∈ V ↦ (𝑑 ∈ ran (LineG‘𝑔) ↦ {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))}))
31	4	fvexi 6900	. . . . . . 7 ⊢ 𝐿 ∈ V
32	31	rnex 7923	. . . . . 6 ⊢ ran 𝐿 ∈ V
33	32	mptex 7230	. . . . 5 ⊢ (𝑑 ∈ ran 𝐿 ↦ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))}) ∈ V
34	29, 30, 33	fvmpt 6994	. . . 4 ⊢ (𝐺 ∈ V → (hpG‘𝐺) = (𝑑 ∈ ran 𝐿 ↦ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))}))
35	1, 2, 34	3syl 19	. . 3 ⊢ (𝜑 → (hpG‘𝐺) = (𝑑 ∈ ran 𝐿 ↦ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))}))
36		difeq2 4057	. . . . . . . . . 10 ⊢ (𝑑 = 𝐷 → (𝑃 ∖ 𝑑) = (𝑃 ∖ 𝐷))
37	36	eleq2d 2846	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → (𝑎 ∈ (𝑃 ∖ 𝑑) ↔ 𝑎 ∈ (𝑃 ∖ 𝐷)))
38	36	eleq2d 2846	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → (𝑐 ∈ (𝑃 ∖ 𝑑) ↔ 𝑐 ∈ (𝑃 ∖ 𝐷)))
39	37, 38	anbi12d 644	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → ((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ↔ (𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷))))
40		rexeq 3315	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → (∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)))
41	39, 40	anbi12d 644	. . . . . . 7 ⊢ (𝑑 = 𝐷 → (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ↔ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐))))
42	36	eleq2d 2846	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → (𝑏 ∈ (𝑃 ∖ 𝑑) ↔ 𝑏 ∈ (𝑃 ∖ 𝐷)))
43	42, 38	anbi12d 644	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ↔ (𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷))))
44		rexeq 3315	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → (∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))
45	43, 44	anbi12d 644	. . . . . . 7 ⊢ (𝑑 = 𝐷 → (((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)) ↔ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))))
46	41, 45	anbi12d 644	. . . . . 6 ⊢ (𝑑 = 𝐷 → ((((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐))) ↔ (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))))
47	46	rexbidv 3186	. . . . 5 ⊢ (𝑑 = 𝐷 → (∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐))) ↔ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))))
48	47	opabbidv 5170	. . . 4 ⊢ (𝑑 = 𝐷 → {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))})
49	48	adantl 487	. . 3 ⊢ ((𝜑 ∧ 𝑑 = 𝐷) → {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))})
50		ishpg.d	. . 3 ⊢ (𝜑 → 𝐷 ∈ ran 𝐿)
51		df-xp 5656	. . . . . 6 ⊢ (𝑃 × 𝑃) = {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)}
52	7	fvexi 6900	. . . . . . 7 ⊢ 𝑃 ∈ V
53	52, 52	xpex 7768	. . . . . 6 ⊢ (𝑃 × 𝑃) ∈ V
54	51, 53	eqeltrri 2857	. . . . 5 ⊢ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)} ∈ V
55		eldifi 4067	. . . . . . . . . 10 ⊢ (𝑎 ∈ (𝑃 ∖ 𝐷) → 𝑎 ∈ 𝑃)
56		eldifi 4067	. . . . . . . . . 10 ⊢ (𝑏 ∈ (𝑃 ∖ 𝐷) → 𝑏 ∈ 𝑃)
57	55, 56	anim12i 625	. . . . . . . . 9 ⊢ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) → (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃))
58	57	ad2ant2r 760	. . . . . . . 8 ⊢ (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ (𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷))) → (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃))
59	58	ad2ant2r 760	. . . . . . 7 ⊢ ((((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))) → (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃))
60	59	rexlimivw 3159	. . . . . 6 ⊢ (∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))) → (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃))
61	60	ssopab2i 5524	. . . . 5 ⊢ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))} ⊆ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)}
62	54, 61	ssexi 5283	. . . 4 ⊢ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))} ∈ V
63	62	a1i 11	. . 3 ⊢ (𝜑 → {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))} ∈ V)
64	35, 49, 50, 63	fvmptd 7002	. 2 ⊢ (𝜑 → ((hpG‘𝐺)‘𝐷) = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))})
65		vex 3454	. . . . . 6 ⊢ 𝑎 ∈ V
66		vex 3454	. . . . . 6 ⊢ 𝑐 ∈ V
67		eleq1w 2843	. . . . . . . 8 ⊢ (𝑒 = 𝑎 → (𝑒 ∈ (𝑃 ∖ 𝐷) ↔ 𝑎 ∈ (𝑃 ∖ 𝐷)))
68	67	anbi1d 643	. . . . . . 7 ⊢ (𝑒 = 𝑎 → ((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ↔ (𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷))))
69		oveq1 7428	. . . . . . . . 9 ⊢ (𝑒 = 𝑎 → (𝑒𝐼𝑓) = (𝑎𝐼𝑓))
70	69	eleq2d 2846	. . . . . . . 8 ⊢ (𝑒 = 𝑎 → (𝑡 ∈ (𝑒𝐼𝑓) ↔ 𝑡 ∈ (𝑎𝐼𝑓)))
71	70	rexbidv 3186	. . . . . . 7 ⊢ (𝑒 = 𝑎 → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑓)))
72	68, 71	anbi12d 644	. . . . . 6 ⊢ (𝑒 = 𝑎 → (((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓)) ↔ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑓))))
73		eleq1w 2843	. . . . . . . 8 ⊢ (𝑓 = 𝑐 → (𝑓 ∈ (𝑃 ∖ 𝐷) ↔ 𝑐 ∈ (𝑃 ∖ 𝐷)))
74	73	anbi2d 642	. . . . . . 7 ⊢ (𝑓 = 𝑐 → ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ↔ (𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷))))
75		oveq2 7429	. . . . . . . . 9 ⊢ (𝑓 = 𝑐 → (𝑎𝐼𝑓) = (𝑎𝐼𝑐))
76	75	eleq2d 2846	. . . . . . . 8 ⊢ (𝑓 = 𝑐 → (𝑡 ∈ (𝑎𝐼𝑓) ↔ 𝑡 ∈ (𝑎𝐼𝑐)))
77	76	rexbidv 3186	. . . . . . 7 ⊢ (𝑓 = 𝑐 → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑓) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)))
78	74, 77	anbi12d 644	. . . . . 6 ⊢ (𝑓 = 𝑐 → (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑓)) ↔ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐))))
79		ishpg.o	. . . . . . 7 ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))}
80		simpl 488	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → 𝑎 = 𝑒)
81	80	eleq1d 2845	. . . . . . . . . 10 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (𝑎 ∈ (𝑃 ∖ 𝐷) ↔ 𝑒 ∈ (𝑃 ∖ 𝐷)))
82		simpr 490	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → 𝑏 = 𝑓)
83	82	eleq1d 2845	. . . . . . . . . 10 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (𝑏 ∈ (𝑃 ∖ 𝐷) ↔ 𝑓 ∈ (𝑃 ∖ 𝐷)))
84	81, 83	anbi12d 644	. . . . . . . . 9 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ↔ (𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷))))
85		oveq12 7430	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (𝑎𝐼𝑏) = (𝑒𝐼𝑓))
86	85	eleq2d 2846	. . . . . . . . . 10 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (𝑡 ∈ (𝑎𝐼𝑏) ↔ 𝑡 ∈ (𝑒𝐼𝑓)))
87	86	rexbidv 3186	. . . . . . . . 9 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓)))
88	84, 87	anbi12d 644	. . . . . . . 8 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏)) ↔ ((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓))))
89	88	cbvopabv 5177	. . . . . . 7 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} = {⟨𝑒, 𝑓⟩ ∣ ((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓))}
90	79, 89	eqtri 2783	. . . . . 6 ⊢ 𝑂 = {⟨𝑒, 𝑓⟩ ∣ ((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓))}
91	65, 66, 72, 78, 90	brab 5517	. . . . 5 ⊢ (𝑎𝑂𝑐 ↔ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)))
92		vex 3454	. . . . . 6 ⊢ 𝑏 ∈ V
93		eleq1w 2843	. . . . . . . 8 ⊢ (𝑒 = 𝑏 → (𝑒 ∈ (𝑃 ∖ 𝐷) ↔ 𝑏 ∈ (𝑃 ∖ 𝐷)))
94	93	anbi1d 643	. . . . . . 7 ⊢ (𝑒 = 𝑏 → ((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ↔ (𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷))))
95		oveq1 7428	. . . . . . . . 9 ⊢ (𝑒 = 𝑏 → (𝑒𝐼𝑓) = (𝑏𝐼𝑓))
96	95	eleq2d 2846	. . . . . . . 8 ⊢ (𝑒 = 𝑏 → (𝑡 ∈ (𝑒𝐼𝑓) ↔ 𝑡 ∈ (𝑏𝐼𝑓)))
97	96	rexbidv 3186	. . . . . . 7 ⊢ (𝑒 = 𝑏 → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑓)))
98	94, 97	anbi12d 644	. . . . . 6 ⊢ (𝑒 = 𝑏 → (((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓)) ↔ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑓))))
99	73	anbi2d 642	. . . . . . 7 ⊢ (𝑓 = 𝑐 → ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ↔ (𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷))))
100		oveq2 7429	. . . . . . . . 9 ⊢ (𝑓 = 𝑐 → (𝑏𝐼𝑓) = (𝑏𝐼𝑐))
101	100	eleq2d 2846	. . . . . . . 8 ⊢ (𝑓 = 𝑐 → (𝑡 ∈ (𝑏𝐼𝑓) ↔ 𝑡 ∈ (𝑏𝐼𝑐)))
102	101	rexbidv 3186	. . . . . . 7 ⊢ (𝑓 = 𝑐 → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑓) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))
103	99, 102	anbi12d 644	. . . . . 6 ⊢ (𝑓 = 𝑐 → (((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑓)) ↔ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))))
104	92, 66, 98, 103, 90	brab 5517	. . . . 5 ⊢ (𝑏𝑂𝑐 ↔ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))
105	91, 104	anbi12i 640	. . . 4 ⊢ ((𝑎𝑂𝑐 ∧ 𝑏𝑂𝑐) ↔ (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))))
106	105	rexbii 3109	. . 3 ⊢ (∃𝑐 ∈ 𝑃 (𝑎𝑂𝑐 ∧ 𝑏𝑂𝑐) ↔ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))))
107	106	opabbii 5171	. 2 ⊢ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (𝑎𝑂𝑐 ∧ 𝑏𝑂𝑐)} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))}
108	64, 107	eqtr4di 2813	1 ⊢ (𝜑 → ((hpG‘𝐺)‘𝐷) = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (𝑎𝑂𝑐 ∧ 𝑏𝑂𝑐)})

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1569 ∈ wcel 2144 ∃wrex 3086 Vcvv 3450 [wsbc 3738 ∖ cdif 4045 class class class wbr 5102 {copab 5166 ↦ cmpt 5185 × cxp 5648 ran crn 5651 ‘cfv 6539 (class class class)co 7421 Basecbs 17393 TarskiGcstrkg 28895 Itvcitv 28901 LineGclng 28902 hpGchpg 29241

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7752

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-id 5545 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-iota 6494 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-ov 7424 df-hpg 29242

This theorem is used by: hpgbr 29244

W3C validator