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 28686

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 3468	. . . 4 ⊢ (𝐺 ∈ TarskiG → 𝐺 ∈ V)
3		fveq2 6858	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → (LineG‘𝑔) = (LineG‘𝐺))
4		ishpg.l	. . . . . . . 8 ⊢ 𝐿 = (LineG‘𝐺)
5	3, 4	eqtr4di 2782	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (LineG‘𝑔) = 𝐿)
6	5	rneqd 5902	. . . . . 6 ⊢ (𝑔 = 𝐺 → ran (LineG‘𝑔) = ran 𝐿)
7		ishpg.p	. . . . . . . 8 ⊢ 𝑃 = (Base‘𝐺)
8		ishpg.i	. . . . . . . 8 ⊢ 𝐼 = (Itv‘𝐺)
9		simpl 482	. . . . . . . . 9 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → 𝑝 = 𝑃)
10	9	difeq1d 4088	. . . . . . . . . . . . 13 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑝 ∖ 𝑑) = (𝑃 ∖ 𝑑))
11	10	eleq2d 2814	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑎 ∈ (𝑝 ∖ 𝑑) ↔ 𝑎 ∈ (𝑃 ∖ 𝑑)))
12	10	eleq2d 2814	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑐 ∈ (𝑝 ∖ 𝑑) ↔ 𝑐 ∈ (𝑃 ∖ 𝑑)))
13	11, 12	anbi12d 632	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → ((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ↔ (𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑))))
14		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → 𝑖 = 𝐼)
15	14	oveqd 7404	. . . . . . . . . . . . 13 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑎𝑖𝑐) = (𝑎𝐼𝑐))
16	15	eleq2d 2814	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑡 ∈ (𝑎𝑖𝑐) ↔ 𝑡 ∈ (𝑎𝐼𝑐)))
17	16	rexbidv 3157	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐) ↔ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)))
18	13, 17	anbi12d 632	. . . . . . . . . 10 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ↔ ((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐))))
19	10	eleq2d 2814	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑏 ∈ (𝑝 ∖ 𝑑) ↔ 𝑏 ∈ (𝑃 ∖ 𝑑)))
20	19, 12	anbi12d 632	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ↔ (𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑))))
21	14	oveqd 7404	. . . . . . . . . . . . 13 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑏𝑖𝑐) = (𝑏𝐼𝑐))
22	21	eleq2d 2814	. . . . . . . . . . . 12 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (𝑡 ∈ (𝑏𝑖𝑐) ↔ 𝑡 ∈ (𝑏𝐼𝑐)))
23	22	rexbidv 3157	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐) ↔ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))
24	20, 23	anbi12d 632	. . . . . . . . . 10 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)) ↔ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐))))
25	18, 24	anbi12d 632	. . . . . . . . 9 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → ((((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐))) ↔ (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))))
26	9, 25	rexeqbidv 3320	. . . . . . . 8 ⊢ ((𝑝 = 𝑃 ∧ 𝑖 = 𝐼) → (∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐))) ↔ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))))
27	7, 8, 26	sbcie2s 17131	. . . . . . 7 ⊢ (𝑔 = 𝐺 → ([(Base‘𝑔) / 𝑝][(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐))) ↔ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))))
28	27	opabbidv 5173	. . . . . 6 ⊢ (𝑔 = 𝐺 → {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))})
29	6, 28	mpteq12dv 5194	. . . . 5 ⊢ (𝑔 = 𝐺 → (𝑑 ∈ ran (LineG‘𝑔) ↦ {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))}) = (𝑑 ∈ ran 𝐿 ↦ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))}))
30		df-hpg 28685	. . . . 5 ⊢ hpG = (𝑔 ∈ V ↦ (𝑑 ∈ ran (LineG‘𝑔) ↦ {⟨𝑎, 𝑏⟩ ∣ [(Base‘𝑔) / 𝑝][(Itv‘𝑔) / 𝑖]∃𝑐 ∈ 𝑝 (((𝑎 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝑖𝑐)) ∧ ((𝑏 ∈ (𝑝 ∖ 𝑑) ∧ 𝑐 ∈ (𝑝 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝑖𝑐)))}))
31	4	fvexi 6872	. . . . . . 7 ⊢ 𝐿 ∈ V
32	31	rnex 7886	. . . . . 6 ⊢ ran 𝐿 ∈ V
33	32	mptex 7197	. . . . 5 ⊢ (𝑑 ∈ ran 𝐿 ↦ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))}) ∈ V
34	29, 30, 33	fvmpt 6968	. . . 4 ⊢ (𝐺 ∈ V → (hpG‘𝐺) = (𝑑 ∈ ran 𝐿 ↦ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))}))
35	1, 2, 34	3syl 18	. . 3 ⊢ (𝜑 → (hpG‘𝐺) = (𝑑 ∈ ran 𝐿 ↦ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))}))
36		difeq2 4083	. . . . . . . . . 10 ⊢ (𝑑 = 𝐷 → (𝑃 ∖ 𝑑) = (𝑃 ∖ 𝐷))
37	36	eleq2d 2814	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → (𝑎 ∈ (𝑃 ∖ 𝑑) ↔ 𝑎 ∈ (𝑃 ∖ 𝐷)))
38	36	eleq2d 2814	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → (𝑐 ∈ (𝑃 ∖ 𝑑) ↔ 𝑐 ∈ (𝑃 ∖ 𝐷)))
39	37, 38	anbi12d 632	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → ((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ↔ (𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷))))
40		rexeq 3295	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → (∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)))
41	39, 40	anbi12d 632	. . . . . . 7 ⊢ (𝑑 = 𝐷 → (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ↔ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐))))
42	36	eleq2d 2814	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → (𝑏 ∈ (𝑃 ∖ 𝑑) ↔ 𝑏 ∈ (𝑃 ∖ 𝐷)))
43	42, 38	anbi12d 632	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ↔ (𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷))))
44		rexeq 3295	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → (∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))
45	43, 44	anbi12d 632	. . . . . . 7 ⊢ (𝑑 = 𝐷 → (((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)) ↔ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))))
46	41, 45	anbi12d 632	. . . . . 6 ⊢ (𝑑 = 𝐷 → ((((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐))) ↔ (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))))
47	46	rexbidv 3157	. . . . 5 ⊢ (𝑑 = 𝐷 → (∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐))) ↔ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))))
48	47	opabbidv 5173	. . . 4 ⊢ (𝑑 = 𝐷 → {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))})
49	48	adantl 481	. . 3 ⊢ ((𝜑 ∧ 𝑑 = 𝐷) → {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝑑) ∧ 𝑐 ∈ (𝑃 ∖ 𝑑)) ∧ ∃𝑡 ∈ 𝑑 𝑡 ∈ (𝑏𝐼𝑐)))} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))})
50		ishpg.d	. . 3 ⊢ (𝜑 → 𝐷 ∈ ran 𝐿)
51		df-xp 5644	. . . . . 6 ⊢ (𝑃 × 𝑃) = {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)}
52	7	fvexi 6872	. . . . . . 7 ⊢ 𝑃 ∈ V
53	52, 52	xpex 7729	. . . . . 6 ⊢ (𝑃 × 𝑃) ∈ V
54	51, 53	eqeltrri 2825	. . . . 5 ⊢ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)} ∈ V
55		eldifi 4094	. . . . . . . . . 10 ⊢ (𝑎 ∈ (𝑃 ∖ 𝐷) → 𝑎 ∈ 𝑃)
56		eldifi 4094	. . . . . . . . . 10 ⊢ (𝑏 ∈ (𝑃 ∖ 𝐷) → 𝑏 ∈ 𝑃)
57	55, 56	anim12i 613	. . . . . . . . 9 ⊢ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) → (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃))
58	57	ad2ant2r 747	. . . . . . . 8 ⊢ (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ (𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷))) → (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃))
59	58	ad2ant2r 747	. . . . . . 7 ⊢ ((((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))) → (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃))
60	59	rexlimivw 3130	. . . . . 6 ⊢ (∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))) → (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃))
61	60	ssopab2i 5510	. . . . 5 ⊢ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))} ⊆ {⟨𝑎, 𝑏⟩ ∣ (𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃)}
62	54, 61	ssexi 5277	. . . 4 ⊢ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))} ∈ V
63	62	a1i 11	. . 3 ⊢ (𝜑 → {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))} ∈ V)
64	35, 49, 50, 63	fvmptd 6975	. 2 ⊢ (𝜑 → ((hpG‘𝐺)‘𝐷) = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))})
65		vex 3451	. . . . . 6 ⊢ 𝑎 ∈ V
66		vex 3451	. . . . . 6 ⊢ 𝑐 ∈ V
67		eleq1w 2811	. . . . . . . 8 ⊢ (𝑒 = 𝑎 → (𝑒 ∈ (𝑃 ∖ 𝐷) ↔ 𝑎 ∈ (𝑃 ∖ 𝐷)))
68	67	anbi1d 631	. . . . . . 7 ⊢ (𝑒 = 𝑎 → ((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ↔ (𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷))))
69		oveq1 7394	. . . . . . . . 9 ⊢ (𝑒 = 𝑎 → (𝑒𝐼𝑓) = (𝑎𝐼𝑓))
70	69	eleq2d 2814	. . . . . . . 8 ⊢ (𝑒 = 𝑎 → (𝑡 ∈ (𝑒𝐼𝑓) ↔ 𝑡 ∈ (𝑎𝐼𝑓)))
71	70	rexbidv 3157	. . . . . . 7 ⊢ (𝑒 = 𝑎 → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑓)))
72	68, 71	anbi12d 632	. . . . . 6 ⊢ (𝑒 = 𝑎 → (((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓)) ↔ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑓))))
73		eleq1w 2811	. . . . . . . 8 ⊢ (𝑓 = 𝑐 → (𝑓 ∈ (𝑃 ∖ 𝐷) ↔ 𝑐 ∈ (𝑃 ∖ 𝐷)))
74	73	anbi2d 630	. . . . . . 7 ⊢ (𝑓 = 𝑐 → ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ↔ (𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷))))
75		oveq2 7395	. . . . . . . . 9 ⊢ (𝑓 = 𝑐 → (𝑎𝐼𝑓) = (𝑎𝐼𝑐))
76	75	eleq2d 2814	. . . . . . . 8 ⊢ (𝑓 = 𝑐 → (𝑡 ∈ (𝑎𝐼𝑓) ↔ 𝑡 ∈ (𝑎𝐼𝑐)))
77	76	rexbidv 3157	. . . . . . 7 ⊢ (𝑓 = 𝑐 → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑓) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)))
78	74, 77	anbi12d 632	. . . . . 6 ⊢ (𝑓 = 𝑐 → (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑓)) ↔ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐))))
79		ishpg.o	. . . . . . 7 ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))}
80		simpl 482	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → 𝑎 = 𝑒)
81	80	eleq1d 2813	. . . . . . . . . 10 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (𝑎 ∈ (𝑃 ∖ 𝐷) ↔ 𝑒 ∈ (𝑃 ∖ 𝐷)))
82		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → 𝑏 = 𝑓)
83	82	eleq1d 2813	. . . . . . . . . 10 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (𝑏 ∈ (𝑃 ∖ 𝐷) ↔ 𝑓 ∈ (𝑃 ∖ 𝐷)))
84	81, 83	anbi12d 632	. . . . . . . . 9 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ↔ (𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷))))
85		oveq12 7396	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (𝑎𝐼𝑏) = (𝑒𝐼𝑓))
86	85	eleq2d 2814	. . . . . . . . . 10 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (𝑡 ∈ (𝑎𝐼𝑏) ↔ 𝑡 ∈ (𝑒𝐼𝑓)))
87	86	rexbidv 3157	. . . . . . . . 9 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓)))
88	84, 87	anbi12d 632	. . . . . . . 8 ⊢ ((𝑎 = 𝑒 ∧ 𝑏 = 𝑓) → (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏)) ↔ ((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓))))
89	88	cbvopabv 5180	. . . . . . 7 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} = {⟨𝑒, 𝑓⟩ ∣ ((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓))}
90	79, 89	eqtri 2752	. . . . . 6 ⊢ 𝑂 = {⟨𝑒, 𝑓⟩ ∣ ((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓))}
91	65, 66, 72, 78, 90	brab 5503	. . . . 5 ⊢ (𝑎𝑂𝑐 ↔ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)))
92		vex 3451	. . . . . 6 ⊢ 𝑏 ∈ V
93		eleq1w 2811	. . . . . . . 8 ⊢ (𝑒 = 𝑏 → (𝑒 ∈ (𝑃 ∖ 𝐷) ↔ 𝑏 ∈ (𝑃 ∖ 𝐷)))
94	93	anbi1d 631	. . . . . . 7 ⊢ (𝑒 = 𝑏 → ((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ↔ (𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷))))
95		oveq1 7394	. . . . . . . . 9 ⊢ (𝑒 = 𝑏 → (𝑒𝐼𝑓) = (𝑏𝐼𝑓))
96	95	eleq2d 2814	. . . . . . . 8 ⊢ (𝑒 = 𝑏 → (𝑡 ∈ (𝑒𝐼𝑓) ↔ 𝑡 ∈ (𝑏𝐼𝑓)))
97	96	rexbidv 3157	. . . . . . 7 ⊢ (𝑒 = 𝑏 → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑓)))
98	94, 97	anbi12d 632	. . . . . 6 ⊢ (𝑒 = 𝑏 → (((𝑒 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑒𝐼𝑓)) ↔ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑓))))
99	73	anbi2d 630	. . . . . . 7 ⊢ (𝑓 = 𝑐 → ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ↔ (𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷))))
100		oveq2 7395	. . . . . . . . 9 ⊢ (𝑓 = 𝑐 → (𝑏𝐼𝑓) = (𝑏𝐼𝑐))
101	100	eleq2d 2814	. . . . . . . 8 ⊢ (𝑓 = 𝑐 → (𝑡 ∈ (𝑏𝐼𝑓) ↔ 𝑡 ∈ (𝑏𝐼𝑐)))
102	101	rexbidv 3157	. . . . . . 7 ⊢ (𝑓 = 𝑐 → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑓) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))
103	99, 102	anbi12d 632	. . . . . 6 ⊢ (𝑓 = 𝑐 → (((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑓 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑓)) ↔ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))))
104	92, 66, 98, 103, 90	brab 5503	. . . . 5 ⊢ (𝑏𝑂𝑐 ↔ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))
105	91, 104	anbi12i 628	. . . 4 ⊢ ((𝑎𝑂𝑐 ∧ 𝑏𝑂𝑐) ↔ (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))))
106	105	rexbii 3076	. . 3 ⊢ (∃𝑐 ∈ 𝑃 (𝑎𝑂𝑐 ∧ 𝑏𝑂𝑐) ↔ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐))))
107	106	opabbii 5174	. 2 ⊢ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (𝑎𝑂𝑐 ∧ 𝑏𝑂𝑐)} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑐)) ∧ ((𝑏 ∈ (𝑃 ∖ 𝐷) ∧ 𝑐 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑏𝐼𝑐)))}
108	64, 107	eqtr4di 2782	1 ⊢ (𝜑 → ((hpG‘𝐺)‘𝐷) = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝑃 (𝑎𝑂𝑐 ∧ 𝑏𝑂𝑐)})

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ∃wrex 3053 Vcvv 3447 [wsbc 3753 ∖ cdif 3911 class class class wbr 5107 {copab 5169 ↦ cmpt 5188 × cxp 5636 ran crn 5639 ‘cfv 6511 (class class class)co 7387 Basecbs 17179 TarskiGcstrkg 28354 Itvcitv 28360 LineGclng 28361 hpGchpg 28684

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 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711

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 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4872 df-iun 4957 df-br 5108 df-opab 5170 df-mpt 5189 df-id 5533 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-ov 7390 df-hpg 28685

This theorem is referenced by: hpgbr 28687

W3C validator