P. 63 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6201-6300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	spc2ed 6201*	Existential specialization with 2 quantifiers, using implicit substitution. (Contributed by Thierry Arnoux, 23-Aug-2017.)
⊢ Ⅎ𝑥𝜒    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (𝜒 → ∃𝑥∃𝑦𝜓))
Theorem	cnvoprab 6202*	The converse of a class abstraction of nested ordered pairs. (Contributed by Thierry Arnoux, 17-Aug-2017.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑎 = ⟨𝑥, 𝑦⟩ → (𝜓 ↔ 𝜑))    &   ⊢ (𝜓 → 𝑎 ∈ (V × V))    ⇒   ⊢ ◡{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨𝑧, 𝑎⟩ ∣ 𝜓}
Theorem	f1od2 6203*	Describe an implicit one-to-one onto function of two variables. (Contributed by Thierry Arnoux, 17-Aug-2017.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → (𝐼 ∈ 𝑋 ∧ 𝐽 ∈ 𝑌))    &   ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ (𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽))))    ⇒   ⊢ (𝜑 → 𝐹:(𝐴 × 𝐵)–1-1-onto→𝐷)
Theorem	disjxp1 6204*	The sets of a cartesian product are disjoint if the sets in the first argument are disjoint. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)    ⇒   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 (𝐵 × 𝐶))
Theorem	disjsnxp 6205*	The sets in the cartesian product of singletons with other sets, are disjoint. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ Disj 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)
2.6.16  Special maps-to operations The following theorems are about maps-to operations (see df-mpo 5847) where the domain of the second argument depends on the domain of the first argument, especially when the first argument is a pair and the base set of the second argument is the first component of the first argument, in short "x-maps-to operations". For labels, the abbreviations "mpox" are used (since "x" usually denotes the first argument). This is in line with the currently used conventions for such cases (see cbvmpox 5920, ovmpox 5970 and fmpox 6168). If the first argument is an ordered pair, as in the following, the abbreviation is extended to "mpoxop", and the maps-to operations are called "x-op maps-to operations" for short.
Theorem	opeliunxp2f 6206*	Membership in a union of Cartesian products, using bound-variable hypothesis for 𝐸 instead of distinct variable conditions as in opeliunxp2 4744. (Contributed by AV, 25-Oct-2020.)
⊢ Ⅎ𝑥𝐸    &   ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐸)    ⇒   ⊢ (⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸))
Theorem	mpoxopn0yelv 6207*	If there is an element of the value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, then the second argument is an element of the first component of the first argument. (Contributed by Alexander van der Vekens, 10-Oct-2017.)
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ 𝐶)    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑁 ∈ (⟨𝑉, 𝑊⟩𝐹𝐾) → 𝐾 ∈ 𝑉))
Theorem	mpoxopoveq 6208*	Value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument. (Contributed by Alexander van der Vekens, 11-Oct-2017.)
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ {𝑛 ∈ (1st ‘𝑥) ∣ 𝜑})    ⇒   ⊢ (((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) ∧ 𝐾 ∈ 𝑉) → (⟨𝑉, 𝑊⟩𝐹𝐾) = {𝑛 ∈ 𝑉 ∣ [⟨𝑉, 𝑊⟩ / 𝑥][𝐾 / 𝑦]𝜑})
Theorem	mpoxopovel 6209*	Element of the value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument. (Contributed by Alexander van der Vekens and Mario Carneiro, 10-Oct-2017.)
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ {𝑛 ∈ (1st ‘𝑥) ∣ 𝜑})    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑁 ∈ (⟨𝑉, 𝑊⟩𝐹𝐾) ↔ (𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ∧ [⟨𝑉, 𝑊⟩ / 𝑥][𝐾 / 𝑦][𝑁 / 𝑛]𝜑)))
Theorem	rbropapd 6210*	Properties of a pair in an extended binary relation. (Contributed by Alexander van der Vekens, 30-Oct-2017.)
⊢ (𝜑 → 𝑀 = {⟨𝑓, 𝑝⟩ ∣ (𝑓𝑊𝑝 ∧ 𝜓)})    &   ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌) → (𝐹𝑀𝑃 ↔ (𝐹𝑊𝑃 ∧ 𝜒))))
Theorem	rbropap 6211*	Properties of a pair in a restricted binary relation 𝑀 expressed as an ordered-pair class abstraction: 𝑀 is the binary relation 𝑊 restricted by the condition 𝜓. (Contributed by AV, 31-Jan-2021.)
⊢ (𝜑 → 𝑀 = {⟨𝑓, 𝑝⟩ ∣ (𝑓𝑊𝑝 ∧ 𝜓)})    &   ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌) → (𝐹𝑀𝑃 ↔ (𝐹𝑊𝑃 ∧ 𝜒)))
2.6.17  Function transposition
Syntax	ctpos 6212	The transposition of a function.
class tpos 𝐹
Definition	df-tpos 6213*	Define the transposition of a function, which is a function 𝐺 = tpos 𝐹 satisfying 𝐺(𝑥, 𝑦) = 𝐹(𝑦, 𝑥). (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥}))
Theorem	tposss 6214	Subset theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (𝐹 ⊆ 𝐺 → tpos 𝐹 ⊆ tpos 𝐺)
Theorem	tposeq 6215	Equality theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (𝐹 = 𝐺 → tpos 𝐹 = tpos 𝐺)
Theorem	tposeqd 6216	Equality theorem for transposition. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ (𝜑 → 𝐹 = 𝐺)    ⇒   ⊢ (𝜑 → tpos 𝐹 = tpos 𝐺)
Theorem	tposssxp 6217	The transposition is a subset of a cross product. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ tpos 𝐹 ⊆ ((◡dom 𝐹 ∪ {∅}) × ran 𝐹)
Theorem	reltpos 6218	The transposition is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ Rel tpos 𝐹
Theorem	brtpos2 6219	Value of the transposition at a pair ⟨𝐴, 𝐵⟩. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (𝐵 ∈ 𝑉 → (𝐴tpos 𝐹𝐵 ↔ (𝐴 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝐴}𝐹𝐵)))
Theorem	brtpos0 6220	The behavior of tpos when the left argument is the empty set (which is not an ordered pair but is the "default" value of an ordered pair when the arguments are proper classes). (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (𝐴 ∈ 𝑉 → (∅tpos 𝐹𝐴 ↔ ∅𝐹𝐴))
Theorem	reldmtpos 6221	Necessary and sufficient condition for dom tpos 𝐹 to be a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (Rel dom tpos 𝐹 ↔ ¬ ∅ ∈ dom 𝐹)
Theorem	brtposg 6222	The transposition swaps arguments of a three-parameter relation. (Contributed by Jim Kingdon, 31-Jan-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (⟨𝐴, 𝐵⟩tpos 𝐹𝐶 ↔ ⟨𝐵, 𝐴⟩𝐹𝐶))
Theorem	ottposg 6223	The transposition swaps the first two elements in a collection of ordered triples. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (⟨𝐴, 𝐵, 𝐶⟩ ∈ tpos 𝐹 ↔ ⟨𝐵, 𝐴, 𝐶⟩ ∈ 𝐹))
Theorem	dmtpos 6224	The domain of tpos 𝐹 when dom 𝐹 is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (Rel dom 𝐹 → dom tpos 𝐹 = ◡dom 𝐹)
Theorem	rntpos 6225	The range of tpos 𝐹 when dom 𝐹 is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (Rel dom 𝐹 → ran tpos 𝐹 = ran 𝐹)
Theorem	tposexg 6226	The transposition of a set is a set. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (𝐹 ∈ 𝑉 → tpos 𝐹 ∈ V)
Theorem	ovtposg 6227	The transposition swaps the arguments in a two-argument function. When 𝐹 is a matrix, which is to say a function from ( 1 ... m ) × ( 1 ... n ) to the reals or some ring, tpos 𝐹 is the transposition of 𝐹, which is where the name comes from. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴tpos 𝐹𝐵) = (𝐵𝐹𝐴))
Theorem	tposfun 6228	The transposition of a function is a function. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (Fun 𝐹 → Fun tpos 𝐹)
Theorem	dftpos2 6229*	Alternate definition of tpos when 𝐹 has relational domain. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (Rel dom 𝐹 → tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ ◡dom 𝐹 ↦ ∪ ◡{𝑥})))
Theorem	dftpos3 6230*	Alternate definition of tpos when 𝐹 has relational domain. Compare df-cnv 4612. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (Rel dom 𝐹 → tpos 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ⟨𝑦, 𝑥⟩𝐹𝑧})
Theorem	dftpos4 6231*	Alternate definition of tpos. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥}))
Theorem	tpostpos 6232	Value of the double transposition for a general class 𝐹. (Contributed by Mario Carneiro, 16-Sep-2015.)
⊢ tpos tpos 𝐹 = (𝐹 ∩ (((V × V) ∪ {∅}) × V))
Theorem	tpostpos2 6233	Value of the double transposition for a relation on triples. (Contributed by Mario Carneiro, 16-Sep-2015.)
⊢ ((Rel 𝐹 ∧ Rel dom 𝐹) → tpos tpos 𝐹 = 𝐹)
Theorem	tposfn2 6234	The domain of a transposition. (Contributed by NM, 10-Sep-2015.)
⊢ (Rel 𝐴 → (𝐹 Fn 𝐴 → tpos 𝐹 Fn ◡𝐴))
Theorem	tposfo2 6235	Condition for a surjective transposition. (Contributed by NM, 10-Sep-2015.)
⊢ (Rel 𝐴 → (𝐹:𝐴–onto→𝐵 → tpos 𝐹:◡𝐴–onto→𝐵))
Theorem	tposf2 6236	The domain and range of a transposition. (Contributed by NM, 10-Sep-2015.)
⊢ (Rel 𝐴 → (𝐹:𝐴⟶𝐵 → tpos 𝐹:◡𝐴⟶𝐵))
Theorem	tposf12 6237	Condition for an injective transposition. (Contributed by NM, 10-Sep-2015.)
⊢ (Rel 𝐴 → (𝐹:𝐴–1-1→𝐵 → tpos 𝐹:◡𝐴–1-1→𝐵))
Theorem	tposf1o2 6238	Condition of a bijective transposition. (Contributed by NM, 10-Sep-2015.)
⊢ (Rel 𝐴 → (𝐹:𝐴–1-1-onto→𝐵 → tpos 𝐹:◡𝐴–1-1-onto→𝐵))
Theorem	tposfo 6239	The domain and range of a transposition. (Contributed by NM, 10-Sep-2015.)
⊢ (𝐹:(𝐴 × 𝐵)–onto→𝐶 → tpos 𝐹:(𝐵 × 𝐴)–onto→𝐶)
Theorem	tposf 6240	The domain and range of a transposition. (Contributed by NM, 10-Sep-2015.)
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → tpos 𝐹:(𝐵 × 𝐴)⟶𝐶)
Theorem	tposfn 6241	Functionality of a transposition. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝐹 Fn (𝐴 × 𝐵) → tpos 𝐹 Fn (𝐵 × 𝐴))
Theorem	tpos0 6242	Transposition of the empty set. (Contributed by NM, 10-Sep-2015.)
⊢ tpos ∅ = ∅
Theorem	tposco 6243	Transposition of a composition. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ tpos (𝐹 ∘ 𝐺) = (𝐹 ∘ tpos 𝐺)
Theorem	tpossym 6244*	Two ways to say a function is symmetric. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝐹 Fn (𝐴 × 𝐴) → (tpos 𝐹 = 𝐹 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝐹𝑦) = (𝑦𝐹𝑥)))
Theorem	tposeqi 6245	Equality theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ 𝐹 = 𝐺    ⇒   ⊢ tpos 𝐹 = tpos 𝐺
Theorem	tposex 6246	A transposition is a set. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ 𝐹 ∈ V    ⇒   ⊢ tpos 𝐹 ∈ V
Theorem	nftpos 6247	Hypothesis builder for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ Ⅎ𝑥𝐹    ⇒   ⊢ Ⅎ𝑥tpos 𝐹
Theorem	tposoprab 6248*	Transposition of a class of ordered triples. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}    ⇒   ⊢ tpos 𝐹 = {⟨⟨𝑦, 𝑥⟩, 𝑧⟩ ∣ 𝜑}
Theorem	tposmpo 6249*	Transposition of a two-argument mapping. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ tpos 𝐹 = (𝑦 ∈ 𝐵, 𝑥 ∈ 𝐴 ↦ 𝐶)
2.6.18  Undefined values
Theorem	pwuninel2 6250	The power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ (∪ 𝐴 ∈ 𝑉 → ¬ 𝒫 ∪ 𝐴 ∈ 𝐴)
Theorem	2pwuninelg 6251	The power set of the power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set. (Contributed by Jim Kingdon, 14-Jan-2020.)
⊢ (𝐴 ∈ 𝑉 → ¬ 𝒫 𝒫 ∪ 𝐴 ∈ 𝐴)
2.6.19  Functions on ordinals; strictly monotone ordinal functions
Theorem	iunon 6252*	The indexed union of a set of ordinal numbers 𝐵(𝑥) is an ordinal number. (Contributed by NM, 13-Oct-2003.) (Revised by Mario Carneiro, 5-Dec-2016.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ On) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ On)
Syntax	wsmo 6253	Introduce the strictly monotone ordinal function. A strictly monotone function is one that is constantly increasing across the ordinals.
wff Smo 𝐴
Definition	df-smo 6254*	Definition of a strictly monotone ordinal function. Definition 7.46 in [TakeutiZaring] p. 50. (Contributed by Andrew Salmon, 15-Nov-2011.)
⊢ (Smo 𝐴 ↔ (𝐴:dom 𝐴⟶On ∧ Ord dom 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦))))
Theorem	dfsmo2 6255*	Alternate definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 4-Mar-2013.)
⊢ (Smo 𝐹 ↔ (𝐹:dom 𝐹⟶On ∧ Ord dom 𝐹 ∧ ∀𝑥 ∈ dom 𝐹∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥)))
Theorem	issmo 6256*	Conditions for which 𝐴 is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 15-Nov-2011.)
⊢ 𝐴:𝐵⟶On    &   ⊢ Ord 𝐵    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)))    &   ⊢ dom 𝐴 = 𝐵    ⇒   ⊢ Smo 𝐴
Theorem	issmo2 6257*	Alternate definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 12-Mar-2013.)
⊢ (𝐹:𝐴⟶𝐵 → ((𝐵 ⊆ On ∧ Ord 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥)) → Smo 𝐹))
Theorem	smoeq 6258	Equality theorem for strictly monotone functions. (Contributed by Andrew Salmon, 16-Nov-2011.)
⊢ (𝐴 = 𝐵 → (Smo 𝐴 ↔ Smo 𝐵))
Theorem	smodm 6259	The domain of a strictly monotone function is an ordinal. (Contributed by Andrew Salmon, 16-Nov-2011.)
⊢ (Smo 𝐴 → Ord dom 𝐴)
Theorem	smores 6260	A strictly monotone function restricted to an ordinal remains strictly monotone. (Contributed by Andrew Salmon, 16-Nov-2011.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
⊢ ((Smo 𝐴 ∧ 𝐵 ∈ dom 𝐴) → Smo (𝐴 ↾ 𝐵))
Theorem	smores3 6261	A strictly monotone function restricted to an ordinal remains strictly monotone. (Contributed by Andrew Salmon, 19-Nov-2011.)
⊢ ((Smo (𝐴 ↾ 𝐵) ∧ 𝐶 ∈ (dom 𝐴 ∩ 𝐵) ∧ Ord 𝐵) → Smo (𝐴 ↾ 𝐶))
Theorem	smores2 6262	A strictly monotone ordinal function restricted to an ordinal is still monotone. (Contributed by Mario Carneiro, 15-Mar-2013.)
⊢ ((Smo 𝐹 ∧ Ord 𝐴) → Smo (𝐹 ↾ 𝐴))
Theorem	smodm2 6263	The domain of a strictly monotone ordinal function is an ordinal. (Contributed by Mario Carneiro, 12-Mar-2013.)
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹) → Ord 𝐴)
Theorem	smofvon2dm 6264	The function values of a strictly monotone ordinal function are ordinals. (Contributed by Mario Carneiro, 12-Mar-2013.)
⊢ ((Smo 𝐹 ∧ 𝐵 ∈ dom 𝐹) → (𝐹‘𝐵) ∈ On)
Theorem	iordsmo 6265	The identity relation restricted to the ordinals is a strictly monotone function. (Contributed by Andrew Salmon, 16-Nov-2011.)
⊢ Ord 𝐴    ⇒   ⊢ Smo ( I ↾ 𝐴)
Theorem	smo0 6266	The null set is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 20-Nov-2011.)
⊢ Smo ∅
Theorem	smofvon 6267	If 𝐵 is a strictly monotone ordinal function, and 𝐴 is in the domain of 𝐵, then the value of the function at 𝐴 is an ordinal. (Contributed by Andrew Salmon, 20-Nov-2011.)
⊢ ((Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵) → (𝐵‘𝐴) ∈ On)
Theorem	smoel 6268	If 𝑥 is less than 𝑦 then a strictly monotone function's value will be strictly less at 𝑥 than at 𝑦. (Contributed by Andrew Salmon, 22-Nov-2011.)
⊢ ((Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐵‘𝐶) ∈ (𝐵‘𝐴))
Theorem	smoiun 6269*	The value of a strictly monotone ordinal function contains its indexed union. (Contributed by Andrew Salmon, 22-Nov-2011.)
⊢ ((Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵) → ∪ 𝑥 ∈ 𝐴 (𝐵‘𝑥) ⊆ (𝐵‘𝐴))
Theorem	smoiso 6270	If 𝐹 is an isomorphism from an ordinal 𝐴 onto 𝐵, which is a subset of the ordinals, then 𝐹 is a strictly monotonic function. Exercise 3 in [TakeutiZaring] p. 50. (Contributed by Andrew Salmon, 24-Nov-2011.)
⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ 𝐵 ⊆ On) → Smo 𝐹)
Theorem	smoel2 6271	A strictly monotone ordinal function preserves the epsilon relation. (Contributed by Mario Carneiro, 12-Mar-2013.)
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵)) → (𝐹‘𝐶) ∈ (𝐹‘𝐵))
2.6.20  "Strong" transfinite recursion
Syntax	crecs 6272	Notation for a function defined by strong transfinite recursion.
class recs(𝐹)
Definition	df-recs 6273*	Define a function recs(𝐹) on On, the class of ordinal numbers, by transfinite recursion given a rule 𝐹 which sets the next value given all values so far. See df-irdg 6338 for more details on why this definition is desirable. Unlike df-irdg 6338 which restricts the update rule to use only the previous value, this version allows the update rule to use all previous values, which is why it is described as "strong", although it is actually more primitive. See tfri1d 6303 and tfri2d 6304 for the primary contract of this definition. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ recs(𝐹) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}
Theorem	recseq 6274	Equality theorem for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ (𝐹 = 𝐺 → recs(𝐹) = recs(𝐺))
Theorem	nfrecs 6275	Bound-variable hypothesis builder for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ Ⅎ𝑥𝐹    ⇒   ⊢ Ⅎ𝑥recs(𝐹)
Theorem	tfrlem1 6276*	A technical lemma for transfinite recursion. Compare Lemma 1 of [TakeutiZaring] p. 47. (Contributed by NM, 23-Mar-1995.) (Revised by Mario Carneiro, 24-May-2019.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → (Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹))    &   ⊢ (𝜑 → (Fun 𝐺 ∧ 𝐴 ⊆ dom 𝐺))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐵‘(𝐹 ↾ 𝑥)))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐺‘𝑥) = (𝐵‘(𝐺 ↾ 𝑥)))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
Theorem	tfrlem3ag 6277*	Lemma for transfinite recursion. This lemma just changes some bound variables in 𝐴 for later use. (Contributed by Jim Kingdon, 5-Jul-2019.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    ⇒   ⊢ (𝐺 ∈ V → (𝐺 ∈ 𝐴 ↔ ∃𝑧 ∈ On (𝐺 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝐺‘𝑤) = (𝐹‘(𝐺 ↾ 𝑤)))))
Theorem	tfrlem3a 6278*	Lemma for transfinite recursion. Let 𝐴 be the class of "acceptable" functions. The final thing we're interested in is the union of all these acceptable functions. This lemma just changes some bound variables in 𝐴 for later use. (Contributed by NM, 9-Apr-1995.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    &   ⊢ 𝐺 ∈ V    ⇒   ⊢ (𝐺 ∈ 𝐴 ↔ ∃𝑧 ∈ On (𝐺 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝐺‘𝑤) = (𝐹‘(𝐺 ↾ 𝑤))))
Theorem	tfrlem3 6279*	Lemma for transfinite recursion. Let 𝐴 be the class of "acceptable" functions. The final thing we're interested in is the union of all these acceptable functions. This lemma just changes some bound variables in 𝐴 for later use. (Contributed by NM, 9-Apr-1995.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    ⇒   ⊢ 𝐴 = {𝑔 ∣ ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))}
Theorem	tfrlem3-2d 6280*	Lemma for transfinite recursion which changes a bound variable (Contributed by Jim Kingdon, 2-Jul-2019.)
⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))    ⇒   ⊢ (𝜑 → (Fun 𝐹 ∧ (𝐹‘𝑔) ∈ V))
Theorem	tfrlem4 6281*	Lemma for transfinite recursion. 𝐴 is the class of all "acceptable" functions, and 𝐹 is their union. First we show that an acceptable function is in fact a function. (Contributed by NM, 9-Apr-1995.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    ⇒   ⊢ (𝑔 ∈ 𝐴 → Fun 𝑔)
Theorem	tfrlem5 6282*	Lemma for transfinite recursion. The values of two acceptable functions are the same within their domains. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 24-May-2019.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    ⇒   ⊢ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣))
Theorem	recsfval 6283*	Lemma for transfinite recursion. The definition recs is the union of all acceptable functions. (Contributed by Mario Carneiro, 9-May-2015.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    ⇒   ⊢ recs(𝐹) = ∪ 𝐴
Theorem	tfrlem6 6284*	Lemma for transfinite recursion. The union of all acceptable functions is a relation. (Contributed by NM, 8-Aug-1994.) (Revised by Mario Carneiro, 9-May-2015.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    ⇒   ⊢ Rel recs(𝐹)
Theorem	tfrlem7 6285*	Lemma for transfinite recursion. The union of all acceptable functions is a function. (Contributed by NM, 9-Aug-1994.) (Revised by Mario Carneiro, 24-May-2019.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    ⇒   ⊢ Fun recs(𝐹)
Theorem	tfrlem8 6286*	Lemma for transfinite recursion. The domain of recs is ordinal. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Alan Sare, 11-Mar-2008.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    ⇒   ⊢ Ord dom recs(𝐹)
Theorem	tfrlem9 6287*	Lemma for transfinite recursion. Here we compute the value of recs (the union of all acceptable functions). (Contributed by NM, 17-Aug-1994.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    ⇒   ⊢ (𝐵 ∈ dom recs(𝐹) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵)))
Theorem	tfrfun 6288	Transfinite recursion produces a function. (Contributed by Jim Kingdon, 20-Aug-2021.)
⊢ Fun recs(𝐹)
Theorem	tfr2a 6289	A weak version of transfinite recursion. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    ⇒   ⊢ (𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = (𝐺‘(𝐹 ↾ 𝐴)))
Theorem	tfr0dm 6290	Transfinite recursion is defined at the empty set. (Contributed by Jim Kingdon, 8-Mar-2022.)
⊢ 𝐹 = recs(𝐺)    ⇒   ⊢ ((𝐺‘∅) ∈ 𝑉 → ∅ ∈ dom 𝐹)
Theorem	tfr0 6291	Transfinite recursion at the empty set. (Contributed by Jim Kingdon, 8-May-2020.)
⊢ 𝐹 = recs(𝐺)    ⇒   ⊢ ((𝐺‘∅) ∈ 𝑉 → (𝐹‘∅) = (𝐺‘∅))
Theorem	tfrlemisucfn 6292*	We can extend an acceptable function by one element to produce a function. Lemma for tfrlemi1 6300. (Contributed by Jim Kingdon, 2-Jul-2019.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    &   ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))    &   ⊢ (𝜑 → 𝑧 ∈ On)    &   ⊢ (𝜑 → 𝑔 Fn 𝑧)    &   ⊢ (𝜑 → 𝑔 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐹‘𝑔)⟩}) Fn suc 𝑧)
Theorem	tfrlemisucaccv 6293*	We can extend an acceptable function by one element to produce an acceptable function. Lemma for tfrlemi1 6300. (Contributed by Jim Kingdon, 4-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    &   ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))    &   ⊢ (𝜑 → 𝑧 ∈ On)    &   ⊢ (𝜑 → 𝑔 Fn 𝑧)    &   ⊢ (𝜑 → 𝑔 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑔 ∪ {⟨𝑧, (𝐹‘𝑔)⟩}) ∈ 𝐴)
Theorem	tfrlemibacc 6294*	Each element of 𝐵 is an acceptable function. Lemma for tfrlemi1 6300. (Contributed by Jim Kingdon, 14-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    &   ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))    &   ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {⟨𝑧, (𝐹‘𝑔)⟩}))}    &   ⊢ (𝜑 → 𝑥 ∈ On)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))    ⇒   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
Theorem	tfrlemibxssdm 6295*	The union of 𝐵 is defined on all ordinals. Lemma for tfrlemi1 6300. (Contributed by Jim Kingdon, 18-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    &   ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))    &   ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {⟨𝑧, (𝐹‘𝑔)⟩}))}    &   ⊢ (𝜑 → 𝑥 ∈ On)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))    ⇒   ⊢ (𝜑 → 𝑥 ⊆ dom ∪ 𝐵)
Theorem	tfrlemibfn 6296*	The union of 𝐵 is a function defined on 𝑥. Lemma for tfrlemi1 6300. (Contributed by Jim Kingdon, 18-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    &   ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))    &   ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {⟨𝑧, (𝐹‘𝑔)⟩}))}    &   ⊢ (𝜑 → 𝑥 ∈ On)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))    ⇒   ⊢ (𝜑 → ∪ 𝐵 Fn 𝑥)
Theorem	tfrlemibex 6297*	The set 𝐵 exists. Lemma for tfrlemi1 6300. (Contributed by Jim Kingdon, 17-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    &   ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))    &   ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {⟨𝑧, (𝐹‘𝑔)⟩}))}    &   ⊢ (𝜑 → 𝑥 ∈ On)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))    ⇒   ⊢ (𝜑 → 𝐵 ∈ V)
Theorem	tfrlemiubacc 6298*	The union of 𝐵 satisfies the recursion rule (lemma for tfrlemi1 6300). (Contributed by Jim Kingdon, 22-Apr-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    &   ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))    &   ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {⟨𝑧, (𝐹‘𝑔)⟩}))}    &   ⊢ (𝜑 → 𝑥 ∈ On)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))    ⇒   ⊢ (𝜑 → ∀𝑢 ∈ 𝑥 (∪ 𝐵‘𝑢) = (𝐹‘(∪ 𝐵 ↾ 𝑢)))
Theorem	tfrlemiex 6299*	Lemma for tfrlemi1 6300. (Contributed by Jim Kingdon, 18-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    &   ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))    &   ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {⟨𝑧, (𝐹‘𝑔)⟩}))}    &   ⊢ (𝜑 → 𝑥 ∈ On)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤))))    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑢 ∈ 𝑥 (𝑓‘𝑢) = (𝐹‘(𝑓 ↾ 𝑢))))
Theorem	tfrlemi1 6300*	We can define an acceptable function on any ordinal. As with many of the transfinite recursion theorems, we have a hypothesis that states that 𝐹 is a function and that it is defined for all ordinals. (Contributed by Jim Kingdon, 4-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))}    &   ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V))    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ On) → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢))))