plngcplem - Metamath Proof Explorer

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

Theorem plngcplem 29015

Description: Lemma for plngcp 29016. (Contributed by Thierry Arnoux, 17-Jun-2026.)

**Hypotheses**
Ref	Expression
plngval.p	⊢ 𝑃 = (Base‘𝐺)
plngval.i	⊢ 𝐼 = (Itv‘𝐺)
plngval.1	⊢ 𝐿 = (LineG‘𝐺)
plngval.e	⊢ 𝐸 = (hlG‘𝐺)
plngval.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
plngcp.a	⊢ (𝜑 → 𝐴 ∈ ran 𝐿)
plngcp.r	⊢ (𝜑 → 𝑅 ∈ (𝑃 ∖ 𝐴))
plngcp.s	⊢ (𝜑 → 𝑆 ∈ ((𝐴𝐸𝑅) ∖ 𝐴))
plngcplem.1	⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ 𝐴) ∧ 𝑏 ∈ (𝑃 ∖ 𝐴)) ∧ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑎𝐼𝑏))}

**Assertion**
Ref	Expression
plngcplem	⊢ (𝜑 → (𝐴𝐸𝑅) = (𝐴𝐸𝑆))

Distinct variable groups: 𝐴,𝑎,𝑏,𝑡 𝐺,𝑎,𝑏,𝑡 𝐼,𝑎,𝑏,𝑡 𝐿,𝑎,𝑏,𝑡 𝑂,𝑎,𝑏,𝑡 𝑃,𝑎,𝑏,𝑡 𝑅,𝑎,𝑏,𝑡 𝑆,𝑎,𝑏,𝑡 𝜑,𝑡 Allowed substitution hints: 𝜑(𝑎,𝑏) 𝐸(𝑡,𝑎,𝑏)

