Metamath Proof Explorer

Theorem outpasch

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)

Ref Expression
Hypotheses 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 outpasch ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑄 ∈ ( 𝑅 𝐼 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 outpasch.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 outpasch.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 outpasch.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
4 outpasch.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 outpasch.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6 outpasch.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7 outpasch.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8 outpasch.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑃 )
9 outpasch.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
10 outpasch.1 ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐼 𝑅 ) )
11 outpasch.2 ⊢ ( 𝜑 → 𝑄 ∈ ( 𝐵 𝐼 𝐶 ) )
12 5 adantr ⊢ ( ( 𝜑 ∧ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) → 𝐴 ∈ 𝑃 )
13 simpr ⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐴 ) → 𝑥 = 𝐴 )
14 13 eleq1d ⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐴 ) → ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ↔ 𝐴 ∈ ( 𝐴 𝐼 𝐵 ) ) )
15 13 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐴 ) → ( 𝑅 𝐼 𝑥 ) = ( 𝑅 𝐼 𝐴 ) )
16 15 eleq2d ⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐴 ) → ( 𝑄 ∈ ( 𝑅 𝐼 𝑥 ) ↔ 𝑄 ∈ ( 𝑅 𝐼 𝐴 ) ) )
17 14 16 anbi12d ⊢ ( ( ( 𝜑 ∧ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐴 ) → ( ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑄 ∈ ( 𝑅 𝐼 𝑥 ) ) ↔ ( 𝐴 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑄 ∈ ( 𝑅 𝐼 𝐴 ) ) ) )
18 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
19 1 18 2 4 5 6 tgbtwntriv1 ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 𝐼 𝐵 ) )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) → 𝐴 ∈ ( 𝐴 𝐼 𝐵 ) )
21 4 adantr ⊢ ( ( 𝜑 ∧ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) → 𝐺 ∈ TarskiG )
22 8 adantr ⊢ ( ( 𝜑 ∧ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) → 𝑅 ∈ 𝑃 )
23 9 adantr ⊢ ( ( 𝜑 ∧ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) → 𝑄 ∈ 𝑃 )
24 7 adantr ⊢ ( ( 𝜑 ∧ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) → 𝐶 ∈ 𝑃 )
25 simpr ⊢ ( ( 𝜑 ∧ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) → 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) )
26 1 18 2 4 5 7 8 10 tgbtwncom ⊢ ( 𝜑 → 𝐶 ∈ ( 𝑅 𝐼 𝐴 ) )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) → 𝐶 ∈ ( 𝑅 𝐼 𝐴 ) )
28 1 18 2 21 22 23 24 12 25 27 tgbtwnexch ⊢ ( ( 𝜑 ∧ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) → 𝑄 ∈ ( 𝑅 𝐼 𝐴 ) )
29 20 28 jca ⊢ ( ( 𝜑 ∧ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) → ( 𝐴 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑄 ∈ ( 𝑅 𝐼 𝐴 ) ) )
30 12 17 29 rspcedvd ⊢ ( ( 𝜑 ∧ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑄 ∈ ( 𝑅 𝐼 𝑥 ) ) )
31 30 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑄 ∈ ( 𝑅 𝐼 𝑥 ) ) )
32 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) → 𝐵 ∈ 𝑃 )
33 eleq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ↔ 𝐵 ∈ ( 𝐴 𝐼 𝐵 ) ) )
34 oveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝑅 𝐼 𝑥 ) = ( 𝑅 𝐼 𝐵 ) )
35 34 eleq2d ⊢ ( 𝑥 = 𝐵 → ( 𝑄 ∈ ( 𝑅 𝐼 𝑥 ) ↔ 𝑄 ∈ ( 𝑅 𝐼 𝐵 ) ) )
36 33 35 anbi12d ⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑄 ∈ ( 𝑅 𝐼 𝑥 ) ) ↔ ( 𝐵 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑄 ∈ ( 𝑅 𝐼 𝐵 ) ) ) )
37 36 adantl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → ( ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑄 ∈ ( 𝑅 𝐼 𝑥 ) ) ↔ ( 𝐵 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑄 ∈ ( 𝑅 𝐼 𝐵 ) ) ) )
38 1 18 2 4 5 6 tgbtwntriv2 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐵 ) )
39 38 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) → 𝐵 ∈ ( 𝐴 𝐼 𝐵 ) )
40 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝑅 ∈ ( 𝑄 𝐼 𝐶 ) ) → 𝐺 ∈ TarskiG )
41 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝑅 ∈ ( 𝑄 𝐼 𝐶 ) ) → 𝐶 ∈ 𝑃 )
42 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝑅 ∈ ( 𝑄 𝐼 𝐶 ) ) → 𝑅 ∈ 𝑃 )
43 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝑅 ∈ ( 𝑄 𝐼 𝐶 ) ) → 𝑄 ∈ 𝑃 )
44 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝑅 ∈ ( 𝑄 𝐼 𝐶 ) ) → 𝐵 ∈ 𝑃 )
45 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝑅 ∈ ( 𝑄 𝐼 𝐶 ) ) → 𝑅 ∈ ( 𝑄 𝐼 𝐶 ) )
46 1 18 2 40 43 42 41 45 tgbtwncom ⊢ ( ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝑅 ∈ ( 𝑄 𝐼 𝐶 ) ) → 𝑅 ∈ ( 𝐶 𝐼 𝑄 ) )
47 1 18 2 4 6 9 7 11 tgbtwncom ⊢ ( 𝜑 → 𝑄 ∈ ( 𝐶 𝐼 𝐵 ) )
48 47 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝑅 ∈ ( 𝑄 𝐼 𝐶 ) ) → 𝑄 ∈ ( 𝐶 𝐼 𝐵 ) )
49 1 18 2 40 41 42 43 44 46 48 tgbtwnexch3 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝑅 ∈ ( 𝑄 𝐼 𝐶 ) ) → 𝑄 ∈ ( 𝑅 𝐼 𝐵 ) )
50 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝐶 ∈ ( 𝑄 𝐼 𝑅 ) ) → 𝐺 ∈ TarskiG )
51 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝐶 ∈ ( 𝑄 𝐼 𝑅 ) ) → 𝐵 ∈ 𝑃 )
52 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝐶 ∈ ( 𝑄 𝐼 𝑅 ) ) → 𝑄 ∈ 𝑃 )
53 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝐶 ∈ ( 𝑄 𝐼 𝑅 ) ) → 𝑅 ∈ 𝑃 )
54 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝐶 ∈ ( 𝑄 𝐼 𝑅 ) ) → 𝐶 ∈ 𝑃 )
55 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝐶 ∈ ( 𝑄 𝐼 𝑅 ) ) ∧ 𝑄 = 𝐶 ) → 𝑄 = 𝐶 )
56 1 18 2 4 8 7 tgbtwntriv2 ⊢ ( 𝜑 → 𝐶 ∈ ( 𝑅 𝐼 𝐶 ) )
57 56 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝐶 ∈ ( 𝑄 𝐼 𝑅 ) ) ∧ 𝑄 = 𝐶 ) → 𝐶 ∈ ( 𝑅 𝐼 𝐶 ) )
58 55 57 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝐶 ∈ ( 𝑄 𝐼 𝑅 ) ) ∧ 𝑄 = 𝐶 ) → 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) )
59 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝐶 ∈ ( 𝑄 𝐼 𝑅 ) ) ∧ 𝑄 = 𝐶 ) → ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) )
60 58 59 pm2.65da ⊢ ( ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝐶 ∈ ( 𝑄 𝐼 𝑅 ) ) → ¬ 𝑄 = 𝐶 )
61 60 neqned ⊢ ( ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝐶 ∈ ( 𝑄 𝐼 𝑅 ) ) → 𝑄 ≠ 𝐶 )
62 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝐶 ∈ ( 𝑄 𝐼 𝑅 ) ) → 𝑄 ∈ ( 𝐵 𝐼 𝐶 ) )
63 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝐶 ∈ ( 𝑄 𝐼 𝑅 ) ) → 𝐶 ∈ ( 𝑄 𝐼 𝑅 ) )
64 1 18 2 50 51 52 54 53 61 62 63 tgbtwnouttr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝐶 ∈ ( 𝑄 𝐼 𝑅 ) ) → 𝑄 ∈ ( 𝐵 𝐼 𝑅 ) )
65 1 18 2 50 51 52 53 64 tgbtwncom ⊢ ( ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) ∧ 𝐶 ∈ ( 𝑄 𝐼 𝑅 ) ) → 𝑄 ∈ ( 𝑅 𝐼 𝐵 ) )
66 1 3 2 4 9 7 8 tgcolg ⊢ ( 𝜑 → ( ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ↔ ( 𝑅 ∈ ( 𝑄 𝐼 𝐶 ) ∨ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝑄 𝐼 𝑅 ) ) ) )
67 66 biimpa ⊢ ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) → ( 𝑅 ∈ ( 𝑄 𝐼 𝐶 ) ∨ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝑄 𝐼 𝑅 ) ) )
68 3orcoma ⊢ ( ( 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ∨ 𝑅 ∈ ( 𝑄 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝑄 𝐼 𝑅 ) ) ↔ ( 𝑅 ∈ ( 𝑄 𝐼 𝐶 ) ∨ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝑄 𝐼 𝑅 ) ) )
69 3orass ⊢ ( ( 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ∨ 𝑅 ∈ ( 𝑄 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝑄 𝐼 𝑅 ) ) ↔ ( 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ∨ ( 𝑅 ∈ ( 𝑄 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝑄 𝐼 𝑅 ) ) ) )
70 68 69 bitr3i ⊢ ( ( 𝑅 ∈ ( 𝑄 𝐼 𝐶 ) ∨ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝑄 𝐼 𝑅 ) ) ↔ ( 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ∨ ( 𝑅 ∈ ( 𝑄 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝑄 𝐼 𝑅 ) ) ) )
71 67 70 sylib ⊢ ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) → ( 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ∨ ( 𝑅 ∈ ( 𝑄 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝑄 𝐼 𝑅 ) ) ) )
72 71 orcanai ⊢ ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) → ( 𝑅 ∈ ( 𝑄 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝑄 𝐼 𝑅 ) ) )
73 49 65 72 mpjaodan ⊢ ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) → 𝑄 ∈ ( 𝑅 𝐼 𝐵 ) )
74 39 73 jca ⊢ ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) → ( 𝐵 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑄 ∈ ( 𝑅 𝐼 𝐵 ) ) )
75 32 37 74 rspcedvd ⊢ ( ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝑄 ∈ ( 𝑅 𝐼 𝐶 ) ) → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑄 ∈ ( 𝑅 𝐼 𝑥 ) ) )
76 31 75 pm2.61dan ⊢ ( ( 𝜑 ∧ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑄 ∈ ( 𝑅 𝐼 𝑥 ) ) )
77 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝐵 ∈ 𝑃 )
78 36 adantl ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 = 𝐵 ) → ( ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑄 ∈ ( 𝑅 𝐼 𝑥 ) ) ↔ ( 𝐵 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑄 ∈ ( 𝑅 𝐼 𝐵 ) ) ) )
79 38 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝐵 ∈ ( 𝐴 𝐼 𝐵 ) )
80 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝐺 ∈ TarskiG )
81 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝑅 ∈ 𝑃 )
82 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝑄 ∈ 𝑃 )
83 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝐶 ∈ 𝑃 )
84 simplr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) )
85 simpr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) )
86 4 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) → 𝐺 ∈ TarskiG )
87 8 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) → 𝑅 ∈ 𝑃 )
88 9 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) → 𝑄 ∈ 𝑃 )
89 7 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) → 𝐶 ∈ 𝑃 )
90 simpr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) → ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) )
91 1 2 3 86 87 88 89 90 ncolne1 ⊢ ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) → 𝑅 ≠ 𝑄 )
92 1 2 3 86 87 88 91 tglinerflx2 ⊢ ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) → 𝑄 ∈ ( 𝑅 𝐿 𝑄 ) )
93 92 adantr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝑄 ∈ ( 𝑅 𝐿 𝑄 ) )
94 1 3 2 86 88 89 87 90 ncolcom ⊢ ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) → ¬ ( 𝑅 ∈ ( 𝐶 𝐿 𝑄 ) ∨ 𝐶 = 𝑄 ) )
95 1 3 2 86 89 88 87 94 ncolrot1 ⊢ ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) → ¬ ( 𝐶 ∈ ( 𝑄 𝐿 𝑅 ) ∨ 𝑄 = 𝑅 ) )
96 1 2 3 86 89 88 87 95 ncolne1 ⊢ ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) → 𝐶 ≠ 𝑄 )
97 96 adantr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝐶 ≠ 𝑄 )
98 47 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝑄 ∈ ( 𝐶 𝐼 𝐵 ) )
99 1 2 3 80 83 82 77 97 98 btwnlng3 ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝐵 ∈ ( 𝐶 𝐿 𝑄 ) )
100 1 2 3 80 83 82 97 tglinerflx2 ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝑄 ∈ ( 𝐶 𝐿 𝑄 ) )
101 1 2 3 80 81 82 83 82 84 85 93 99 100 tglineinteq ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝐵 = 𝑄 )
102 1 18 2 4 8 6 tgbtwntriv2 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝑅 𝐼 𝐵 ) )
103 102 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝐵 ∈ ( 𝑅 𝐼 𝐵 ) )
104 101 103 eqeltrrd ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝑄 ∈ ( 𝑅 𝐼 𝐵 ) )
105 79 104 jca ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → ( 𝐵 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑄 ∈ ( 𝑅 𝐼 𝐵 ) ) )
106 77 78 105 rspcedvd ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑄 ∈ ( 𝑅 𝐼 𝑥 ) ) )
107 eleq1 ⊢ ( 𝑡 = 𝑥 → ( 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ↔ 𝑥 ∈ ( 𝑎 𝐼 𝑏 ) ) )
108 107 cbvrexvw ⊢ ( ∃ 𝑡 ∈ ( 𝑅 𝐿 𝑄 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ↔ ∃ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) 𝑥 ∈ ( 𝑎 𝐼 𝑏 ) )
109 108 anbi2i ⊢ ( ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑅 𝐿 𝑄 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑅 𝐿 𝑄 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) ↔ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑅 𝐿 𝑄 ) ) ) ∧ ∃ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) 𝑥 ∈ ( 𝑎 𝐼 𝑏 ) ) )
110 109 opabbii ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑅 𝐿 𝑄 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑅 𝐿 𝑄 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑅 𝐿 𝑄 ) ) ) ∧ ∃ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) 𝑥 ∈ ( 𝑎 𝐼 𝑏 ) ) }
111 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝐺 ∈ TarskiG )
112 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝑅 ∈ 𝑃 )
113 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝑄 ∈ 𝑃 )
114 91 adantr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝑅 ≠ 𝑄 )
115 1 2 3 111 112 113 114 tgelrnln ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → ( 𝑅 𝐿 𝑄 ) ∈ ran 𝐿 )
116 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
117 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝐶 ∈ 𝑃 )
118 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝐴 ∈ 𝑃 )
119 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝐵 ∈ 𝑃 )
120 92 adantr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝑄 ∈ ( 𝑅 𝐿 𝑄 ) )
121 1 3 2 86 88 89 87 90 ncolrot2 ⊢ ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) → ¬ ( 𝐶 ∈ ( 𝑅 𝐿 𝑄 ) ∨ 𝑅 = 𝑄 ) )
122 pm2.45 ⊢ ( ¬ ( 𝐶 ∈ ( 𝑅 𝐿 𝑄 ) ∨ 𝑅 = 𝑄 ) → ¬ 𝐶 ∈ ( 𝑅 𝐿 𝑄 ) )
123 121 122 syl ⊢ ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) → ¬ 𝐶 ∈ ( 𝑅 𝐿 𝑄 ) )
124 123 adantr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → ¬ 𝐶 ∈ ( 𝑅 𝐿 𝑄 ) )
125 simpr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) )
126 47 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝑄 ∈ ( 𝐶 𝐼 𝐵 ) )
127 1 18 2 110 117 119 120 124 125 126 islnoppd ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝐶 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑅 𝐿 𝑄 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑅 𝐿 𝑄 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) } 𝐵 )
128 1 2 3 86 87 88 91 tglinerflx1 ⊢ ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) → 𝑅 ∈ ( 𝑅 𝐿 𝑄 ) )
129 128 adantr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝑅 ∈ ( 𝑅 𝐿 𝑄 ) )
130 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝐶 ∈ ( 𝑅 𝐼 𝐴 ) )
131 1 2 3 86 89 87 88 121 ncolne1 ⊢ ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) → 𝐶 ≠ 𝑅 )
132 131 adantr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝐶 ≠ 𝑅 )
133 1 18 2 111 112 117 118 130 132 tgbtwnne ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝑅 ≠ 𝐴 )
134 1 2 116 112 118 117 111 118 130 133 132 btwnhl1 ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝐶 ( ( hlG ‘ 𝐺 ) ‘ 𝑅 ) 𝐴 )
135 1 18 2 110 3 115 111 116 117 118 119 127 129 134 opphl ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → 𝐴 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑅 𝐿 𝑄 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑅 𝐿 𝑄 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) } 𝐵 )
136 1 18 2 110 118 119 islnopp ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → ( 𝐴 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑅 𝐿 𝑄 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑅 𝐿 𝑄 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) } 𝐵 ↔ ( ( ¬ 𝐴 ∈ ( 𝑅 𝐿 𝑄 ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ ∃ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) ) )
137 135 136 mpbid ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → ( ( ¬ 𝐴 ∈ ( 𝑅 𝐿 𝑄 ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ ∃ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) )
138 137 simprd ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → ∃ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) )
139 111 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐺 ∈ TarskiG )
140 115 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) → ( 𝑅 𝐿 𝑄 ) ∈ ran 𝐿 )
141 simplr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) )
142 1 3 2 139 140 141 tglnpt ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝑥 ∈ 𝑃 )
143 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) )
144 139 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝐺 ∈ TarskiG )
145 87 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝑅 ∈ 𝑃 )
146 145 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝑅 ∈ 𝑃 )
147 88 ad5antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝑄 ∈ 𝑃 )
148 117 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐶 ∈ 𝑃 )
149 148 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝐶 ∈ 𝑃 )
150 90 ad5antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) )
151 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝑡 ∈ 𝑃 )
152 114 ad4antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝑅 ≠ 𝑄 )
153 142 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝑥 ∈ 𝑃 )
154 91 necomd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) → 𝑄 ≠ 𝑅 )
155 154 ad5antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝑄 ≠ 𝑅 )
156 141 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) )
157 1 2 3 144 147 146 153 155 156 lncom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝑥 ∈ ( 𝑄 𝐿 𝑅 ) )
158 simprl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) )
159 1 2 3 144 153 147 146 151 157 158 coltr3 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝑡 ∈ ( 𝑄 𝐿 𝑅 ) )
160 1 2 3 144 146 147 151 152 159 lncom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝑡 ∈ ( 𝑅 𝐿 𝑄 ) )
161 92 ad5antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝑄 ∈ ( 𝑅 𝐿 𝑄 ) )
162 96 ad5antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝐶 ≠ 𝑄 )
163 119 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐵 ∈ 𝑃 )
164 163 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝐵 ∈ 𝑃 )
165 6 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) → 𝐵 ∈ 𝑃 )
166 96 necomd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) → 𝑄 ≠ 𝐶 )
167 11 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) → 𝑄 ∈ ( 𝐵 𝐼 𝐶 ) )
168 1 2 3 86 88 89 165 166 167 btwnlng2 ⊢ ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) → 𝐵 ∈ ( 𝑄 𝐿 𝐶 ) )
169 168 ad5antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝐵 ∈ ( 𝑄 𝐿 𝐶 ) )
170 simprr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝑡 ∈ ( 𝐶 𝐼 𝐵 ) )
171 1 18 2 144 149 151 164 170 tgbtwncom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝑡 ∈ ( 𝐵 𝐼 𝐶 ) )
172 1 2 3 144 164 147 149 151 169 171 coltr3 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝑡 ∈ ( 𝑄 𝐿 𝐶 ) )
173 1 2 3 144 149 147 151 162 172 lncom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝑡 ∈ ( 𝐶 𝐿 𝑄 ) )
174 1 2 3 86 89 88 96 tglinerflx2 ⊢ ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) → 𝑄 ∈ ( 𝐶 𝐿 𝑄 ) )
175 174 ad5antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝑄 ∈ ( 𝐶 𝐿 𝑄 ) )
176 1 2 3 144 146 147 149 147 150 160 161 173 175 tglineinteq ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝑡 = 𝑄 )
177 1 18 2 144 153 151 146 158 tgbtwncom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝑡 ∈ ( 𝑅 𝐼 𝑥 ) )
178 176 177 eqeltrrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝐵 ) ) ) → 𝑄 ∈ ( 𝑅 𝐼 𝑥 ) )
179 118 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐴 ∈ 𝑃 )
180 1 18 2 139 179 142 163 143 tgbtwncom ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝑥 ∈ ( 𝐵 𝐼 𝐴 ) )
181 26 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝐶 ∈ ( 𝑅 𝐼 𝐴 ) )
182 1 18 2 139 163 145 179 142 148 180 181 axtgpasch ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) → ∃ 𝑡 ∈ 𝑃 ( 𝑡 ∈ ( 𝑥 𝐼 𝑅 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝐵 ) ) )
183 178 182 r19.29a ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) → 𝑄 ∈ ( 𝑅 𝐼 𝑥 ) )
184 142 143 183 jca32 ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) → ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑄 ∈ ( 𝑅 𝐼 𝑥 ) ) ) )
185 184 expl ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → ( ( 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ) → ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑄 ∈ ( 𝑅 𝐼 𝑥 ) ) ) ) )
186 185 reximdv2 ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → ( ∃ 𝑥 ∈ ( 𝑅 𝐿 𝑄 ) 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑄 ∈ ( 𝑅 𝐼 𝑥 ) ) ) )
187 138 186 mpd ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) ∧ ¬ 𝐵 ∈ ( 𝑅 𝐿 𝑄 ) ) → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑄 ∈ ( 𝑅 𝐼 𝑥 ) ) )
188 106 187 pm2.61dan ⊢ ( ( 𝜑 ∧ ¬ ( 𝑅 ∈ ( 𝑄 𝐿 𝐶 ) ∨ 𝑄 = 𝐶 ) ) → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑄 ∈ ( 𝑅 𝐼 𝑥 ) ) )
189 76 188 pm2.61dan ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑄 ∈ ( 𝑅 𝐼 𝑥 ) ) )