Theorem outpasch 28631

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 479	. . . . 5 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝐴 ∈ 𝑃)
3		simpr 483	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑥 = 𝐴) → 𝑥 = 𝐴)
4	3	eleq1d 2810	. . . . . 6 ⊢ (((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑥 = 𝐴) → (𝑥 ∈ (𝐴𝐼𝐵) ↔ 𝐴 ∈ (𝐴𝐼𝐵)))
5	3	oveq2d 7435	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑥 = 𝐴) → (𝑅𝐼𝑥) = (𝑅𝐼𝐴))
6	5	eleq2d 2811	. . . . . 6 ⊢ (((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑥 = 𝐴) → (𝑄 ∈ (𝑅𝐼𝑥) ↔ 𝑄 ∈ (𝑅𝐼𝐴)))
7	4, 6	anbi12d 630	. . . . 5 ⊢ (((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑥 = 𝐴) → ((𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)) ↔ (𝐴 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝐴))))
8		outpasch.p	. . . . . . . 8 ⊢ 𝑃 = (Base‘𝐺)
9		eqid 2725	. . . . . . . 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 28367	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ (𝐴𝐼𝐵))
14	13	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝐴 ∈ (𝐴𝐼𝐵))
15	11	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝐺 ∈ TarskiG)
16		outpasch.r	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ 𝑃)
17	16	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝑅 ∈ 𝑃)
18		outpasch.q	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ 𝑃)
19	18	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝑄 ∈ 𝑃)
20		outpasch.c	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
21	20	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝐶 ∈ 𝑃)
22		simpr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝑄 ∈ (𝑅𝐼𝐶))
23		outpasch.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝑅))
24	8, 9, 10, 11, 1, 20, 16, 23	tgbtwncom 28364	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ (𝑅𝐼𝐴))
25	24	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝐶 ∈ (𝑅𝐼𝐴))
26	8, 9, 10, 15, 17, 19, 21, 2, 22, 25	tgbtwnexch 28374	. . . . . 6 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝑄 ∈ (𝑅𝐼𝐴))
27	14, 26	jca 510	. . . . 5 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → (𝐴 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝐴)))
28	2, 7, 27	rspcedvd 3608	. . . 4 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))
29	28	adantlr 713	. . 3 ⊢ (((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))
30	12	ad2antrr 724	. . . 4 ⊢ (((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝐵 ∈ 𝑃)
31		eleq1 2813	. . . . . 6 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ (𝐴𝐼𝐵) ↔ 𝐵 ∈ (𝐴𝐼𝐵)))
32		oveq2 7427	. . . . . . 7 ⊢ (𝑥 = 𝐵 → (𝑅𝐼𝑥) = (𝑅𝐼𝐵))
33	32	eleq2d 2811	. . . . . 6 ⊢ (𝑥 = 𝐵 → (𝑄 ∈ (𝑅𝐼𝑥) ↔ 𝑄 ∈ (𝑅𝐼𝐵)))
34	31, 33	anbi12d 630	. . . . 5 ⊢ (𝑥 = 𝐵 → ((𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)) ↔ (𝐵 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝐵))))
35	34	adantl 480	. . . 4 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑥 = 𝐵) → ((𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)) ↔ (𝐵 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝐵))))
36	8, 9, 10, 11, 1, 12	tgbtwntriv2 28363	. . . . . 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 483	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝑅 ∈ (𝑄𝐼𝐶))
44	8, 9, 10, 38, 41, 40, 39, 43	tgbtwncom 28364	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝑅 ∈ (𝐶𝐼𝑄))
45		outpasch.2	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ (𝐵𝐼𝐶))
46	8, 9, 10, 11, 12, 18, 20, 45	tgbtwncom 28364	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ (𝐶𝐼𝐵))
47	46	ad3antrrr 728	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝑄 ∈ (𝐶𝐼𝐵))
48	8, 9, 10, 38, 39, 40, 41, 42, 44, 47	tgbtwnexch3 28370	. . . . . 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 483	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) ∧ 𝑄 = 𝐶) → 𝑄 = 𝐶)
55	8, 9, 10, 11, 16, 20	tgbtwntriv2 28363	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ (𝑅𝐼𝐶))
56	55	ad4antr 730	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) ∧ 𝑄 = 𝐶) → 𝐶 ∈ (𝑅𝐼𝐶))
57	54, 56	eqeltrd 2825	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) ∧ 𝑄 = 𝐶) → 𝑄 ∈ (𝑅𝐼𝐶))
58		simpllr 774	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) ∧ 𝑄 = 𝐶) → ¬ 𝑄 ∈ (𝑅𝐼𝐶))
59	57, 58	pm2.65da 815	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → ¬ 𝑄 = 𝐶)
60	59	neqned 2936	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝑄 ≠ 𝐶)
61	45	ad3antrrr 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝑄 ∈ (𝐵𝐼𝐶))
62		simpr 483	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝐶 ∈ (𝑄𝐼𝑅))
63	8, 9, 10, 49, 50, 51, 53, 52, 60, 61, 62	tgbtwnouttr 28373	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝑄 ∈ (𝐵𝐼𝑅))
64	8, 9, 10, 49, 50, 51, 52, 63	tgbtwncom 28364	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝑄 ∈ (𝑅𝐼𝐵))
65		outpasch.l	. . . . . . . . . 10 ⊢ 𝐿 = (LineG‘𝐺)
66	8, 65, 10, 11, 18, 20, 16	tgcolg 28430	. . . . . . . . 9 ⊢ (𝜑 → ((𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶) ↔ (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝑄 ∈ (𝑅𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅))))
67	66	biimpa 475	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝑄 ∈ (𝑅𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅)))
68		3orcoma 1090	. . . . . . . . 9 ⊢ ((𝑄 ∈ (𝑅𝐼𝐶) ∨ 𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅)) ↔ (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝑄 ∈ (𝑅𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅)))
69		3orass 1087	. . . . . . . . 9 ⊢ ((𝑄 ∈ (𝑅𝐼𝐶) ∨ 𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅)) ↔ (𝑄 ∈ (𝑅𝐼𝐶) ∨ (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅))))
70	68, 69	bitr3i 276	. . . . . . . 8 ⊢ ((𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝑄 ∈ (𝑅𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅)) ↔ (𝑄 ∈ (𝑅𝐼𝐶) ∨ (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅))))
71	67, 70	sylib 217	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → (𝑄 ∈ (𝑅𝐼𝐶) ∨ (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅))))
72	71	orcanai 1000	. . . . . 6 ⊢ (((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) → (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅)))
73	48, 64, 72	mpjaodan 956	. . . . 5 ⊢ (((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝑄 ∈ (𝑅𝐼𝐵))
74	37, 73	jca 510	. . . 4 ⊢ (((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) → (𝐵 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝐵)))
75	30, 35, 74	rspcedvd 3608	. . 3 ⊢ (((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))
76	29, 75	pm2.61dan 811	. 2 ⊢ ((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))
77	12	ad2antrr 724	. . . 4 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐵 ∈ 𝑃)
78	34	adantl 480	. . . 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 483	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐵 ∈ (𝑅𝐿𝑄))
86	11	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝐺 ∈ TarskiG)
87	16	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑅 ∈ 𝑃)
88	18	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑄 ∈ 𝑃)
89	20	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝐶 ∈ 𝑃)
90		simpr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶))
91	8, 10, 65, 86, 87, 88, 89, 90	ncolne1 28501	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑅 ≠ 𝑄)
92	8, 10, 65, 86, 87, 88, 91	tglinerflx2 28510	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑄 ∈ (𝑅𝐿𝑄))
93	92	adantr 479	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ (𝑅𝐿𝑄))
94	8, 65, 10, 86, 88, 89, 87, 90	ncolcom 28437	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → ¬ (𝑅 ∈ (𝐶𝐿𝑄) ∨ 𝐶 = 𝑄))
95	8, 65, 10, 86, 89, 88, 87, 94	ncolrot1 28438	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → ¬ (𝐶 ∈ (𝑄𝐿𝑅) ∨ 𝑄 = 𝑅))
96	8, 10, 65, 86, 89, 88, 87, 95	ncolne1 28501	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝐶 ≠ 𝑄)
97	96	adantr 479	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐶 ≠ 𝑄)
98	46	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ (𝐶𝐼𝐵))
99	8, 10, 65, 80, 83, 82, 77, 97, 98	btwnlng3 28497	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐵 ∈ (𝐶𝐿𝑄))
100	8, 10, 65, 80, 83, 82, 97	tglinerflx2 28510	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ (𝐶𝐿𝑄))
101	8, 10, 65, 80, 81, 82, 83, 82, 84, 85, 93, 99, 100	tglineinteq 28521	. . . . . 6 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐵 = 𝑄)
102	8, 9, 10, 11, 16, 12	tgbtwntriv2 28363	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ (𝑅𝐼𝐵))
103	102	ad2antrr 724	. . . . . 6 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐵 ∈ (𝑅𝐼𝐵))
104	101, 103	eqeltrrd 2826	. . . . 5 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ (𝑅𝐼𝐵))
105	79, 104	jca 510	. . . 4 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → (𝐵 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝐵)))
106	77, 78, 105	rspcedvd 3608	. . 3 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))
107		eleq1 2813	. . . . . . . . . 10 ⊢ (𝑡 = 𝑥 → (𝑡 ∈ (𝑎𝐼𝑏) ↔ 𝑥 ∈ (𝑎𝐼𝑏)))
108	107	cbvrexvw 3225	. . . . . . . . 9 ⊢ (∃𝑡 ∈ (𝑅𝐿𝑄)𝑡 ∈ (𝑎𝐼𝑏) ↔ ∃𝑥 ∈ (𝑅𝐿𝑄)𝑥 ∈ (𝑎𝐼𝑏))
109	108	anbi2i 621	. . . . . . . 8 ⊢ (((𝑎 ∈ (𝑃 ∖ (𝑅𝐿𝑄)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑅𝐿𝑄))) ∧ ∃𝑡 ∈ (𝑅𝐿𝑄)𝑡 ∈ (𝑎𝐼𝑏)) ↔ ((𝑎 ∈ (𝑃 ∖ (𝑅𝐿𝑄)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑅𝐿𝑄))) ∧ ∃𝑥 ∈ (𝑅𝐿𝑄)𝑥 ∈ (𝑎𝐼𝑏)))
110	109	opabbii 5216	. . . . . . 7 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑅𝐿𝑄)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑅𝐿𝑄))) ∧ ∃𝑡 ∈ (𝑅𝐿𝑄)𝑡 ∈ (𝑎𝐼𝑏))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑅𝐿𝑄)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑅𝐿𝑄))) ∧ ∃𝑥 ∈ (𝑅𝐿𝑄)𝑥 ∈ (𝑎𝐼𝑏))}
111	11	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐺 ∈ TarskiG)
112	16	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑅 ∈ 𝑃)
113	18	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ 𝑃)
114	91	adantr 479	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑅 ≠ 𝑄)
115	8, 10, 65, 111, 112, 113, 114	tgelrnln 28506	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → (𝑅𝐿𝑄) ∈ ran 𝐿)
116		eqid 2725	. . . . . . 7 ⊢ (hlG‘𝐺) = (hlG‘𝐺)
117	20	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐶 ∈ 𝑃)
118	1	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐴 ∈ 𝑃)
119	12	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐵 ∈ 𝑃)
120	92	adantr 479	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ (𝑅𝐿𝑄))
121	8, 65, 10, 86, 88, 89, 87, 90	ncolrot2 28439	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → ¬ (𝐶 ∈ (𝑅𝐿𝑄) ∨ 𝑅 = 𝑄))
122		pm2.45 879	. . . . . . . . . 10 ⊢ (¬ (𝐶 ∈ (𝑅𝐿𝑄) ∨ 𝑅 = 𝑄) → ¬ 𝐶 ∈ (𝑅𝐿𝑄))
123	121, 122	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → ¬ 𝐶 ∈ (𝑅𝐿𝑄))
124	123	adantr 479	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → ¬ 𝐶 ∈ (𝑅𝐿𝑄))
125		simpr 483	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → ¬ 𝐵 ∈ (𝑅𝐿𝑄))
126	46	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ (𝐶𝐼𝐵))
127	8, 9, 10, 110, 117, 119, 120, 124, 125, 126	islnoppd 28616	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐶{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑅𝐿𝑄)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑅𝐿𝑄))) ∧ ∃𝑡 ∈ (𝑅𝐿𝑄)𝑡 ∈ (𝑎𝐼𝑏))}𝐵)
128	8, 10, 65, 86, 87, 88, 91	tglinerflx1 28509	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑅 ∈ (𝑅𝐿𝑄))
129	128	adantr 479	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑅 ∈ (𝑅𝐿𝑄))
130	24	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐶 ∈ (𝑅𝐼𝐴))
131	8, 10, 65, 86, 89, 87, 88, 121	ncolne1 28501	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝐶 ≠ 𝑅)
132	131	adantr 479	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐶 ≠ 𝑅)
133	8, 9, 10, 111, 112, 117, 118, 130, 132	tgbtwnne 28366	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑅 ≠ 𝐴)
134	8, 10, 116, 112, 118, 117, 111, 118, 130, 133, 132	btwnhl1 28488	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐶((hlG‘𝐺)‘𝑅)𝐴)
135	8, 9, 10, 110, 65, 115, 111, 116, 117, 118, 119, 127, 129, 134	opphl 28630	. . . . . 6 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐴{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑅𝐿𝑄)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑅𝐿𝑄))) ∧ ∃𝑡 ∈ (𝑅𝐿𝑄)𝑡 ∈ (𝑎𝐼𝑏))}𝐵)
136	8, 9, 10, 110, 118, 119	islnopp 28615	. . . . . 6 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → (𝐴{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑅𝐿𝑄)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑅𝐿𝑄))) ∧ ∃𝑡 ∈ (𝑅𝐿𝑄)𝑡 ∈ (𝑎𝐼𝑏))}𝐵 ↔ ((¬ 𝐴 ∈ (𝑅𝐿𝑄) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ ∃𝑥 ∈ (𝑅𝐿𝑄)𝑥 ∈ (𝐴𝐼𝐵))))
137	135, 136	mpbid 231	. . . . 5 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → ((¬ 𝐴 ∈ (𝑅𝐿𝑄) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ ∃𝑥 ∈ (𝑅𝐿𝑄)𝑥 ∈ (𝐴𝐼𝐵)))
138	137	simprd 494	. . . 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 28425	. . . . . . 7 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝑥 ∈ 𝑃)
143		simpr 483	. . . . . . 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 2985	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑄 ≠ 𝑅)
155	154	ad5antr 732	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑄 ≠ 𝑅)
156	141	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑥 ∈ (𝑅𝐿𝑄))
157	8, 10, 65, 144, 147, 146, 153, 155, 156	lncom 28498	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑥 ∈ (𝑄𝐿𝑅))
158		simprl 769	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝑥𝐼𝑅))
159	8, 10, 65, 144, 153, 147, 146, 151, 157, 158	coltr3 28524	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝑄𝐿𝑅))
160	8, 10, 65, 144, 146, 147, 151, 152, 159	lncom 28498	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝑅𝐿𝑄))
161	92	ad5antr 732	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑄 ∈ (𝑅𝐿𝑄))
162	96	ad5antr 732	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝐶 ≠ 𝑄)
163	119	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝐵 ∈ 𝑃)
164	163	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝐵 ∈ 𝑃)
165	12	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝐵 ∈ 𝑃)
166	96	necomd 2985	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑄 ≠ 𝐶)
167	45	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑄 ∈ (𝐵𝐼𝐶))
168	8, 10, 65, 86, 88, 89, 165, 166, 167	btwnlng2 28496	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝐵 ∈ (𝑄𝐿𝐶))
169	168	ad5antr 732	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝐵 ∈ (𝑄𝐿𝐶))
170		simprr 771	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝐶𝐼𝐵))
171	8, 9, 10, 144, 149, 151, 164, 170	tgbtwncom 28364	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝐵𝐼𝐶))
172	8, 10, 65, 144, 164, 147, 149, 151, 169, 171	coltr3 28524	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝑄𝐿𝐶))
173	8, 10, 65, 144, 149, 147, 151, 162, 172	lncom 28498	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝐶𝐿𝑄))
174	8, 10, 65, 86, 89, 88, 96	tglinerflx2 28510	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑄 ∈ (𝐶𝐿𝑄))
175	174	ad5antr 732	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑄 ∈ (𝐶𝐿𝑄))
176	8, 10, 65, 144, 146, 147, 149, 147, 150, 160, 161, 173, 175	tglineinteq 28521	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 = 𝑄)
177	8, 9, 10, 144, 153, 151, 146, 158	tgbtwncom 28364	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝑅𝐼𝑥))
178	176, 177	eqeltrrd 2826	. . . . . . . 8 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑄 ∈ (𝑅𝐼𝑥))
179	118	ad2antrr 724	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝐴 ∈ 𝑃)
180	8, 9, 10, 139, 179, 142, 163, 143	tgbtwncom 28364	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝑥 ∈ (𝐵𝐼𝐴))
181	24	ad4antr 730	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝐶 ∈ (𝑅𝐼𝐴))
182	8, 9, 10, 139, 163, 145, 179, 142, 148, 180, 181	axtgpasch 28343	. . . . . . . 8 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → ∃𝑡 ∈ 𝑃 (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵)))
183	178, 182	r19.29a 3151	. . . . . . 7 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝑄 ∈ (𝑅𝐼𝑥))
184	142, 143, 183	jca32 514	. . . . . 6 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥))))
185	184	expl 456	. . . . 5 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → ((𝑥 ∈ (𝑅𝐿𝑄) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))))
186	185	reximdv2 3153	. . . 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 394   ∨ wo 845   ∨ w3o 1083   = wceq 1533   ∈ wcel 2098   ≠ wne 2929  ∃wrex 3059   ∖ cdif 3941   class class class wbr 5149  {copab 5211  ran crn 5679  ‘cfv 6549  (class class class)co 7419  Basecbs 17183  distcds 17245  TarskiGcstrkg 28303  Itvcitv 28309  LineGclng 28310  hlGchlg 28476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-cnex 11196  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216  ax-pre-mulgt0 11217

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4910  df-int 4951  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7872  df-1st 7994  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-oadd 8491  df-er 8725  df-map 8847  df-pm 8848  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-dju 9926  df-card 9964  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-sub 11478  df-neg 11479  df-nn 12246  df-2 12308  df-3 12309  df-n0 12506  df-xnn0 12578  df-z 12592  df-uz 12856  df-fz 13520  df-fzo 13663  df-hash 14326  df-word 14501  df-concat 14557  df-s1 14582  df-s2 14835  df-s3 14836  df-trkgc 28324  df-trkgb 28325  df-trkgcb 28326  df-trkgld 28328  df-trkg 28329  df-cgrg 28387  df-leg 28459  df-hlg 28477  df-mir 28529  df-rag 28570  df-perpg 28572

This theorem is referenced by:  hlpasch  28632