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 29024

Description: Lemma for plngcp 29025. (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 3925	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 ∈ 𝑃)
11	10	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑆𝑂𝑅) → 𝑅 ∈ 𝑃)
12		simplr 780	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑆𝑂𝑅) → 𝑥 ∈ 𝑃)
13		plngval.e	. . . . . . . . . . . . . 14 ⊢ 𝐸 = (hlG‘𝐺)
14		plngcp.s	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑆 ∈ ((𝐴𝐸𝑅) ∖ 𝐴))
15	14	eldifad 3925	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ∈ (𝐴𝐸𝑅))
16	1, 2, 3, 13, 5, 7, 9, 15	plngssp 29020	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ∈ 𝑃)
17	16	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑆𝑂𝑅) → 𝑆 ∈ 𝑃)
18		eqid 2769	. . . . . . . . . . . . 13 ⊢ (dist‘𝐺) = (dist‘𝐺)
19		simpr 489	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑆𝑂𝑅) → 𝑆𝑂𝑅)
20	1, 18, 2, 4, 3, 8, 6, 17, 11, 19	oppcom 28983	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑆𝑂𝑅) → 𝑅𝑂𝑆)
21	1, 2, 3, 4, 6, 8, 11, 12, 17, 20	lnopp2hpgb 29003	. . . . . . . . . . 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 29007	. . . . . . . . . . 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 29007	. . . . . . . . . . 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 29003	. . . . . . . . . . 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 29007	. . . . . . . . . . 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 29007	. . . . . . . . . . 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 29007	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥((hpG‘𝐺)‘𝐴)𝑅) → 𝑅((hpG‘𝐺)‘𝐴)𝑆)
64	1, 2, 3, 56, 57, 58, 4, 59, 60, 61, 63	hpgtr 29008	. . . . . . . . 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 29008	. . . . . . . . 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 29007	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑅) → 𝑅((hpG‘𝐺)‘𝐴)𝑆)
81		simpr 489	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑅) → 𝑥𝑂𝑅)
82	1, 18, 2, 4, 3, 74, 75, 77, 78, 81	oppcom 28983	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑅) → 𝑅𝑂𝑥)
83	1, 2, 3, 4, 75, 74, 78, 76, 77, 82	lnopp2hpgb 29003	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑅) → (𝑆𝑂𝑥 ↔ 𝑅((hpG‘𝐺)‘𝐴)𝑆))
84	80, 83	mpbird 260	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑅) → 𝑆𝑂𝑥)
85	1, 18, 2, 4, 3, 74, 75, 76, 77, 84	oppcom 28983	. . . . . . . . 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 28983	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑆) → 𝑆𝑂𝑥)
94	1, 2, 3, 4, 87, 86, 91, 88, 89, 93	lnopp2hpgb 29003	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑆) → (𝑅𝑂𝑥 ↔ 𝑆((hpG‘𝐺)‘𝐴)𝑅))
95	90, 94	mpbird 260	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑆) → 𝑅𝑂𝑥)
96	1, 18, 2, 4, 3, 86, 87, 88, 89, 95	oppcom 28983	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) ∧ 𝑥𝑂𝑆) → 𝑥𝑂𝑅)
97	85, 96	impbida 812	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) → (𝑥𝑂𝑅 ↔ 𝑥𝑂𝑆))
98	73, 97	orbi12d 931	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ ¬ 𝑥 ∈ 𝐴) ∧ 𝑆((hpG‘𝐺)‘𝐴)𝑅) → ((𝑥((hpG‘𝐺)‘𝐴)𝑅 ∨ 𝑥𝑂𝑅) ↔ (𝑥((hpG‘𝐺)‘𝐴)𝑆 ∨ 𝑥𝑂𝑆)))
99		eleq1 2857	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑆 → (𝑦 ∈ 𝐴 ↔ 𝑆 ∈ 𝐴))
100		breq1 5116	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑆 → (𝑦((hpG‘𝐺)‘𝐴)𝑅 ↔ 𝑆((hpG‘𝐺)‘𝐴)𝑅))
101		oveq1 7418	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑆 → (𝑦𝐼𝑅) = (𝑆𝐼𝑅))
102	101	eleq2d 2855	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑆 → (𝑡 ∈ (𝑦𝐼𝑅) ↔ 𝑡 ∈ (𝑆𝐼𝑅)))
103	102	rexbidv 3195	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑆 → (∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑦𝐼𝑅) ↔ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑆𝐼𝑅)))
104	99, 100, 103	3orbi123d 1461	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑆 → ((𝑦 ∈ 𝐴 ∨ 𝑦((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑦𝐼𝑅)) ↔ (𝑆 ∈ 𝐴 ∨ 𝑆((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑆𝐼𝑅))))
105	1, 2, 3, 13, 5, 7, 9	plngval 29016	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴𝐸𝑅) = {𝑦 ∈ 𝑃 ∣ (𝑦 ∈ 𝐴 ∨ 𝑦((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑦𝐼𝑅))})
106	15, 105	eleqtrd 2871	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ∈ {𝑦 ∈ 𝑃 ∣ (𝑦 ∈ 𝐴 ∨ 𝑦((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑦𝐼𝑅))})
107	104, 106	elrabrd 3662	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 ∈ 𝐴 ∨ 𝑆((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑆𝐼𝑅)))
108		3orass 1104	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ 𝐴 ∨ 𝑆((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑆𝐼𝑅)) ↔ (𝑆 ∈ 𝐴 ∨ (𝑆((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑆𝐼𝑅))))
109	107, 108	sylib 221	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆 ∈ 𝐴 ∨ (𝑆((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑆𝐼𝑅))))
110	14	eldifbd 3926	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ 𝑆 ∈ 𝐴)
111	109, 110	orcnd 891	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑆𝐼𝑅)))
112	1, 18, 2, 4, 16, 10	islnopp 28978	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆𝑂𝑅 ↔ ((¬ 𝑆 ∈ 𝐴 ∧ ¬ 𝑅 ∈ 𝐴) ∧ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑆𝐼𝑅))))
113	9	eldifbd 3926	. . . . . . . . . . . . . 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 28978	. . . . . . . . 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 28978	. . . . . . . . 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 3429	. 2 ⊢ (𝜑 → {𝑥 ∈ 𝑃 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑅))} = {𝑥 ∈ 𝑃 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥((hpG‘𝐺)‘𝐴)𝑆 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑆))})
150	1, 2, 3, 13, 5, 7, 9	plngval 29016	. 2 ⊢ (𝜑 → (𝐴𝐸𝑅) = {𝑥 ∈ 𝑃 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥((hpG‘𝐺)‘𝐴)𝑅 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑅))})
151	16, 110	eldifd 3924	. . 3 ⊢ (𝜑 → 𝑆 ∈ (𝑃 ∖ 𝐴))
152	1, 2, 3, 13, 5, 7, 151	plngval 29016	. 2 ⊢ (𝜑 → (𝐴𝐸𝑆) = {𝑥 ∈ 𝑃 ∣ (𝑥 ∈ 𝐴 ∨ 𝑥((hpG‘𝐺)‘𝐴)𝑆 ∨ ∃𝑡 ∈ 𝐴 𝑡 ∈ (𝑥𝐼𝑆))})
153	149, 150, 152	3eqtr4d 2814	1 ⊢ (𝜑 → (𝐴𝐸𝑅) = (𝐴𝐸𝑆))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 ∨ w3o 1100 = wceq 1567 ∈ wcel 2149 ∃wrex 3095 {crab 3423 ∖ cdif 3910 class class class wbr 5113 {copab 5177 ran crn 5663 ‘cfv 6537 (class class class)co 7411 Basecbs 17268 distcds 17318 TarskiGcstrkg 28661 Itvcitv 28667 LineGclng 28668 hpGchpg 28997 hlGcplng 29012

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-tp 4599 df-op 4601 df-uni 4877 df-int 4917 df-iun 4962 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7862 df-1st 7985 df-2nd 7986 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-oadd 8456 df-er 8693 df-map 8825 df-pm 8826 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-dju 9886 df-card 9924 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-nn 12233 df-2 12302 df-3 12303 df-n0 12504 df-xnn0 12577 df-z 12591 df-uz 12862 df-fz 13535 df-fzo 13682 df-hash 14366 df-word 14550 df-concat 14607 df-s1 14633 df-s2 14884 df-s3 14885 df-trkgc 28682 df-trkgb 28683 df-trkgcb 28684 df-trkgld 28686 df-trkg 28687 df-cgrg 28745 df-leg 28817 df-hlg 28835 df-mir 28891 df-rag 28932 df-perpg 28934 df-hpg 28998 df-plng 29013

This theorem is referenced by: plngcp 29025

W3C validator