Theorem outpasch 29120

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 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝐴 ∈ 𝑃)
3		simpr 490	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑥 = 𝐴) → 𝑥 = 𝐴)
4	3	eleq1d 2847	. . . . . 6 ⊢ (((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑥 = 𝐴) → (𝑥 ∈ (𝐴𝐼𝐵) ↔ 𝐴 ∈ (𝐴𝐼𝐵)))
5	3	oveq2d 7433	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑥 = 𝐴) → (𝑅𝐼𝑥) = (𝑅𝐼𝐴))
6	5	eleq2d 2848	. . . . . 6 ⊢ (((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑥 = 𝐴) → (𝑄 ∈ (𝑅𝐼𝑥) ↔ 𝑄 ∈ (𝑅𝐼𝐴)))
7	4, 6	anbi12d 644	. . . . 5 ⊢ (((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑥 = 𝐴) → ((𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)) ↔ (𝐴 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝐴))))
8		outpasch.p	. . . . . . . 8 ⊢ 𝑃 = (Base‘𝐺)
9		eqid 2762	. . . . . . . 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 28841	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ (𝐴𝐼𝐵))
14	13	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝐴 ∈ (𝐴𝐼𝐵))
15	11	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝐺 ∈ TarskiG)
16		outpasch.r	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ 𝑃)
17	16	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝑅 ∈ 𝑃)
18		outpasch.q	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ 𝑃)
19	18	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝑄 ∈ 𝑃)
20		outpasch.c	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
21	20	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝐶 ∈ 𝑃)
22		simpr 490	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝑄 ∈ (𝑅𝐼𝐶))
23		outpasch.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼𝑅))
24	8, 9, 10, 11, 1, 20, 16, 23	tgbtwncom 28838	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ (𝑅𝐼𝐴))
25	24	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝐶 ∈ (𝑅𝐼𝐴))
26	8, 9, 10, 15, 17, 19, 21, 2, 22, 25	tgbtwnexch 28848	. . . . . 6 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝑄 ∈ (𝑅𝐼𝐴))
27	14, 26	jca 521	. . . . 5 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → (𝐴 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝐴)))
28	2, 7, 27	rspcedvd 3581	. . . 4 ⊢ ((𝜑 ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))
29	28	adantlr 728	. . 3 ⊢ (((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝑄 ∈ (𝑅𝐼𝐶)) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))
30	12	ad2antrr 739	. . . 4 ⊢ (((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝐵 ∈ 𝑃)
31		eleq1 2850	. . . . . 6 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ (𝐴𝐼𝐵) ↔ 𝐵 ∈ (𝐴𝐼𝐵)))
32		oveq2 7425	. . . . . . 7 ⊢ (𝑥 = 𝐵 → (𝑅𝐼𝑥) = (𝑅𝐼𝐵))
33	32	eleq2d 2848	. . . . . 6 ⊢ (𝑥 = 𝐵 → (𝑄 ∈ (𝑅𝐼𝑥) ↔ 𝑄 ∈ (𝑅𝐼𝐵)))
34	31, 33	anbi12d 644	. . . . 5 ⊢ (𝑥 = 𝐵 → ((𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)) ↔ (𝐵 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝐵))))
35	34	adantl 487	. . . 4 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑥 = 𝐵) → ((𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)) ↔ (𝐵 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝐵))))
36	8, 9, 10, 11, 1, 12	tgbtwntriv2 28837	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐵))
37	36	ad2antrr 739	. . . . 5 ⊢ (((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝐵 ∈ (𝐴𝐼𝐵))
38	11	ad3antrrr 743	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝐺 ∈ TarskiG)
39	20	ad3antrrr 743	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝐶 ∈ 𝑃)
40	16	ad3antrrr 743	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝑅 ∈ 𝑃)
41	18	ad3antrrr 743	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝑄 ∈ 𝑃)
42	12	ad3antrrr 743	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝐵 ∈ 𝑃)
43		simpr 490	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝑅 ∈ (𝑄𝐼𝐶))
44	8, 9, 10, 38, 41, 40, 39, 43	tgbtwncom 28838	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝑅 ∈ (𝐶𝐼𝑄))
45		outpasch.2	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ (𝐵𝐼𝐶))
46	8, 9, 10, 11, 12, 18, 20, 45	tgbtwncom 28838	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ (𝐶𝐼𝐵))
47	46	ad3antrrr 743	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝑄 ∈ (𝐶𝐼𝐵))
48	8, 9, 10, 38, 39, 40, 41, 42, 44, 47	tgbtwnexch3 28844	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝑅 ∈ (𝑄𝐼𝐶)) → 𝑄 ∈ (𝑅𝐼𝐵))
49	11	ad3antrrr 743	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝐺 ∈ TarskiG)
50	12	ad3antrrr 743	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝐵 ∈ 𝑃)
51	18	ad3antrrr 743	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝑄 ∈ 𝑃)
52	16	ad3antrrr 743	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝑅 ∈ 𝑃)
53	20	ad3antrrr 743	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝐶 ∈ 𝑃)
54		simpr 490	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) ∧ 𝑄 = 𝐶) → 𝑄 = 𝐶)
55	8, 9, 10, 11, 16, 20	tgbtwntriv2 28837	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ (𝑅𝐼𝐶))
56	55	ad4antr 745	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) ∧ 𝑄 = 𝐶) → 𝐶 ∈ (𝑅𝐼𝐶))
57	54, 56	eqeltrd 2862	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) ∧ 𝑄 = 𝐶) → 𝑄 ∈ (𝑅𝐼𝐶))
58		simpllr 788	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) ∧ 𝑄 = 𝐶) → ¬ 𝑄 ∈ (𝑅𝐼𝐶))
59	57, 58	pm2.65da 829	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → ¬ 𝑄 = 𝐶)
60	59	neqned 2964	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝑄 ≠ 𝐶)
61	45	ad3antrrr 743	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝑄 ∈ (𝐵𝐼𝐶))
62		simpr 490	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝐶 ∈ (𝑄𝐼𝑅))
63	8, 9, 10, 49, 50, 51, 53, 52, 60, 61, 62	tgbtwnouttr 28847	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝑄 ∈ (𝐵𝐼𝑅))
64	8, 9, 10, 49, 50, 51, 52, 63	tgbtwncom 28838	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) ∧ 𝐶 ∈ (𝑄𝐼𝑅)) → 𝑄 ∈ (𝑅𝐼𝐵))
65		outpasch.l	. . . . . . . . . 10 ⊢ 𝐿 = (LineG‘𝐺)
66	8, 65, 10, 11, 18, 20, 16	tgcolg 28904	. . . . . . . . 9 ⊢ (𝜑 → ((𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶) ↔ (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝑄 ∈ (𝑅𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅))))
67	66	biimpa 482	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝑄 ∈ (𝑅𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅)))
68		3orcoma 1109	. . . . . . . . 9 ⊢ ((𝑄 ∈ (𝑅𝐼𝐶) ∨ 𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅)) ↔ (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝑄 ∈ (𝑅𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅)))
69		3orass 1106	. . . . . . . . 9 ⊢ ((𝑄 ∈ (𝑅𝐼𝐶) ∨ 𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅)) ↔ (𝑄 ∈ (𝑅𝐼𝐶) ∨ (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅))))
70	68, 69	bitr3i 280	. . . . . . . 8 ⊢ ((𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝑄 ∈ (𝑅𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅)) ↔ (𝑄 ∈ (𝑅𝐼𝐶) ∨ (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅))))
71	67, 70	sylib 221	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → (𝑄 ∈ (𝑅𝐼𝐶) ∨ (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅))))
72	71	orcanai 1018	. . . . . 6 ⊢ (((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) → (𝑅 ∈ (𝑄𝐼𝐶) ∨ 𝐶 ∈ (𝑄𝐼𝑅)))
73	48, 64, 72	mpjaodan 973	. . . . 5 ⊢ (((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) → 𝑄 ∈ (𝑅𝐼𝐵))
74	37, 73	jca 521	. . . 4 ⊢ (((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) → (𝐵 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝐵)))
75	30, 35, 74	rspcedvd 3581	. . 3 ⊢ (((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝑄 ∈ (𝑅𝐼𝐶)) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))
76	29, 75	pm2.61dan 825	. 2 ⊢ ((𝜑 ∧ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))
77	12	ad2antrr 739	. . . 4 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐵 ∈ 𝑃)
78	34	adantl 487	. . . 4 ⊢ ((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 = 𝐵) → ((𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)) ↔ (𝐵 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝐵))))
79	36	ad2antrr 739	. . . . 5 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐵 ∈ (𝐴𝐼𝐵))
80	11	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐺 ∈ TarskiG)
81	16	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑅 ∈ 𝑃)
82	18	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ 𝑃)
83	20	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐶 ∈ 𝑃)
84		simplr 781	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶))
85		simpr 490	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐵 ∈ (𝑅𝐿𝑄))
86	11	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝐺 ∈ TarskiG)
87	16	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑅 ∈ 𝑃)
88	18	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑄 ∈ 𝑃)
89	20	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝐶 ∈ 𝑃)
90		simpr 490	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶))
91	8, 10, 65, 86, 87, 88, 89, 90	ncolne1 28980	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑅 ≠ 𝑄)
92	8, 10, 65, 86, 87, 88, 91	tglinerflx2 28989	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑄 ∈ (𝑅𝐿𝑄))
93	92	adantr 486	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ (𝑅𝐿𝑄))
94	8, 65, 10, 86, 88, 89, 87, 90	ncolcom 28911	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → ¬ (𝑅 ∈ (𝐶𝐿𝑄) ∨ 𝐶 = 𝑄))
95	8, 65, 10, 86, 89, 88, 87, 94	ncolrot1 28912	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → ¬ (𝐶 ∈ (𝑄𝐿𝑅) ∨ 𝑄 = 𝑅))
96	8, 10, 65, 86, 89, 88, 87, 95	ncolne1 28980	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝐶 ≠ 𝑄)
97	96	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐶 ≠ 𝑄)
98	46	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ (𝐶𝐼𝐵))
99	8, 10, 65, 80, 83, 82, 77, 97, 98	btwnlng3 28976	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐵 ∈ (𝐶𝐿𝑄))
100	8, 10, 65, 80, 83, 82, 97	tglinerflx2 28989	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ (𝐶𝐿𝑄))
101	8, 10, 65, 80, 81, 82, 83, 82, 84, 85, 93, 99, 100	tglineinteq 29001	. . . . . 6 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐵 = 𝑄)
102	8, 9, 10, 11, 16, 12	tgbtwntriv2 28837	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ (𝑅𝐼𝐵))
103	102	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐵 ∈ (𝑅𝐼𝐵))
104	101, 103	eqeltrrd 2863	. . . . 5 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ (𝑅𝐼𝐵))
105	79, 104	jca 521	. . . 4 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → (𝐵 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝐵)))
106	77, 78, 105	rspcedvd 3581	. . 3 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ 𝐵 ∈ (𝑅𝐿𝑄)) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))
107		eleq1 2850	. . . . . . . . . 10 ⊢ (𝑡 = 𝑥 → (𝑡 ∈ (𝑎𝐼𝑏) ↔ 𝑥 ∈ (𝑎𝐼𝑏)))
108	107	cbvrexvw 3243	. . . . . . . . 9 ⊢ (∃𝑡 ∈ (𝑅𝐿𝑄)𝑡 ∈ (𝑎𝐼𝑏) ↔ ∃𝑥 ∈ (𝑅𝐿𝑄)𝑥 ∈ (𝑎𝐼𝑏))
109	108	anbi2i 635	. . . . . . . 8 ⊢ (((𝑎 ∈ (𝑃 ∖ (𝑅𝐿𝑄)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑅𝐿𝑄))) ∧ ∃𝑡 ∈ (𝑅𝐿𝑄)𝑡 ∈ (𝑎𝐼𝑏)) ↔ ((𝑎 ∈ (𝑃 ∖ (𝑅𝐿𝑄)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑅𝐿𝑄))) ∧ ∃𝑥 ∈ (𝑅𝐿𝑄)𝑥 ∈ (𝑎𝐼𝑏)))
110	109	opabbii 5176	. . . . . . 7 ⊢ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑅𝐿𝑄)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑅𝐿𝑄))) ∧ ∃𝑡 ∈ (𝑅𝐿𝑄)𝑡 ∈ (𝑎𝐼𝑏))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑅𝐿𝑄)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑅𝐿𝑄))) ∧ ∃𝑥 ∈ (𝑅𝐿𝑄)𝑥 ∈ (𝑎𝐼𝑏))}
111	11	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐺 ∈ TarskiG)
112	16	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑅 ∈ 𝑃)
113	18	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ 𝑃)
114	91	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑅 ≠ 𝑄)
115	8, 10, 65, 111, 112, 113, 114	tgelrnln 28985	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → (𝑅𝐿𝑄) ∈ ran 𝐿)
116		eqid 2762	. . . . . . 7 ⊢ (hlG‘𝐺) = (hlG‘𝐺)
117	20	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐶 ∈ 𝑃)
118	1	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐴 ∈ 𝑃)
119	12	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐵 ∈ 𝑃)
120	92	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ (𝑅𝐿𝑄))
121	8, 65, 10, 86, 88, 89, 87, 90	ncolrot2 28913	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → ¬ (𝐶 ∈ (𝑅𝐿𝑄) ∨ 𝑅 = 𝑄))
122		pm2.45 895	. . . . . . . . . 10 ⊢ (¬ (𝐶 ∈ (𝑅𝐿𝑄) ∨ 𝑅 = 𝑄) → ¬ 𝐶 ∈ (𝑅𝐿𝑄))
123	121, 122	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → ¬ 𝐶 ∈ (𝑅𝐿𝑄))
124	123	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → ¬ 𝐶 ∈ (𝑅𝐿𝑄))
125		simpr 490	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → ¬ 𝐵 ∈ (𝑅𝐿𝑄))
126	46	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑄 ∈ (𝐶𝐼𝐵))
127	8, 9, 10, 110, 117, 119, 120, 124, 125, 126	islnoppd 29103	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐶{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑅𝐿𝑄)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑅𝐿𝑄))) ∧ ∃𝑡 ∈ (𝑅𝐿𝑄)𝑡 ∈ (𝑎𝐼𝑏))}𝐵)
128	8, 10, 65, 86, 87, 88, 91	tglinerflx1 28988	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑅 ∈ (𝑅𝐿𝑄))
129	128	adantr 486	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑅 ∈ (𝑅𝐿𝑄))
130	24	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐶 ∈ (𝑅𝐼𝐴))
131	8, 10, 65, 86, 89, 87, 88, 121	ncolne1 28980	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝐶 ≠ 𝑅)
132	131	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐶 ≠ 𝑅)
133	8, 9, 10, 111, 112, 117, 118, 130, 132	tgbtwnne 28840	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝑅 ≠ 𝐴)
134	8, 10, 116, 112, 118, 117, 111, 118, 130, 133, 132	btwnhl1 28965	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐶((hlG‘𝐺)‘𝑅)𝐴)
135	8, 9, 10, 110, 65, 115, 111, 116, 117, 118, 119, 127, 129, 134	opphl 29117	. . . . . 6 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → 𝐴{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑅𝐿𝑄)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑅𝐿𝑄))) ∧ ∃𝑡 ∈ (𝑅𝐿𝑄)𝑡 ∈ (𝑎𝐼𝑏))}𝐵)
136	8, 9, 10, 110, 118, 119	islnopp 29102	. . . . . 6 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → (𝐴{⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑅𝐿𝑄)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑅𝐿𝑄))) ∧ ∃𝑡 ∈ (𝑅𝐿𝑄)𝑡 ∈ (𝑎𝐼𝑏))}𝐵 ↔ ((¬ 𝐴 ∈ (𝑅𝐿𝑄) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ ∃𝑥 ∈ (𝑅𝐿𝑄)𝑥 ∈ (𝐴𝐼𝐵))))
137	135, 136	mpbid 235	. . . . 5 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → ((¬ 𝐴 ∈ (𝑅𝐿𝑄) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ ∃𝑥 ∈ (𝑅𝐿𝑄)𝑥 ∈ (𝐴𝐼𝐵)))
138	137	simprd 501	. . . 4 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → ∃𝑥 ∈ (𝑅𝐿𝑄)𝑥 ∈ (𝐴𝐼𝐵))
139	111	ad2antrr 739	. . . . . . . 8 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝐺 ∈ TarskiG)
140	115	ad2antrr 739	. . . . . . . 8 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → (𝑅𝐿𝑄) ∈ ran 𝐿)
141		simplr 781	. . . . . . . 8 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝑥 ∈ (𝑅𝐿𝑄))
142	8, 65, 10, 139, 140, 141	tglnpt 28899	. . . . . . 7 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝑥 ∈ 𝑃)
143		simpr 490	. . . . . . 7 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝑥 ∈ (𝐴𝐼𝐵))
144	139	ad2antrr 739	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝐺 ∈ TarskiG)
145	87	ad3antrrr 743	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝑅 ∈ 𝑃)
146	145	ad2antrr 739	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑅 ∈ 𝑃)
147	88	ad5antr 747	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑄 ∈ 𝑃)
148	117	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝐶 ∈ 𝑃)
149	148	ad2antrr 739	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝐶 ∈ 𝑃)
150	90	ad5antr 747	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶))
151		simplr 781	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ 𝑃)
152	114	ad4antr 745	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑅 ≠ 𝑄)
153	142	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑥 ∈ 𝑃)
154	91	necomd 3012	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑄 ≠ 𝑅)
155	154	ad5antr 747	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑄 ≠ 𝑅)
156	141	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑥 ∈ (𝑅𝐿𝑄))
157	8, 10, 65, 144, 147, 146, 153, 155, 156	lncom 28977	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑥 ∈ (𝑄𝐿𝑅))
158		simprl 783	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝑥𝐼𝑅))
159	8, 10, 65, 144, 153, 147, 146, 151, 157, 158	coltr3 29004	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝑄𝐿𝑅))
160	8, 10, 65, 144, 146, 147, 151, 152, 159	lncom 28977	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝑅𝐿𝑄))
161	92	ad5antr 747	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑄 ∈ (𝑅𝐿𝑄))
162	96	ad5antr 747	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝐶 ≠ 𝑄)
163	119	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝐵 ∈ 𝑃)
164	163	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝐵 ∈ 𝑃)
165	12	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝐵 ∈ 𝑃)
166	96	necomd 3012	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑄 ≠ 𝐶)
167	45	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑄 ∈ (𝐵𝐼𝐶))
168	8, 10, 65, 86, 88, 89, 165, 166, 167	btwnlng2 28975	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝐵 ∈ (𝑄𝐿𝐶))
169	168	ad5antr 747	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝐵 ∈ (𝑄𝐿𝐶))
170		simprr 785	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝐶𝐼𝐵))
171	8, 9, 10, 144, 149, 151, 164, 170	tgbtwncom 28838	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝐵𝐼𝐶))
172	8, 10, 65, 144, 164, 147, 149, 151, 169, 171	coltr3 29004	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝑄𝐿𝐶))
173	8, 10, 65, 144, 149, 147, 151, 162, 172	lncom 28977	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝐶𝐿𝑄))
174	8, 10, 65, 86, 89, 88, 96	tglinerflx2 28989	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → 𝑄 ∈ (𝐶𝐿𝑄))
175	174	ad5antr 747	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑄 ∈ (𝐶𝐿𝑄))
176	8, 10, 65, 144, 146, 147, 149, 147, 150, 160, 161, 173, 175	tglineinteq 29001	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 = 𝑄)
177	8, 9, 10, 144, 153, 151, 146, 158	tgbtwncom 28838	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑡 ∈ (𝑅𝐼𝑥))
178	176, 177	eqeltrrd 2863	. . . . . . . 8 ⊢ (((((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) ∧ 𝑡 ∈ 𝑃) ∧ (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵))) → 𝑄 ∈ (𝑅𝐼𝑥))
179	118	ad2antrr 739	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝐴 ∈ 𝑃)
180	8, 9, 10, 139, 179, 142, 163, 143	tgbtwncom 28838	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝑥 ∈ (𝐵𝐼𝐴))
181	24	ad4antr 745	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝐶 ∈ (𝑅𝐼𝐴))
182	8, 9, 10, 139, 163, 145, 179, 142, 148, 180, 181	axtgpasch 28816	. . . . . . . 8 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → ∃𝑡 ∈ 𝑃 (𝑡 ∈ (𝑥𝐼𝑅) ∧ 𝑡 ∈ (𝐶𝐼𝐵)))
183	178, 182	r19.29a 3172	. . . . . . 7 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → 𝑄 ∈ (𝑅𝐼𝑥))
184	142, 143, 183	jca32 525	. . . . . 6 ⊢ (((((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝑅𝐿𝑄)) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥))))
185	184	expl 463	. . . . 5 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → ((𝑥 ∈ (𝑅𝐿𝑄) ∧ 𝑥 ∈ (𝐴𝐼𝐵)) → (𝑥 ∈ 𝑃 ∧ (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))))
186	185	reximdv2 3174	. . . 4 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → (∃𝑥 ∈ (𝑅𝐿𝑄)𝑥 ∈ (𝐴𝐼𝐵) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥))))
187	138, 186	mpd 16	. . 3 ⊢ (((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) ∧ ¬ 𝐵 ∈ (𝑅𝐿𝑄)) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))
188	106, 187	pm2.61dan 825	. 2 ⊢ ((𝜑 ∧ ¬ (𝑅 ∈ (𝑄𝐿𝐶) ∨ 𝑄 = 𝐶)) → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))
189	76, 188	pm2.61dan 825	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐴𝐼𝐵) ∧ 𝑄 ∈ (𝑅𝐼𝑥)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∨ w3o 1102   = wceq 1570   ∈ wcel 2145   ≠ wne 2957  ∃wrex 3088   ∖ cdif 3899   class class class wbr 5107  {copab 5171  ran crn 5660  ‘cfv 6537  (class class class)co 7417  Basecbs 17307  distcds 17357  TarskiGcstrkg 28776  Itvcitv 28782  LineGclng 28783  hlGchlg 28950

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740  ax-cnex 11184  ax-resscn 11185  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-addrcl 11189  ax-mulcl 11190  ax-mulrcl 11191  ax-mulcom 11192  ax-addass 11193  ax-mulass 11194  ax-distr 11195  ax-i2m1 11196  ax-1ne0 11197  ax-1rid 11198  ax-rnegex 11199  ax-rrecex 11200  ax-cnre 11201  ax-pre-lttri 11202  ax-pre-lttrn 11203  ax-pre-ltadd 11204  ax-pre-mulgt0 11205

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4871  df-int 4911  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  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 7374  df-ov 7420  df-oprab 7421  df-mpo 7422  df-om 7867  df-1st 7990  df-2nd 7991  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-1o 8459  df-oadd 8463  df-er 8700  df-map 8832  df-pm 8833  df-en 8957  df-dom 8958  df-sdom 8959  df-fin 8960  df-dju 9910  df-card 9948  df-pnf 11273  df-mnf 11274  df-xr 11275  df-ltxr 11276  df-le 11277  df-sub 11471  df-neg 11472  df-nn 12262  df-2 12331  df-3 12332  df-n0 12533  df-xnn0 12606  df-z 12620  df-uz 12892  df-fz 13566  df-fzo 13714  df-hash 14399  df-word 14583  df-concat 14640  df-s1 14667  df-s2 14923  df-s3 14924  df-trkgc 28797  df-trkgb 28798  df-trkgcb 28799  df-trkgld 28801  df-trkg 28802  df-cgrg 28861  df-leg 28933  df-hlg 28951  df-mir 29012  df-rag 29056  df-perpg 29058

This theorem is used by:  hlpasch  29121