P. 361 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36001-36100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	brapply 36001	Binary relation form of the Apply function. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩Apply𝐶 ↔ 𝐶 = (𝐴‘𝐵))
Theorem	brcup 36002	Binary relation form of the Cup function. (Contributed by Scott Fenton, 14-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩Cup𝐶 ↔ 𝐶 = (𝐴 ∪ 𝐵))
Theorem	brcap 36003	Binary relation form of the Cap function. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩Cap𝐶 ↔ 𝐶 = (𝐴 ∩ 𝐵))
Theorem	lemsuccf 36004*	Lemma for unfolding different forms of the Succ function. (Contributed by Scott Fenton, 14-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (∃𝑥(𝐴( I ⊗ Singleton)𝑥 ∧ 𝑥Cup𝐵) ↔ 𝐵 = suc 𝐴)
Theorem	brsuccf 36005	Binary relation form of the Succ function. (Contributed by Scott Fenton, 14-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴Succ𝐵 ↔ 𝐵 = suc 𝐴)
Theorem	dfsuccf2 36006*	Alternate definition of Scott Fenton's version of Succ, cf. df-sucmap 38495. (Contributed by Peter Mazsa, 6-Jan-2026.)
⊢ Succ = {⟨𝑚, 𝑛⟩ ∣ suc 𝑚 = 𝑛}
Theorem	funpartlem 36007*	Lemma for funpartfun 36008. Show membership in the restriction. (Contributed by Scott Fenton, 4-Dec-2017.)
⊢ (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )) ↔ ∃𝑥(𝐹 “ {𝐴}) = {𝑥})
Theorem	funpartfun 36008	The functional part of 𝐹 is a function. (Contributed by Scott Fenton, 16-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ Fun Funpart𝐹
Theorem	funpartss 36009	The functional part of 𝐹 is a subset of 𝐹. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ Funpart𝐹 ⊆ 𝐹
Theorem	funpartfv 36010	The function value of the functional part is identical to the original functional value. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (Funpart𝐹‘𝐴) = (𝐹‘𝐴)
Theorem	fullfunfnv 36011	The full functional part of 𝐹 is a function over V. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ FullFun𝐹 Fn V
Theorem	fullfunfv 36012	The function value of the full function of 𝐹 agrees with 𝐹. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (FullFun𝐹‘𝐴) = (𝐹‘𝐴)
Theorem	brfullfun 36013	A binary relation form condition for the full function. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴FullFun𝐹𝐵 ↔ 𝐵 = (𝐹‘𝐴))
Theorem	brrestrict 36014	Binary relation form of the Restrict function. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩Restrict𝐶 ↔ 𝐶 = (𝐴 ↾ 𝐵))
Theorem	dfrecs2 36015	A quantifier-free definition of recs. (Contributed by Scott Fenton, 17-Jul-2020.)
⊢ recs(𝐹) = ∪ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict))))
Theorem	dfrdg4 36016	A quantifier-free definition of the recursive definition generator. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ rec(𝐹, 𝐴) = ∪ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))))
Theorem	dfint3 36017	Quantifier-free definition of class intersection. (Contributed by Scott Fenton, 13-Apr-2018.)
⊢ ∩ 𝐴 = (V ∖ (◡(V ∖ E ) “ 𝐴))
Theorem	imagesset 36018	The Image functor applied to the converse of the subset relationship yields a subset of the subset relationship. (Contributed by Scott Fenton, 14-Apr-2018.)
⊢ Image◡ SSet ⊆ SSet
Theorem	brub 36019*	Binary relation form of the upper bound functor. (Contributed by Scott Fenton, 3-May-2018.)
⊢ 𝑆 ∈ V    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ (𝑆UB𝑅𝐴 ↔ ∀𝑥 ∈ 𝑆 𝑥𝑅𝐴)
Theorem	brlb 36020*	Binary relation form of the lower bound functor. (Contributed by Scott Fenton, 3-May-2018.)
⊢ 𝑆 ∈ V    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ (𝑆LB𝑅𝐴 ↔ ∀𝑥 ∈ 𝑆 𝐴𝑅𝑥)
21.11.16  Alternate ordered pairs
Syntax	caltop 36021	Declare the syntax for an alternate ordered pair.
class ⟪𝐴, 𝐵⟫
Syntax	caltxp 36022	Declare the syntax for an alternate Cartesian product.
class (𝐴 ×× 𝐵)
Definition	df-altop 36023	An alternative definition of ordered pairs. This definition removes a hypothesis from its defining theorem (see altopth 36034), making it more convenient in some circumstances. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ ⟪𝐴, 𝐵⟫ = {{𝐴}, {𝐴, {𝐵}}}
Definition	df-altxp 36024*	Define Cartesian products of alternative ordered pairs. (Contributed by Scott Fenton, 23-Mar-2012.)
⊢ (𝐴 ×× 𝐵) = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = ⟪𝑥, 𝑦⟫}
Theorem	altopex 36025	Alternative ordered pairs always exist. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ ⟪𝐴, 𝐵⟫ ∈ V
Theorem	altopthsn 36026	Two alternate ordered pairs are equal iff the singletons of their respective elements are equal. Note that this holds regardless of sethood of any of the elements. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ ({𝐴} = {𝐶} ∧ {𝐵} = {𝐷}))
Theorem	altopeq12 36027	Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → ⟪𝐴, 𝐶⟫ = ⟪𝐵, 𝐷⟫)
Theorem	altopeq1 36028	Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ (𝐴 = 𝐵 → ⟪𝐴, 𝐶⟫ = ⟪𝐵, 𝐶⟫)
Theorem	altopeq2 36029	Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ (𝐴 = 𝐵 → ⟪𝐶, 𝐴⟫ = ⟪𝐶, 𝐵⟫)
Theorem	altopth1 36030	Equality of the first members of equal alternate ordered pairs, which holds regardless of the second members' sethood. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ (𝐴 ∈ 𝑉 → (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ → 𝐴 = 𝐶))
Theorem	altopth2 36031	Equality of the second members of equal alternate ordered pairs, which holds regardless of the first members' sethood. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ (𝐵 ∈ 𝑉 → (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ → 𝐵 = 𝐷))
Theorem	altopthg 36032	Alternate ordered pair theorem. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	altopthbg 36033	Alternate ordered pair theorem. (Contributed by Scott Fenton, 14-Apr-2012.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	altopth 36034	The alternate ordered pair theorem. If two alternate ordered pairs are equal, their first elements are equal and their second elements are equal. Note that 𝐶 and 𝐷 are not required to be a set due to a peculiarity of our specific ordered pair definition, as opposed to the regular ordered pairs used here, which (as in opth 5419), requires 𝐷 to be a set. (Contributed by Scott Fenton, 23-Mar-2012.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	altopthb 36035	Alternate ordered pair theorem with different sethood requirements. See altopth 36034 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	altopthc 36036	Alternate ordered pair theorem with different sethood requirements. See altopth 36034 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	altopthd 36037	Alternate ordered pair theorem with different sethood requirements. See altopth 36034 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.)
⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	altxpeq1 36038	Equality for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.)
⊢ (𝐴 = 𝐵 → (𝐴 ×× 𝐶) = (𝐵 ×× 𝐶))
Theorem	altxpeq2 36039	Equality for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.)
⊢ (𝐴 = 𝐵 → (𝐶 ×× 𝐴) = (𝐶 ×× 𝐵))
Theorem	elaltxp 36040*	Membership in alternate Cartesian products. (Contributed by Scott Fenton, 23-Mar-2012.)
⊢ (𝑋 ∈ (𝐴 ×× 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑋 = ⟪𝑥, 𝑦⟫)
Theorem	altopelaltxp 36041	Alternate ordered pair membership in a Cartesian product. Note that, unlike opelxp 5655, there is no sethood requirement here. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ (⟪𝑋, 𝑌⟫ ∈ (𝐴 ×× 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵))
Theorem	altxpsspw 36042	An inclusion rule for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.)
⊢ (𝐴 ×× 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝒫 𝐵)
Theorem	altxpexg 36043	The alternate Cartesian product of two sets is a set. (Contributed by Scott Fenton, 24-Mar-2012.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ×× 𝐵) ∈ V)
Theorem	rankaltopb 36044	Compute the rank of an alternate ordered pair. (Contributed by Scott Fenton, 18-Dec-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) → (rank‘⟪𝐴, 𝐵⟫) = suc suc ((rank‘𝐴) ∪ suc (rank‘𝐵)))
Theorem	nfaltop 36045	Bound-variable hypothesis builder for alternate ordered pairs. (Contributed by Scott Fenton, 25-Sep-2015.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥⟪𝐴, 𝐵⟫
Theorem	sbcaltop 36046*	Distribution of class substitution over alternate ordered pairs. (Contributed by Scott Fenton, 25-Sep-2015.)
⊢ (𝐴 ∈ V → ⦋𝐴 / 𝑥⦌⟪𝐶, 𝐷⟫ = ⟪⦋𝐴 / 𝑥⦌𝐶, ⦋𝐴 / 𝑥⦌𝐷⟫)
21.11.17  Geometry in the Euclidean space
21.11.17.1  Congruence properties
Syntax	cofs 36047	Declare the syntax for the outer five segment configuration.
class OuterFiveSeg
Definition	df-ofs 36048*	The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom (ax5seg 28918). See brofs 36070 and 5segofs 36071 for how it is used. Definition 2.10 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 21-Sep-2013.)
⊢ OuterFiveSeg = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))}
Theorem	cgrrflx2d 36049	Deduction form of axcgrrflx 28894. (Contributed by Scott Fenton, 13-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    ⇒   ⊢ (𝜑 → ⟨𝐴, 𝐵⟩Cgr⟨𝐵, 𝐴⟩)
Theorem	cgrtr4d 36050	Deduction form of axcgrtr 28895. (Contributed by Scott Fenton, 13-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩)    &   ⊢ (𝜑 → ⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩)    ⇒   ⊢ (𝜑 → ⟨𝐶, 𝐷⟩Cgr⟨𝐸, 𝐹⟩)
Theorem	cgrtr4and 36051	Deduction form of axcgrtr 28895. (Contributed by Scott Fenton, 13-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩)    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐶, 𝐷⟩Cgr⟨𝐸, 𝐹⟩)
Theorem	cgrrflx 36052	Reflexivity law for congruence. Theorem 2.1 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → ⟨𝐴, 𝐵⟩Cgr⟨𝐴, 𝐵⟩)
Theorem	cgrrflxd 36053	Deduction form of cgrrflx 36052. (Contributed by Scott Fenton, 13-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    ⇒   ⊢ (𝜑 → ⟨𝐴, 𝐵⟩Cgr⟨𝐴, 𝐵⟩)
Theorem	cgrcomim 36054	Congruence commutes on the two sides. Implication version. Theorem 2.2 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐷⟩Cgr⟨𝐴, 𝐵⟩))
Theorem	cgrcom 36055	Congruence commutes between the two sides. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩ ↔ ⟨𝐶, 𝐷⟩Cgr⟨𝐴, 𝐵⟩))
Theorem	cgrcomand 36056	Deduction form of cgrcom 36055. (Contributed by Scott Fenton, 13-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐶, 𝐷⟩Cgr⟨𝐴, 𝐵⟩)
Theorem	cgrtr 36057	Transitivity law for congruence. Theorem 2.3 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 24-Sep-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐸, 𝐹⟩) → ⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩))
Theorem	cgrtrand 36058	Deduction form of cgrtr 36057. (Contributed by Scott Fenton, 13-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩)    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐶, 𝐷⟩Cgr⟨𝐸, 𝐹⟩)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩)
Theorem	cgrtr3 36059	Transitivity law for congruence. (Contributed by Scott Fenton, 7-Oct-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐸, 𝐹⟩) → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩))
Theorem	cgrtr3and 36060	Deduction form of cgrtr3 36059. (Contributed by Scott Fenton, 13-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩)    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐶, 𝐷⟩Cgr⟨𝐸, 𝐹⟩)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩)
Theorem	cgrcoml 36061	Congruence commutes on the left. Biconditional version of Theorem 2.4 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩ ↔ ⟨𝐵, 𝐴⟩Cgr⟨𝐶, 𝐷⟩))
Theorem	cgrcomr 36062	Congruence commutes on the right. Biconditional version of Theorem 2.5 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩ ↔ ⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝐶⟩))
Theorem	cgrcomlr 36063	Congruence commutes on both sides. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩ ↔ ⟨𝐵, 𝐴⟩Cgr⟨𝐷, 𝐶⟩))
Theorem	cgrcomland 36064	Deduction form of cgrcoml 36061. (Contributed by Scott Fenton, 14-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐵, 𝐴⟩Cgr⟨𝐶, 𝐷⟩)
Theorem	cgrcomrand 36065	Deduction form of cgrcoml 36061. (Contributed by Scott Fenton, 14-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝐶⟩)
Theorem	cgrcomlrand 36066	Deduction form of cgrcomlr 36063. (Contributed by Scott Fenton, 14-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐵, 𝐴⟩Cgr⟨𝐷, 𝐶⟩)
Theorem	cgrtriv 36067	Degenerate segments are congruent. Theorem 2.8 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → ⟨𝐴, 𝐴⟩Cgr⟨𝐵, 𝐵⟩)
Theorem	cgrid2 36068	Identity law for congruence. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (⟨𝐴, 𝐴⟩Cgr⟨𝐵, 𝐶⟩ → 𝐵 = 𝐶))
Theorem	cgrdegen 36069	Two congruent segments are either both degenerate or both nondegenerate. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩ → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)))
Theorem	brofs 36070	Binary relation form of the outer five segment predicate. (Contributed by Scott Fenton, 21-Sep-2013.)
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))))
Theorem	5segofs 36071	Rephrase ax5seg 28918 using the outer five segment predicate. Theorem 2.10 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 21-Sep-2013.)
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ∧ 𝐴 ≠ 𝐵) → ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))
Theorem	ofscom 36072	The outer five segment predicate commutes. (Contributed by Scott Fenton, 26-Sep-2013.)
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ OuterFiveSeg ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩))
Theorem	cgrextend 36073	Link congruence over a pair of line segments. Theorem 2.11 of [Schwabhauser] p. 29. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝐹⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝐸⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐸, 𝐹⟩)) → ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩))
Theorem	cgrextendand 36074	Deduction form of cgrextend 36073. (Contributed by Scott Fenton, 14-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → 𝐵 Btwn ⟨𝐴, 𝐶⟩)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝐸 Btwn ⟨𝐷, 𝐹⟩)    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝐸⟩)    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐵, 𝐶⟩Cgr⟨𝐸, 𝐹⟩)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩)
Theorem	segconeq 36075	Two points that satisfy the conclusion of axsegcon 28907 are identical. Uniqueness portion of Theorem 2.12 of [Schwabhauser] p. 29. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁) ∧ 𝑌 ∈ (𝔼‘𝑁))) → ((𝑄 ≠ 𝐴 ∧ (𝐴 Btwn ⟨𝑄, 𝑋⟩ ∧ ⟨𝐴, 𝑋⟩Cgr⟨𝐵, 𝐶⟩) ∧ (𝐴 Btwn ⟨𝑄, 𝑌⟩ ∧ ⟨𝐴, 𝑌⟩Cgr⟨𝐵, 𝐶⟩)) → 𝑋 = 𝑌))
Theorem	segconeu 36076*	Existential uniqueness version of segconeq 36075. (Contributed by Scott Fenton, 19-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ 𝐶 ≠ 𝐷)) → ∃!𝑟 ∈ (𝔼‘𝑁)(𝐷 Btwn ⟨𝐶, 𝑟⟩ ∧ ⟨𝐷, 𝑟⟩Cgr⟨𝐴, 𝐵⟩))
21.11.17.2  Betweenness properties
Theorem	btwntriv2 36077	Betweenness always holds for the second endpoint. Theorem 3.1 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝐵 Btwn ⟨𝐴, 𝐵⟩)
Theorem	btwncomim 36078	Betweenness commutes. Implication version. Theorem 3.2 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Btwn ⟨𝐵, 𝐶⟩ → 𝐴 Btwn ⟨𝐶, 𝐵⟩))
Theorem	btwncom 36079	Betweenness commutes. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 Btwn ⟨𝐵, 𝐶⟩ ↔ 𝐴 Btwn ⟨𝐶, 𝐵⟩))
Theorem	btwncomand 36080	Deduction form of btwncom 36079. (Contributed by Scott Fenton, 14-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → 𝐴 Btwn ⟨𝐵, 𝐶⟩)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝐴 Btwn ⟨𝐶, 𝐵⟩)
Theorem	btwntriv1 36081	Betweenness always holds for the first endpoint. Theorem 3.3 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝐴 Btwn ⟨𝐴, 𝐵⟩)
Theorem	btwnswapid 36082	If you can swap the first two arguments of a betweenness statement, then those arguments are identical. Theorem 3.4 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝐴 Btwn ⟨𝐵, 𝐶⟩ ∧ 𝐵 Btwn ⟨𝐴, 𝐶⟩) → 𝐴 = 𝐵))
Theorem	btwnswapid2 36083	If you can swap arguments one and three of a betweenness statement, then those arguments are identical. (Contributed by Scott Fenton, 7-Oct-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝐴 Btwn ⟨𝐵, 𝐶⟩ ∧ 𝐶 Btwn ⟨𝐵, 𝐴⟩) → 𝐴 = 𝐶))
Theorem	btwnintr 36084	Inner transitivity law for betweenness. Left-hand side of Theorem 3.5 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn ⟨𝐴, 𝐷⟩ ∧ 𝐶 Btwn ⟨𝐵, 𝐷⟩) → 𝐵 Btwn ⟨𝐴, 𝐶⟩))
Theorem	btwnexch3 36085	Exchange the first endpoint in betweenness. Left-hand side of Theorem 3.6 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝐷⟩) → 𝐶 Btwn ⟨𝐵, 𝐷⟩))
Theorem	btwnexch3and 36086	Deduction form of btwnexch3 36085. (Contributed by Scott Fenton, 13-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → 𝐵 Btwn ⟨𝐴, 𝐶⟩)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝐶 Btwn ⟨𝐴, 𝐷⟩)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝐶 Btwn ⟨𝐵, 𝐷⟩)
Theorem	btwnouttr2 36087	Outer transitivity law for betweenness. Left-hand side of Theorem 3.1 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐶 Btwn ⟨𝐵, 𝐷⟩) → 𝐶 Btwn ⟨𝐴, 𝐷⟩))
Theorem	btwnexch2 36088	Exchange the outer point of two betweenness statements. Right-hand side of Theorem 3.5 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 14-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn ⟨𝐴, 𝐷⟩ ∧ 𝐶 Btwn ⟨𝐵, 𝐷⟩) → 𝐶 Btwn ⟨𝐴, 𝐷⟩))
Theorem	btwnouttr 36089	Outer transitivity law for betweenness. Right-hand side of Theorem 3.7 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 14-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐶 Btwn ⟨𝐵, 𝐷⟩) → 𝐵 Btwn ⟨𝐴, 𝐷⟩))
Theorem	btwnexch 36090	Outer transitivity law for betweenness. Right-hand side of Theorem 3.6 of [Schwabhauser] p. 30. (Contributed by Scott Fenton, 24-Sep-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐶 Btwn ⟨𝐴, 𝐷⟩) → 𝐵 Btwn ⟨𝐴, 𝐷⟩))
Theorem	btwnexchand 36091	Deduction form of btwnexch 36090. (Contributed by Scott Fenton, 13-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → 𝐵 Btwn ⟨𝐴, 𝐶⟩)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝐶 Btwn ⟨𝐴, 𝐷⟩)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝐵 Btwn ⟨𝐴, 𝐷⟩)
Theorem	btwndiff 36092*	There is always a 𝑐 distinct from 𝐵 such that 𝐵 lies between 𝐴 and 𝑐. Theorem 3.14 of [Schwabhauser] p. 32. (Contributed by Scott Fenton, 24-Sep-2013.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → ∃𝑐 ∈ (𝔼‘𝑁)(𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝐵 ≠ 𝑐))
Theorem	trisegint 36093*	A line segment between two sides of a triange intersects a segment crossing from the remaining side to the opposite vertex. Theorem 3.17 of [Schwabhauser] p. 33. (Contributed by Scott Fenton, 24-Sep-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐸 Btwn ⟨𝐷, 𝐶⟩ ∧ 𝑃 Btwn ⟨𝐴, 𝐷⟩) → ∃𝑞 ∈ (𝔼‘𝑁)(𝑞 Btwn ⟨𝑃, 𝐶⟩ ∧ 𝑞 Btwn ⟨𝐵, 𝐸⟩)))
21.11.17.3  Segment Transportation
Syntax	ctransport 36094	Declare the syntax for the segment transport function.
class TransportTo
Definition	df-transport 36095*	Define the segment transport function. See fvtransport 36097 for an explanation of the function. (Contributed by Scott Fenton, 18-Oct-2013.)
⊢ TransportTo = {⟨⟨𝑝, 𝑞⟩, 𝑥⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st ‘𝑞) ≠ (2nd ‘𝑞)) ∧ 𝑥 = (℩𝑟 ∈ (𝔼‘𝑛)((2nd ‘𝑞) Btwn ⟨(1st ‘𝑞), 𝑟⟩ ∧ ⟨(2nd ‘𝑞), 𝑟⟩Cgr𝑝)))}
Theorem	funtransport 36096	The TransportTo relationship is a function. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ Fun TransportTo
Theorem	fvtransport 36097*	Calculate the value of the TransportTo function. This function takes four points, 𝐴 through 𝐷, where 𝐶 and 𝐷 are distinct. It then returns the point that extends 𝐶𝐷 by the length of 𝐴𝐵. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ 𝐶 ≠ 𝐷)) → (⟨𝐴, 𝐵⟩TransportTo⟨𝐶, 𝐷⟩) = (℩𝑟 ∈ (𝔼‘𝑁)(𝐷 Btwn ⟨𝐶, 𝑟⟩ ∧ ⟨𝐷, 𝑟⟩Cgr⟨𝐴, 𝐵⟩)))
Theorem	transportcl 36098	Closure law for segment transport. (Contributed by Scott Fenton, 19-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ 𝐶 ≠ 𝐷)) → (⟨𝐴, 𝐵⟩TransportTo⟨𝐶, 𝐷⟩) ∈ (𝔼‘𝑁))
Theorem	transportprops 36099	Calculate the defining properties of the transport function. (Contributed by Scott Fenton, 19-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ 𝐶 ≠ 𝐷)) → (𝐷 Btwn ⟨𝐶, (⟨𝐴, 𝐵⟩TransportTo⟨𝐶, 𝐷⟩)⟩ ∧ ⟨𝐷, (⟨𝐴, 𝐵⟩TransportTo⟨𝐶, 𝐷⟩)⟩Cgr⟨𝐴, 𝐵⟩))
21.11.17.4  Properties relating betweenness and congruence
Syntax	cifs 36100	Declare the syntax for the inner five segment predicate.
class InnerFiveSeg