Theorem outpasch 25447

Description: Axiom of Pasch, outer form. This was proven by Gupta from other axioms and is therefore presented as Theorem 9.6 in [Schwabhauser] p. 70. (Contributed by Thierry Arnoux, 16-Aug-2020.)

Hypotheses

Ref	Expression
outpasch.p	⊢ 𝑃 = (Base‘𝐺)
outpasch.i	⊢ 𝐼 = (Itv‘𝐺)
outpasch.l	⊢ 𝐿 = (LineG‘𝐺)
outpasch.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
outpasch.a	⊢ (𝜑 → 𝐴 ∈ 𝑃)
outpasch.b	⊢ (𝜑 → 𝐵 ∈ 𝑃)
outpasch.c	⊢ (𝜑 → 𝐶 ∈ 𝑃)
outpasch.r	⊢ (𝜑 → 𝑅 ∈ 𝑃)
outpasch.q	⊢ (𝜑 → 𝑄 ∈ 𝑃)
outpasch.1	⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝑅))
outpasch.2	⊢ (𝜑 → 𝑄 ∈ (𝐵𝐼𝐶))

Assertion

Ref	Expression
outpasch	⊢ (𝜑 → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐶   𝑥,𝐺   𝑥,𝐼   𝑥,𝐿   𝑥,𝑃   𝑥,𝑄   𝑥,𝑅   𝜑,𝑥

Proof of Theorem outpasch

Dummy variables 𝑡 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		outpasch.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
2	1	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝐴 ∈ 𝑃)
3		simpr 476	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑥 = 𝐴) → 𝑥 = 𝐴)
4	3	eleq1d 2672	. . . . . 6 ⊢ (((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑥 = 𝐴) → (𝑥 ∈ (𝐴𝐼𝐵) ↔ 𝐴 ∈ (𝐴𝐼𝐵)))
5	3	oveq2d 6565	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑥 = 𝐴) → (𝑅𝐼𝑥) = (𝑅𝐼𝐴))
6	5	eleq2d 2673	. . . . . 6 ⊢ (((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑥 = 𝐴) → (𝑄 ∈ (𝑅𝐼𝑥) ↔ 𝑄 ∈ (𝑅𝐼𝐴)))
7	4, 6	anbi12d 743	. . . . 5 ⊢ (((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑥 = 𝐴) → ((𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)) ↔ (𝐴 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝐴))))
8		outpasch.p	. . . . . . . 8 ⊢ 𝑃 = (Base‘𝐺)
9		eqid 2610	. . . . . . . 8 ⊢ (dist‘𝐺) = (dist‘𝐺)
10		outpasch.i	. . . . . . . 8 ⊢ 𝐼 = (Itv‘𝐺)
11		outpasch.g	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
12		outpasch.b	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
13	8, 9, 10, 11, 1, 12	tgbtwntriv1 25186	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ (𝐴𝐼𝐵))
14	13	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝐴 ∈ (𝐴𝐼𝐵))
15	11	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝐺 ∈ TarskiG)
16		outpasch.r	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ 𝑃)
17	16	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝑅 ∈ 𝑃)
18		outpasch.q	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ 𝑃)
19	18	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝑄 ∈ 𝑃)
20		outpasch.c	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
21	20	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝐶 ∈ 𝑃)
22		simpr 476	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝑄 ∈ (𝑅𝐼𝐶))
23		outpasch.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝑅))
24	8, 9, 10, 11, 1, 20, 16, 23	tgbtwncom 25183	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ (𝑅𝐼𝐴))
25	24	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝐶 ∈ (𝑅𝐼𝐴))
26	8, 9, 10, 15, 17, 19, 21, 2, 22, 25	tgbtwnexch 25193	. . . . . 6 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝑄 ∈ (𝑅𝐼𝐴))
27	14, 26	jca 553	. . . . 5 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → (𝐴 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝐴)))
28	2, 7, 27	rspcedvd 3289	. . . 4 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))
29	28	adantlr 747	. . 3 ⊢ (((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))
30	12	ad2antrr 758	. . . 4 ⊢ (((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝐵 ∈ 𝑃)
31		eleq1 2676	. . . . . 6 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ (𝐴𝐼𝐵) ↔ 𝐵 ∈ (𝐴𝐼𝐵)))
32		eqidd 2611	. . . . . . 7 ⊢ (𝑥 = 𝐵 → 𝑄 = 𝑄)
33		oveq2 6557	. . . . . . 7 ⊢ (𝑥 = 𝐵 → (𝑅𝐼𝑥) = (𝑅𝐼𝐵))
34	32, 33	eleq12d 2682	. . . . . 6 ⊢ (𝑥 = 𝐵 → (𝑄 ∈ (𝑅𝐼𝑥) ↔ 𝑄 ∈ (𝑅𝐼𝐵)))
35	31, 34	anbi12d 743	. . . . 5 ⊢ (𝑥 = 𝐵 → ((𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)) ↔ (𝐵 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝐵))))
36	35	adantl 481	. . . 4 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑥 = 𝐵) → ((𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)) ↔ (𝐵 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝐵))))
37	8, 9, 10, 11, 1, 12	tgbtwntriv2 25182	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐵))
38	37	ad2antrr 758	. . . . 5 ⊢ (((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝐵 ∈ (𝐴𝐼𝐵))
39	11	ad2antrr 758	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝐺 ∈ TarskiG)
40	39	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝐺 ∈ TarskiG)
41	20	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝐶 ∈ 𝑃)
42	16	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝑅 ∈ 𝑃)
43	18	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝑄 ∈ 𝑃)
44	30	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝐵 ∈ 𝑃)
45		simpr 476	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝑅 ∈ (𝑄𝐼𝐶))
46	8, 9, 10, 40, 43, 42, 41, 45	tgbtwncom 25183	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝑅 ∈ (𝐶𝐼𝑄))
47		outpasch.2	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ (𝐵𝐼𝐶))
48	8, 9, 10, 11, 12, 18, 20, 47	tgbtwncom 25183	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ (𝐶𝐼𝐵))
49	48	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝑄 ∈ (𝐶𝐼𝐵))
50	8, 9, 10, 40, 41, 42, 43, 44, 46, 49	tgbtwnexch3 25189	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝑄 ∈ (𝑅𝐼𝐵))
51	39	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝐺 ∈ TarskiG)
52	30	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝐵 ∈ 𝑃)
53	18	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝑄 ∈ 𝑃)
54	16	ad3antrrr 762	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝑅 ∈ 𝑃)
55	20	ad3antrrr 762	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝐶 ∈ 𝑃)
56		simpr 476	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) ∧ 𝑄 = 𝐶) → 𝑄 = 𝐶)
57	8, 9, 10, 11, 16, 20	tgbtwntriv2 25182	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ (𝑅𝐼𝐶))
58	57	ad4antr 764	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) ∧ 𝑄 = 𝐶) → 𝐶 ∈ (𝑅𝐼𝐶))
59	56, 58	eqeltrd 2688	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) ∧ 𝑄 = 𝐶) → 𝑄 ∈ (𝑅𝐼𝐶))
60		simpllr 795	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) ∧ 𝑄 = 𝐶) → ¬ 𝑄 ∈ (𝑅𝐼𝐶))
61	59, 60	pm2.65da 598	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → ¬ 𝑄 = 𝐶)
62	61	neqned 2789	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝑄 ≠ 𝐶)
63	47	ad3antrrr 762	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝑄 ∈ (𝐵𝐼𝐶))
64		simpr 476	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝐶 ∈ (𝑄𝐼𝑅))
65	8, 9, 10, 51, 52, 53, 55, 54, 62, 63, 64	tgbtwnouttr 25192	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝑄 ∈ (𝐵𝐼𝑅))
66	8, 9, 10, 51, 52, 53, 54, 65	tgbtwncom 25183	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝑄 ∈ (𝑅𝐼𝐵))
67		outpasch.l	. . . . . . . . . . 11 ⊢ 𝐿 = (LineG‘𝐺)
68	8, 67, 10, 11, 18, 20, 16	tgcolg 25249	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶) ↔ (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝑄 ∈ (𝑅𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅))))
69	68	biimpa 500	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝑄 ∈ (𝑅𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅)))
70		3orcoma 1039	. . . . . . . . . 10 ⊢ ((𝑄 ∈ (𝑅𝐼𝐶) ∨ 𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅)) ↔ (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝑄 ∈ (𝑅𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅)))
71		3orass 1034	. . . . . . . . . 10 ⊢ ((𝑄 ∈ (𝑅𝐼𝐶) ∨ 𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅)) ↔ (𝑄 ∈ (𝑅𝐼𝐶) ∨ (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅))))
72	70, 71	bitr3i 265	. . . . . . . . 9 ⊢ ((𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝑄 ∈ (𝑅𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅)) ↔ (𝑄 ∈ (𝑅𝐼𝐶) ∨ (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅))))
73	69, 72	sylib 207	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → (𝑄 ∈ (𝑅𝐼𝐶) ∨ (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅))))
74	73	ord 391	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → (¬ 𝑄 ∈ (𝑅𝐼𝐶) → (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅))))
75	74	imp 444	. . . . . 6 ⊢ (((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) → (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅)))
76	50, 66, 75	mpjaodan 823	. . . . 5 ⊢ (((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝑄 ∈ (𝑅𝐼𝐵))
77	38, 76	jca 553	. . . 4 ⊢ (((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) → (𝐵 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝐵)))
78	30, 36, 77	rspcedvd 3289	. . 3 ⊢ (((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))
79	29, 78	pm2.61dan 828	. 2 ⊢ ((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))
80	12	ad2antrr 758	. . . 4 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐵 ∈ 𝑃)
81	35	adantl 481	. . . 4 ⊢ ((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 = 𝐵) → ((𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)) ↔ (𝐵 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝐵))))
82	37	ad2antrr 758	. . . . 5 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐵 ∈ (𝐴𝐼𝐵))
83	11	ad2antrr 758	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐺 ∈ TarskiG)
84	16	ad2antrr 758	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑅 ∈ 𝑃)
85	18	ad2antrr 758	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ 𝑃)
86	20	ad2antrr 758	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐶 ∈ 𝑃)
87		simplr 788	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶))
88		simpr 476	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐵 ∈ (𝑅𝐿𝑄))
89	11	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝐺 ∈ TarskiG)
90	16	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑅 ∈ 𝑃)
91	18	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑄 ∈ 𝑃)
92	20	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝐶 ∈ 𝑃)
93		simpr 476	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶))
94	8, 10, 67, 89, 90, 91, 92, 93	ncolne1 25320	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑅 ≠ 𝑄)
95	8, 10, 67, 89, 90, 91, 94	tglinerflx2 25329	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑄 ∈ (𝑅𝐿𝑄))
96	95	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ (𝑅𝐿𝑄))
97	8, 67, 10, 89, 91, 92, 90, 93	ncolcom 25256	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → ¬ (𝑅 ∈ (𝐶𝐿𝑄) ∨ 𝐶 = 𝑄))
98	8, 67, 10, 89, 92, 91, 90, 97	ncolrot1 25257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → ¬ (𝐶 ∈ (𝑄𝐿𝑅) ∨ 𝑄 = 𝑅))
99	8, 10, 67, 89, 92, 91, 90, 98	ncolne1 25320	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝐶 ≠ 𝑄)
100	99	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐶 ≠ 𝑄)
101	48	ad2antrr 758	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ (𝐶𝐼𝐵))
102	8, 10, 67, 83, 86, 85, 80, 100, 101	btwnlng3 25316	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐵 ∈ (𝐶𝐿𝑄))
103	8, 10, 67, 83, 86, 85, 100	tglinerflx2 25329	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ (𝐶𝐿𝑄))
104	8, 10, 67, 83, 84, 85, 86, 85, 87, 88, 96, 102, 103	tglineinteq 25340	. . . . . 6 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐵 = 𝑄)
105	8, 9, 10, 11, 16, 12	tgbtwntriv2 25182	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ (𝑅𝐼𝐵))
106	105	ad2antrr 758	. . . . . 6 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐵 ∈ (𝑅𝐼𝐵))
107	104, 106	eqeltrrd 2689	. . . . 5 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ (𝑅𝐼𝐵))
108	82, 107	jca 553	. . . 4 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → (𝐵 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝐵)))
109	80, 81, 108	rspcedvd 3289	. . 3 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))
110		eleq1 2676	. . . . . . . . . 10 ⊢ (𝑡 = 𝑥 → (𝑡 ∈ (𝑎𝐼𝑏) ↔ 𝑥 ∈ (𝑎𝐼𝑏)))
111	110	cbvrexv 3148	. . . . . . . . 9 ⊢ (∃𝑡 ∈ (𝑅𝐿𝑄)𝑡 ∈ (𝑎𝐼𝑏) ↔ ∃𝑥 ∈ (𝑅𝐿𝑄)𝑥 ∈ (𝑎𝐼𝑏))
112	111	anbi2i 726	. . . . . . . 8 ⊢ (((𝑎 ∈ (𝑃 ∖ (𝑅𝐿𝑄)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑅𝐿𝑄))) ∧ ∃𝑡 ∈ (𝑅𝐿𝑄)𝑡 ∈ (𝑎𝐼𝑏)) ↔ ((𝑎 ∈ (𝑃 ∖ (𝑅𝐿𝑄)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑅𝐿𝑄))) ∧ ∃𝑥 ∈ (𝑅𝐿𝑄)𝑥 ∈ (𝑎𝐼𝑏)))
113	112	opabbii 4649	. . . . . . 7 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑅𝐿𝑄)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑅𝐿𝑄))) ∧ ∃𝑡 ∈ (𝑅𝐿𝑄)𝑡 ∈ (𝑎𝐼𝑏))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑅𝐿𝑄)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑅𝐿𝑄))) ∧ ∃𝑥 ∈ (𝑅𝐿𝑄)𝑥 ∈ (𝑎𝐼𝑏))}
114	89	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐺 ∈ TarskiG)
115	90	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑅 ∈ 𝑃)
116	91	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ 𝑃)
117	94	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑅 ≠ 𝑄)
118	8, 10, 67, 114, 115, 116, 117	tgelrnln 25325	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → (𝑅𝐿𝑄) ∈ ran 𝐿)
119		eqid 2610	. . . . . . 7 ⊢ (hlG‘𝐺) = (hlG‘𝐺)
120	20	ad2antrr 758	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐶 ∈ 𝑃)
121	1	ad2antrr 758	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐴 ∈ 𝑃)
122	12	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝐵 ∈ 𝑃)
123	122	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐵 ∈ 𝑃)
124	95	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ (𝑅𝐿𝑄))
125	8, 67, 10, 89, 91, 92, 90, 93	ncolrot2 25258	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → ¬ (𝐶 ∈ (𝑅𝐿𝑄) ∨ 𝑅 = 𝑄))
126		pm2.45 411	. . . . . . . . . 10 ⊢ (¬ (𝐶 ∈ (𝑅𝐿𝑄) ∨ 𝑅 = 𝑄) → ¬ 𝐶 ∈ (𝑅𝐿𝑄))
127	125, 126	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → ¬ 𝐶 ∈ (𝑅𝐿𝑄))
128	127	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → ¬ 𝐶 ∈ (𝑅𝐿𝑄))
129		simpr 476	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → ¬ 𝐵 ∈ (𝑅𝐿𝑄))
130	48	ad2antrr 758	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ (𝐶𝐼𝐵))
131	8, 9, 10, 113, 120, 123, 124, 128, 129, 130	islnoppd 25432	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐶{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑅𝐿𝑄)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑅𝐿𝑄))) ∧ ∃𝑡 ∈ (𝑅𝐿𝑄)𝑡 ∈ (𝑎𝐼𝑏))}𝐵)
132	8, 10, 67, 89, 90, 91, 94	tglinerflx1 25328	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑅 ∈ (𝑅𝐿𝑄))
133	132	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑅 ∈ (𝑅𝐿𝑄))
134	23	ad2antrr 758	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐶 ∈ (𝐴𝐼𝑅))
135	24	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐶 ∈ (𝑅𝐼𝐴))
136	8, 10, 67, 89, 92, 90, 91, 125	ncolne1 25320	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝐶 ≠ 𝑅)
137	136	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐶 ≠ 𝑅)
138	8, 9, 10, 114, 115, 120, 121, 135, 137	tgbtwnne 25185	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑅 ≠ 𝐴)
139	138	necomd 2837	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐴 ≠ 𝑅)
140	8, 10, 119, 121, 115, 120, 114, 121, 134, 139, 137	btwnhl2 25308	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐶((hlG‘𝐺)‘𝑅)𝐴)
141	8, 9, 10, 113, 67, 118, 114, 119, 120, 121, 123, 131, 133, 140	opphl 25446	. . . . . 6 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐴{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑅𝐿𝑄)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑅𝐿𝑄))) ∧ ∃𝑡 ∈ (𝑅𝐿𝑄)𝑡 ∈ (𝑎𝐼𝑏))}𝐵)
142	8, 9, 10, 113, 121, 123	islnopp 25431	. . . . . 6 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → (𝐴{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑅𝐿𝑄)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑅𝐿𝑄))) ∧ ∃𝑡 ∈ (𝑅𝐿𝑄)𝑡 ∈ (𝑎𝐼𝑏))}𝐵 ↔ ((¬ 𝐴 ∈ (𝑅𝐿𝑄) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ ∃𝑥 ∈ (𝑅𝐿𝑄)𝑥 ∈ (𝐴𝐼𝐵))))
143	141, 142	mpbid 221	. . . . 5 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → ((¬ 𝐴 ∈ (𝑅𝐿𝑄) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ ∃𝑥 ∈ (𝑅𝐿𝑄)𝑥 ∈ (𝐴𝐼𝐵)))
144	143	simprd 478	. . . 4 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → ∃𝑥 ∈ (𝑅𝐿𝑄)𝑥 ∈ (𝐴𝐼𝐵))
145	114	ad2antrr 758	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝐺 ∈ TarskiG)
146	118	ad2antrr 758	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → (𝑅𝐿𝑄) ∈ ran 𝐿)
147		simplr 788	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝑥 ∈ (𝑅𝐿𝑄))
148	8, 67, 10, 145, 146, 147	tglnpt 25244	. . . . . . . 8 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝑥 ∈ 𝑃)
149		simpr 476	. . . . . . . 8 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝑥 ∈ (𝐴𝐼𝐵))
150	145	ad2antrr 758	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝐺 ∈ TarskiG)
151	90	ad3antrrr 762	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝑅 ∈ 𝑃)
152	151	ad2antrr 758	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑅 ∈ 𝑃)
153	91	ad5antr 766	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑄 ∈ 𝑃)
154	120	ad2antrr 758	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝐶 ∈ 𝑃)
155	154	ad2antrr 758	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝐶 ∈ 𝑃)
156	93	ad5antr 766	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶))
157		simplr 788	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ 𝑃)
158	117	ad4antr 764	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑅 ≠ 𝑄)
159	148	ad2antrr 758	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑥 ∈ 𝑃)
160	94	necomd 2837	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑄 ≠ 𝑅)
161	160	ad5antr 766	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑄 ≠ 𝑅)
162	147	ad2antrr 758	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑥 ∈ (𝑅𝐿𝑄))
163	8, 10, 67, 150, 153, 152, 159, 161, 162	lncom 25317	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑥 ∈ (𝑄𝐿𝑅))
164		simprl 790	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝑥𝐼𝑅))
165	8, 10, 67, 150, 159, 153, 152, 157, 163, 164	coltr3 25343	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝑄𝐿𝑅))
166	8, 10, 67, 150, 152, 153, 157, 158, 165	lncom 25317	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝑅𝐿𝑄))
167	95	ad5antr 766	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑄 ∈ (𝑅𝐿𝑄))
168	99	ad5antr 766	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝐶 ≠ 𝑄)
169	123	ad2antrr 758	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝐵 ∈ 𝑃)
170	169	ad2antrr 758	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝐵 ∈ 𝑃)
171	99	necomd 2837	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑄 ≠ 𝐶)
172	47	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑄 ∈ (𝐵𝐼𝐶))
173	8, 10, 67, 89, 91, 92, 122, 171, 172	btwnlng2 25315	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝐵 ∈ (𝑄𝐿𝐶))
174	173	ad5antr 766	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝐵 ∈ (𝑄𝐿𝐶))
175		simprr 792	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝐶𝐼𝐵))
176	8, 9, 10, 150, 155, 157, 170, 175	tgbtwncom 25183	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝐵𝐼𝐶))
177	8, 10, 67, 150, 170, 153, 155, 157, 174, 176	coltr3 25343	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝑄𝐿𝐶))
178	8, 10, 67, 150, 155, 153, 157, 168, 177	lncom 25317	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝐶𝐿𝑄))
179	8, 10, 67, 89, 92, 91, 99	tglinerflx2 25329	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑄 ∈ (𝐶𝐿𝑄))
180	179	ad5antr 766	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑄 ∈ (𝐶𝐿𝑄))
181	8, 10, 67, 150, 152, 153, 155, 153, 156, 166, 167, 178, 180	tglineinteq 25340	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 = 𝑄)
182	8, 9, 10, 150, 159, 157, 152, 164	tgbtwncom 25183	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝑅𝐼𝑥))
183	181, 182	eqeltrrd 2689	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑄 ∈ (𝑅𝐼𝑥))
184	121	ad2antrr 758	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝐴 ∈ 𝑃)
185	8, 9, 10, 145, 184, 148, 169, 149	tgbtwncom 25183	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝑥 ∈ (𝐵𝐼𝐴))
186	24	ad4antr 764	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝐶 ∈ (𝑅𝐼𝐴))
187	8, 9, 10, 145, 169, 151, 184, 148, 154, 185, 186	axtgpasch 25166	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → ∃𝑡 ∈ 𝑃 (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵)))
188	183, 187	r19.29a 3060	. . . . . . . 8 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝑄 ∈ (𝑅𝐼𝑥))
189	148, 149, 188	jca32 556	. . . . . . 7 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥))))
190	189	anasss 677	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ (𝑥 ∈ (𝑅𝐿𝑄) ∧ 𝑥 ∈ (𝐴𝐼𝐵))) → (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥))))
191	190	ex 449	. . . . 5 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → ((𝑥 ∈ (𝑅𝐿𝑄) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))))
192	191	reximdv2 2997	. . . 4 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → (∃𝑥 ∈ (𝑅𝐿𝑄)𝑥 ∈ (𝐴𝐼𝐵) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥))))
193	144, 192	mpd 15	. . 3 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))
194	109, 193	pm2.61dan 828	. 2 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))
195	79, 194	pm2.61dan 828	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∨ w3o 1030   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∃wrex 2897   ∖ cdif 3537   class class class wbr 4583  {copab 4642  ran crn 5039  ‘cfv 5804  (class class class)co 6549  Basecbs 15695  distcds 15777  TarskiGcstrkg 25129  Itvcitv 25135  LineGclng 25136  hlGchlg 25295

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-xnn0 11241  df-z 11255  df-uz 11564  df-fz 12198  df-fzo 12335  df-hash 12980  df-word 13154  df-concat 13156  df-s1 13157  df-s2 13444  df-s3 13445  df-trkgc 25147  df-trkgb 25148  df-trkgcb 25149  df-trkgld 25151  df-trkg 25152  df-cgrg 25206  df-leg 25278  df-hlg 25296  df-mir 25348  df-rag 25389  df-perpg 25391

This theorem is referenced by:  hlpasch  25448