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
Definition	df-outsideof 36101	The outside of relationship. This relationship expresses that 𝑃, 𝐴, and 𝐵 fall on a line, but 𝑃 is not on the segment 𝐴𝐵. This definition is taken from theorem 6.4 of [Schwabhauser] p. 43, since it requires no dummy variables. (Contributed by Scott Fenton, 17-Oct-2013.)
⊢ OutsideOf = ( Colinear ∖ Btwn )
Theorem	broutsideof 36102	Binary relation form of OutsideOf. Theorem 6.4 of [Schwabhauser] p. 43. (Contributed by Scott Fenton, 17-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (𝑃OutsideOf⟨𝐴, 𝐵⟩ ↔ (𝑃 Colinear ⟨𝐴, 𝐵⟩ ∧ ¬ 𝑃 Btwn ⟨𝐴, 𝐵⟩))
Theorem	broutsideof2 36103	Alternate form of OutsideOf. Definition 6.1 of [Schwabhauser] p. 43. (Contributed by Scott Fenton, 17-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf⟨𝐴, 𝐵⟩ ↔ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ (𝐴 Btwn ⟨𝑃, 𝐵⟩ ∨ 𝐵 Btwn ⟨𝑃, 𝐴⟩))))
Theorem	outsidene1 36104	Outsideness implies inequality. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf⟨𝐴, 𝐵⟩ → 𝐴 ≠ 𝑃))
Theorem	outsidene2 36105	Outsideness implies inequality. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf⟨𝐴, 𝐵⟩ → 𝐵 ≠ 𝑃))
Theorem	btwnoutside 36106	A principle linking outsideness to betweenness. Theorem 6.2 of [Schwabhauser] p. 43. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → (((𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ 𝐶 ≠ 𝑃) ∧ 𝑃 Btwn ⟨𝐴, 𝐶⟩) → (𝑃 Btwn ⟨𝐵, 𝐶⟩ ↔ 𝑃OutsideOf⟨𝐴, 𝐵⟩)))
Theorem	broutsideof3 36107*	Characterization of outsideness in terms of relationship to a fourth point. Theorem 6.3 of [Schwabhauser] p. 43. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf⟨𝐴, 𝐵⟩ ↔ (𝐴 ≠ 𝑃 ∧ 𝐵 ≠ 𝑃 ∧ ∃𝑐 ∈ (𝔼‘𝑁)(𝑐 ≠ 𝑃 ∧ 𝑃 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑃 Btwn ⟨𝐵, 𝑐⟩))))
Theorem	outsideofrflx 36108	Reflexivity of outsideness. Theorem 6.5 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (𝐴 ≠ 𝑃 → 𝑃OutsideOf⟨𝐴, 𝐴⟩))
Theorem	outsideofcom 36109	Commutativity law for outsideness. Theorem 6.6 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf⟨𝐴, 𝐵⟩ ↔ 𝑃OutsideOf⟨𝐵, 𝐴⟩))
Theorem	outsideoftr 36110	Transitivity law for outsideness. Theorem 6.7 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 18-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁))) → ((𝑃OutsideOf⟨𝐴, 𝐵⟩ ∧ 𝑃OutsideOf⟨𝐵, 𝐶⟩) → 𝑃OutsideOf⟨𝐴, 𝐶⟩))
Theorem	outsideofeq 36111	Uniqueness law for OutsideOf. Analogue of segconeq 35991. (Contributed by Scott Fenton, 24-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑋 ∈ (𝔼‘𝑁) ∧ 𝑌 ∈ (𝔼‘𝑁))) → (((𝐴OutsideOf⟨𝑋, 𝑅⟩ ∧ ⟨𝐴, 𝑋⟩Cgr⟨𝐵, 𝐶⟩) ∧ (𝐴OutsideOf⟨𝑌, 𝑅⟩ ∧ ⟨𝐴, 𝑌⟩Cgr⟨𝐵, 𝐶⟩)) → 𝑋 = 𝑌))
Theorem	outsideofeu 36112*	Given a nondegenerate ray, there is a unique point congruent to the segment 𝐵𝐶 lying on the ray 𝐴𝑅. Theorem 6.11 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 23-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝑅 ≠ 𝐴 ∧ 𝐵 ≠ 𝐶) → ∃!𝑥 ∈ (𝔼‘𝑁)(𝐴OutsideOf⟨𝑥, 𝑅⟩ ∧ ⟨𝐴, 𝑥⟩Cgr⟨𝐵, 𝐶⟩)))
Theorem	outsidele 36113	Relate OutsideOf to Seg≤. Theorem 6.13 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 24-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁))) → (𝑃OutsideOf⟨𝐴, 𝐵⟩ → (⟨𝑃, 𝐴⟩ Seg≤ ⟨𝑃, 𝐵⟩ ↔ 𝐴 Btwn ⟨𝑃, 𝐵⟩)))
Theorem	outsideofcol 36114	Outside of implies colinearity. (Contributed by Scott Fenton, 26-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (𝑃OutsideOf⟨𝑄, 𝑅⟩ → 𝑃 Colinear ⟨𝑄, 𝑅⟩)
21.11.18.8  Lines and Rays
Syntax	cline2 36115	Declare the constant for the line function.
class Line
Syntax	cray 36116	Declare the constant for the ray function.
class Ray
Syntax	clines2 36117	Declare the constant for the set of all lines.
class LinesEE
Definition	df-line2 36118*	Define the Line function. This function generates the line passing through the distinct points 𝑎 and 𝑏. Adapted from definition 6.14 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 25-Oct-2013.)
⊢ Line = {⟨⟨𝑎, 𝑏⟩, 𝑙⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [⟨𝑎, 𝑏⟩]◡ Colinear )}
Definition	df-ray 36119*	Define the Ray function. This function generates the set of all points that lie on the ray starting at 𝑝 and passing through 𝑎. Definition 6.8 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 21-Oct-2013.)
⊢ Ray = {⟨⟨𝑝, 𝑎⟩, 𝑟⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf⟨𝑎, 𝑥⟩})}
Definition	df-lines2 36120	Define the set of all lines. Definition 6.14, part 2 of [Schwabhauser] p. 45. See ellines 36133 for membership. (Contributed by Scott Fenton, 28-Oct-2013.)
⊢ LinesEE = ran Line
Theorem	funray 36121	Show that the Ray relationship is a function. (Contributed by Scott Fenton, 21-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ Fun Ray
Theorem	fvray 36122*	Calculate the value of the Ray function. (Contributed by Scott Fenton, 21-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝐴)) → (𝑃Ray𝐴) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩})
Theorem	funline 36123	Show that the Line relationship is a function. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ Fun Line
Theorem	linedegen 36124	When Line is applied with the same argument, the result is the empty set. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (𝐴Line𝐴) = ∅
Theorem	fvline 36125*	Calculate the value of the Line function. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵)) → (𝐴Line𝐵) = {𝑥 ∣ 𝑥 Colinear ⟨𝐴, 𝐵⟩})
Theorem	liness 36126	A line is a subset of the space its two points lie in. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵)) → (𝐴Line𝐵) ⊆ (𝔼‘𝑁))
Theorem	fvline2 36127*	Alternate definition of a line. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵)) → (𝐴Line𝐵) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝐴, 𝐵⟩})
Theorem	lineunray 36128	A line is composed of a point and the two rays emerging from it. Theorem 6.15 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 26-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (𝑃 Btwn ⟨𝑄, 𝑅⟩ → (𝑃Line𝑄) = (((𝑃Ray𝑄) ∪ {𝑃}) ∪ (𝑃Ray𝑅))))
Theorem	lineelsb2 36129	If 𝑆 lies on 𝑃𝑄, then 𝑃𝑄 = 𝑃𝑆. Theorem 6.16 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 27-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → (𝑆 ∈ (𝑃Line𝑄) → (𝑃Line𝑄) = (𝑃Line𝑆)))
Theorem	linerflx1 36130	Reflexivity law for line membership. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → 𝑃 ∈ (𝑃Line𝑄))
Theorem	linecom 36131	Commutativity law for lines. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → (𝑃Line𝑄) = (𝑄Line𝑃))
Theorem	linerflx2 36132	Reflexivity law for line membership. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → 𝑄 ∈ (𝑃Line𝑄))
Theorem	ellines 36133*	Membership in the set of all lines. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (𝐴 ∈ LinesEE ↔ ∃𝑛 ∈ ℕ ∃𝑝 ∈ (𝔼‘𝑛)∃𝑞 ∈ (𝔼‘𝑛)(𝑝 ≠ 𝑞 ∧ 𝐴 = (𝑝Line𝑞)))
Theorem	linethru 36134	If 𝐴 is a line containing two distinct points 𝑃 and 𝑄, then 𝐴 is the line through 𝑃 and 𝑄. Theorem 6.18 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝐴 ∈ LinesEE ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → 𝐴 = (𝑃Line𝑄))
Theorem	hilbert1.1 36135*	There is a line through any two distinct points. Hilbert's axiom I.1 for geometry. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → ∃𝑥 ∈ LinesEE (𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥))
Theorem	hilbert1.2 36136*	There is at most one line through any two distinct points. Hilbert's axiom I.2 for geometry. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by NM, 17-Jun-2017.)
⊢ (𝑃 ≠ 𝑄 → ∃*𝑥 ∈ LinesEE (𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥))
Theorem	linethrueu 36137*	There is a unique line going through any two distinct points. Theorem 6.19 of [Schwabhauser] p. 46. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → ∃!𝑥 ∈ LinesEE (𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥))
Theorem	lineintmo 36138*	Two distinct lines intersect in at most one point. Theorem 6.21 of [Schwabhauser] p. 46. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝐴 ∈ LinesEE ∧ 𝐵 ∈ LinesEE ∧ 𝐴 ≠ 𝐵) → ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
21.11.19  Forward difference
Syntax	cfwddif 36139	Declare the syntax for the forward difference operator.
class △
Definition	df-fwddif 36140*	Define the forward difference operator. This is a discrete analogue of the derivative operator. Definition 2.42 of [GramKnuthPat], p. 47. (Contributed by Scott Fenton, 18-May-2020.)
⊢ △ = (𝑓 ∈ (ℂ ↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ dom 𝑓 ∣ (𝑦 + 1) ∈ dom 𝑓} ↦ ((𝑓‘(𝑥 + 1)) − (𝑓‘𝑥))))
Syntax	cfwddifn 36141	Declare the syntax for the nth forward difference operator.
class △n
Definition	df-fwddifn 36142*	Define the nth forward difference operator. This works out to be the forward difference operator iterated 𝑛 times. (Contributed by Scott Fenton, 28-May-2020.)
⊢ △n = (𝑛 ∈ ℕ0, 𝑓 ∈ (ℂ ↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓} ↦ Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((-1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘))))))
Theorem	fwddifval 36143	Calculate the value of the forward difference operator at a point. (Contributed by Scott Fenton, 18-May-2020.)
⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑋 + 1) ∈ 𝐴)    ⇒   ⊢ (𝜑 → (( △ ‘𝐹)‘𝑋) = ((𝐹‘(𝑋 + 1)) − (𝐹‘𝑋)))
Theorem	fwddifnval 36144*	The value of the forward difference operator at a point. (Contributed by Scott Fenton, 28-May-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑋 + 𝑘) ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((𝑁 △n 𝐹)‘𝑋) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))))
Theorem	fwddifn0 36145	The value of the n-iterated forward difference operator at zero is just the function value. (Contributed by Scott Fenton, 28-May-2020.)
⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((0 △n 𝐹)‘𝑋) = (𝐹‘𝑋))
Theorem	fwddifnp1 36146*	The value of the n-iterated forward difference at a successor. (Contributed by Scott Fenton, 28-May-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑋 + 𝑘) ∈ 𝐴)    ⇒   ⊢ (𝜑 → (((𝑁 + 1) △n 𝐹)‘𝑋) = (((𝑁 △n 𝐹)‘(𝑋 + 1)) − ((𝑁 △n 𝐹)‘𝑋)))
21.11.20  Rank theorems
Theorem	rankung 36147	The rank of the union of two sets. Closed form of rankun 9893. (Contributed by Scott Fenton, 15-Jul-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (rank‘(𝐴 ∪ 𝐵)) = ((rank‘𝐴) ∪ (rank‘𝐵)))
Theorem	ranksng 36148	The rank of a singleton. Closed form of ranksn 9891. (Contributed by Scott Fenton, 15-Jul-2015.)
⊢ (𝐴 ∈ 𝑉 → (rank‘{𝐴}) = suc (rank‘𝐴))
Theorem	rankelg 36149	The membership relation is inherited by the rank function. Closed form of rankel 9876. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝐵) → (rank‘𝐴) ∈ (rank‘𝐵))
Theorem	rankpwg 36150	The rank of a power set. Closed form of rankpw 9880. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ (𝐴 ∈ 𝑉 → (rank‘𝒫 𝐴) = suc (rank‘𝐴))
Theorem	rank0 36151	The rank of the empty set is ∅. (Contributed by Scott Fenton, 17-Jul-2015.)
⊢ (rank‘∅) = ∅
Theorem	rankeq1o 36152	The only set with rank 1o is the singleton of the empty set. (Contributed by Scott Fenton, 17-Jul-2015.)
⊢ ((rank‘𝐴) = 1o ↔ 𝐴 = {∅})
21.11.21  Hereditarily Finite Sets
Syntax	chf 36153	The constant Hf is a class.
class Hf
Definition	df-hf 36154	Define the hereditarily finite sets. These are the finite sets whose elements are finite, and so forth. (Contributed by Scott Fenton, 9-Jul-2015.)
⊢ Hf = ∪ (𝑅1 “ ω)
Theorem	elhf 36155*	Membership in the hereditarily finite sets. (Contributed by Scott Fenton, 9-Jul-2015.)
⊢ (𝐴 ∈ Hf ↔ ∃𝑥 ∈ ω 𝐴 ∈ (𝑅1‘𝑥))
Theorem	elhf2 36156	Alternate form of membership in the hereditarily finite sets. (Contributed by Scott Fenton, 13-Jul-2015.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ Hf ↔ (rank‘𝐴) ∈ ω)
Theorem	elhf2g 36157	Hereditarily finiteness via rank. Closed form of elhf2 36156. (Contributed by Scott Fenton, 15-Jul-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Hf ↔ (rank‘𝐴) ∈ ω))
Theorem	0hf 36158	The empty set is a hereditarily finite set. (Contributed by Scott Fenton, 9-Jul-2015.)
⊢ ∅ ∈ Hf
Theorem	hfun 36159	The union of two HF sets is an HF set. (Contributed by Scott Fenton, 15-Jul-2015.)
⊢ ((𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) → (𝐴 ∪ 𝐵) ∈ Hf )
Theorem	hfsn 36160	The singleton of an HF set is an HF set. (Contributed by Scott Fenton, 15-Jul-2015.)
⊢ (𝐴 ∈ Hf → {𝐴} ∈ Hf )
Theorem	hfadj 36161	Adjoining one HF element to an HF set preserves HF status. (Contributed by Scott Fenton, 15-Jul-2015.)
⊢ ((𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) → (𝐴 ∪ {𝐵}) ∈ Hf )
Theorem	hfelhf 36162	Any member of an HF set is itself an HF set. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ Hf ) → 𝐴 ∈ Hf )
Theorem	hftr 36163	The class of all hereditarily finite sets is transitive. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ Tr Hf
Theorem	hfext 36164*	Extensionality for HF sets depends only on comparison of HF elements. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ ((𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ Hf (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)))
Theorem	hfuni 36165	The union of an HF set is itself hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ (𝐴 ∈ Hf → ∪ 𝐴 ∈ Hf )
Theorem	hfpw 36166	The power class of an HF set is hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ (𝐴 ∈ Hf → 𝒫 𝐴 ∈ Hf )
Theorem	hfninf 36167	ω is not hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ ¬ ω ∈ Hf
21.12  Mathbox for Gino Giotto
21.12.1  Equality theorems.
21.12.1.1  Inference versions.
Theorem	rmoeqi 36168	Equality inference for restricted at-most-one quantifier. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜓)
Theorem	rmoeqbii 36169	Equality inference for restricted at-most-one quantifier. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜒)
Theorem	reueqi 36170	Equality inference for restricted existential uniqueness quantifier. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐵 𝜓)
Theorem	reueqbii 36171	Equality inference for restricted existential uniqueness quantifier. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐵 𝜒)
Theorem	sbceqbii 36172	Formula-building inference for class substitution. General version of sbcbii 3851. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜓)
Theorem	disjeq1i 36173	Equality theorem for disjoint collection. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶)
Theorem	disjeq12i 36174	Equality theorem for disjoint collection. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐷)
Theorem	rabeqbii 36175	Equality theorem for restricted class abstractions. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜓}
Theorem	iuneq12i 36176	Equality theorem for indexed union. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷
Theorem	iineq1i 36177	Equality theorem for indexed intersection. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐶
Theorem	iineq12i 36178	Equality theorem for indexed intersection. Inference version. General version of iineq1i 36177. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐷
Theorem	riotaeqbii 36179	Equivalent wff's and equal domains yield equal restricted iotas. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜓)
Theorem	riotaeqi 36180	Equal domains yield equal restricted iotas. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜑)
Theorem	ixpeq1i 36181	Equality inference for infinite Cartesian product. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶
Theorem	ixpeq12i 36182	Equality inference for infinite Cartesian product. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐷
Theorem	sumeq2si 36183	Equality inference for sum. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶
Theorem	sumeq12si 36184	Equality inference for sum. General version of sumeq2si 36183. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ Σ𝑥 ∈ 𝐴 𝐶 = Σ𝑥 ∈ 𝐵 𝐷
Theorem	prodeq2si 36185	Equality inference for product. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶
Theorem	prodeq12si 36186	Equality inference for product. General version of prodeq2si 36185. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ∏𝑥 ∈ 𝐴 𝐶 = ∏𝑥 ∈ 𝐵 𝐷
Theorem	itgeq12i 36187	Equality inference for an integral. General version of itgeq1i 36188 and itgeq2i 36189. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑥
Theorem	itgeq1i 36188	Equality inference for an integral. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ∫𝐴𝐶 d𝑥 = ∫𝐵𝐶 d𝑥
Theorem	itgeq2i 36189	Equality inference for an integral. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑥
Theorem	ditgeq123i 36190	Equality inference for the directed integral. General version of ditgeq12i 36191 and ditgeq3i 36192. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    &   ⊢ 𝐸 = 𝐹    ⇒   ⊢ ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐹 d𝑥
Theorem	ditgeq12i 36191	Equality inference for the directed integral. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐸 d𝑥
Theorem	ditgeq3i 36192	Equality inference for the directed integral. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐶 = 𝐷    ⇒   ⊢ ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑥
21.12.1.2  Deduction versions.
Theorem	rmoeqdv 36193*	Formula-building rule for restricted at-most-one quantifier. Deduction form. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜓))
Theorem	rmoeqbidv 36194*	Formula-building rule for restricted at-most-one quantifier. Deduction form. General version of rmobidv 3394. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜒))
Theorem	reueqbidv 36195*	Formula-building rule for restricted existential uniqueness quantifier. Deduction form. General version of reubidv 3395. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐵 𝜒))
Theorem	sbequbidv 36196*	Deduction substituting both sides of a biconditional. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝑢 = 𝑣)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑢 / 𝑥]𝜓 ↔ [𝑣 / 𝑥]𝜒))
Theorem	disjeq12dv 36197*	Equality theorem for disjoint collection. Deduction version. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐷))
Theorem	ixpeq12dv 36198*	Equality theorem for infinite Cartesian product. Deduction version. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐷)
Theorem	sumeq12sdv 36199*	Equality deduction for sum. General version of sumeq2sdv 15735. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷)
Theorem	prodeq12sdv 36200*	Equality deduction for product. General version of prodeq2sdv 15955. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷)