P. 337 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33601-33700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	inffz 33601	The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by AV, 10-Oct-2021.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → inf((𝑀...𝑁), ℤ, < ) = 𝑀)
Theorem	fz0n 33602	The sequence (0...(𝑁 − 1)) is empty iff 𝑁 is zero. (Contributed by Scott Fenton, 16-May-2014.)
⊢ (𝑁 ∈ ℕ0 → ((0...(𝑁 − 1)) = ∅ ↔ 𝑁 = 0))
Theorem	shftvalg 33603	Value of a sequence shifted by 𝐴. (Contributed by Scott Fenton, 16-Dec-2017.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘𝐵) = (𝐹‘(𝐵 − 𝐴)))
Theorem	divcnvlin 33604*	Limit of the ratio of two linear functions. (Contributed by Scott Fenton, 17-Dec-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = ((𝑘 + 𝐴) / (𝑘 + 𝐵)))    ⇒   ⊢ (𝜑 → 𝐹 ⇝ 1)
Theorem	climlec3 33605*	Comparison of a constant to the limit of a sequence. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ≤ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐵)
Theorem	logi 33606	Calculate the logarithm of i. (Contributed by Scott Fenton, 13-Apr-2020.)
⊢ (log‘i) = (i · (π / 2))
Theorem	iexpire 33607	i raised to itself is real. (Contributed by Scott Fenton, 13-Apr-2020.)
⊢ (i↑𝑐i) ∈ ℝ
Theorem	bcneg1 33608	The binomial coefficent over negative one is zero. (Contributed by Scott Fenton, 29-May-2020.)
⊢ (𝑁 ∈ ℕ0 → (𝑁C-1) = 0)
Theorem	bcm1nt 33609	The proportion of one bionmial coefficient to another with 𝑁 decreased by 1. (Contributed by Scott Fenton, 23-Jun-2020.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...(𝑁 − 1))) → (𝑁C𝐾) = (((𝑁 − 1)C𝐾) · (𝑁 / (𝑁 − 𝐾))))
Theorem	bcprod 33610*	A product identity for binomial coefficents. (Contributed by Scott Fenton, 23-Jun-2020.)
⊢ (𝑁 ∈ ℕ → ∏𝑘 ∈ (1...(𝑁 − 1))((𝑁 − 1)C𝑘) = ∏𝑘 ∈ (1...(𝑁 − 1))(𝑘↑((2 · 𝑘) − 𝑁)))
Theorem	bccolsum 33611*	A column-sum rule for binomial coefficents. (Contributed by Scott Fenton, 24-Jun-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → Σ𝑘 ∈ (0...𝑁)(𝑘C𝐶) = ((𝑁 + 1)C(𝐶 + 1)))
20.9.6  Infinite products
Theorem	iprodefisumlem 33612	Lemma for iprodefisum 33613. (Contributed by Scott Fenton, 11-Feb-2018.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℂ)    ⇒   ⊢ (𝜑 → seq𝑀( · , (exp ∘ 𝐹)) = (exp ∘ seq𝑀( + , 𝐹)))
Theorem	iprodefisum 33613*	Applying the exponential function to an infinite sum yields an infinite product. (Contributed by Scott Fenton, 11-Feb-2018.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝑍 (exp‘𝐵) = (exp‘Σ𝑘 ∈ 𝑍 𝐵))
Theorem	iprodgam 33614*	An infinite product version of Euler's gamma function. (Contributed by Scott Fenton, 12-Feb-2018.)
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))    ⇒   ⊢ (𝜑 → (Γ‘𝐴) = (∏𝑘 ∈ ℕ (((1 + (1 / 𝑘))↑𝑐𝐴) / (1 + (𝐴 / 𝑘))) / 𝐴))
20.9.7  Factorial limits
Theorem	faclimlem1 33615*	Lemma for faclim 33618. Closed form for a particular sequence. (Contributed by Scott Fenton, 15-Dec-2017.)
⊢ (𝑀 ∈ ℕ0 → seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) = (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1))))))
Theorem	faclimlem2 33616*	Lemma for faclim 33618. Show a limit for the inductive step. (Contributed by Scott Fenton, 15-Dec-2017.)
⊢ (𝑀 ∈ ℕ0 → seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) ⇝ (𝑀 + 1))
Theorem	faclimlem3 33617	Lemma for faclim 33618. Algebraic manipulation for the final induction. (Contributed by Scott Fenton, 15-Dec-2017.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝐵 ∈ ℕ) → (((1 + (1 / 𝐵))↑(𝑀 + 1)) / (1 + ((𝑀 + 1) / 𝐵))) = ((((1 + (1 / 𝐵))↑𝑀) / (1 + (𝑀 / 𝐵))) · (((1 + (𝑀 / 𝐵)) · (1 + (1 / 𝐵))) / (1 + ((𝑀 + 1) / 𝐵)))))
Theorem	faclim 33618*	An infinite product expression relating to factorials. Originally due to Euler. (Contributed by Scott Fenton, 22-Nov-2017.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((1 + (1 / 𝑛))↑𝐴) / (1 + (𝐴 / 𝑛))))    ⇒   ⊢ (𝐴 ∈ ℕ0 → seq1( · , 𝐹) ⇝ (!‘𝐴))
Theorem	iprodfac 33619*	An infinite product expression for factorial. (Contributed by Scott Fenton, 15-Dec-2017.)
⊢ (𝐴 ∈ ℕ0 → (!‘𝐴) = ∏𝑘 ∈ ℕ (((1 + (1 / 𝑘))↑𝐴) / (1 + (𝐴 / 𝑘))))
Theorem	faclim2 33620*	Another factorial limit due to Euler. (Contributed by Scott Fenton, 17-Dec-2017.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((!‘𝑛) · ((𝑛 + 1)↑𝑀)) / (!‘(𝑛 + 𝑀))))    ⇒   ⊢ (𝑀 ∈ ℕ0 → 𝐹 ⇝ 1)
20.9.8  Greatest common divisor and divisibility
Theorem	gcd32 33621	Swap the second and third arguments of a gcd. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((𝐴 gcd 𝐵) gcd 𝐶) = ((𝐴 gcd 𝐶) gcd 𝐵))
Theorem	gcdabsorb 33622	Absorption law for gcd. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) gcd 𝐵) = (𝐴 gcd 𝐵))
20.9.9  Properties of relationships
Theorem	brtp 33623	A condition for a binary relation over an unordered triple. (Contributed by Scott Fenton, 8-Jun-2011.)
⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    ⇒   ⊢ (𝑋{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩, ⟨𝐸, 𝐹⟩}𝑌 ↔ ((𝑋 = 𝐴 ∧ 𝑌 = 𝐵) ∨ (𝑋 = 𝐶 ∧ 𝑌 = 𝐷) ∨ (𝑋 = 𝐸 ∧ 𝑌 = 𝐹)))
Theorem	dftr6 33624	A potential definition of transitivity for sets. (Contributed by Scott Fenton, 18-Mar-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (Tr 𝐴 ↔ 𝐴 ∈ (V ∖ ran (( E ∘ E ) ∖ E )))
Theorem	coep 33625*	Composition with the membership relation. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴( E ∘ 𝑅)𝐵 ↔ ∃𝑥 ∈ 𝐵 𝐴𝑅𝑥)
Theorem	coepr 33626*	Composition with the converse membership relation. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴(𝑅 ∘ ◡ E )𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑥𝑅𝐵)
Theorem	dffr5 33627	A quantifier-free definition of a well-founded relationship. (Contributed by Scott Fenton, 11-Apr-2011.)
⊢ (𝑅 Fr 𝐴 ↔ (𝒫 𝐴 ∖ {∅}) ⊆ ran ( E ∖ ( E ∘ ◡𝑅)))
Theorem	dfso2 33628	Quantifier-free definition of a strict order. (Contributed by Scott Fenton, 22-Feb-2013.)
⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ (𝐴 × 𝐴) ⊆ (𝑅 ∪ ( I ∪ ◡𝑅))))
Theorem	br8 33629*	Substitution for an eight-place predicate. (Contributed by Scott Fenton, 26-Sep-2013.) (Revised by Mario Carneiro, 3-May-2015.)
⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑒 = 𝐸 → (𝜏 ↔ 𝜂))    &   ⊢ (𝑓 = 𝐹 → (𝜂 ↔ 𝜁))    &   ⊢ (𝑔 = 𝐺 → (𝜁 ↔ 𝜎))    &   ⊢ (ℎ = 𝐻 → (𝜎 ↔ 𝜌))    &   ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄)    &   ⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑)}    ⇒   ⊢ (((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩𝑅⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ 𝜌))
Theorem	br6 33630*	Substitution for a six-place predicate. (Contributed by Scott Fenton, 4-Oct-2013.) (Revised by Mario Carneiro, 3-May-2015.)
⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑒 = 𝐸 → (𝜏 ↔ 𝜂))    &   ⊢ (𝑓 = 𝐹 → (𝜂 ↔ 𝜁))    &   ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄)    &   ⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)}    ⇒   ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) → (⟨𝐴, ⟨𝐵, 𝐶⟩⟩𝑅⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ 𝜁))
Theorem	br4 33631*	Substitution for a four-place predicate. (Contributed by Scott Fenton, 9-Oct-2013.) (Revised by Mario Carneiro, 14-Oct-2013.)
⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄)    &   ⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑)}    ⇒   ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) → (⟨𝐴, 𝐵⟩𝑅⟨𝐶, 𝐷⟩ ↔ 𝜏))
Theorem	cnvco1 33632	Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.)
⊢ ◡(◡𝐴 ∘ 𝐵) = (◡𝐵 ∘ 𝐴)
Theorem	cnvco2 33633	Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.)
⊢ ◡(𝐴 ∘ ◡𝐵) = (𝐵 ∘ ◡𝐴)
Theorem	eldm3 33634	Quantifier-free definition of membership in a domain. (Contributed by Scott Fenton, 21-Jan-2017.)
⊢ (𝐴 ∈ dom 𝐵 ↔ (𝐵 ↾ {𝐴}) ≠ ∅)
Theorem	elrn3 33635	Quantifier-free definition of membership in a range. (Contributed by Scott Fenton, 21-Jan-2017.)
⊢ (𝐴 ∈ ran 𝐵 ↔ (𝐵 ∩ (V × {𝐴})) ≠ ∅)
Theorem	pocnv 33636	The converse of a partial ordering is still a partial ordering. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ (𝑅 Po 𝐴 → ◡𝑅 Po 𝐴)
Theorem	socnv 33637	The converse of a strict ordering is still a strict ordering. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ (𝑅 Or 𝐴 → ◡𝑅 Or 𝐴)
Theorem	sotrd 33638	Transitivity law for strict orderings, deduction form. (Contributed by Scott Fenton, 24-Nov-2021.)
⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋𝑅𝑌)    &   ⊢ (𝜑 → 𝑌𝑅𝑍)    ⇒   ⊢ (𝜑 → 𝑋𝑅𝑍)
Theorem	sotr3 33639	Transitivity law for strict orderings. (Contributed by Scott Fenton, 24-Nov-2021.)
⊢ ((𝑅 Or 𝐴 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴)) → ((𝑋𝑅𝑌 ∧ ¬ 𝑍𝑅𝑌) → 𝑋𝑅𝑍))
Theorem	sotrine 33640	Trichotomy law for strict orderings. (Contributed by Scott Fenton, 8-Dec-2021.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 ≠ 𝐶 ↔ (𝐵𝑅𝐶 ∨ 𝐶𝑅𝐵)))
Theorem	eqfunresadj 33641	Law for adjoining an element to restrictions of functions. (Contributed by Scott Fenton, 6-Dec-2021.)
⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (𝐹 ↾ 𝑋) = (𝐺 ↾ 𝑋) ∧ (𝑌 ∈ dom 𝐹 ∧ 𝑌 ∈ dom 𝐺 ∧ (𝐹‘𝑌) = (𝐺‘𝑌))) → (𝐹 ↾ (𝑋 ∪ {𝑌})) = (𝐺 ↾ (𝑋 ∪ {𝑌})))
Theorem	eqfunressuc 33642	Law for equality of restriction to successors. This is primarily useful when 𝑋 is an ordinal, but it does not require that. (Contributed by Scott Fenton, 6-Dec-2021.)
⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (𝐹 ↾ 𝑋) = (𝐺 ↾ 𝑋) ∧ (𝑋 ∈ dom 𝐹 ∧ 𝑋 ∈ dom 𝐺 ∧ (𝐹‘𝑋) = (𝐺‘𝑋))) → (𝐹 ↾ suc 𝑋) = (𝐺 ↾ suc 𝑋))
Theorem	funeldmb 33643	If ∅ is not part of the range of a function 𝐹, then 𝐴 is in the domain of 𝐹 iff (𝐹‘𝐴) ≠ ∅. (Contributed by Scott Fenton, 7-Dec-2021.)
⊢ ((Fun 𝐹 ∧ ¬ ∅ ∈ ran 𝐹) → (𝐴 ∈ dom 𝐹 ↔ (𝐹‘𝐴) ≠ ∅))
Theorem	elintfv 33644*	Membership in an intersection of function values. (Contributed by Scott Fenton, 9-Dec-2021.)
⊢ 𝑋 ∈ V    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝑋 ∈ ∩ (𝐹 “ 𝐵) ↔ ∀𝑦 ∈ 𝐵 𝑋 ∈ (𝐹‘𝑦)))
20.9.10  Properties of functions and mappings
Theorem	funpsstri 33645	A condition for subset trichotomy for functions. (Contributed by Scott Fenton, 19-Apr-2011.)
⊢ ((Fun 𝐻 ∧ (𝐹 ⊆ 𝐻 ∧ 𝐺 ⊆ 𝐻) ∧ (dom 𝐹 ⊆ dom 𝐺 ∨ dom 𝐺 ⊆ dom 𝐹)) → (𝐹 ⊊ 𝐺 ∨ 𝐹 = 𝐺 ∨ 𝐺 ⊊ 𝐹))
Theorem	fundmpss 33646	If a class 𝐹 is a proper subset of a function 𝐺, then dom 𝐹 ⊊ dom 𝐺. (Contributed by Scott Fenton, 20-Apr-2011.)
⊢ (Fun 𝐺 → (𝐹 ⊊ 𝐺 → dom 𝐹 ⊊ dom 𝐺))
Theorem	fvresval 33647	The value of a function at a restriction is either null or the same as the function itself. (Contributed by Scott Fenton, 4-Sep-2011.)
⊢ (((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴) ∨ ((𝐹 ↾ 𝐵)‘𝐴) = ∅)
Theorem	funsseq 33648	Given two functions with equal domains, equality only requires one direction of the subset relationship. (Contributed by Scott Fenton, 24-Apr-2012.) (Proof shortened by Mario Carneiro, 3-May-2015.)
⊢ ((Fun 𝐹 ∧ Fun 𝐺 ∧ dom 𝐹 = dom 𝐺) → (𝐹 = 𝐺 ↔ 𝐹 ⊆ 𝐺))
Theorem	fununiq 33649	The uniqueness condition of functions. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (Fun 𝐹 → ((𝐴𝐹𝐵 ∧ 𝐴𝐹𝐶) → 𝐵 = 𝐶))
Theorem	funbreq 33650	An equality condition for functions. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ ((Fun 𝐹 ∧ 𝐴𝐹𝐵) → (𝐴𝐹𝐶 ↔ 𝐵 = 𝐶))
Theorem	br1steq 33651	Uniqueness condition for the binary relation 1st. (Contributed by Scott Fenton, 11-Apr-2014.) (Proof shortened by Mario Carneiro, 3-May-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩1st 𝐶 ↔ 𝐶 = 𝐴)
Theorem	br2ndeq 33652	Uniqueness condition for the binary relation 2nd. (Contributed by Scott Fenton, 11-Apr-2014.) (Proof shortened by Mario Carneiro, 3-May-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩2nd 𝐶 ↔ 𝐶 = 𝐵)
Theorem	dfdm5 33653	Definition of domain in terms of 1st and image. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ dom 𝐴 = ((1st ↾ (V × V)) “ 𝐴)
Theorem	dfrn5 33654	Definition of range in terms of 2nd and image. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ ran 𝐴 = ((2nd ↾ (V × V)) “ 𝐴)
Theorem	opelco3 33655	Alternate way of saying that an ordered pair is in a composition. (Contributed by Scott Fenton, 6-May-2018.)
⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 ∘ 𝐷) ↔ 𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})))
Theorem	elima4 33656	Quantifier-free expression saying that a class is a member of an image. (Contributed by Scott Fenton, 8-May-2018.)
⊢ (𝐴 ∈ (𝑅 “ 𝐵) ↔ (𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅)
Theorem	fv1stcnv 33657	The value of the converse of 1st restricted to a singleton. (Contributed by Scott Fenton, 2-Jul-2020.)
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → (◡(1st ↾ (𝐴 × {𝑌}))‘𝑋) = ⟨𝑋, 𝑌⟩)
Theorem	fv2ndcnv 33658	The value of the converse of 2nd restricted to a singleton. (Contributed by Scott Fenton, 2-Jul-2020.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → (◡(2nd ↾ ({𝑋} × 𝐴))‘𝑌) = ⟨𝑋, 𝑌⟩)
Theorem	imaindm 33659	The image is unaffected by intersection with the domain. (Contributed by Scott Fenton, 17-Dec-2021.)
⊢ (𝑅 “ 𝐴) = (𝑅 “ (𝐴 ∩ dom 𝑅))
20.9.11  Set induction (or epsilon induction)
Theorem	setinds 33660*	Principle of set induction (or E-induction). If a property passes from all elements of 𝑥 to 𝑥 itself, then it holds for all 𝑥. (Contributed by Scott Fenton, 10-Mar-2011.)
⊢ (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	setinds2f 33661*	E induction schema, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2011.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (∀𝑦 ∈ 𝑥 𝜓 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	setinds2 33662*	E induction schema, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2011.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (∀𝑦 ∈ 𝑥 𝜓 → 𝜑)    ⇒   ⊢ 𝜑
20.9.12  Ordinal numbers
Theorem	elpotr 33663*	A class of transitive sets is partially ordered by E. (Contributed by Scott Fenton, 15-Oct-2010.)
⊢ (∀𝑧 ∈ 𝐴 Tr 𝑧 → E Po 𝐴)
Theorem	dford5reg 33664	Given ax-reg 9281, an ordinal is a transitive class totally ordered by the membership relation. (Contributed by Scott Fenton, 28-Jan-2011.)
⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E Or 𝐴))
Theorem	dfon2lem1 33665	Lemma for dfon2 33674. (Contributed by Scott Fenton, 28-Feb-2011.)
⊢ Tr ∪ {𝑥 ∣ (𝜑 ∧ Tr 𝑥 ∧ 𝜓)}
Theorem	dfon2lem2 33666*	Lemma for dfon2 33674. (Contributed by Scott Fenton, 28-Feb-2011.)
⊢ ∪ {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝜑 ∧ 𝜓)} ⊆ 𝐴
Theorem	dfon2lem3 33667*	Lemma for dfon2 33674. All sets satisfying the new definition are transitive and untangled. (Contributed by Scott Fenton, 25-Feb-2011.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) → (Tr 𝐴 ∧ ∀𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑧)))
Theorem	dfon2lem4 33668*	Lemma for dfon2 33674. If two sets satisfy the new definition, then one is a subset of the other. (Contributed by Scott Fenton, 25-Feb-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) ∧ ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴))
Theorem	dfon2lem5 33669*	Lemma for dfon2 33674. Two sets satisfying the new definition also satisfy trichotomy with respect to ∈. (Contributed by Scott Fenton, 25-Feb-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) ∧ ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))
Theorem	dfon2lem6 33670*	Lemma for dfon2 33674. A transitive class of sets satisfying the new definition satisfies the new definition. (Contributed by Scott Fenton, 25-Feb-2011.)
⊢ ((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) → ∀𝑦((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → 𝑦 ∈ 𝑆))
Theorem	dfon2lem7 33671*	Lemma for dfon2 33674. All elements of a new ordinal are new ordinals. (Contributed by Scott Fenton, 25-Feb-2011.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) → (𝐵 ∈ 𝐴 → ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)))
Theorem	dfon2lem8 33672*	Lemma for dfon2 33674. The intersection of a nonempty class 𝐴 of new ordinals is itself a new ordinal and is contained within 𝐴 (Contributed by Scott Fenton, 26-Feb-2011.)
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) ∧ ∩ 𝐴 ∈ 𝐴))
Theorem	dfon2lem9 33673*	Lemma for dfon2 33674. A class of new ordinals is well-founded by E. (Contributed by Scott Fenton, 3-Mar-2011.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → E Fr 𝐴)
Theorem	dfon2 33674*	On consists of all sets that contain all its transitive proper subsets. This definition comes from J. R. Isbell, "A Definition of Ordinal Numbers", American Mathematical Monthly, vol 67 (1960), pp. 51-52. (Contributed by Scott Fenton, 20-Feb-2011.)
⊢ On = {𝑥 ∣ ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)}
Theorem	rdgprc0 33675	The value of the recursive definition generator at ∅ when the base value is a proper class. (Contributed by Scott Fenton, 26-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (¬ 𝐼 ∈ V → (rec(𝐹, 𝐼)‘∅) = ∅)
Theorem	rdgprc 33676	The value of the recursive definition generator when 𝐼 is a proper class. (Contributed by Scott Fenton, 26-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (¬ 𝐼 ∈ V → rec(𝐹, 𝐼) = rec(𝐹, ∅))
Theorem	dfrdg2 33677*	Alternate definition of the recursive function generator when 𝐼 is a set. (Contributed by Scott Fenton, 26-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (𝐼 ∈ 𝑉 → rec(𝐹, 𝐼) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))})
Theorem	dfrdg3 33678*	Generalization of dfrdg2 33677 to remove sethood requirement. (Contributed by Scott Fenton, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ rec(𝐹, 𝐼) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐼 ∈ V, 𝐼, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))}
20.9.13  Defined equality axioms
Theorem	axextdfeq 33679	A version of ax-ext 2709 for use with defined equality. (Contributed by Scott Fenton, 12-Dec-2010.)
⊢ ∃𝑧((𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦) → ((𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥) → (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)))
Theorem	ax8dfeq 33680	A version of ax-8 2110 for use with defined equality. (Contributed by Scott Fenton, 12-Dec-2010.)
⊢ ∃𝑧((𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦) → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑦))
Theorem	axextdist 33681	ax-ext 2709 with distinctors instead of distinct variable conditions. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦))
Theorem	axextbdist 33682	axextb 2712 with distinctors instead of distinct variable conditions. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (𝑥 = 𝑦 ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)))
Theorem	19.12b 33683*	Version of 19.12vv 2347 with not-free hypotheses, instead of distinct variable conditions. (Contributed by Scott Fenton, 13-Dec-2010.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃𝑥∀𝑦(𝜑 → 𝜓) ↔ ∀𝑦∃𝑥(𝜑 → 𝜓))
Theorem	exnel 33684	There is always a set not in 𝑦. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ ∃𝑥 ¬ 𝑥 ∈ 𝑦
Theorem	distel 33685	Distinctors in terms of membership. (NOTE: this only works with relations where we can prove el 5287 and elirrv 9285.) (Contributed by Scott Fenton, 15-Dec-2010.)
⊢ (¬ ∀𝑦 𝑦 = 𝑥 ↔ ¬ ∀𝑦 ¬ 𝑥 ∈ 𝑦)
Theorem	axextndbi 33686	axextnd 10278 as a biconditional. (Contributed by Scott Fenton, 14-Dec-2010.)
⊢ ∃𝑧(𝑥 = 𝑦 ↔ (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
20.9.14  Hypothesis builders
Theorem	hbntg 33687	A more general form of hbnt 2294. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜓) → (¬ 𝜓 → ∀𝑥 ¬ 𝜑))
Theorem	hbimtg 33688	A more general and closed form of hbim 2299. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ ((∀𝑥(𝜑 → ∀𝑥𝜒) ∧ (𝜓 → ∀𝑥𝜃)) → ((𝜒 → 𝜓) → ∀𝑥(𝜑 → 𝜃)))
Theorem	hbaltg 33689	A more general and closed form of hbal 2169. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ (∀𝑥(𝜑 → ∀𝑦𝜓) → (∀𝑥𝜑 → ∀𝑦∀𝑥𝜓))
Theorem	hbng 33690	A more general form of hbn 2295. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ (𝜑 → ∀𝑥𝜓)    ⇒   ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜑)
Theorem	hbimg 33691	A more general form of hbim 2299. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ (𝜑 → ∀𝑥𝜓)    &   ⊢ (𝜒 → ∀𝑥𝜃)    ⇒   ⊢ ((𝜓 → 𝜒) → ∀𝑥(𝜑 → 𝜃))
20.9.15  (Trans)finite Recursion Theorems
Theorem	tfisg 33692*	A closed form of tfis 7676. (Contributed by Scott Fenton, 8-Jun-2011.)
⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 → 𝜑) → ∀𝑥 ∈ On 𝜑)
20.9.16  Transitive closure of a relation
Syntax	cttrcl 33693	Declare the syntax for the transitive closure of a class.
class t++𝑅
Definition	df-ttrcl 33694*	Define the transitive closure of a class. This is the smallest relationship containing 𝑅 (or more precisely, the relation (𝑅 ↾ V) induced by 𝑅) and having the transitive property. Definition from [Levy] p. 59, who denotes it as 𝑅∗ and calls it the "ancestral" of 𝑅. (Contributed by Scott Fenton, 17-Oct-2024.)
⊢ t++𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚))}
Theorem	ttrcleq 33695	Equality theorem for transitive closure. (Contributed by Scott Fenton, 17-Oct-2024.)
⊢ (𝑅 = 𝑆 → t++𝑅 = t++𝑆)
Theorem	nfttrcld 33696	Bound variable hypothesis builder for transitive closure. Deduction form. (Contributed by Scott Fenton, 26-Oct-2024.)
⊢ (𝜑 → Ⅎ𝑥𝑅)    ⇒   ⊢ (𝜑 → Ⅎ𝑥t++𝑅)
Theorem	nfttrcl 33697	Bound variable hypothesis builder for transitive closure. (Contributed by Scott Fenton, 17-Oct-2024.)
⊢ Ⅎ𝑥𝑅    ⇒   ⊢ Ⅎ𝑥t++𝑅
Theorem	relttrcl 33698	The transitive closure of a class is a relation. (Contributed by Scott Fenton, 17-Oct-2024.)
⊢ Rel t++𝑅
Theorem	brttrcl 33699*	Characterization of elements of the transitive closure of a relation. (Contributed by Scott Fenton, 18-Aug-2024.)
⊢ (𝐴t++𝑅𝐵 ↔ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝐴 ∧ (𝑓‘𝑛) = 𝐵) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
Theorem	brttrcl2 33700*	Characterization of elements of the transitive closure of a relation. (Contributed by Scott Fenton, 24-Aug-2024.)
⊢ (𝐴t++𝑅𝐵 ↔ ∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝐴 ∧ (𝑓‘suc 𝑛) = 𝐵) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))