P. 327 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32601-32700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dffix2 32601	The fixpoints of a class in terms of its range. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix 𝐴 = ran (𝐴 ∩ I )
Theorem	fixssdm 32602	The fixpoints of a class are a subset of its domain. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix 𝐴 ⊆ dom 𝐴
Theorem	fixssrn 32603	The fixpoints of a class are a subset of its range. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix 𝐴 ⊆ ran 𝐴
Theorem	fixcnv 32604	The fixpoints of a class are the same as those of its converse. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix 𝐴 = Fix ◡𝐴
Theorem	fixun 32605	The fixpoint operator distributes over union. (Contributed by Scott Fenton, 16-Apr-2012.)
⊢ Fix (𝐴 ∪ 𝐵) = ( Fix 𝐴 ∪ Fix 𝐵)
Theorem	ellimits 32606	Membership in the class of all limit ordinals. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ Limits ↔ Lim 𝐴)
Theorem	limitssson 32607	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 32608	A quantifier-free definition of ω that does not depend on ax-inf 8832. (Note: label was changed from dfom5 8844 to dfom5b 32608 to prevent naming conflict. NM, 12-Feb-2013.) (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ ω = (On ∩ ∩ Limits )
Theorem	sscoid 32609	A condition for subset and composition with identity. (Contributed by Scott Fenton, 13-Apr-2018.)
⊢ (𝐴 ⊆ ( I ∘ 𝐵) ↔ (Rel 𝐴 ∧ 𝐴 ⊆ 𝐵))
Theorem	dffun10 32610	Another potential definition of functionhood. 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 32611	Membership in the class of all functions. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (𝐹 ∈ Funs ↔ Fun 𝐹)
Theorem	elfunsg 32612	Closed form of elfuns 32611. (Contributed by Scott Fenton, 2-May-2014.)
⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ Funs ↔ Fun 𝐹))
Theorem	brsingle 32613	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 32614*	Membership in the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ (𝐴 ∈ Singletons ↔ ∃𝑥 𝐴 = {𝑥})
Theorem	fnsingle 32615	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 32616	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 32617*	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 32618	A singleton is a member of the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {𝐴} ∈ Singletons
Theorem	dfiota3 32619	A definiton of iota using minimal quantifiers. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ (℩𝑥𝜑) = ∪ ∪ ({{𝑥 ∣ 𝜑}} ∩ Singletons )
Theorem	dffv5 32620	Another quantifier free definition of function value. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ (𝐹‘𝐴) = ∪ ∪ ({(𝐹 “ {𝐴})} ∩ Singletons )
Theorem	unisnif 32621	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 32622	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 32623	Closed form of brimage 32622. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴Image𝑅𝐵 ↔ 𝐵 = (𝑅 “ 𝐴)))
Theorem	funimage 32624	Image𝐴 is a function. (Contributed by Scott Fenton, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ Fun Image𝐴
Theorem	fnimage 32625*	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 32626*	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 32627	Value of the image functor. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅 “ 𝐴) ∈ 𝑊) → (Image𝑅‘𝐴) = (𝑅 “ 𝐴))
Theorem	brcart 32628	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 32629	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 32630	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 32631	Closed form of brdomain 32629. (Contributed by Scott Fenton, 2-May-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴Domain𝐵 ↔ 𝐵 = dom 𝐴))
Theorem	brrangeg 32632	Closed form of brrange 32630. (Contributed by Scott Fenton, 3-May-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴Range𝐵 ↔ 𝐵 = ran 𝐴))
Theorem	brimg 32633	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 32634	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 32635	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 32636	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	brsuccf 32637	Binary relation form of the Succ function. (Contributed by Scott Fenton, 14-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴Succ𝐵 ↔ 𝐵 = suc 𝐴)
Theorem	funpartlem 32638*	Lemma for funpartfun 32639. Show membership in the restriction. (Contributed by Scott Fenton, 4-Dec-2017.)
⊢ (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )) ↔ ∃𝑥(𝐹 “ {𝐴}) = {𝑥})
Theorem	funpartfun 32639	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 32640	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 32641	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 32642	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 32643	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 32644	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 32645	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 32646	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 32647	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 32648	Quantifier-free definition of class intersection. (Contributed by Scott Fenton, 13-Apr-2018.)
⊢ ∩ 𝐴 = (V ∖ (◡(V ∖ E ) “ 𝐴))
Theorem	imagesset 32649	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 32650*	Binary relation form of the upper bound functor. (Contributed by Scott Fenton, 3-May-2018.)
⊢ 𝑆 ∈ V    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ (𝑆UB𝑅𝐴 ↔ ∀𝑥 ∈ 𝑆 𝑥𝑅𝐴)
Theorem	brlb 32651*	Binary relation form of the lower bound functor. (Contributed by Scott Fenton, 3-May-2018.)
⊢ 𝑆 ∈ V    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ (𝑆LB𝑅𝐴 ↔ ∀𝑥 ∈ 𝑆 𝐴𝑅𝑥)
20.8.31  Alternate ordered pairs
Syntax	caltop 32652	Declare the syntax for an alternate ordered pair.
class ⟪𝐴, 𝐵⟫
Syntax	caltxp 32653	Declare the syntax for an alternate Cartesian product.
class (𝐴 ×× 𝐵)
Definition	df-altop 32654	An alternative definition of ordered pairs. This definition removes a hypothesis from its defining theorem (see altopth 32665), making it more convenient in some circumstances. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ ⟪𝐴, 𝐵⟫ = {{𝐴}, {𝐴, {𝐵}}}
Definition	df-altxp 32655*	Define Cartesian products of alternative ordered pairs. (Contributed by Scott Fenton, 23-Mar-2012.)
⊢ (𝐴 ×× 𝐵) = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = ⟪𝑥, 𝑦⟫}
Theorem	altopex 32656	Alternative ordered pairs always exist. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ ⟪𝐴, 𝐵⟫ ∈ V
Theorem	altopthsn 32657	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 32658	Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → ⟪𝐴, 𝐶⟫ = ⟪𝐵, 𝐷⟫)
Theorem	altopeq1 32659	Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ (𝐴 = 𝐵 → ⟪𝐴, 𝐶⟫ = ⟪𝐵, 𝐶⟫)
Theorem	altopeq2 32660	Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ (𝐴 = 𝐵 → ⟪𝐶, 𝐴⟫ = ⟪𝐶, 𝐵⟫)
Theorem	altopth1 32661	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 32662	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 32663	Alternate ordered pair theorem. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	altopthbg 32664	Alternate ordered pair theorem. (Contributed by Scott Fenton, 14-Apr-2012.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	altopth 32665	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 5176), requires 𝐷 to be a set. (Contributed by Scott Fenton, 23-Mar-2012.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	altopthb 32666	Alternate ordered pair theorem with different sethood requirements. See altopth 32665 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	altopthc 32667	Alternate ordered pair theorem with different sethood requirements. See altopth 32665 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	altopthd 32668	Alternate ordered pair theorem with different sethood requirements. See altopth 32665 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.)
⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	altxpeq1 32669	Equality for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.)
⊢ (𝐴 = 𝐵 → (𝐴 ×× 𝐶) = (𝐵 ×× 𝐶))
Theorem	altxpeq2 32670	Equality for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.)
⊢ (𝐴 = 𝐵 → (𝐶 ×× 𝐴) = (𝐶 ×× 𝐵))
Theorem	elaltxp 32671*	Membership in alternate Cartesian products. (Contributed by Scott Fenton, 23-Mar-2012.)
⊢ (𝑋 ∈ (𝐴 ×× 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑋 = ⟪𝑥, 𝑦⟫)
Theorem	altopelaltxp 32672	Alternate ordered pair membership in a Cartesian product. Note that, unlike opelxp 5391, there is no sethood requirement here. (Contributed by Scott Fenton, 22-Mar-2012.)
⊢ (⟪𝑋, 𝑌⟫ ∈ (𝐴 ×× 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵))
Theorem	altxpsspw 32673	An inclusion rule for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.)
⊢ (𝐴 ×× 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝒫 𝐵)
Theorem	altxpexg 32674	The alternate Cartesian product of two sets is a set. (Contributed by Scott Fenton, 24-Mar-2012.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ×× 𝐵) ∈ V)
Theorem	rankaltopb 32675	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 32676	Bound-variable hypothesis builder for alternate ordered pairs. (Contributed by Scott Fenton, 25-Sep-2015.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥⟪𝐴, 𝐵⟫
Theorem	sbcaltop 32677*	Distribution of class substitution over alternate ordered pairs. (Contributed by Scott Fenton, 25-Sep-2015.)
⊢ (𝐴 ∈ V → ⦋𝐴 / 𝑥⦌⟪𝐶, 𝐷⟫ = ⟪⦋𝐴 / 𝑥⦌𝐶, ⦋𝐴 / 𝑥⦌𝐷⟫)
20.8.32  Geometry in the Euclidean space
20.8.32.1  Congruence properties
Syntax	cofs 32678	Declare the syntax for the outer five segment configuration.
class OuterFiveSeg
Definition	df-ofs 32679*	The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom (ax5seg 26287). See brofs 32701 and 5segofs 32702 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 32680	Deduction form of axcgrrflx 26263. (Contributed by Scott Fenton, 13-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    ⇒   ⊢ (𝜑 → ⟨𝐴, 𝐵⟩Cgr⟨𝐵, 𝐴⟩)
Theorem	cgrtr4d 32681	Deduction form of axcgrtr 26264. (Contributed by Scott Fenton, 13-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩)    &   ⊢ (𝜑 → ⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩)    ⇒   ⊢ (𝜑 → ⟨𝐶, 𝐷⟩Cgr⟨𝐸, 𝐹⟩)
Theorem	cgrtr4and 32682	Deduction form of axcgrtr 26264. (Contributed by Scott Fenton, 13-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩)    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐶, 𝐷⟩Cgr⟨𝐸, 𝐹⟩)
Theorem	cgrrflx 32683	Reflexivity law for congruence. Theorem 2.1 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → ⟨𝐴, 𝐵⟩Cgr⟨𝐴, 𝐵⟩)
Theorem	cgrrflxd 32684	Deduction form of cgrrflx 32683. (Contributed by Scott Fenton, 13-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    ⇒   ⊢ (𝜑 → ⟨𝐴, 𝐵⟩Cgr⟨𝐴, 𝐵⟩)
Theorem	cgrcomim 32685	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 32686	Congruence commutes between the two sides. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩ ↔ ⟨𝐶, 𝐷⟩Cgr⟨𝐴, 𝐵⟩))
Theorem	cgrcomand 32687	Deduction form of cgrcom 32686. (Contributed by Scott Fenton, 13-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐶, 𝐷⟩Cgr⟨𝐴, 𝐵⟩)
Theorem	cgrtr 32688	Transitivity law for congruence. Theorem 2.3 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 24-Sep-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐸, 𝐹⟩) → ⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩))
Theorem	cgrtrand 32689	Deduction form of cgrtr 32688. (Contributed by Scott Fenton, 13-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩)    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐶, 𝐷⟩Cgr⟨𝐸, 𝐹⟩)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩)
Theorem	cgrtr3 32690	Transitivity law for congruence. (Contributed by Scott Fenton, 7-Oct-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐸, 𝐹⟩) → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩))
Theorem	cgrtr3and 32691	Deduction form of cgrtr3 32690. (Contributed by Scott Fenton, 13-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩)    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐶, 𝐷⟩Cgr⟨𝐸, 𝐹⟩)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩)
Theorem	cgrcoml 32692	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 32693	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 32694	Congruence commutes on both sides. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩ ↔ ⟨𝐵, 𝐴⟩Cgr⟨𝐷, 𝐶⟩))
Theorem	cgrcomland 32695	Deduction form of cgrcoml 32692. (Contributed by Scott Fenton, 14-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐵, 𝐴⟩Cgr⟨𝐶, 𝐷⟩)
Theorem	cgrcomrand 32696	Deduction form of cgrcoml 32692. (Contributed by Scott Fenton, 14-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝐶⟩)
Theorem	cgrcomlrand 32697	Deduction form of cgrcomlr 32694. (Contributed by Scott Fenton, 14-Oct-2013.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁))    &   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ⟨𝐵, 𝐴⟩Cgr⟨𝐷, 𝐶⟩)
Theorem	cgrtriv 32698	Degenerate segments are congruent. Theorem 2.8 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → ⟨𝐴, 𝐴⟩Cgr⟨𝐵, 𝐵⟩)
Theorem	cgrid2 32699	Identity law for congruence. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (⟨𝐴, 𝐴⟩Cgr⟨𝐵, 𝐶⟩ → 𝐵 = 𝐶))
Theorem	cgrdegen 32700	Two congruent segments are either both degenerate or both nondegenerate. (Contributed by Scott Fenton, 12-Jun-2013.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (⟨𝐴, 𝐵⟩Cgr⟨𝐶, 𝐷⟩ → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)))