Proof of Theorem plngcplem Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		plngval.p	. . . . . . . . . . . 12 ⊢ 𝑃 = (Base‘𝐺)
2		plngval.i	. . . . . . . . . . . 12 ⊢ 𝐼 = (Itv‘𝐺)
3		plngval.1	. . . . . . . . . . . 12 ⊢ 𝐿 = (LineG‘𝐺)
4		plngcplem.1	. . . . . . . . . . . 12 ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ 𝐴) ∧ 𝑏 ∈ (𝑃 ∖ 𝐴)) ∧ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑎𝐼𝑏))}
5		plngval.g	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
6	5	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑆𝑂𝑅) → 𝐺 ∈ TarskiG)
7		plngcp.a	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ ran 𝐿)
8	7	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑆𝑂𝑅) → 𝐴 ∈ ran 𝐿)
9		plngcp.r	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ (𝑃 ∖ 𝐴))
10	9	eldifad 3919	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 ∈ 𝑃)
11	10	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑆𝑂𝑅) → 𝑅 ∈ 𝑃)
12		simplr 780	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑆𝑂𝑅) → 𝑥 ∈ 𝑃)
13		plngval.e	. . . . . . . . . . . . . 14 ⊢ 𝐸 = (hlG‘𝐺)
14		plngcp.s	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑆 ∈ ((𝐴𝐸𝑅) ∖ 𝐴))
15	14	eldifad 3919	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ∈ (𝐴𝐸𝑅))
16	1, 2, 3, 13, 5, 7, 9, 15	plngssp 29011	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ∈ 𝑃)
17	16	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑆𝑂𝑅) → 𝑆 ∈ 𝑃)
18		eqid 2765	. . . . . . . . . . . . 13 ⊢ (dist‘𝐺) = (dist‘𝐺)
19		simpr 489	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑆𝑂𝑅) → 𝑆𝑂𝑅)
20	1, 18, 2, 4, 3, 8, 6, 17, 11, 19	oppcom 28975	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑆𝑂𝑅) → 𝑅𝑂𝑆)
21	1, 2, 3, 4, 6, 8, 11, 12, 17, 20	lnopp2hpgb 28994	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑆𝑂𝑅) → (𝑥𝑂𝑆 ↔ 𝑅((hpG‘𝐺)‘𝐴)𝑥))
22	21	adantlr 727	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) → (𝑥𝑂𝑆 ↔ 𝑅((hpG‘𝐺)‘𝐴)𝑥))
23	5	ad4antr 744	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) ∧ 𝑅((hpG‘𝐺)‘𝐴)𝑥) → 𝐺 ∈ TarskiG)
24	7	ad4antr 744	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) ∧ 𝑅((hpG‘𝐺)‘𝐴)𝑥) → 𝐴 ∈ ran 𝐿)
25	10	ad4antr 744	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) ∧ 𝑅((hpG‘𝐺)‘𝐴)𝑥) → 𝑅 ∈ 𝑃)
26		simp-4r 795	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) ∧ 𝑅((hpG‘𝐺)‘𝐴)𝑥) → 𝑥 ∈ 𝑃)
27		simpr 489	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) ∧ 𝑅((hpG‘𝐺)‘𝐴)𝑥) → 𝑅((hpG‘𝐺)‘𝐴)𝑥)
28	1, 2, 3, 23, 24, 25, 4, 26, 27	hpgcom 28998	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) ∧ 𝑅((hpG‘𝐺)‘𝐴)𝑥) → 𝑥((hpG‘𝐺)‘𝐴)𝑅)
29	5	ad4antr 744	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑅) → 𝐺 ∈ TarskiG)
30	7	ad4antr 744	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑅) → 𝐴 ∈ ran 𝐿)
31		simp-4r 795	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑅) → 𝑥 ∈ 𝑃)
32	10	ad4antr 744	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑅) → 𝑅 ∈ 𝑃)
33		simpr 489	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑅) → 𝑥((hpG‘𝐺)‘𝐴)𝑅)
34	1, 2, 3, 29, 30, 31, 4, 32, 33	hpgcom 28998	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑅) → 𝑅((hpG‘𝐺)‘𝐴)𝑥)
35	28, 34	impbida 812	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) → (𝑅((hpG‘𝐺)‘𝐴)𝑥 ↔ 𝑥((hpG‘𝐺)‘𝐴)𝑅))
36	22, 35	bitr2d 283	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) → (𝑥((hpG‘𝐺)‘𝐴)𝑅 ↔ 𝑥𝑂𝑆))
37	1, 2, 3, 4, 6, 8, 17, 12, 11, 19	lnopp2hpgb 28994	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑆𝑂𝑅) → (𝑥𝑂𝑅 ↔ 𝑆((hpG‘𝐺)‘𝐴)𝑥))
38	37	adantlr 727	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) → (𝑥𝑂𝑅 ↔ 𝑆((hpG‘𝐺)‘𝐴)𝑥))
39	5	ad4antr 744	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑥) → 𝐺 ∈ TarskiG)
40	7	ad4antr 744	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑥) → 𝐴 ∈ ran 𝐿)
41	16	ad4antr 744	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑥) → 𝑆 ∈ 𝑃)
42		simp-4r 795	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑥) → 𝑥 ∈ 𝑃)
43		simpr 489	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑥) → 𝑆((hpG‘𝐺)‘𝐴)𝑥)
44	1, 2, 3, 39, 40, 41, 4, 42, 43	hpgcom 28998	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑥) → 𝑥((hpG‘𝐺)‘𝐴)𝑆)
45	5	ad4antr 744	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑆) → 𝐺 ∈ TarskiG)
46	7	ad4antr 744	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑆) → 𝐴 ∈ ran 𝐿)
47		simp-4r 795	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑆) → 𝑥 ∈ 𝑃)
48	16	ad4antr 744	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑆) → 𝑆 ∈ 𝑃)
49		simpr 489	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑆) → 𝑥((hpG‘𝐺)‘𝐴)𝑆)
50	1, 2, 3, 45, 46, 47, 4, 48, 49	hpgcom 28998	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑆) → 𝑆((hpG‘𝐺)‘𝐴)𝑥)
51	44, 50	impbida 812	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) → (𝑆((hpG‘𝐺)‘𝐴)𝑥 ↔ 𝑥((hpG‘𝐺)‘𝐴)𝑆))
52	38, 51	bitrd 282	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) → (𝑥𝑂𝑅 ↔ 𝑥((hpG‘𝐺)‘𝐴)𝑆))
53	36, 52	orbi12d 931	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) → ((𝑥((hpG‘𝐺)‘𝐴)𝑅 ∨ 𝑥𝑂𝑅) ↔ (𝑥𝑂𝑆 ∨ 𝑥((hpG‘𝐺)‘𝐴)𝑆)))
54		orcom 883	. . . . . . . 8 ⊢ ((𝑥𝑂𝑆 ∨ 𝑥((hpG‘𝐺)‘𝐴)𝑆) ↔ (𝑥((hpG‘𝐺)‘𝐴)𝑆 ∨ 𝑥𝑂𝑆))
55	53, 54	bitrdi 290	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆𝑂𝑅) → ((𝑥((hpG‘𝐺)‘𝐴)𝑅 ∨ 𝑥𝑂𝑅) ↔ (𝑥((hpG‘𝐺)‘𝐴)𝑆 ∨ 𝑥𝑂𝑆)))
56	5	ad4antr 744	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑅) → 𝐺 ∈ TarskiG)
57	7	ad4antr 744	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑅) → 𝐴 ∈ ran 𝐿)
58		simp-4r 795	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑅) → 𝑥 ∈ 𝑃)
59	10	ad4antr 744	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑅) → 𝑅 ∈ 𝑃)
60		simpr 489	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑅) → 𝑥((hpG‘𝐺)‘𝐴)𝑅)
61	16	ad4antr 744	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑅) → 𝑆 ∈ 𝑃)
62		simplr 780	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑅) → 𝑆((hpG‘𝐺)‘𝐴)𝑅)
63	1, 2, 3, 56, 57, 61, 4, 59, 62	hpgcom 28998	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑅) → 𝑅((hpG‘𝐺)‘𝐴)𝑆)
64	1, 2, 3, 56, 57, 58, 4, 59, 60, 61, 63	hpgtr 28999	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑅) → 𝑥((hpG‘𝐺)‘𝐴)𝑆)
65	5	ad4antr 744	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑆) → 𝐺 ∈ TarskiG)
66	7	ad4antr 744	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑆) → 𝐴 ∈ ran 𝐿)
67		simp-4r 795	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑆) → 𝑥 ∈ 𝑃)
68	16	ad4antr 744	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑆) → 𝑆 ∈ 𝑃)
69		simpr 489	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑆) → 𝑥((hpG‘𝐺)‘𝐴)𝑆)
70	10	ad4antr 744	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑆) → 𝑅 ∈ 𝑃)
71		simplr 780	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑆) → 𝑆((hpG‘𝐺)‘𝐴)𝑅)
72	1, 2, 3, 65, 66, 67, 4, 68, 69, 70, 71	hpgtr 28999	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑆) → 𝑥((hpG‘𝐺)‘𝐴)𝑅)
73	64, 72	impbida 812	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) → (𝑥((hpG‘𝐺)‘𝐴)𝑅 ↔ 𝑥((hpG‘𝐺)‘𝐴)𝑆))
74	7	ad4antr 744	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑅) → 𝐴 ∈ ran 𝐿)
75	5	ad4antr 744	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑅) → 𝐺 ∈ TarskiG)
76	16	ad4antr 744	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑅) → 𝑆 ∈ 𝑃)
77		simp-4r 795	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑅) → 𝑥 ∈ 𝑃)
78	10	ad4antr 744	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑅) → 𝑅 ∈ 𝑃)
79		simplr 780	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑅) → 𝑆((hpG‘𝐺)‘𝐴)𝑅)
80	1, 2, 3, 75, 74, 76, 4, 78, 79	hpgcom 28998	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑅) → 𝑅((hpG‘𝐺)‘𝐴)𝑆)
81		simpr 489	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑅) → 𝑥𝑂𝑅)
82	1, 18, 2, 4, 3, 74, 75, 77, 78, 81	oppcom 28975	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑅) → 𝑅𝑂𝑥)
83	1, 2, 3, 4, 75, 74, 78, 76, 77, 82	lnopp2hpgb 28994	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑅) → (𝑆𝑂𝑥 ↔ 𝑅((hpG‘𝐺)‘𝐴)𝑆))
84	80, 83	mpbird 260	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑅) → 𝑆𝑂𝑥)
85	1, 18, 2, 4, 3, 74, 75, 76, 77, 84	oppcom 28975	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑅) → 𝑥𝑂𝑆)
86	7	ad4antr 744	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑆) → 𝐴 ∈ ran 𝐿)
87	5	ad4antr 744	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑆) → 𝐺 ∈ TarskiG)
88	10	ad4antr 744	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑆) → 𝑅 ∈ 𝑃)
89		simp-4r 795	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑆) → 𝑥 ∈ 𝑃)
90		simplr 780	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑆) → 𝑆((hpG‘𝐺)‘𝐴)𝑅)
91	16	ad4antr 744	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑆) → 𝑆 ∈ 𝑃)
92		simpr 489	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑆) → 𝑥𝑂𝑆)
93	1, 18, 2, 4, 3, 86, 87, 89, 91, 92	oppcom 28975	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑆) → 𝑆𝑂𝑥)
94	1, 2, 3, 4, 87, 86, 91, 88, 89, 93	lnopp2hpgb 28994	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑆) → (𝑅𝑂𝑥 ↔ 𝑆((hpG‘𝐺)‘𝐴)𝑅))
95	90, 94	mpbird 260	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑆) → 𝑅𝑂𝑥)
96	1, 18, 2, 4, 3, 86, 87, 88, 89, 95	oppcom 28975	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑆) → 𝑥𝑂𝑅)
97	85, 96	impbida 812	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) → (𝑥𝑂𝑅 ↔ 𝑥𝑂𝑆))
98	73, 97	orbi12d 931	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) → ((𝑥((hpG‘𝐺)‘𝐴)𝑅 ∨ 𝑥𝑂𝑅) ↔ (𝑥((hpG‘𝐺)‘𝐴)𝑆 ∨ 𝑥𝑂𝑆)))
99		eleq1 2853	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑆 → (𝑦 ∈ 𝐴 ↔ 𝑆 ∈ 𝐴))
100		breq1 5108	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑆 → (𝑦((hpG‘𝐺)‘𝐴)𝑅 ↔ 𝑆((hpG‘𝐺)‘𝐴)𝑅))
101		oveq1 7407	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑆 → (𝑦𝐼𝑅) = (𝑆𝐼𝑅))
102	101	eleq2d 2851	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑆 → (𝑡 ∈ (𝑦𝐼𝑅) ↔ 𝑡 ∈ (𝑆𝐼𝑅)))
103	102	rexbidv 3189	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑆 → (∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑦𝐼𝑅) ↔ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑆𝐼𝑅)))
104	99, 100, 103	3orbi123d 1459	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑆 → ((𝑦 ∈ 𝐴 ∨ 𝑦((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑦𝐼𝑅)) ↔ (𝑆 ∈ 𝐴 ∨ 𝑆((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑆𝐼𝑅))))
105	1, 2, 3, 13, 5, 7, 9	plngval 29007	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴𝐸𝑅) = {𝑦 ∈ 𝑃 ∣ (𝑦 ∈ 𝐴 ∨ 𝑦((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑦𝐼𝑅))})
106	15, 105	eleqtrd 2867	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ∈ {𝑦 ∈ 𝑃 ∣ (𝑦 ∈ 𝐴 ∨ 𝑦((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑦𝐼𝑅))})
107	104, 106	elrabrd 3656	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 ∈ 𝐴 ∨ 𝑆((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑆𝐼𝑅)))
108		3orass 1104	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ 𝐴 ∨ 𝑆((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑆𝐼𝑅)) ↔ (𝑆 ∈ 𝐴 ∨ (𝑆((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑆𝐼𝑅))))
109	107, 108	sylib 221	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆 ∈ 𝐴 ∨ (𝑆((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑆𝐼𝑅))))
110	14	eldifbd 3920	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ 𝑆 ∈ 𝐴)
111	109, 110	orcnd 891	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑆𝐼𝑅)))
112	1, 18, 2, 4, 16, 10	islnopp 28970	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆𝑂𝑅 ↔ ((¬ 𝑆 ∈ 𝐴 ∧ ¬ 𝑅 ∈ 𝐴) ∧ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑆𝐼𝑅))))
113	9	eldifbd 3920	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ 𝑅 ∈ 𝐴)
114	110, 113	jca 520	. . . . . . . . . . . . 13 ⊢ (𝜑 → (¬ 𝑆 ∈ 𝐴 ∧ ¬ 𝑅 ∈ 𝐴))
115	114	biantrurd 541	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑆𝐼𝑅) ↔ ((¬ 𝑆 ∈ 𝐴 ∧ ¬ 𝑅 ∈ 𝐴) ∧ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑆𝐼𝑅))))
116	112, 115	bitr4d 285	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆𝑂𝑅 ↔ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑆𝐼𝑅)))
117	116	orbi2d 928	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑆((hpG‘𝐺)‘𝐴)𝑅 ∨ 𝑆𝑂𝑅) ↔ (𝑆((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑆𝐼𝑅))))
118	111, 117	mpbird 260	. . . . . . . . 9 ⊢ (𝜑 → (𝑆((hpG‘𝐺)‘𝐴)𝑅 ∨ 𝑆𝑂𝑅))
119	118	orcomd 884	. . . . . . . 8 ⊢ (𝜑 → (𝑆𝑂𝑅 ∨ 𝑆((hpG‘𝐺)‘𝐴)𝑅))
120	119	ad2antrr 738	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑆𝑂𝑅 ∨ 𝑆((hpG‘𝐺)‘𝐴)𝑅))
121	55, 98, 120	mpjaodan 973	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) → ((𝑥((hpG‘𝐺)‘𝐴)𝑅 ∨ 𝑥𝑂𝑅) ↔ (𝑥((hpG‘𝐺)‘𝐴)𝑆 ∨ 𝑥𝑂𝑆)))
122		simpr 489	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) → ¬ 𝑥 ∈ 𝐴)
123	113	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) → ¬ 𝑅 ∈ 𝐴)
124	122, 123	jca 520	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) → (¬ 𝑥 ∈ 𝐴 ∧ ¬ 𝑅 ∈ 𝐴))
125	124	biantrurd 541	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) → (∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑅) ↔ ((¬ 𝑥 ∈ 𝐴 ∧ ¬ 𝑅 ∈ 𝐴) ∧ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑅))))
126		simpr 489	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → 𝑥 ∈ 𝑃)
127	10	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → 𝑅 ∈ 𝑃)
128	1, 18, 2, 4, 126, 127	islnopp 28970	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → (𝑥𝑂𝑅 ↔ ((¬ 𝑥 ∈ 𝐴 ∧ ¬ 𝑅 ∈ 𝐴) ∧ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑅))))
129	128	adantr 485	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑥𝑂𝑅 ↔ ((¬ 𝑥 ∈ 𝐴 ∧ ¬ 𝑅 ∈ 𝐴) ∧ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑅))))
130	125, 129	bitr4d 285	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) → (∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑅) ↔ 𝑥𝑂𝑅))
131	130	orbi2d 928	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) → ((𝑥((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑅)) ↔ (𝑥((hpG‘𝐺)‘𝐴)𝑅 ∨ 𝑥𝑂𝑅)))
132	110	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) → ¬ 𝑆 ∈ 𝐴)
133	122, 132	jca 520	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) → (¬ 𝑥 ∈ 𝐴 ∧ ¬ 𝑆 ∈ 𝐴))
134	133	biantrurd 541	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) → (∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑆) ↔ ((¬ 𝑥 ∈ 𝐴 ∧ ¬ 𝑆 ∈ 𝐴) ∧ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑆))))
135	16	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → 𝑆 ∈ 𝑃)
136	1, 18, 2, 4, 126, 135	islnopp 28970	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → (𝑥𝑂𝑆 ↔ ((¬ 𝑥 ∈ 𝐴 ∧ ¬ 𝑆 ∈ 𝐴) ∧ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑆))))
137	136	adantr 485	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑥𝑂𝑆 ↔ ((¬ 𝑥 ∈ 𝐴 ∧ ¬ 𝑆 ∈ 𝐴) ∧ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑆))))
138	134, 137	bitr4d 285	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) → (∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑆) ↔ 𝑥𝑂𝑆))
139	138	orbi2d 928	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) → ((𝑥((hpG‘𝐺)‘𝐴)𝑆 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑆)) ↔ (𝑥((hpG‘𝐺)‘𝐴)𝑆 ∨ 𝑥𝑂𝑆)))
140	121, 131, 139	3bitr4d 314	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) → ((𝑥((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑅)) ↔ (𝑥((hpG‘𝐺)‘𝐴)𝑆 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑆))))
141	140	pm5.74da 815	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → ((¬ 𝑥 ∈ 𝐴 → (𝑥((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑅))) ↔ (¬ 𝑥 ∈ 𝐴 → (𝑥((hpG‘𝐺)‘𝐴)𝑆 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑆)))))
142		3orass 1104	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑅)) ↔ (𝑥 ∈ 𝐴 ∨ (𝑥((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑅))))
143		df-or 861	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∨ (𝑥((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑅))) ↔ (¬ 𝑥 ∈ 𝐴 → (𝑥((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑅))))
144	142, 143	bitri 278	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑅)) ↔ (¬ 𝑥 ∈ 𝐴 → (𝑥((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑅))))
145		3orass 1104	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥((hpG‘𝐺)‘𝐴)𝑆 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑆)) ↔ (𝑥 ∈ 𝐴 ∨ (𝑥((hpG‘𝐺)‘𝐴)𝑆 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑆))))
146		df-or 861	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∨ (𝑥((hpG‘𝐺)‘𝐴)𝑆 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑆))) ↔ (¬ 𝑥 ∈ 𝐴 → (𝑥((hpG‘𝐺)‘𝐴)𝑆 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑆))))
147	145, 146	bitri 278	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥((hpG‘𝐺)‘𝐴)𝑆 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑆)) ↔ (¬ 𝑥 ∈ 𝐴 → (𝑥((hpG‘𝐺)‘𝐴)𝑆 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑆))))
148	141, 144, 147	3bitr4g 317	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑃) → ((𝑥 ∈ 𝐴 ∨ 𝑥((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑅)) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥((hpG‘𝐺)‘𝐴)𝑆 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑆))))
149	148	rabbidva 3423	. 2 ⊢ (𝜑 → {𝑥 ∈ 𝑃 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑅))} = {𝑥 ∈ 𝑃 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥((hpG‘𝐺)‘𝐴)𝑆 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑆))})
150	1, 2, 3, 13, 5, 7, 9	plngval 29007	. 2 ⊢ (𝜑 → (𝐴𝐸𝑅) = {𝑥 ∈ 𝑃 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑅))})
151	16, 110	eldifd 3918	. . 3 ⊢ (𝜑 → 𝑆 ∈ (𝑃 ∖ 𝐴))
152	1, 2, 3, 13, 5, 7, 151	plngval 29007	. 2 ⊢ (𝜑 → (𝐴𝐸𝑆) = {𝑥 ∈ 𝑃 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥((hpG‘𝐺)‘𝐴)𝑆 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑆))})
153	149, 150, 152	3eqtr4d 2810	1 ⊢ (𝜑 → (𝐴𝐸𝑅) = (𝐴𝐸𝑆))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 ∨ w3o 1100 = wceq 1563 ∈ wcel 2145 ∃wrex 3089 {crab 3417 ∖ cdif 3904 class class class wbr 5105 {copab 5167 ran crn 5653 ‘cfv 6525 (class class class)co 7400 Basecbs 17259 distcds 17309 TarskiGcstrkg 28654 Itvcitv 28660 LineGclng 28661 hpGchpg 28988 hlGcplng 29003

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-rep 5232 ax-sep 5251 ax-nul 5261 ax-pow 5327 ax-pr 5395 ax-un 7722 ax-cnex 11144 ax-resscn 11145 ax-1cn 11146 ax-icn 11147 ax-addcl 11148 ax-addrcl 11149 ax-mulcl 11150 ax-mulrcl 11151 ax-mulcom 11152 ax-addass 11153 ax-mulass 11154 ax-distr 11155 ax-i2m1 11156 ax-1ne0 11157 ax-1rid 11158 ax-rnegex 11159 ax-rrecex 11160 ax-cnre 11161 ax-pre-lttri 11162 ax-pre-lttrn 11163 ax-pre-ltadd 11164 ax-pre-mulgt0 11165

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3370 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4869 df-int 4909 df-iun 4954 df-br 5106 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5547 df-eprel 5552 df-po 5560 df-so 5561 df-fr 5605 df-we 5607 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-res 5664 df-ima 5665 df-pred 6292 df-ord 6353 df-on 6354 df-lim 6355 df-suc 6356 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-riota 7357 df-ov 7403 df-oprab 7404 df-mpo 7405 df-om 7851 df-1st 7974 df-2nd 7975 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-1o 8441 df-oadd 8445 df-er 8682 df-map 8814 df-pm 8815 df-en 8932 df-dom 8933 df-sdom 8934 df-fin 8935 df-dju 9875 df-card 9913 df-pnf 11233 df-mnf 11234 df-xr 11235 df-ltxr 11236 df-le 11237 df-sub 11431 df-neg 11432 df-nn 12225 df-2 12294 df-3 12295 df-n0 12496 df-xnn0 12569 df-z 12583 df-uz 12854 df-fz 13527 df-fzo 13674 df-hash 14358 df-word 14541 df-concat 14598 df-s1 14624 df-s2 14875 df-s3 14876 df-trkgc 28675 df-trkgb 28676 df-trkgcb 28677 df-trkgld 28679 df-trkg 28680 df-cgrg 28738 df-leg 28810 df-hlg 28828 df-mir 28884 df-rag 28925 df-perpg 28927 df-hpg 28989 df-plng 29004

This theorem is referenced by: plngcp 29016

W3C validator