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 28782

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 3499	. . . 4 ⊢ (𝐺 ∈ TarskiG → 𝐺 ∈ V)
3		fveq2 6907	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → (LineG‘𝑔) = (LineG‘𝐺))
4		ishpg.l	. . . . . . . 8 ⊢ 𝐿 = (LineG‘𝐺)
5	3, 4	eqtr4di 2793	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (LineG‘𝑔) = 𝐿)
6	5	rneqd 5952	. . . . . 6 ⊢ (𝑔 = 𝐺 → ran (LineG‘𝑔) = ran 𝐿)
7		ishpg.p	. . . . . . . 8 ⊢ 𝑃 = (Base‘𝐺)
8		ishpg.i	. . . . . . . 8 ⊢ 𝐼 = (Itv‘𝐺)
9		simpl 482	. . . . . . . . 9 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → 𝑝 = 𝑃)
10	9	difeq1d 4135	. . . . . . . . . . . . 13 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑝 ∖ 𝑑) = (𝑃 ∖ 𝑑))
11	10	eleq2d 2825	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑎 ∈ (𝑝 ∖ 𝑑) ↔ 𝑎 ∈ (𝑃 ∖ 𝑑)))
12	10	eleq2d 2825	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑐 ∈ (𝑝 ∖ 𝑑) ↔ 𝑐 ∈ (𝑃 ∖ 𝑑)))
13	11, 12	anbi12d 632	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → ((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ↔ (𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑))))
14		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → 𝑖 = 𝐼)
15	14	oveqd 7448	. . . . . . . . . . . . 13 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑎𝑖𝑐) = (𝑎𝐼𝑐))
16	15	eleq2d 2825	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑡 ∈ (𝑎𝑖𝑐) ↔ 𝑡 ∈ (𝑎𝐼𝑐)))
17	16	rexbidv 3177	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐) ↔ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)))
18	13, 17	anbi12d 632	. . . . . . . . . 10 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ↔ ((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐))))
19	10	eleq2d 2825	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑏 ∈ (𝑝 ∖ 𝑑) ↔ 𝑏 ∈ (𝑃 ∖ 𝑑)))
20	19, 12	anbi12d 632	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ↔ (𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑))))
21	14	oveqd 7448	. . . . . . . . . . . . 13 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑏𝑖𝑐) = (𝑏𝐼𝑐))
22	21	eleq2d 2825	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑡 ∈ (𝑏𝑖𝑐) ↔ 𝑡 ∈ (𝑏𝐼𝑐)))
23	22	rexbidv 3177	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐) ↔ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))
24	20, 23	anbi12d 632	. . . . . . . . . 10 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)) ↔ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐))))
25	18, 24	anbi12d 632	. . . . . . . . 9 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → ((((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐))) ↔ (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))))
26	9, 25	rexeqbidv 3345	. . . . . . . 8 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐))) ↔ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))))
27	7, 8, 26	sbcie2s 17195	. . . . . . 7 ⊢ (𝑔 = 𝐺 → ([(Base‘𝑔) / 𝑝][(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐))) ↔ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))))
28	27	opabbidv 5214	. . . . . 6 ⊢ (𝑔 = 𝐺 → {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))})
29	6, 28	mpteq12dv 5239	. . . . 5 ⊢ (𝑔 = 𝐺 → (𝑑 ∈ ran (LineG‘𝑔) ↦ {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))}) = (𝑑 ∈ ran 𝐿 ↦ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))}))
30		df-hpg 28781	. . . . 5 ⊢ hpG = (𝑔 ∈ V ↦ (𝑑 ∈ ran (LineG‘𝑔) ↦ {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))}))
31	4	fvexi 6921	. . . . . . 7 ⊢ 𝐿 ∈ V
32	31	rnex 7933	. . . . . 6 ⊢ ran 𝐿 ∈ V
33	32	mptex 7243	. . . . 5 ⊢ (𝑑 ∈ ran 𝐿 ↦ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))}) ∈ V
34	29, 30, 33	fvmpt 7016	. . . 4 ⊢ (𝐺 ∈ V → (hpG‘𝐺) = (𝑑 ∈ ran 𝐿 ↦ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))}))
35	1, 2, 34	3syl 18	. . 3 ⊢ (𝜑 → (hpG‘𝐺) = (𝑑 ∈ ran 𝐿 ↦ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))}))
36		difeq2 4130	. . . . . . . . . 10 ⊢ (𝑑 = 𝐷 → (𝑃 ∖ 𝑑) = (𝑃 ∖ 𝐷))
37	36	eleq2d 2825	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → (𝑎 ∈ (𝑃 ∖ 𝑑) ↔ 𝑎 ∈ (𝑃 ∖ 𝐷)))
38	36	eleq2d 2825	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → (𝑐 ∈ (𝑃 ∖ 𝑑) ↔ 𝑐 ∈ (𝑃 ∖ 𝐷)))
39	37, 38	anbi12d 632	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → ((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ↔ (𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷))))
40		rexeq 3320	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → (∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)))
41	39, 40	anbi12d 632	. . . . . . 7 ⊢ (𝑑 = 𝐷 → (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ↔ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐))))
42	36	eleq2d 2825	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → (𝑏 ∈ (𝑃 ∖ 𝑑) ↔ 𝑏 ∈ (𝑃 ∖ 𝐷)))
43	42, 38	anbi12d 632	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ↔ (𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷))))
44		rexeq 3320	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → (∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))
45	43, 44	anbi12d 632	. . . . . . 7 ⊢ (𝑑 = 𝐷 → (((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)) ↔ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))))
46	41, 45	anbi12d 632	. . . . . 6 ⊢ (𝑑 = 𝐷 → ((((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐))) ↔ (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))))
47	46	rexbidv 3177	. . . . 5 ⊢ (𝑑 = 𝐷 → (∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐))) ↔ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))))
48	47	opabbidv 5214	. . . 4 ⊢ (𝑑 = 𝐷 → {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))})
49	48	adantl 481	. . 3 ⊢ ((𝜑 ∧ 𝑑 = 𝐷) → {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))})
50		ishpg.d	. . 3 ⊢ (𝜑 → 𝐷 ∈ ran 𝐿)
51		df-xp 5695	. . . . . 6 ⊢ (𝑃 × 𝑃) = {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)}
52	7	fvexi 6921	. . . . . . 7 ⊢ 𝑃 ∈ V
53	52, 52	xpex 7772	. . . . . 6 ⊢ (𝑃 × 𝑃) ∈ V
54	51, 53	eqeltrri 2836	. . . . 5 ⊢ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)} ∈ V
55		eldifi 4141	. . . . . . . . . 10 ⊢ (𝑎 ∈ (𝑃 ∖ 𝐷) → 𝑎 ∈ 𝑃)
56		eldifi 4141	. . . . . . . . . 10 ⊢ (𝑏 ∈ (𝑃 ∖ 𝐷) → 𝑏 ∈ 𝑃)
57	55, 56	anim12i 613	. . . . . . . . 9 ⊢ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) → (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃))
58	57	ad2ant2r 747	. . . . . . . 8 ⊢ (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ (𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷))) → (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃))
59	58	ad2ant2r 747	. . . . . . 7 ⊢ ((((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))) → (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃))
60	59	rexlimivw 3149	. . . . . 6 ⊢ (∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))) → (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃))
61	60	ssopab2i 5560	. . . . 5 ⊢ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))} ⊆ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)}
62	54, 61	ssexi 5328	. . . 4 ⊢ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))} ∈ V
63	62	a1i 11	. . 3 ⊢ (𝜑 → {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))} ∈ V)
64	35, 49, 50, 63	fvmptd 7023	. 2 ⊢ (𝜑 → ((hpG‘𝐺)‘𝐷) = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))})
65		vex 3482	. . . . . 6 ⊢ 𝑎 ∈ V
66		vex 3482	. . . . . 6 ⊢ 𝑐 ∈ V
67		eleq1w 2822	. . . . . . . 8 ⊢ (𝑒 = 𝑎 → (𝑒 ∈ (𝑃 ∖ 𝐷) ↔ 𝑎 ∈ (𝑃 ∖ 𝐷)))
68	67	anbi1d 631	. . . . . . 7 ⊢ (𝑒 = 𝑎 → ((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ↔ (𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷))))
69		oveq1 7438	. . . . . . . . 9 ⊢ (𝑒 = 𝑎 → (𝑒𝐼𝑓) = (𝑎𝐼𝑓))
70	69	eleq2d 2825	. . . . . . . 8 ⊢ (𝑒 = 𝑎 → (𝑡 ∈ (𝑒𝐼𝑓) ↔ 𝑡 ∈ (𝑎𝐼𝑓)))
71	70	rexbidv 3177	. . . . . . 7 ⊢ (𝑒 = 𝑎 → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑓)))
72	68, 71	anbi12d 632	. . . . . 6 ⊢ (𝑒 = 𝑎 → (((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓)) ↔ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑓))))
73		eleq1w 2822	. . . . . . . 8 ⊢ (𝑓 = 𝑐 → (𝑓 ∈ (𝑃 ∖ 𝐷) ↔ 𝑐 ∈ (𝑃 ∖ 𝐷)))
74	73	anbi2d 630	. . . . . . 7 ⊢ (𝑓 = 𝑐 → ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ↔ (𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷))))
75		oveq2 7439	. . . . . . . . 9 ⊢ (𝑓 = 𝑐 → (𝑎𝐼𝑓) = (𝑎𝐼𝑐))
76	75	eleq2d 2825	. . . . . . . 8 ⊢ (𝑓 = 𝑐 → (𝑡 ∈ (𝑎𝐼𝑓) ↔ 𝑡 ∈ (𝑎𝐼𝑐)))
77	76	rexbidv 3177	. . . . . . 7 ⊢ (𝑓 = 𝑐 → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑓) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)))
78	74, 77	anbi12d 632	. . . . . 6 ⊢ (𝑓 = 𝑐 → (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑓)) ↔ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐))))
79		ishpg.o	. . . . . . 7 ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))}
80		simpl 482	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → 𝑎 = 𝑒)
81	80	eleq1d 2824	. . . . . . . . . 10 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (𝑎 ∈ (𝑃 ∖ 𝐷) ↔ 𝑒 ∈ (𝑃 ∖ 𝐷)))
82		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → 𝑏 = 𝑓)
83	82	eleq1d 2824	. . . . . . . . . 10 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (𝑏 ∈ (𝑃 ∖ 𝐷) ↔ 𝑓 ∈ (𝑃 ∖ 𝐷)))
84	81, 83	anbi12d 632	. . . . . . . . 9 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ↔ (𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷))))
85		oveq12 7440	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (𝑎𝐼𝑏) = (𝑒𝐼𝑓))
86	85	eleq2d 2825	. . . . . . . . . 10 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (𝑡 ∈ (𝑎𝐼𝑏) ↔ 𝑡 ∈ (𝑒𝐼𝑓)))
87	86	rexbidv 3177	. . . . . . . . 9 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓)))
88	84, 87	anbi12d 632	. . . . . . . 8 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏)) ↔ ((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓))))
89	88	cbvopabv 5221	. . . . . . 7 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} = {⟨𝑒, 𝑓⟩ ∣ ((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓))}
90	79, 89	eqtri 2763	. . . . . 6 ⊢ 𝑂 = {⟨𝑒, 𝑓⟩ ∣ ((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓))}
91	65, 66, 72, 78, 90	brab 5553	. . . . 5 ⊢ (𝑎𝑂𝑐 ↔ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)))
92		vex 3482	. . . . . 6 ⊢ 𝑏 ∈ V
93		eleq1w 2822	. . . . . . . 8 ⊢ (𝑒 = 𝑏 → (𝑒 ∈ (𝑃 ∖ 𝐷) ↔ 𝑏 ∈ (𝑃 ∖ 𝐷)))
94	93	anbi1d 631	. . . . . . 7 ⊢ (𝑒 = 𝑏 → ((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ↔ (𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷))))
95		oveq1 7438	. . . . . . . . 9 ⊢ (𝑒 = 𝑏 → (𝑒𝐼𝑓) = (𝑏𝐼𝑓))
96	95	eleq2d 2825	. . . . . . . 8 ⊢ (𝑒 = 𝑏 → (𝑡 ∈ (𝑒𝐼𝑓) ↔ 𝑡 ∈ (𝑏𝐼𝑓)))
97	96	rexbidv 3177	. . . . . . 7 ⊢ (𝑒 = 𝑏 → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑓)))
98	94, 97	anbi12d 632	. . . . . 6 ⊢ (𝑒 = 𝑏 → (((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓)) ↔ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑓))))
99	73	anbi2d 630	. . . . . . 7 ⊢ (𝑓 = 𝑐 → ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ↔ (𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷))))
100		oveq2 7439	. . . . . . . . 9 ⊢ (𝑓 = 𝑐 → (𝑏𝐼𝑓) = (𝑏𝐼𝑐))
101	100	eleq2d 2825	. . . . . . . 8 ⊢ (𝑓 = 𝑐 → (𝑡 ∈ (𝑏𝐼𝑓) ↔ 𝑡 ∈ (𝑏𝐼𝑐)))
102	101	rexbidv 3177	. . . . . . 7 ⊢ (𝑓 = 𝑐 → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑓) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))
103	99, 102	anbi12d 632	. . . . . 6 ⊢ (𝑓 = 𝑐 → (((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑓)) ↔ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))))
104	92, 66, 98, 103, 90	brab 5553	. . . . 5 ⊢ (𝑏𝑂𝑐 ↔ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))
105	91, 104	anbi12i 628	. . . 4 ⊢ ((𝑎𝑂𝑐 ∧ 𝑏𝑂𝑐) ↔ (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))))
106	105	rexbii 3092	. . 3 ⊢ (∃𝑐 ∈ 𝑃 (𝑎𝑂𝑐 ∧ 𝑏𝑂𝑐) ↔ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))))
107	106	opabbii 5215	. 2 ⊢ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (𝑎𝑂𝑐 ∧ 𝑏𝑂𝑐)} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))}
108	64, 107	eqtr4di 2793	1 ⊢ (𝜑 → ((hpG‘𝐺)‘𝐷) = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (𝑎𝑂𝑐 ∧ 𝑏𝑂𝑐)})

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1537 ∈ wcel 2106 ∃wrex 3068 Vcvv 3478 [wsbc 3791 ∖ cdif 3960 class class class wbr 5148 {copab 5210 ↦ cmpt 5231 × cxp 5687 ran crn 5690 ‘cfv 6563 (class class class)co 7431 Basecbs 17245 TarskiGcstrkg 28450 Itvcitv 28456 LineGclng 28457 hpGchpg 28780

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 ax-rep 5285 ax-sep 5302 ax-nul 5312 ax-pow 5371 ax-pr 5438 ax-un 7754

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-nf 1781 df-sb 2063 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ne 2939 df-ral 3060 df-rex 3069 df-reu 3379 df-rab 3434 df-v 3480 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-nul 4340 df-if 4532 df-pw 4607 df-sn 4632 df-pr 4634 df-op 4638 df-uni 4913 df-iun 4998 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5583 df-xp 5695 df-rel 5696 df-cnv 5697 df-co 5698 df-dm 5699 df-rn 5700 df-res 5701 df-ima 5702 df-iota 6516 df-fun 6565 df-fn 6566 df-f 6567 df-f1 6568 df-fo 6569 df-f1o 6570 df-fv 6571 df-ov 7434 df-hpg 28781

This theorem is referenced by: hpgbr 28783

W3C validator