P. 362 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36101-36200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	idsset 36101	I is equal to the intersection of SSet and its converse. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ I = ( SSet ∩ ◡ SSet )
Theorem	eltrans 36102	Membership in the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ Trans ↔ Tr 𝐴)
Theorem	dfon3 36103	A quantifier-free definition of On. (Contributed by Scott Fenton, 5-Apr-2012.)
⊢ On = (V ∖ ran (( SSet ∩ ( Trans × V)) ∖ ( I ∪ E )))
Theorem	dfon4 36104	Another quantifier-free definition of On. (Contributed by Scott Fenton, 4-May-2014.)
⊢ On = (V ∖ (( SSet ∖ ( I ∪ E )) “ Trans ))
Theorem	brtxpsd 36105*	Expansion of a common form used in quantifier-free definitions. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (¬ 𝐴ran ((V ⊗ E ) △ (𝑅 ⊗ V))𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥𝑅𝐴))
Theorem	brtxpsd2 36106*	Another common abbreviation for quantifier-free definitions. (Contributed by Scott Fenton, 21-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑅 = (𝐶 ∖ ran ((V ⊗ E ) △ (𝑆 ⊗ V)))    &   ⊢ 𝐴𝐶𝐵    ⇒   ⊢ (𝐴𝑅𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥𝑆𝐴))
Theorem	brtxpsd3 36107*	A third common abbreviation for quantifier-free definitions. (Contributed by Scott Fenton, 3-May-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑅 = (𝐶 ∖ ran ((V ⊗ E ) △ (𝑆 ⊗ V)))    &   ⊢ 𝐴𝐶𝐵    &   ⊢ (𝑥 ∈ 𝑋 ↔ 𝑥𝑆𝐴)    ⇒   ⊢ (𝐴𝑅𝐵 ↔ 𝐵 = 𝑋)
Theorem	relbigcup 36108	The Bigcup relationship is a relationship. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Rel Bigcup
Theorem	brbigcup 36109	Binary relation over Bigcup . (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 Bigcup 𝐵 ↔ ∪ 𝐴 = 𝐵)
Theorem	dfbigcup2 36110	Bigcup using maps-to notation. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Bigcup = (𝑥 ∈ V ↦ ∪ 𝑥)
Theorem	fobigcup 36111	Bigcup maps the universe onto itself. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Bigcup :V–onto→V
Theorem	fnbigcup 36112	Bigcup is a function over the universal class. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Bigcup Fn V
Theorem	fvbigcup 36113	For sets, Bigcup yields union. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ( Bigcup ‘𝐴) = ∪ 𝐴
Theorem	elfix 36114	Membership in the fixpoints of a class. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ Fix 𝑅 ↔ 𝐴𝑅𝐴)
Theorem	elfix2 36115	Alternative membership in the fixpoint of a class. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Rel 𝑅    ⇒   ⊢ (𝐴 ∈ Fix 𝑅 ↔ 𝐴𝑅𝐴)
Theorem	dffix2 36116	The fixpoints of a class in terms of its range. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix 𝐴 = ran (𝐴 ∩ I )
Theorem	fixssdm 36117	The fixpoints of a class are a subset of its domain. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix 𝐴 ⊆ dom 𝐴
Theorem	fixssrn 36118	The fixpoints of a class are a subset of its range. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix 𝐴 ⊆ ran 𝐴
Theorem	fixcnv 36119	The fixpoints of a class are the same as those of its converse. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix 𝐴 = Fix ◡𝐴
Theorem	fixun 36120	The fixpoint operator distributes over union. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix (𝐴 ∪ 𝐵) = ( Fix 𝐴 ∪ Fix 𝐵)
Theorem	ellimits 36121	Membership in the class of all limit ordinals. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ Limits ↔ Lim 𝐴)
Theorem	limitssson 36122	The class of all limit ordinals is a subclass of the class of all ordinals. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Limits ⊆ On
Theorem	dfom5b 36123	A quantifier-free definition of ω that does not depend on ax-inf 9559. (Note: label was changed from dfom5 9571 to dfom5b 36123 to prevent naming conflict. NM, 12-Feb-2013.) (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ ω = (On ∩ ∩ Limits )
Theorem	sscoid 36124	A condition for subset and composition with identity. (Contributed by Scott Fenton, 13-Apr-2018.)
⊢ (𝐴 ⊆ ( I ∘ 𝐵) ↔ (Rel 𝐴 ∧ 𝐴 ⊆ 𝐵))
Theorem	dffun10 36125	Another potential definition of functionality. Based on statements in http://people.math.gatech.edu/~belinfan/research/autoreas/otter/sum/fs/. (Contributed by Scott Fenton, 30-Aug-2017.)
⊢ (Fun 𝐹 ↔ 𝐹 ⊆ ( I ∘ (V ∖ ((V ∖ I ) ∘ 𝐹))))
Theorem	elfuns 36126	Membership in the class of all functions. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (𝐹 ∈ Funs ↔ Fun 𝐹)
Theorem	elfunsg 36127	Closed form of elfuns 36126. (Contributed by Scott Fenton, 2-May-2014.)
⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ Funs ↔ Fun 𝐹))
Theorem	brsingle 36128	The binary relation form of the singleton function. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴Singleton𝐵 ↔ 𝐵 = {𝐴})
Theorem	elsingles 36129*	Membership in the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ (𝐴 ∈ Singletons ↔ ∃𝑥 𝐴 = {𝑥})
Theorem	fnsingle 36130	The singleton relationship is a function over the universe. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ Singleton Fn V
Theorem	fvsingle 36131	The value of the singleton function. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Revised by Scott Fenton, 13-Apr-2018.)
⊢ (Singleton‘𝐴) = {𝐴}
Theorem	dfsingles2 36132*	Alternate definition of the class of all singletons. (Contributed by Scott Fenton, 20-Nov-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ Singletons = {𝑥 ∣ ∃𝑦 𝑥 = {𝑦}}
Theorem	snelsingles 36133	A singleton is a member of the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝐴} ∈ Singletons
Theorem	dfiota3 36134	A definition of iota using minimal quantifiers. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ (℩𝑥𝜑) = ∪ ∪ ({{𝑥 ∣ 𝜑}} ∩ Singletons )
Theorem	dffv5 36135	Another quantifier-free definition of function value. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ (𝐹‘𝐴) = ∪ ∪ ({(𝐹 “ {𝐴})} ∩ Singletons )
Theorem	unisnif 36136	Express union of singleton in terms of if. (Contributed by Scott Fenton, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ∪ {𝐴} = if(𝐴 ∈ V, 𝐴, ∅)
Theorem	brimage 36137	Binary relation form of the Image functor. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴Image𝑅𝐵 ↔ 𝐵 = (𝑅 “ 𝐴))
Theorem	brimageg 36138	Closed form of brimage 36137. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴Image𝑅𝐵 ↔ 𝐵 = (𝑅 “ 𝐴)))
Theorem	funimage 36139	Image𝐴 is a function. (Contributed by Scott Fenton, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ Fun Image𝐴
Theorem	fnimage 36140*	Image𝑅 is a function over the set-like portion of 𝑅. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ Image𝑅 Fn {𝑥 ∣ (𝑅 “ 𝑥) ∈ V}
Theorem	imageval 36141*	The image functor in maps-to notation. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ Image𝑅 = (𝑥 ∈ V ↦ (𝑅 “ 𝑥))
Theorem	fvimage 36142	Value of the image functor. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅 “ 𝐴) ∈ 𝑊) → (Image𝑅‘𝐴) = (𝑅 “ 𝐴))
Theorem	brcart 36143	Binary relation form of the cartesian product operator. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩Cart𝐶 ↔ 𝐶 = (𝐴 × 𝐵))
Theorem	brdomain 36144	Binary relation form of the domain function. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴Domain𝐵 ↔ 𝐵 = dom 𝐴)
Theorem	brrange 36145	Binary relation form of the range function. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴Range𝐵 ↔ 𝐵 = ran 𝐴)
Theorem	brdomaing 36146	Closed form of brdomain 36144. (Contributed by Scott Fenton, 2-May-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴Domain𝐵 ↔ 𝐵 = dom 𝐴))
Theorem	brrangeg 36147	Closed form of brrange 36145. (Contributed by Scott Fenton, 3-May-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴Range𝐵 ↔ 𝐵 = ran 𝐴))
Theorem	brimg 36148	Binary relation form of the Img 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    ⇒   ⊢ (⟨𝐴, 𝐵⟩Img𝐶 ↔ 𝐶 = (𝐴 “ 𝐵))
Theorem	brapply 36149	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 36150	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 36151	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 36152*	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 36153	Binary relation form of the Succ function. (Contributed by Scott Fenton, 14-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴Succ𝐵 ↔ 𝐵 = suc 𝐴)
Theorem	dfsuccf2 36154*	Alternate definition of Scott Fenton's version of Succ, cf. df-sucmap 38707. (Contributed by Peter Mazsa, 6-Jan-2026.)
⊢ Succ = {⟨𝑚, 𝑛⟩ ∣ suc 𝑚 = 𝑛}
Theorem	funpartlem 36155*	Lemma for funpartfun 36156. Show membership in the restriction. (Contributed by Scott Fenton, 4-Dec-2017.)
⊢ (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )) ↔ ∃𝑥(𝐹 “ {𝐴}) = {𝑥})
Theorem	funpartfun 36156	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 36157	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 36158	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 36159	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 36160	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 36161	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 36162	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 36163	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 36164	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 36165	Quantifier-free definition of class intersection. (Contributed by Scott Fenton, 13-Apr-2018.)
⊢ ∩ 𝐴 = (V ∖ (◡(V ∖ E ) “ 𝐴))
Theorem	imagesset 36166	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 36167*	Binary relation form of the upper bound functor. (Contributed by Scott Fenton, 3-May-2018.)
⊢ 𝑆 ∈ V    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ (𝑆UB𝑅𝐴 ↔ ∀𝑥 ∈ 𝑆 𝑥𝑅𝐴)
Theorem	brlb 36168*	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 36169	Declare the syntax for an alternate ordered pair.
class ⟪𝐴, 𝐵⟫
Syntax	caltxp 36170	Declare the syntax for an alternate Cartesian product.
class (𝐴 ×× 𝐵)
Definition	df-altop 36171	An alternative definition of ordered pairs. This definition removes a hypothesis from its defining theorem (see altopth 36182), making it more convenient in some circumstances. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ ⟪𝐴, 𝐵⟫ = {{𝐴}, {𝐴, {𝐵}}}
Definition	df-altxp 36172*	Define Cartesian products of alternative ordered pairs. (Contributed by Scott Fenton, 23-Mar-2012.)
⊢ (𝐴 ×× 𝐵) = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = ⟪𝑥, 𝑦⟫}
Theorem	altopex 36173	Alternative ordered pairs always exist. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ ⟪𝐴, 𝐵⟫ ∈ V
Theorem	altopthsn 36174	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 36175	Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → ⟪𝐴, 𝐶⟫ = ⟪𝐵, 𝐷⟫)
Theorem	altopeq1 36176	Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ (𝐴 = 𝐵 → ⟪𝐴, 𝐶⟫ = ⟪𝐵, 𝐶⟫)
Theorem	altopeq2 36177	Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ (𝐴 = 𝐵 → ⟪𝐶, 𝐴⟫ = ⟪𝐶, 𝐵⟫)
Theorem	altopth1 36178	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 36179	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 36180	Alternate ordered pair theorem. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	altopthbg 36181	Alternate ordered pair theorem. (Contributed by Scott Fenton, 14-Apr-2012.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	altopth 36182	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 5432), requires 𝐷 to be a set. (Contributed by Scott Fenton, 23-Mar-2012.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	altopthb 36183	Alternate ordered pair theorem with different sethood requirements. See altopth 36182 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	altopthc 36184	Alternate ordered pair theorem with different sethood requirements. See altopth 36182 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	altopthd 36185	Alternate ordered pair theorem with different sethood requirements. See altopth 36182 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.)
⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	altxpeq1 36186	Equality for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.)
⊢ (𝐴 = 𝐵 → (𝐴 ×× 𝐶) = (𝐵 ×× 𝐶))
Theorem	altxpeq2 36187	Equality for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.)
⊢ (𝐴 = 𝐵 → (𝐶 ×× 𝐴) = (𝐶 ×× 𝐵))
Theorem	elaltxp 36188*	Membership in alternate Cartesian products. (Contributed by Scott Fenton, 23-Mar-2012.)
⊢ (𝑋 ∈ (𝐴 ×× 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑋 = ⟪𝑥, 𝑦⟫)
Theorem	altopelaltxp 36189	Alternate ordered pair membership in a Cartesian product. Note that, unlike opelxp 5668, there is no sethood requirement here. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ (⟪𝑋, 𝑌⟫ ∈ (𝐴 ×× 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵))
Theorem	altxpsspw 36190	An inclusion rule for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.)
⊢ (𝐴 ×× 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝒫 𝐵)
Theorem	altxpexg 36191	The alternate Cartesian product of two sets is a set. (Contributed by Scott Fenton, 24-Mar-2012.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ×× 𝐵) ∈ V)
Theorem	rankaltopb 36192	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 36193	Bound-variable hypothesis builder for alternate ordered pairs. (Contributed by Scott Fenton, 25-Sep-2015.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥⟪𝐴, 𝐵⟫
Theorem	sbcaltop 36194*	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 36195	Declare the syntax for the outer five segment configuration.
class OuterFiveSeg
Definition	df-ofs 36196*	The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom (ax5seg 29023). See brofs 36218 and 5segofs 36219 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 36197	Deduction form of axcgrrflx 28999. (Contributed by Scott Fenton, 13-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    ⇒   ⊢ (𝜑 → ⟨𝐴, 𝐵⟩Cgr⟨𝐵, 𝐴⟩)
Theorem	cgrtr4d 36198	Deduction form of axcgrtr 29000. (Contributed by Scott Fenton, 13-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩)    &   ⊢ (𝜑 → ⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩)    ⇒   ⊢ (𝜑 → ⟨𝐶, 𝐷⟩Cgr⟨𝐸, 𝐹⟩)
Theorem	cgrtr4and 36199	Deduction form of axcgrtr 29000. (Contributed by Scott Fenton, 13-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩)    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐶, 𝐷⟩Cgr⟨𝐸, 𝐹⟩)
Theorem	cgrrflx 36200	Reflexivity law for congruence. Theorem 2.1 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → ⟨𝐴, 𝐵⟩Cgr⟨𝐴, 𝐵⟩)