Metamath Proof Explorer

Theorem tglineeltr

Description: Transitivity law for lines, one half of tglineelsb2 . (Contributed by Thierry Arnoux, 25-May-2019)

Ref Expression
Hypotheses tglineelsb2.p ⊢ 𝐵 = ( Base ‘ 𝐺 )
tglineelsb2.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tglineelsb2.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
tglineelsb2.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tglineelsb2.1 ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
tglineelsb2.2 ⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
tglineelsb2.4 ⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
tglineelsb2.3 ⊢ ( 𝜑 → 𝑆 ∈ 𝐵 )
tglineelsb2.5 ⊢ ( 𝜑 → 𝑆 ≠ 𝑃 )
tglineelsb2.6 ⊢ ( 𝜑 → 𝑆 ∈ ( 𝑃 𝐿 𝑄 ) )
tglineeltr.7 ⊢ ( 𝜑 → 𝑅 ∈ 𝐵 )
tglineeltr.8 ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑃 𝐿 𝑆 ) )
Assertion tglineeltr ( 𝜑 → 𝑅 ∈ ( 𝑃 𝐿 𝑄 ) )

Proof

Step Hyp Ref Expression
1 tglineelsb2.p ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 tglineelsb2.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 tglineelsb2.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
4 tglineelsb2.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 tglineelsb2.1 ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
6 tglineelsb2.2 ⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
7 tglineelsb2.4 ⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
8 tglineelsb2.3 ⊢ ( 𝜑 → 𝑆 ∈ 𝐵 )
9 tglineelsb2.5 ⊢ ( 𝜑 → 𝑆 ≠ 𝑃 )
10 tglineelsb2.6 ⊢ ( 𝜑 → 𝑆 ∈ ( 𝑃 𝐿 𝑄 ) )
11 tglineeltr.7 ⊢ ( 𝜑 → 𝑅 ∈ 𝐵 )
12 tglineeltr.8 ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑃 𝐿 𝑆 ) )
13 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → 𝐺 ∈ TarskiG )
14 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → 𝑃 ∈ 𝐵 )
15 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → 𝑄 ∈ 𝐵 )
16 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → 𝑅 ∈ 𝐵 )
17 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
18 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → 𝑆 ∈ 𝐵 )
19 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) )
20 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) )
21 1 17 2 13 14 16 18 15 19 20 tgbtwnexch ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → 𝑅 ∈ ( 𝑃 𝐼 𝑄 ) )
22 1 3 2 13 14 15 16 21 btwncolg1 ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → ( 𝑅 ∈ ( 𝑃 𝐿 𝑄 ) ∨ 𝑃 = 𝑄 ) )
23 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → 𝐺 ∈ TarskiG )
24 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → 𝑃 ∈ 𝐵 )
25 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → 𝑄 ∈ 𝐵 )
26 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → 𝑅 ∈ 𝐵 )
27 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → 𝑆 ∈ 𝐵 )
28 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) )
29 1 17 2 23 24 26 27 28 tgbtwncom ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → 𝑅 ∈ ( 𝑆 𝐼 𝑃 ) )
30 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) )
31 1 17 2 23 27 26 24 25 29 30 tgbtwnexch3 ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → 𝑃 ∈ ( 𝑅 𝐼 𝑄 ) )
32 1 3 2 23 24 25 26 31 btwncolg2 ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → ( 𝑅 ∈ ( 𝑃 𝐿 𝑄 ) ∨ 𝑃 = 𝑄 ) )
33 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) ∧ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) → 𝐺 ∈ TarskiG )
34 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) ∧ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) → 𝑃 ∈ 𝐵 )
35 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) ∧ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) → 𝑅 ∈ 𝐵 )
36 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) ∧ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) → 𝑄 ∈ 𝐵 )
37 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) ∧ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) → 𝑆 ∈ 𝐵 )
38 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) ∧ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) → 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) )
39 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) ∧ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) → 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) )
40 1 2 33 34 35 36 37 38 39 3 tgbtwnconnln3 ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) ∧ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) → ( 𝑅 ∈ ( 𝑃 𝐿 𝑄 ) ∨ 𝑃 = 𝑄 ) )
41 1 3 2 4 5 6 7 8 tgellng ⊢ ( 𝜑 → ( 𝑆 ∈ ( 𝑃 𝐿 𝑄 ) ↔ ( 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ∨ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ∨ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) ) )
42 10 41 mpbid ⊢ ( 𝜑 → ( 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ∨ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ∨ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) )
43 42 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) → ( 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ∨ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ∨ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) )
44 22 32 40 43 mpjao3dan ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) → ( 𝑅 ∈ ( 𝑃 𝐿 𝑄 ) ∨ 𝑃 = 𝑄 ) )
45 44 an32s ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) ∧ 𝑅 ∈ 𝐵 ) → ( 𝑅 ∈ ( 𝑃 𝐿 𝑄 ) ∨ 𝑃 = 𝑄 ) )
46 11 45 mpidan ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ) → ( 𝑅 ∈ ( 𝑃 𝐿 𝑄 ) ∨ 𝑃 = 𝑄 ) )
47 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → 𝐺 ∈ TarskiG )
48 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → 𝑃 ∈ 𝐵 )
49 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → 𝑄 ∈ 𝐵 )
50 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → 𝑅 ∈ 𝐵 )
51 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → 𝑆 ∈ 𝐵 )
52 9 necomd ⊢ ( 𝜑 → 𝑃 ≠ 𝑆 )
53 52 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → 𝑃 ≠ 𝑆 )
54 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) )
55 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) )
56 1 17 2 47 50 48 51 49 53 54 55 tgbtwnouttr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → 𝑃 ∈ ( 𝑅 𝐼 𝑄 ) )
57 1 3 2 47 48 49 50 56 btwncolg2 ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → ( 𝑅 ∈ ( 𝑃 𝐿 𝑄 ) ∨ 𝑃 = 𝑄 ) )
58 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → 𝐺 ∈ TarskiG )
59 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → 𝑄 ∈ 𝐵 )
60 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → 𝑅 ∈ 𝐵 )
61 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → 𝑃 ∈ 𝐵 )
62 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → 𝑆 ∈ 𝐵 )
63 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → 𝑆 ≠ 𝑃 )
64 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) )
65 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) )
66 1 17 2 58 60 61 62 65 tgbtwncom ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → 𝑃 ∈ ( 𝑆 𝐼 𝑅 ) )
67 1 2 58 62 61 59 60 3 63 64 66 tgbtwnconnln2 ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → ( 𝑃 ∈ ( 𝑄 𝐿 𝑅 ) ∨ 𝑄 = 𝑅 ) )
68 1 3 2 58 59 60 61 67 colrot2 ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → ( 𝑅 ∈ ( 𝑃 𝐿 𝑄 ) ∨ 𝑃 = 𝑄 ) )
69 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) → 𝐺 ∈ TarskiG )
70 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) → 𝑄 ∈ 𝐵 )
71 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) → 𝑃 ∈ 𝐵 )
72 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) → 𝑅 ∈ 𝐵 )
73 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) → 𝑆 ∈ 𝐵 )
74 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) → 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) )
75 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) → 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) )
76 1 17 2 69 70 71 72 73 74 75 tgbtwnintr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) → 𝑃 ∈ ( 𝑄 𝐼 𝑅 ) )
77 1 3 2 69 70 71 72 76 btwncolg3 ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) → ( 𝑅 ∈ ( 𝑄 𝐿 𝑃 ) ∨ 𝑄 = 𝑃 ) )
78 1 3 2 69 70 71 72 77 colcom ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) → ( 𝑅 ∈ ( 𝑃 𝐿 𝑄 ) ∨ 𝑃 = 𝑄 ) )
79 42 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) → ( 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ∨ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ∨ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) )
80 57 68 78 79 mpjao3dan ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) → ( 𝑅 ∈ ( 𝑃 𝐿 𝑄 ) ∨ 𝑃 = 𝑄 ) )
81 80 an32s ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) ∧ 𝑅 ∈ 𝐵 ) → ( 𝑅 ∈ ( 𝑃 𝐿 𝑄 ) ∨ 𝑃 = 𝑄 ) )
82 11 81 mpidan ⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ) → ( 𝑅 ∈ ( 𝑃 𝐿 𝑄 ) ∨ 𝑃 = 𝑄 ) )
83 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → 𝐺 ∈ TarskiG )
84 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → 𝑄 ∈ 𝐵 )
85 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → 𝑅 ∈ 𝐵 )
86 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → 𝑃 ∈ 𝐵 )
87 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → 𝑆 ∈ 𝐵 )
88 52 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → 𝑃 ≠ 𝑆 )
89 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) )
90 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) )
91 1 2 83 86 87 84 85 3 88 89 90 tgbtwnconnln1 ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → ( 𝑃 ∈ ( 𝑄 𝐿 𝑅 ) ∨ 𝑄 = 𝑅 ) )
92 1 3 2 83 84 85 86 91 colrot2 ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ) → ( 𝑅 ∈ ( 𝑃 𝐿 𝑄 ) ∨ 𝑃 = 𝑄 ) )
93 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → 𝐺 ∈ TarskiG )
94 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → 𝑃 ∈ 𝐵 )
95 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → 𝑄 ∈ 𝐵 )
96 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → 𝑅 ∈ 𝐵 )
97 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → 𝑆 ∈ 𝐵 )
98 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → 𝑆 ≠ 𝑃 )
99 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) )
100 1 17 2 93 94 97 96 99 tgbtwncom ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → 𝑆 ∈ ( 𝑅 𝐼 𝑃 ) )
101 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) )
102 1 17 2 93 96 97 94 95 98 100 101 tgbtwnouttr2 ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → 𝑃 ∈ ( 𝑅 𝐼 𝑄 ) )
103 1 3 2 93 94 95 96 102 btwncolg2 ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ) → ( 𝑅 ∈ ( 𝑃 𝐿 𝑄 ) ∨ 𝑃 = 𝑄 ) )
104 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) → 𝐺 ∈ TarskiG )
105 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) → 𝑃 ∈ 𝐵 )
106 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) → 𝑄 ∈ 𝐵 )
107 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) → 𝑅 ∈ 𝐵 )
108 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) → 𝑆 ∈ 𝐵 )
109 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) → 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) )
110 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) → 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) )
111 1 17 2 104 105 106 108 107 109 110 tgbtwnexch ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) → 𝑄 ∈ ( 𝑃 𝐼 𝑅 ) )
112 1 3 2 104 105 106 107 111 btwncolg3 ⊢ ( ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) → ( 𝑅 ∈ ( 𝑃 𝐿 𝑄 ) ∨ 𝑃 = 𝑄 ) )
113 42 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) → ( 𝑆 ∈ ( 𝑃 𝐼 𝑄 ) ∨ 𝑃 ∈ ( 𝑆 𝐼 𝑄 ) ∨ 𝑄 ∈ ( 𝑃 𝐼 𝑆 ) ) )
114 92 103 112 113 mpjao3dan ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) → ( 𝑅 ∈ ( 𝑃 𝐿 𝑄 ) ∨ 𝑃 = 𝑄 ) )
115 114 an32s ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ∧ 𝑅 ∈ 𝐵 ) → ( 𝑅 ∈ ( 𝑃 𝐿 𝑄 ) ∨ 𝑃 = 𝑄 ) )
116 11 115 mpidan ⊢ ( ( 𝜑 ∧ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) → ( 𝑅 ∈ ( 𝑃 𝐿 𝑄 ) ∨ 𝑃 = 𝑄 ) )
117 id ⊢ ( 𝜑 → 𝜑 )
118 4 adantr ⊢ ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) → 𝐺 ∈ TarskiG )
119 5 adantr ⊢ ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) → 𝑃 ∈ 𝐵 )
120 8 adantr ⊢ ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) → 𝑆 ∈ 𝐵 )
121 52 adantr ⊢ ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) → 𝑃 ≠ 𝑆 )
122 simpr ⊢ ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) → 𝑅 ∈ 𝐵 )
123 1 3 2 118 119 120 121 122 tgellng ⊢ ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) → ( 𝑅 ∈ ( 𝑃 𝐿 𝑆 ) ↔ ( 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ∨ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ∨ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) ) )
124 123 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑅 ∈ 𝐵 ) ∧ 𝑅 ∈ ( 𝑃 𝐿 𝑆 ) ) → ( 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ∨ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ∨ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) )
125 117 11 12 124 syl21anc ⊢ ( 𝜑 → ( 𝑅 ∈ ( 𝑃 𝐼 𝑆 ) ∨ 𝑃 ∈ ( 𝑅 𝐼 𝑆 ) ∨ 𝑆 ∈ ( 𝑃 𝐼 𝑅 ) ) )
126 46 82 116 125 mpjao3dan ⊢ ( 𝜑 → ( 𝑅 ∈ ( 𝑃 𝐿 𝑄 ) ∨ 𝑃 = 𝑄 ) )
127 7 neneqd ⊢ ( 𝜑 → ¬ 𝑃 = 𝑄 )
128 pm5.61 ⊢ ( ( ( 𝑅 ∈ ( 𝑃 𝐿 𝑄 ) ∨ 𝑃 = 𝑄 ) ∧ ¬ 𝑃 = 𝑄 ) ↔ ( 𝑅 ∈ ( 𝑃 𝐿 𝑄 ) ∧ ¬ 𝑃 = 𝑄 ) )
129 128 simplbi ⊢ ( ( ( 𝑅 ∈ ( 𝑃 𝐿 𝑄 ) ∨ 𝑃 = 𝑄 ) ∧ ¬ 𝑃 = 𝑄 ) → 𝑅 ∈ ( 𝑃 𝐿 𝑄 ) )
130 126 127 129 syl2anc ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑃 𝐿 𝑄 ) )