Theorem outpasch 27697

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 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝐴 ∈ 𝑃)
3		simpr 485	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑥 = 𝐴) → 𝑥 = 𝐴)
4	3	eleq1d 2822	. . . . . 6 ⊢ (((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑥 = 𝐴) → (𝑥 ∈ (𝐴𝐼𝐵) ↔ 𝐴 ∈ (𝐴𝐼𝐵)))
5	3	oveq2d 7373	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑥 = 𝐴) → (𝑅𝐼𝑥) = (𝑅𝐼𝐴))
6	5	eleq2d 2823	. . . . . 6 ⊢ (((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑥 = 𝐴) → (𝑄 ∈ (𝑅𝐼𝑥) ↔ 𝑄 ∈ (𝑅𝐼𝐴)))
7	4, 6	anbi12d 631	. . . . 5 ⊢ (((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑥 = 𝐴) → ((𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)) ↔ (𝐴 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝐴))))
8		outpasch.p	. . . . . . . 8 ⊢ 𝑃 = (Base‘𝐺)
9		eqid 2736	. . . . . . . 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 27433	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ (𝐴𝐼𝐵))
14	13	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝐴 ∈ (𝐴𝐼𝐵))
15	11	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝐺 ∈ TarskiG)
16		outpasch.r	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ 𝑃)
17	16	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝑅 ∈ 𝑃)
18		outpasch.q	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ 𝑃)
19	18	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝑄 ∈ 𝑃)
20		outpasch.c	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
21	20	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝐶 ∈ 𝑃)
22		simpr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝑄 ∈ (𝑅𝐼𝐶))
23		outpasch.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝑅))
24	8, 9, 10, 11, 1, 20, 16, 23	tgbtwncom 27430	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ (𝑅𝐼𝐴))
25	24	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝐶 ∈ (𝑅𝐼𝐴))
26	8, 9, 10, 15, 17, 19, 21, 2, 22, 25	tgbtwnexch 27440	. . . . . 6 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝑄 ∈ (𝑅𝐼𝐴))
27	14, 26	jca 512	. . . . 5 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → (𝐴 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝐴)))
28	2, 7, 27	rspcedvd 3583	. . . 4 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))
29	28	adantlr 713	. . 3 ⊢ (((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))
30	12	ad2antrr 724	. . . 4 ⊢ (((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝐵 ∈ 𝑃)
31		eleq1 2825	. . . . . 6 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ (𝐴𝐼𝐵) ↔ 𝐵 ∈ (𝐴𝐼𝐵)))
32		oveq2 7365	. . . . . . 7 ⊢ (𝑥 = 𝐵 → (𝑅𝐼𝑥) = (𝑅𝐼𝐵))
33	32	eleq2d 2823	. . . . . 6 ⊢ (𝑥 = 𝐵 → (𝑄 ∈ (𝑅𝐼𝑥) ↔ 𝑄 ∈ (𝑅𝐼𝐵)))
34	31, 33	anbi12d 631	. . . . 5 ⊢ (𝑥 = 𝐵 → ((𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)) ↔ (𝐵 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝐵))))
35	34	adantl 482	. . . 4 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑥 = 𝐵) → ((𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)) ↔ (𝐵 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝐵))))
36	8, 9, 10, 11, 1, 12	tgbtwntriv2 27429	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐵))
37	36	ad2antrr 724	. . . . 5 ⊢ (((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝐵 ∈ (𝐴𝐼𝐵))
38	11	ad3antrrr 728	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝐺 ∈ TarskiG)
39	20	ad3antrrr 728	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝐶 ∈ 𝑃)
40	16	ad3antrrr 728	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝑅 ∈ 𝑃)
41	18	ad3antrrr 728	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝑄 ∈ 𝑃)
42	12	ad3antrrr 728	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝐵 ∈ 𝑃)
43		simpr 485	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝑅 ∈ (𝑄𝐼𝐶))
44	8, 9, 10, 38, 41, 40, 39, 43	tgbtwncom 27430	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝑅 ∈ (𝐶𝐼𝑄))
45		outpasch.2	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ (𝐵𝐼𝐶))
46	8, 9, 10, 11, 12, 18, 20, 45	tgbtwncom 27430	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ (𝐶𝐼𝐵))
47	46	ad3antrrr 728	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝑄 ∈ (𝐶𝐼𝐵))
48	8, 9, 10, 38, 39, 40, 41, 42, 44, 47	tgbtwnexch3 27436	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝑄 ∈ (𝑅𝐼𝐵))
49	11	ad3antrrr 728	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝐺 ∈ TarskiG)
50	12	ad3antrrr 728	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝐵 ∈ 𝑃)
51	18	ad3antrrr 728	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝑄 ∈ 𝑃)
52	16	ad3antrrr 728	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝑅 ∈ 𝑃)
53	20	ad3antrrr 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝐶 ∈ 𝑃)
54		simpr 485	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) ∧ 𝑄 = 𝐶) → 𝑄 = 𝐶)
55	8, 9, 10, 11, 16, 20	tgbtwntriv2 27429	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ (𝑅𝐼𝐶))
56	55	ad4antr 730	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) ∧ 𝑄 = 𝐶) → 𝐶 ∈ (𝑅𝐼𝐶))
57	54, 56	eqeltrd 2838	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) ∧ 𝑄 = 𝐶) → 𝑄 ∈ (𝑅𝐼𝐶))
58		simpllr 774	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) ∧ 𝑄 = 𝐶) → ¬ 𝑄 ∈ (𝑅𝐼𝐶))
59	57, 58	pm2.65da 815	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → ¬ 𝑄 = 𝐶)
60	59	neqned 2950	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝑄 ≠ 𝐶)
61	45	ad3antrrr 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝑄 ∈ (𝐵𝐼𝐶))
62		simpr 485	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝐶 ∈ (𝑄𝐼𝑅))
63	8, 9, 10, 49, 50, 51, 53, 52, 60, 61, 62	tgbtwnouttr 27439	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝑄 ∈ (𝐵𝐼𝑅))
64	8, 9, 10, 49, 50, 51, 52, 63	tgbtwncom 27430	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝑄 ∈ (𝑅𝐼𝐵))
65		outpasch.l	. . . . . . . . . 10 ⊢ 𝐿 = (LineG‘𝐺)
66	8, 65, 10, 11, 18, 20, 16	tgcolg 27496	. . . . . . . . 9 ⊢ (𝜑 → ((𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶) ↔ (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝑄 ∈ (𝑅𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅))))
67	66	biimpa 477	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝑄 ∈ (𝑅𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅)))
68		3orcoma 1093	. . . . . . . . 9 ⊢ ((𝑄 ∈ (𝑅𝐼𝐶) ∨ 𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅)) ↔ (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝑄 ∈ (𝑅𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅)))
69		3orass 1090	. . . . . . . . 9 ⊢ ((𝑄 ∈ (𝑅𝐼𝐶) ∨ 𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅)) ↔ (𝑄 ∈ (𝑅𝐼𝐶) ∨ (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅))))
70	68, 69	bitr3i 276	. . . . . . . 8 ⊢ ((𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝑄 ∈ (𝑅𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅)) ↔ (𝑄 ∈ (𝑅𝐼𝐶) ∨ (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅))))
71	67, 70	sylib 217	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → (𝑄 ∈ (𝑅𝐼𝐶) ∨ (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅))))
72	71	orcanai 1001	. . . . . 6 ⊢ (((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) → (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅)))
73	48, 64, 72	mpjaodan 957	. . . . 5 ⊢ (((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝑄 ∈ (𝑅𝐼𝐵))
74	37, 73	jca 512	. . . 4 ⊢ (((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) → (𝐵 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝐵)))
75	30, 35, 74	rspcedvd 3583	. . 3 ⊢ (((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))
76	29, 75	pm2.61dan 811	. 2 ⊢ ((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))
77	12	ad2antrr 724	. . . 4 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐵 ∈ 𝑃)
78	34	adantl 482	. . . 4 ⊢ ((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 = 𝐵) → ((𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)) ↔ (𝐵 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝐵))))
79	36	ad2antrr 724	. . . . 5 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐵 ∈ (𝐴𝐼𝐵))
80	11	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐺 ∈ TarskiG)
81	16	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑅 ∈ 𝑃)
82	18	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ 𝑃)
83	20	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐶 ∈ 𝑃)
84		simplr 767	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶))
85		simpr 485	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐵 ∈ (𝑅𝐿𝑄))
86	11	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝐺 ∈ TarskiG)
87	16	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑅 ∈ 𝑃)
88	18	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑄 ∈ 𝑃)
89	20	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝐶 ∈ 𝑃)
90		simpr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶))
91	8, 10, 65, 86, 87, 88, 89, 90	ncolne1 27567	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑅 ≠ 𝑄)
92	8, 10, 65, 86, 87, 88, 91	tglinerflx2 27576	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑄 ∈ (𝑅𝐿𝑄))
93	92	adantr 481	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ (𝑅𝐿𝑄))
94	8, 65, 10, 86, 88, 89, 87, 90	ncolcom 27503	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → ¬ (𝑅 ∈ (𝐶𝐿𝑄) ∨ 𝐶 = 𝑄))
95	8, 65, 10, 86, 89, 88, 87, 94	ncolrot1 27504	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → ¬ (𝐶 ∈ (𝑄𝐿𝑅) ∨ 𝑄 = 𝑅))
96	8, 10, 65, 86, 89, 88, 87, 95	ncolne1 27567	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝐶 ≠ 𝑄)
97	96	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐶 ≠ 𝑄)
98	46	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ (𝐶𝐼𝐵))
99	8, 10, 65, 80, 83, 82, 77, 97, 98	btwnlng3 27563	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐵 ∈ (𝐶𝐿𝑄))
100	8, 10, 65, 80, 83, 82, 97	tglinerflx2 27576	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ (𝐶𝐿𝑄))
101	8, 10, 65, 80, 81, 82, 83, 82, 84, 85, 93, 99, 100	tglineinteq 27587	. . . . . 6 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐵 = 𝑄)
102	8, 9, 10, 11, 16, 12	tgbtwntriv2 27429	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ (𝑅𝐼𝐵))
103	102	ad2antrr 724	. . . . . 6 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐵 ∈ (𝑅𝐼𝐵))
104	101, 103	eqeltrrd 2839	. . . . 5 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ (𝑅𝐼𝐵))
105	79, 104	jca 512	. . . 4 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → (𝐵 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝐵)))
106	77, 78, 105	rspcedvd 3583	. . 3 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))
107		eleq1 2825	. . . . . . . . . 10 ⊢ (𝑡 = 𝑥 → (𝑡 ∈ (𝑎𝐼𝑏) ↔ 𝑥 ∈ (𝑎𝐼𝑏)))
108	107	cbvrexvw 3226	. . . . . . . . 9 ⊢ (∃𝑡 ∈ (𝑅𝐿𝑄)𝑡 ∈ (𝑎𝐼𝑏) ↔ ∃𝑥 ∈ (𝑅𝐿𝑄)𝑥 ∈ (𝑎𝐼𝑏))
109	108	anbi2i 623	. . . . . . . 8 ⊢ (((𝑎 ∈ (𝑃 ∖ (𝑅𝐿𝑄)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑅𝐿𝑄))) ∧ ∃𝑡 ∈ (𝑅𝐿𝑄)𝑡 ∈ (𝑎𝐼𝑏)) ↔ ((𝑎 ∈ (𝑃 ∖ (𝑅𝐿𝑄)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑅𝐿𝑄))) ∧ ∃𝑥 ∈ (𝑅𝐿𝑄)𝑥 ∈ (𝑎𝐼𝑏)))
110	109	opabbii 5172	. . . . . . 7 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑅𝐿𝑄)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑅𝐿𝑄))) ∧ ∃𝑡 ∈ (𝑅𝐿𝑄)𝑡 ∈ (𝑎𝐼𝑏))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑅𝐿𝑄)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑅𝐿𝑄))) ∧ ∃𝑥 ∈ (𝑅𝐿𝑄)𝑥 ∈ (𝑎𝐼𝑏))}
111	11	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐺 ∈ TarskiG)
112	16	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑅 ∈ 𝑃)
113	18	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ 𝑃)
114	91	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑅 ≠ 𝑄)
115	8, 10, 65, 111, 112, 113, 114	tgelrnln 27572	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → (𝑅𝐿𝑄) ∈ ran 𝐿)
116		eqid 2736	. . . . . . 7 ⊢ (hlG‘𝐺) = (hlG‘𝐺)
117	20	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐶 ∈ 𝑃)
118	1	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐴 ∈ 𝑃)
119	12	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐵 ∈ 𝑃)
120	92	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ (𝑅𝐿𝑄))
121	8, 65, 10, 86, 88, 89, 87, 90	ncolrot2 27505	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → ¬ (𝐶 ∈ (𝑅𝐿𝑄) ∨ 𝑅 = 𝑄))
122		pm2.45 880	. . . . . . . . . 10 ⊢ (¬ (𝐶 ∈ (𝑅𝐿𝑄) ∨ 𝑅 = 𝑄) → ¬ 𝐶 ∈ (𝑅𝐿𝑄))
123	121, 122	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → ¬ 𝐶 ∈ (𝑅𝐿𝑄))
124	123	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → ¬ 𝐶 ∈ (𝑅𝐿𝑄))
125		simpr 485	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → ¬ 𝐵 ∈ (𝑅𝐿𝑄))
126	46	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ (𝐶𝐼𝐵))
127	8, 9, 10, 110, 117, 119, 120, 124, 125, 126	islnoppd 27682	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐶{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑅𝐿𝑄)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑅𝐿𝑄))) ∧ ∃𝑡 ∈ (𝑅𝐿𝑄)𝑡 ∈ (𝑎𝐼𝑏))}𝐵)
128	8, 10, 65, 86, 87, 88, 91	tglinerflx1 27575	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑅 ∈ (𝑅𝐿𝑄))
129	128	adantr 481	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑅 ∈ (𝑅𝐿𝑄))
130	24	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐶 ∈ (𝑅𝐼𝐴))
131	8, 10, 65, 86, 89, 87, 88, 121	ncolne1 27567	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝐶 ≠ 𝑅)
132	131	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐶 ≠ 𝑅)
133	8, 9, 10, 111, 112, 117, 118, 130, 132	tgbtwnne 27432	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑅 ≠ 𝐴)
134	8, 10, 116, 112, 118, 117, 111, 118, 130, 133, 132	btwnhl1 27554	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐶((hlG‘𝐺)‘𝑅)𝐴)
135	8, 9, 10, 110, 65, 115, 111, 116, 117, 118, 119, 127, 129, 134	opphl 27696	. . . . . 6 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐴{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑅𝐿𝑄)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑅𝐿𝑄))) ∧ ∃𝑡 ∈ (𝑅𝐿𝑄)𝑡 ∈ (𝑎𝐼𝑏))}𝐵)
136	8, 9, 10, 110, 118, 119	islnopp 27681	. . . . . 6 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → (𝐴{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑅𝐿𝑄)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑅𝐿𝑄))) ∧ ∃𝑡 ∈ (𝑅𝐿𝑄)𝑡 ∈ (𝑎𝐼𝑏))}𝐵 ↔ ((¬ 𝐴 ∈ (𝑅𝐿𝑄) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ ∃𝑥 ∈ (𝑅𝐿𝑄)𝑥 ∈ (𝐴𝐼𝐵))))
137	135, 136	mpbid 231	. . . . 5 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → ((¬ 𝐴 ∈ (𝑅𝐿𝑄) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ ∃𝑥 ∈ (𝑅𝐿𝑄)𝑥 ∈ (𝐴𝐼𝐵)))
138	137	simprd 496	. . . 4 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → ∃𝑥 ∈ (𝑅𝐿𝑄)𝑥 ∈ (𝐴𝐼𝐵))
139	111	ad2antrr 724	. . . . . . . 8 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝐺 ∈ TarskiG)
140	115	ad2antrr 724	. . . . . . . 8 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → (𝑅𝐿𝑄) ∈ ran 𝐿)
141		simplr 767	. . . . . . . 8 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝑥 ∈ (𝑅𝐿𝑄))
142	8, 65, 10, 139, 140, 141	tglnpt 27491	. . . . . . 7 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝑥 ∈ 𝑃)
143		simpr 485	. . . . . . 7 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝑥 ∈ (𝐴𝐼𝐵))
144	139	ad2antrr 724	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝐺 ∈ TarskiG)
145	87	ad3antrrr 728	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝑅 ∈ 𝑃)
146	145	ad2antrr 724	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑅 ∈ 𝑃)
147	88	ad5antr 732	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑄 ∈ 𝑃)
148	117	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝐶 ∈ 𝑃)
149	148	ad2antrr 724	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝐶 ∈ 𝑃)
150	90	ad5antr 732	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶))
151		simplr 767	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ 𝑃)
152	114	ad4antr 730	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑅 ≠ 𝑄)
153	142	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑥 ∈ 𝑃)
154	91	necomd 2999	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑄 ≠ 𝑅)
155	154	ad5antr 732	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑄 ≠ 𝑅)
156	141	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑥 ∈ (𝑅𝐿𝑄))
157	8, 10, 65, 144, 147, 146, 153, 155, 156	lncom 27564	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑥 ∈ (𝑄𝐿𝑅))
158		simprl 769	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝑥𝐼𝑅))
159	8, 10, 65, 144, 153, 147, 146, 151, 157, 158	coltr3 27590	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝑄𝐿𝑅))
160	8, 10, 65, 144, 146, 147, 151, 152, 159	lncom 27564	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝑅𝐿𝑄))
161	92	ad5antr 732	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑄 ∈ (𝑅𝐿𝑄))
162	96	ad5antr 732	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝐶 ≠ 𝑄)
163	119	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝐵 ∈ 𝑃)
164	163	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝐵 ∈ 𝑃)
165	12	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝐵 ∈ 𝑃)
166	96	necomd 2999	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑄 ≠ 𝐶)
167	45	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑄 ∈ (𝐵𝐼𝐶))
168	8, 10, 65, 86, 88, 89, 165, 166, 167	btwnlng2 27562	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝐵 ∈ (𝑄𝐿𝐶))
169	168	ad5antr 732	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝐵 ∈ (𝑄𝐿𝐶))
170		simprr 771	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝐶𝐼𝐵))
171	8, 9, 10, 144, 149, 151, 164, 170	tgbtwncom 27430	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝐵𝐼𝐶))
172	8, 10, 65, 144, 164, 147, 149, 151, 169, 171	coltr3 27590	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝑄𝐿𝐶))
173	8, 10, 65, 144, 149, 147, 151, 162, 172	lncom 27564	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝐶𝐿𝑄))
174	8, 10, 65, 86, 89, 88, 96	tglinerflx2 27576	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑄 ∈ (𝐶𝐿𝑄))
175	174	ad5antr 732	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑄 ∈ (𝐶𝐿𝑄))
176	8, 10, 65, 144, 146, 147, 149, 147, 150, 160, 161, 173, 175	tglineinteq 27587	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 = 𝑄)
177	8, 9, 10, 144, 153, 151, 146, 158	tgbtwncom 27430	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝑅𝐼𝑥))
178	176, 177	eqeltrrd 2839	. . . . . . . 8 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑄 ∈ (𝑅𝐼𝑥))
179	118	ad2antrr 724	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝐴 ∈ 𝑃)
180	8, 9, 10, 139, 179, 142, 163, 143	tgbtwncom 27430	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝑥 ∈ (𝐵𝐼𝐴))
181	24	ad4antr 730	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝐶 ∈ (𝑅𝐼𝐴))
182	8, 9, 10, 139, 163, 145, 179, 142, 148, 180, 181	axtgpasch 27409	. . . . . . . 8 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → ∃𝑡 ∈ 𝑃 (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵)))
183	178, 182	r19.29a 3159	. . . . . . 7 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝑄 ∈ (𝑅𝐼𝑥))
184	142, 143, 183	jca32 516	. . . . . 6 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥))))
185	184	expl 458	. . . . 5 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → ((𝑥 ∈ (𝑅𝐿𝑄) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))))
186	185	reximdv2 3161	. . . 4 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → (∃𝑥 ∈ (𝑅𝐿𝑄)𝑥 ∈ (𝐴𝐼𝐵) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥))))
187	138, 186	mpd 15	. . 3 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))
188	106, 187	pm2.61dan 811	. 2 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))
189	76, 188	pm2.61dan 811	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   ∨ w3o 1086   = wceq 1541   ∈ wcel 2106   ≠ wne 2943  ∃wrex 3073   ∖ cdif 3907   class class class wbr 5105  {copab 5167  ran crn 5634  ‘cfv 6496  (class class class)co 7357  Basecbs 17083  distcds 17142  TarskiGcstrkg 27369  Itvcitv 27375  LineGclng 27376  hlGchlg 27542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-oadd 8416  df-er 8648  df-map 8767  df-pm 8768  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-dju 9837  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-2 12216  df-3 12217  df-n0 12414  df-xnn0 12486  df-z 12500  df-uz 12764  df-fz 13425  df-fzo 13568  df-hash 14231  df-word 14403  df-concat 14459  df-s1 14484  df-s2 14737  df-s3 14738  df-trkgc 27390  df-trkgb 27391  df-trkgcb 27392  df-trkgld 27394  df-trkg 27395  df-cgrg 27453  df-leg 27525  df-hlg 27543  df-mir 27595  df-rag 27636  df-perpg 27638

This theorem is referenced by:  hlpasch  27698