P. 454 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 45301-45400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	founiiun0 45301*	Union expressed as an indexed union, when a map onto is given. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝐹:𝐴–onto→(𝐵 ∪ {∅}) → ∪ 𝐵 = ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥))
Theorem	disjf1o 45302*	A bijection built from disjoint sets. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)    &   ⊢ 𝐶 = {𝑥 ∈ 𝐴 ∣ 𝐵 ≠ ∅}    &   ⊢ 𝐷 = (ran 𝐹 ∖ {∅})    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶–1-1-onto→𝐷)
Theorem	disjinfi 45303*	Only a finite number of disjoint sets can have a nonempty intersection with a finite set 𝐶. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)    &   ⊢ (𝜑 → 𝐶 ∈ Fin)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝐶) ≠ ∅} ∈ Fin)
Theorem	fvovco 45304	Value of the composition of an operator, with a given function. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝐹:𝑋⟶(𝑉 × 𝑊))    &   ⊢ (𝜑 → 𝑌 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ((𝑂 ∘ 𝐹)‘𝑌) = ((1st ‘(𝐹‘𝑌))𝑂(2nd ‘(𝐹‘𝑌))))
Theorem	ssnnf1octb 45305*	There exists a bijection between a subset of ℕ and a given nonempty countable set. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ ((𝐴 ≼ ω ∧ 𝐴 ≠ ∅) → ∃𝑓(dom 𝑓 ⊆ ℕ ∧ 𝑓:dom 𝑓–1-1-onto→𝐴))
Theorem	nnf1oxpnn 45306	There is a bijection between the set of positive integers and the Cartesian product of the set of positive integers with itself. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ ∃𝑓 𝑓:ℕ–1-1-onto→(ℕ × ℕ)
Theorem	rnmptssd 45307*	The range of a function given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → ran 𝐹 ⊆ 𝐶)
Theorem	projf1o 45308*	A biijection from a set to a projection in a two dimensional space. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ ⟨𝐴, 𝑥⟩)    ⇒   ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→({𝐴} × 𝐵))
Theorem	fvmap 45309	Function value for a member of a set exponentiation. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐴 ↑m 𝐵))    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹‘𝐶) ∈ 𝐴)
Theorem	fvixp2 45310*	Projection of a factor of an indexed Cartesian product. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ ((𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
Theorem	choicefi 45311*	For a finite set, a choice function exists, without using the axiom of choice. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ ∅)    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵))
Theorem	mpct 45312	The exponentiation of a countable set to a finite set is countable. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐴 ≼ ω)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    ⇒   ⊢ (𝜑 → (𝐴 ↑m 𝐵) ≼ ω)
Theorem	cnmetcoval 45313	Value of the distance function of the metric space of complex numbers, composed with a function. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ 𝐷 = (abs ∘ − )    &   ⊢ (𝜑 → 𝐹:𝐴⟶(ℂ × ℂ))    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((𝐷 ∘ 𝐹)‘𝐵) = (abs‘((1st ‘(𝐹‘𝐵)) − (2nd ‘(𝐹‘𝐵)))))
Theorem	fcomptss 45314*	Express composition of two functions as a maps-to applying both in sequence. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐶)    &   ⊢ (𝜑 → 𝐺:𝐶⟶𝐷)    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ (𝐺‘(𝐹‘𝑥))))
Theorem	elmapsnd 45315	Membership in a set exponentiated to a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐹 Fn {𝐴})    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝐹‘𝐴) ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑m {𝐴}))
Theorem	mapss2 45316	Subset inheritance for set exponentiation. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑍)    &   ⊢ (𝜑 → 𝐶 ≠ ∅)    ⇒   ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶)))
Theorem	fsneq 45317	Equality condition for two functions defined on a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ 𝐵 = {𝐴}    &   ⊢ (𝜑 → 𝐹 Fn 𝐵)    &   ⊢ (𝜑 → 𝐺 Fn 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 = 𝐺 ↔ (𝐹‘𝐴) = (𝐺‘𝐴)))
Theorem	difmap 45318	Difference of two sets exponentiations. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑍)    &   ⊢ (𝜑 → 𝐶 ≠ ∅)    ⇒   ⊢ (𝜑 → ((𝐴 ∖ 𝐵) ↑m 𝐶) ⊆ ((𝐴 ↑m 𝐶) ∖ (𝐵 ↑m 𝐶)))
Theorem	unirnmap 45319	Given a subset of a set exponentiation, the base set can be restricted. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ⊆ (𝐵 ↑m 𝐴))    ⇒   ⊢ (𝜑 → 𝑋 ⊆ (ran ∪ 𝑋 ↑m 𝐴))
Theorem	inmap 45320	Intersection of two sets exponentiations. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑍)    ⇒   ⊢ (𝜑 → ((𝐴 ↑m 𝐶) ∩ (𝐵 ↑m 𝐶)) = ((𝐴 ∩ 𝐵) ↑m 𝐶))
Theorem	fcoss 45321	Composition of two mappings. Similar to fco 6683, but with a weaker condition on the domain of 𝐹. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐺:𝐷⟶𝐶)    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝐺):𝐷⟶𝐵)
Theorem	fsneqrn 45322	Equality condition for two functions defined on a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ 𝐵 = {𝐴}    &   ⊢ (𝜑 → 𝐹 Fn 𝐵)    &   ⊢ (𝜑 → 𝐺 Fn 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 = 𝐺 ↔ (𝐹‘𝐴) ∈ ran 𝐺))
Theorem	difmapsn 45323	Difference of two sets exponentiatiated to a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑍)    ⇒   ⊢ (𝜑 → ((𝐴 ↑m {𝐶}) ∖ (𝐵 ↑m {𝐶})) = ((𝐴 ∖ 𝐵) ↑m {𝐶}))
Theorem	mapssbi 45324	Subset inheritance for set exponentiation. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑍)    &   ⊢ (𝜑 → 𝐶 ≠ ∅)    ⇒   ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶)))
Theorem	unirnmapsn 45325	Equality theorem for a subset of a set exponentiation, where the exponent is a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝐶 = {𝐴}    &   ⊢ (𝜑 → 𝑋 ⊆ (𝐵 ↑m 𝐶))    ⇒   ⊢ (𝜑 → 𝑋 = (ran ∪ 𝑋 ↑m 𝐶))
Theorem	iunmapss 45326*	The indexed union of set exponentiations is a subset of the set exponentiation of the indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 (𝐵 ↑m 𝐶) ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐶))
Theorem	ssmapsn 45327*	A subset 𝐶 of a set exponentiation to a singleton, is its projection 𝐷 exponentiated to the singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ Ⅎ𝑓𝐷    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ⊆ (𝐵 ↑m {𝐴}))    &   ⊢ 𝐷 = ∪ 𝑓 ∈ 𝐶 ran 𝑓    ⇒   ⊢ (𝜑 → 𝐶 = (𝐷 ↑m {𝐴}))
Theorem	iunmapsn 45328*	The indexed union of set exponentiations to a singleton is equal to the set exponentiation of the indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑍)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 (𝐵 ↑m {𝐶}) = (∪ 𝑥 ∈ 𝐴 𝐵 ↑m {𝐶}))
Theorem	absfico 45329	Mapping domain and codomain of the absolute value function. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ abs:ℂ⟶(0[,)+∞)
Theorem	icof 45330	The set of left-closed right-open intervals of extended reals maps to subsets of extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ [,):(ℝ* × ℝ*)⟶𝒫 ℝ*
Theorem	elpmrn 45331	The range of a partial function. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) → ran 𝐹 ⊆ 𝐴)
Theorem	imaexi 45332	The image of a set is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) (Proof shortened by SN, 27-Apr-2025.)
⊢ 𝐴 ∈ 𝑉    ⇒   ⊢ (𝐴 “ 𝐵) ∈ V
Theorem	axccdom 45333*	Relax the constraint on ax-cc to dominance instead of equinumerosity. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝑋 ≼ ω)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → 𝑧 ≠ ∅)    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝑋 ∧ ∀𝑧 ∈ 𝑋 (𝑓‘𝑧) ∈ 𝑧))
Theorem	dmmptdff 45334	The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ 𝐴 = (𝑥 ∈ 𝐵 ↦ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → dom 𝐴 = 𝐵)
Theorem	dmmptdf 45335*	The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐴 = (𝑥 ∈ 𝐵 ↦ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → dom 𝐴 = 𝐵)
Theorem	elpmi2 45336	The domain of a partial function. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) → dom 𝐹 ⊆ 𝐵)
Theorem	dmrelrnrel 45337*	A relation preserving function. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐹‘𝑥)𝑆(𝐹‘𝑦)))    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → (𝐹‘𝐵)𝑆(𝐹‘𝐶))
Theorem	fvcod 45338	Value of a function composition. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝐺)    &   ⊢ 𝐻 = (𝐹 ∘ 𝐺)    ⇒   ⊢ (𝜑 → (𝐻‘𝐴) = (𝐹‘(𝐺‘𝐴)))
Theorem	elrnmpoid 45339*	Membership in the range of an operation class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)    ⇒   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉) → (𝑥𝐹𝑦) ∈ ran 𝐹)
Theorem	axccd 45340*	An alternative version of the axiom of countable choice. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ≈ ω)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ≠ ∅)    ⇒   ⊢ (𝜑 → ∃𝑓∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝑥)
Theorem	axccd2 45341*	An alternative version of the axiom of countable choice. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
⊢ (𝜑 → 𝐴 ≼ ω)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ≠ ∅)    ⇒   ⊢ (𝜑 → ∃𝑓∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝑥)
Theorem	feqresmptf 45342*	Express a restricted function as a mapping. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
Theorem	dmmptssf 45343	The domain of a mapping is a subset of its base class. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝐴    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ dom 𝐹 ⊆ 𝐴
Theorem	dmmptdf2 45344	The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ 𝐴 = (𝑥 ∈ 𝐵 ↦ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → dom 𝐴 = 𝐵)
Theorem	dmuz 45345	Domain of the upper integers function. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ dom ℤ≥ = ℤ
Theorem	fmptd2f 45346*	Domain and codomain of the mapping operation; deduction form. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)
Theorem	mpteq1df 45347	An equality theorem for the maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) (Proof shortened by SN, 11-Nov-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	mptexf 45348	If the domain of a function given by maps-to notation is a set, the function is a set. Inference version of mptexg 7164. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝐴    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V
Theorem	fvmpt4 45349*	Value of a function given by the maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
Theorem	fmptf 45350*	Functionality of the mapping operation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝐵    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)
Theorem	resimass 45351	The image of a restriction is a subset of the original image. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ ((𝐴 ↾ 𝐵) “ 𝐶) ⊆ (𝐴 “ 𝐶)
Theorem	mptssid 45352	The mapping operation expressed with its actual domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝐴    &   ⊢ 𝐶 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐵)
Theorem	mptfnd 45353	The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013.) (Revised by Thierry Arnoux, 10-May-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴)
Theorem	rnmptlb 45354*	Boundness below of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧)
Theorem	rnmptbddlem 45355*	Boundness of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦)
Theorem	rnmptbdd 45356*	Boundness of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦)    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦)
Theorem	funimaeq 45357*	Membership relation for the values of a function whose image is a subclass. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → Fun 𝐺)    &   ⊢ (𝜑 → 𝐴 ⊆ dom 𝐹)    &   ⊢ (𝜑 → 𝐴 ⊆ dom 𝐺)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐺‘𝑥))    ⇒   ⊢ (𝜑 → (𝐹 “ 𝐴) = (𝐺 “ 𝐴))
Theorem	rnmptssf 45358*	The range of a function given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝐶    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶)
Theorem	rnmptbd2lem 45359*	Boundness below of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ↔ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧))
Theorem	rnmptbd2 45360*	Boundness below of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ↔ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦 ≤ 𝑧))
Theorem	infnsuprnmpt 45361*	The indexed infimum of real numbers is the negative of the indexed supremum of the negative values. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑦 ≤ 𝐵)    ⇒   ⊢ (𝜑 → inf(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ, < ) = -sup(ran (𝑥 ∈ 𝐴 ↦ -𝐵), ℝ, < ))
Theorem	suprclrnmpt 45362*	Closure of the indexed supremum of a nonempty bounded set of reals. Range of a function in maps-to notation can be used, to express an indexed supremum. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦)    ⇒   ⊢ (𝜑 → sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ, < ) ∈ ℝ)
Theorem	suprubrnmpt2 45363*	A member of a nonempty indexed set of reals is less than or equal to the set's upper bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐷 ∈ ℝ)    &   ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → 𝐷 ≤ sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ, < ))
Theorem	suprubrnmpt 45364*	A member of a nonempty indexed set of reals is less than or equal to the set's upper bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ sup(ran (𝑥 ∈ 𝐴 ↦ 𝐵), ℝ, < ))
Theorem	rnmptssdf 45365*	The range of a function given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → ran 𝐹 ⊆ 𝐶)
Theorem	rnmptbdlem 45366*	Boundness above of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦))
Theorem	rnmptbd 45367*	Boundness above of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ≤ 𝑦))
Theorem	rnmptss2 45368*	The range of a function given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ran (𝑥 ∈ 𝐴 ↦ 𝐶) ⊆ ran (𝑥 ∈ 𝐵 ↦ 𝐶))
Theorem	elmptima 45369*	The image of a function in maps-to notation. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ 𝐵) “ 𝐷) ↔ ∃𝑥 ∈ (𝐴 ∩ 𝐷)𝐶 = 𝐵))
Theorem	ralrnmpt3 45370*	A restricted quantifier over an image set. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))
Theorem	rnmptssbi 45371*	The range of a function given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (ran 𝐹 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶))
Theorem	imass2d 45372	Subset theorem for image. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 “ 𝐴) ⊆ (𝐶 “ 𝐵))
Theorem	imassmpt 45373*	Membership relation for the values of a function whose image is a subclass. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐶)) → 𝐵 ∈ 𝑉)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝜑 → ((𝐹 “ 𝐶) ⊆ 𝐷 ↔ ∀𝑥 ∈ (𝐴 ∩ 𝐶)𝐵 ∈ 𝐷))
Theorem	fpmd 45374	A total function is a partial function. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐶⟶𝐵)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑pm 𝐴))
Theorem	fconst7 45375*	An alternative way to express a constant function. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝐹 Fn 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)    ⇒   ⊢ (𝜑 → 𝐹 = (𝐴 × {𝐵}))
Theorem	fnmptif 45376	Functionality and domain of an ordered-pair class abstraction. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ 𝐹 Fn 𝐴
Theorem	dmmptif 45377	Domain of the mapping operation. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
⊢ Ⅎ𝑥𝐴    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ dom 𝐹 = 𝐴
Theorem	mpteq2dfa 45378	Slightly more general equality inference for the maps-to notation. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
Theorem	dmmpt1 45379	The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 5-Jan-2025.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉)    ⇒   ⊢ (𝜑 → dom (𝑥 ∈ 𝐵 ↦ 𝐶) = 𝐵)
Theorem	fmptff 45380	Functionality of the mapping operation. (Contributed by Glauco Siliprandi, 5-Jan-2025.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)
Theorem	fvmptelcdmf 45381	The value of a function at a point of its domain belongs to its codomain. (Contributed by Glauco Siliprandi, 5-Jan-2025.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)
Theorem	fmptdff 45382	A version of fmptd 7056 using bound-variable hypothesis instead of a distinct variable condition for 𝜑. (Contributed by Glauco Siliprandi, 5-Jan-2025.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)
Theorem	fvmpt2df 45383	Deduction version of fvmpt2 6949. (Contributed by Glauco Siliprandi, 24-Jan-2025.)
⊢ Ⅎ𝑥𝐴    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)
Theorem	rn1st 45384	The range of a function with a first-countable domain is itself first-countable. This is a variation of 1stcrestlem 23377, with a not-free hypothesis replacing a disjoint variable constraint. (Contributed by Glauco Siliprandi, 24-Jan-2025.)
⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐵 ≼ ω → ran (𝑥 ∈ 𝐵 ↦ 𝐶) ≼ ω)
Theorem	rnmptssff 45385	The range of a function given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 24-Jan-2025.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶)
Theorem	rnmptssdff 45386	The range of a function given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 24-Jan-2025.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)    ⇒   ⊢ (𝜑 → ran 𝐹 ⊆ 𝐶)
Theorem	fvmpt4d 45387	Value of a function given by the maps-to notation. (Contributed by Glauco Siliprandi, 15-Feb-2025.)
⊢ Ⅎ𝑥𝐴    &   ⊢ (𝜑 → 𝐵 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑥 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵)
21.43.3  Ordering on real numbers - Real and complex numbers basic operations
Theorem	sub2times 45388	Subtracting from a number, twice the number itself, gives negative the number. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ ℂ → (𝐴 − (2 · 𝐴)) = -𝐴)
Theorem	nnxrd 45389	A natural number is an extended real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ*)
Theorem	nnxr 45390	A natural number is an extended real. (Contributed by Glauco Siliprandi, 24-Jan-2025.)
⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ*)
Theorem	abssubrp 45391	The distance of two distinct complex number is a strictly positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐴 ≠ 𝐵) → (abs‘(𝐴 − 𝐵)) ∈ ℝ+)
Theorem	elfzfzo 45392	Relationship between membership in a half-open finite set of sequential integers and membership in a finite set of sequential intergers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ (𝑀..^𝑁) ↔ (𝐴 ∈ (𝑀...𝑁) ∧ 𝐴 < 𝑁))
Theorem	oddfl 45393	Odd number representation by using the floor function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 mod 2) ≠ 0) → 𝐾 = ((2 · (⌊‘(𝐾 / 2))) + 1))
Theorem	abscosbd 45394	Bound for the absolute value of the cosine of a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ ℝ → (abs‘(cos‘𝐴)) ≤ 1)
Theorem	mul13d 45395	Commutative/associative law that swaps the first and the third factor in a triple product. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · (𝐵 · 𝐶)) = (𝐶 · (𝐵 · 𝐴)))
Theorem	negpilt0 45396	Negative π is negative. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ -π < 0
Theorem	dstregt0 45397*	A complex number 𝐴 that is not real, has a distance from the reals that is strictly larger than 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ ℝ))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ ℝ 𝑥 < (abs‘(𝐴 − 𝑦)))
Theorem	subadd4b 45398	Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) + (𝐶 − 𝐷)) = ((𝐴 − 𝐷) + (𝐶 − 𝐵)))
Theorem	xrlttri5d 45399	Not equal and not larger implies smaller. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → ¬ 𝐵 < 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 < 𝐵)
Theorem	zltlesub 45400	If an integer 𝑁 is less than or equal to a real, and we subtract a quantity less than 1, then 𝑁 is less than or equal to the result. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 < 1)    &   ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℤ)    ⇒   ⊢ (𝜑 → 𝑁 ≤ (𝐴 − 𝐵))