Metamath Proof Explorer

Theorem outsideoftr

Description: Transitivity law for outsideness. Theorem 6.7 of Schwabhauser p. 44. (Contributed by Scott Fenton, 18-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion outsideoftr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N→POutsideOfAB∧POutsideOfBC→POutsideOfAC

Proof

Step Hyp Ref Expression
1 simpll ⊢A≠P∧B≠P∧B≠P∧C≠P→A≠P
2 simplr ⊢A≠P∧B≠P∧B≠P∧C≠P→B≠P
3 simprr ⊢A≠P∧B≠P∧B≠P∧C≠P→C≠P
4 1 2 3 3jca ⊢A≠P∧B≠P∧B≠P∧C≠P→A≠P∧B≠P∧C≠P
5 simplr1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧ABtwnPB∨BBtwnPA∧BBtwnPC∨CBtwnPB→A≠P
6 simplr3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧ABtwnPB∨BBtwnPA∧BBtwnPC∨CBtwnPB→C≠P
7 df-3an ⊢A≠P∧B≠P∧C≠P∧ABtwnPB∧BBtwnPC↔A≠P∧B≠P∧C≠P∧ABtwnPB∧BBtwnPC
8 simp1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N→N∈ℕ
9 simp3r ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N→P∈𝔼⁡N
10 simp2l ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N→A∈𝔼⁡N
11 simp2r ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N→B∈𝔼⁡N
12 simp3l ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N→C∈𝔼⁡N
13 simpr2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧ABtwnPB∧BBtwnPC→ABtwnPB
14 simpr3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧ABtwnPB∧BBtwnPC→BBtwnPC
15 8 9 10 11 12 13 14 btwnexchand ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧ABtwnPB∧BBtwnPC→ABtwnPC
16 15 orcd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧ABtwnPB∧BBtwnPC→ABtwnPC∨CBtwnPA
17 7 16 sylan2br ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧ABtwnPB∧BBtwnPC→ABtwnPC∨CBtwnPA
18 17 expr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧ABtwnPB→BBtwnPC→ABtwnPC∨CBtwnPA
19 simprlr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧ABtwnPB∧CBtwnPB→ABtwnPB
20 simprr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧ABtwnPB∧CBtwnPB→CBtwnPB
21 btwnconn3 ⊢N∈ℕ∧P∈𝔼⁡N∧A∈𝔼⁡N∧C∈𝔼⁡N∧B∈𝔼⁡N→ABtwnPB∧CBtwnPB→ABtwnPC∨CBtwnPA
22 8 9 10 12 11 21 syl122anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N→ABtwnPB∧CBtwnPB→ABtwnPC∨CBtwnPA
23 22 adantr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧ABtwnPB∧CBtwnPB→ABtwnPB∧CBtwnPB→ABtwnPC∨CBtwnPA
24 19 20 23 mp2and ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧ABtwnPB∧CBtwnPB→ABtwnPC∨CBtwnPA
25 24 expr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧ABtwnPB→CBtwnPB→ABtwnPC∨CBtwnPA
26 18 25 jaod ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧ABtwnPB→BBtwnPC∨CBtwnPB→ABtwnPC∨CBtwnPA
27 26 expr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P→ABtwnPB→BBtwnPC∨CBtwnPB→ABtwnPC∨CBtwnPA
28 simpll2 ⊢A≠P∧B≠P∧C≠P∧BBtwnPA∧BBtwnPC→B≠P
29 28 adantl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧BBtwnPA∧BBtwnPC→B≠P
30 29 necomd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧BBtwnPA∧BBtwnPC→P≠B
31 simprlr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧BBtwnPA∧BBtwnPC→BBtwnPA
32 simprr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧BBtwnPA∧BBtwnPC→BBtwnPC
33 btwnconn1 ⊢N∈ℕ∧P∈𝔼⁡N∧B∈𝔼⁡N∧A∈𝔼⁡N∧C∈𝔼⁡N→P≠B∧BBtwnPA∧BBtwnPC→ABtwnPC∨CBtwnPA
34 8 9 11 10 12 33 syl122anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N→P≠B∧BBtwnPA∧BBtwnPC→ABtwnPC∨CBtwnPA
35 34 adantr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧BBtwnPA∧BBtwnPC→P≠B∧BBtwnPA∧BBtwnPC→ABtwnPC∨CBtwnPA
36 30 31 32 35 mp3and ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧BBtwnPA∧BBtwnPC→ABtwnPC∨CBtwnPA
37 36 expr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧BBtwnPA→BBtwnPC→ABtwnPC∨CBtwnPA
38 df-3an ⊢A≠P∧B≠P∧C≠P∧BBtwnPA∧CBtwnPB↔A≠P∧B≠P∧C≠P∧BBtwnPA∧CBtwnPB
39 simpr3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧BBtwnPA∧CBtwnPB→CBtwnPB
40 simpr2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧BBtwnPA∧CBtwnPB→BBtwnPA
41 8 9 12 11 10 39 40 btwnexchand ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧BBtwnPA∧CBtwnPB→CBtwnPA
42 41 olcd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧BBtwnPA∧CBtwnPB→ABtwnPC∨CBtwnPA
43 38 42 sylan2br ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧BBtwnPA∧CBtwnPB→ABtwnPC∨CBtwnPA
44 43 expr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧BBtwnPA→CBtwnPB→ABtwnPC∨CBtwnPA
45 37 44 jaod ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧BBtwnPA→BBtwnPC∨CBtwnPB→ABtwnPC∨CBtwnPA
46 45 expr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P→BBtwnPA→BBtwnPC∨CBtwnPB→ABtwnPC∨CBtwnPA
47 27 46 jaod ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P→ABtwnPB∨BBtwnPA→BBtwnPC∨CBtwnPB→ABtwnPC∨CBtwnPA
48 47 imp32 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧ABtwnPB∨BBtwnPA∧BBtwnPC∨CBtwnPB→ABtwnPC∨CBtwnPA
49 5 6 48 3jca ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N∧A≠P∧B≠P∧C≠P∧ABtwnPB∨BBtwnPA∧BBtwnPC∨CBtwnPB→A≠P∧C≠P∧ABtwnPC∨CBtwnPA
50 49 exp31 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N→A≠P∧B≠P∧C≠P→ABtwnPB∨BBtwnPA∧BBtwnPC∨CBtwnPB→A≠P∧C≠P∧ABtwnPC∨CBtwnPA
51 4 50 syl5 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N→A≠P∧B≠P∧B≠P∧C≠P→ABtwnPB∨BBtwnPA∧BBtwnPC∨CBtwnPB→A≠P∧C≠P∧ABtwnPC∨CBtwnPA
52 51 impd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N→A≠P∧B≠P∧B≠P∧C≠P∧ABtwnPB∨BBtwnPA∧BBtwnPC∨CBtwnPB→A≠P∧C≠P∧ABtwnPC∨CBtwnPA
53 broutsideof2 ⊢N∈ℕ∧P∈𝔼⁡N∧A∈𝔼⁡N∧B∈𝔼⁡N→POutsideOfAB↔A≠P∧B≠P∧ABtwnPB∨BBtwnPA
54 8 9 10 11 53 syl13anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N→POutsideOfAB↔A≠P∧B≠P∧ABtwnPB∨BBtwnPA
55 broutsideof2 ⊢N∈ℕ∧P∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→POutsideOfBC↔B≠P∧C≠P∧BBtwnPC∨CBtwnPB
56 8 9 11 12 55 syl13anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N→POutsideOfBC↔B≠P∧C≠P∧BBtwnPC∨CBtwnPB
57 54 56 anbi12d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N→POutsideOfAB∧POutsideOfBC↔A≠P∧B≠P∧ABtwnPB∨BBtwnPA∧B≠P∧C≠P∧BBtwnPC∨CBtwnPB
58 df-3an ⊢A≠P∧B≠P∧ABtwnPB∨BBtwnPA↔A≠P∧B≠P∧ABtwnPB∨BBtwnPA
59 df-3an ⊢B≠P∧C≠P∧BBtwnPC∨CBtwnPB↔B≠P∧C≠P∧BBtwnPC∨CBtwnPB
60 58 59 anbi12i ⊢A≠P∧B≠P∧ABtwnPB∨BBtwnPA∧B≠P∧C≠P∧BBtwnPC∨CBtwnPB↔A≠P∧B≠P∧ABtwnPB∨BBtwnPA∧B≠P∧C≠P∧BBtwnPC∨CBtwnPB
61 an4 ⊢A≠P∧B≠P∧B≠P∧C≠P∧ABtwnPB∨BBtwnPA∧BBtwnPC∨CBtwnPB↔A≠P∧B≠P∧ABtwnPB∨BBtwnPA∧B≠P∧C≠P∧BBtwnPC∨CBtwnPB
62 60 61 bitr4i ⊢A≠P∧B≠P∧ABtwnPB∨BBtwnPA∧B≠P∧C≠P∧BBtwnPC∨CBtwnPB↔A≠P∧B≠P∧B≠P∧C≠P∧ABtwnPB∨BBtwnPA∧BBtwnPC∨CBtwnPB
63 57 62 bitrdi ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N→POutsideOfAB∧POutsideOfBC↔A≠P∧B≠P∧B≠P∧C≠P∧ABtwnPB∨BBtwnPA∧BBtwnPC∨CBtwnPB
64 broutsideof2 ⊢N∈ℕ∧P∈𝔼⁡N∧A∈𝔼⁡N∧C∈𝔼⁡N→POutsideOfAC↔A≠P∧C≠P∧ABtwnPC∨CBtwnPA
65 8 9 10 12 64 syl13anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N→POutsideOfAC↔A≠P∧C≠P∧ABtwnPC∨CBtwnPA
66 52 63 65 3imtr4d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧P∈𝔼⁡N→POutsideOfAB∧POutsideOfBC→POutsideOfAC