Theorem List for Intuitionistic Logic Explorer - 5601-5700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | ffvelrni 5601 |
A function's value belongs to its codomain. (Contributed by NM,
6-Apr-2005.)
|
⊢ 𝐹:𝐴⟶𝐵 ⇒ ⊢ (𝐶 ∈ 𝐴 → (𝐹‘𝐶) ∈ 𝐵) |
|
Theorem | ffvelrnda 5602 |
A function's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵) |
|
Theorem | ffvelrnd 5603 |
A function's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
& ⊢ (𝜑 → 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐹‘𝐶) ∈ 𝐵) |
|
Theorem | rexrn 5604* |
Restricted existential quantification over the range of a function.
(Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario
Carneiro, 20-Aug-2014.)
|
⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐹 Fn 𝐴 → (∃𝑥 ∈ ran 𝐹𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)) |
|
Theorem | ralrn 5605* |
Restricted universal quantification over the range of a function.
(Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario
Carneiro, 20-Aug-2014.)
|
⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)) |
|
Theorem | elrnrexdm 5606* |
For any element in the range of a function there is an element in the
domain of the function for which the function value is the element of
the range. (Contributed by Alexander van der Vekens, 8-Dec-2017.)
|
⊢ (Fun 𝐹 → (𝑌 ∈ ran 𝐹 → ∃𝑥 ∈ dom 𝐹 𝑌 = (𝐹‘𝑥))) |
|
Theorem | elrnrexdmb 5607* |
For any element in the range of a function there is an element in the
domain of the function for which the function value is the element of
the range. (Contributed by Alexander van der Vekens, 17-Dec-2017.)
|
⊢ (Fun 𝐹 → (𝑌 ∈ ran 𝐹 ↔ ∃𝑥 ∈ dom 𝐹 𝑌 = (𝐹‘𝑥))) |
|
Theorem | eldmrexrn 5608* |
For any element in the domain of a function there is an element in the
range of the function which is the function value for the element of the
domain. (Contributed by Alexander van der Vekens, 8-Dec-2017.)
|
⊢ (Fun 𝐹 → (𝑌 ∈ dom 𝐹 → ∃𝑥 ∈ ran 𝐹 𝑥 = (𝐹‘𝑌))) |
|
Theorem | ralrnmpt 5609* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
& ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | rexrnmpt 5610* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
& ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∃𝑦 ∈ ran 𝐹𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | dff2 5611 |
Alternate definition of a mapping. (Contributed by NM, 14-Nov-2007.)
|
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ 𝐹 ⊆ (𝐴 × 𝐵))) |
|
Theorem | dff3im 5612* |
Property of a mapping. (Contributed by Jim Kingdon, 4-Jan-2019.)
|
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦)) |
|
Theorem | dff4im 5613* |
Property of a mapping. (Contributed by Jim Kingdon, 4-Jan-2019.)
|
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥𝐹𝑦)) |
|
Theorem | dffo3 5614* |
An onto mapping expressed in terms of function values. (Contributed by
NM, 29-Oct-2006.)
|
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) |
|
Theorem | dffo4 5615* |
Alternate definition of an onto mapping. (Contributed by NM,
20-Mar-2007.)
|
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑥𝐹𝑦)) |
|
Theorem | dffo5 5616* |
Alternate definition of an onto mapping. (Contributed by NM,
20-Mar-2007.)
|
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 𝑥𝐹𝑦)) |
|
Theorem | fmpt 5617* |
Functionality of the mapping operation. (Contributed by Mario Carneiro,
26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵) |
|
Theorem | f1ompt 5618* |
Express bijection for a mapping operation. (Contributed by Mario
Carneiro, 30-May-2015.) (Revised by Mario Carneiro, 4-Dec-2016.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) ⇒ ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶)) |
|
Theorem | fmpti 5619* |
Functionality of the mapping operation. (Contributed by NM,
19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)
& ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵) ⇒ ⊢ 𝐹:𝐴⟶𝐵 |
|
Theorem | fvmptelrn 5620* |
The value of a function at a point of its domain belongs to its
codomain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) |
|
Theorem | fmptd 5621* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by Mario Carneiro, 13-Jan-2013.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)
& ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) |
|
Theorem | fmpttd 5622* |
Version of fmptd 5621 with inlined definition. Domain and codomain
of the
mapping operation; deduction form. (Contributed by Glauco Siliprandi,
23-Oct-2021.) (Proof shortened by BJ, 16-Aug-2022.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶) |
|
Theorem | fmpt3d 5623* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by Thierry Arnoux, 4-Jun-2017.)
|
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) |
|
Theorem | fmptdf 5624* |
A version of fmptd 5621 using bound-variable hypothesis instead of a
distinct variable condition for 𝜑. (Contributed by Glauco
Siliprandi, 29-Jun-2017.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)
& ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) |
|
Theorem | ffnfv 5625* |
A function maps to a class to which all values belong. (Contributed by
NM, 3-Dec-2003.)
|
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
|
Theorem | ffnfvf 5626 |
A function maps to a class to which all values belong. This version of
ffnfv 5625 uses bound-variable hypotheses instead of
distinct variable
conditions. (Contributed by NM, 28-Sep-2006.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵
& ⊢ Ⅎ𝑥𝐹 ⇒ ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
|
Theorem | fnfvrnss 5627* |
An upper bound for range determined by function values. (Contributed by
NM, 8-Oct-2004.)
|
⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵) |
|
Theorem | rnmptss 5628* |
The range of an operation given by the maps-to notation as a subset.
(Contributed by Thierry Arnoux, 24-Sep-2017.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶) |
|
Theorem | fmpt2d 5629* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by NM, 27-Dec-2014.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)
& ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) |
|
Theorem | ffvresb 5630* |
A necessary and sufficient condition for a restricted function.
(Contributed by Mario Carneiro, 14-Nov-2013.)
|
⊢ (Fun 𝐹 → ((𝐹 ↾ 𝐴):𝐴⟶𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) ∈ 𝐵))) |
|
Theorem | resflem 5631* |
A lemma to bound the range of a restriction. The conclusion would also
hold with (𝑋 ∩ 𝑌) in place of 𝑌 (provided 𝑥 does
not
occur in 𝑋). If that stronger result is
needed, it is however
simpler to use the instance of resflem 5631 where (𝑋 ∩ 𝑌) is
substituted for 𝑌 (in both the conclusion and the
third hypothesis).
(Contributed by BJ, 4-Jul-2022.)
|
⊢ (𝜑 → 𝐹:𝑉⟶𝑋)
& ⊢ (𝜑 → 𝐴 ⊆ 𝑉)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝑌) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴⟶𝑌) |
|
Theorem | f1oresrab 5632* |
Build a bijection between restricted abstract builders, given a
bijection between the base classes, deduction version. (Contributed by
Thierry Arnoux, 17-Aug-2018.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)
& ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) → (𝜒 ↔ 𝜓)) ⇒ ⊢ (𝜑 → (𝐹 ↾ {𝑥 ∈ 𝐴 ∣ 𝜓}):{𝑥 ∈ 𝐴 ∣ 𝜓}–1-1-onto→{𝑦 ∈ 𝐵 ∣ 𝜒}) |
|
Theorem | fmptco 5633* |
Composition of two functions expressed as ordered-pair class
abstractions. If 𝐹 has the equation ( x + 2 ) and 𝐺 the
equation ( 3 * z ) then (𝐺 ∘ 𝐹) has the equation ( 3 * ( x +
2 ) ) . (Contributed by FL, 21-Jun-2012.) (Revised by Mario Carneiro,
24-Jul-2014.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ 𝐵)
& ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅)) & ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆)) & ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝑇)) |
|
Theorem | fmptcof 5634* |
Version of fmptco 5633 where 𝜑 needn't be distinct from 𝑥.
(Contributed by NM, 27-Dec-2014.)
|
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ 𝐵)
& ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅)) & ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆)) & ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝑇)) |
|
Theorem | fmptcos 5635* |
Composition of two functions expressed as mapping abstractions.
(Contributed by NM, 22-May-2006.) (Revised by Mario Carneiro,
31-Aug-2015.)
|
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ 𝐵)
& ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅)) & ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆)) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ ⦋𝑅 / 𝑦⦌𝑆)) |
|
Theorem | cofmpt 5636* |
Express composition of a maps-to function with another function in a
maps-to notation. (Contributed by Thierry Arnoux, 29-Jun-2017.)
|
⊢ (𝜑 → 𝐹:𝐶⟶𝐷)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵))) |
|
Theorem | fcompt 5637* |
Express composition of two functions as a maps-to applying both in
sequence. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Proof shortened
by Mario Carneiro, 27-Dec-2014.)
|
⊢ ((𝐴:𝐷⟶𝐸 ∧ 𝐵:𝐶⟶𝐷) → (𝐴 ∘ 𝐵) = (𝑥 ∈ 𝐶 ↦ (𝐴‘(𝐵‘𝑥)))) |
|
Theorem | fcoconst 5638 |
Composition with a constant function. (Contributed by Stefan O'Rear,
11-Mar-2015.)
|
⊢ ((𝐹 Fn 𝑋 ∧ 𝑌 ∈ 𝑋) → (𝐹 ∘ (𝐼 × {𝑌})) = (𝐼 × {(𝐹‘𝑌)})) |
|
Theorem | fsn 5639 |
A function maps a singleton to a singleton iff it is the singleton of an
ordered pair. (Contributed by NM, 10-Dec-2003.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐹:{𝐴}⟶{𝐵} ↔ 𝐹 = {〈𝐴, 𝐵〉}) |
|
Theorem | fsng 5640 |
A function maps a singleton to a singleton iff it is the singleton of an
ordered pair. (Contributed by NM, 26-Oct-2012.)
|
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐹:{𝐴}⟶{𝐵} ↔ 𝐹 = {〈𝐴, 𝐵〉})) |
|
Theorem | fsn2 5641 |
A function that maps a singleton to a class is the singleton of an
ordered pair. (Contributed by NM, 19-May-2004.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐹:{𝐴}⟶𝐵 ↔ ((𝐹‘𝐴) ∈ 𝐵 ∧ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉})) |
|
Theorem | xpsng 5642 |
The cross product of two singletons. (Contributed by Mario Carneiro,
30-Apr-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} × {𝐵}) = {〈𝐴, 𝐵〉}) |
|
Theorem | xpsn 5643 |
The cross product of two singletons. (Contributed by NM,
4-Nov-2006.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ({𝐴} × {𝐵}) = {〈𝐴, 𝐵〉} |
|
Theorem | dfmpt 5644 |
Alternate definition for the maps-to notation df-mpt 4027 (although it
requires that 𝐵 be a set). (Contributed by NM,
24-Aug-2010.)
(Revised by Mario Carneiro, 30-Dec-2016.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = ∪
𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉} |
|
Theorem | fnasrn 5645 |
A function expressed as the range of another function. (Contributed by
Mario Carneiro, 22-Jun-2013.) (Proof shortened by Mario Carneiro,
31-Aug-2015.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = ran (𝑥 ∈ 𝐴 ↦ 〈𝑥, 𝐵〉) |
|
Theorem | dfmptg 5646 |
Alternate definition for the maps-to notation df-mpt 4027 (which requires
that 𝐵 be a set). (Contributed by Jim
Kingdon, 9-Jan-2019.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) = ∪
𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉}) |
|
Theorem | fnasrng 5647 |
A function expressed as the range of another function. (Contributed by
Jim Kingdon, 9-Jan-2019.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) = ran (𝑥 ∈ 𝐴 ↦ 〈𝑥, 𝐵〉)) |
|
Theorem | ressnop0 5648 |
If 𝐴 is not in 𝐶, then the restriction of
a singleton of
〈𝐴, 𝐵〉 to 𝐶 is null. (Contributed
by Scott Fenton,
15-Apr-2011.)
|
⊢ (¬ 𝐴 ∈ 𝐶 → ({〈𝐴, 𝐵〉} ↾ 𝐶) = ∅) |
|
Theorem | fpr 5649 |
A function with a domain of two elements. (Contributed by Jeff Madsen,
20-Jun-2010.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈
V ⇒ ⊢ (𝐴 ≠ 𝐵 → {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}:{𝐴, 𝐵}⟶{𝐶, 𝐷}) |
|
Theorem | fprg 5650 |
A function with a domain of two elements. (Contributed by FL,
2-Feb-2014.)
|
⊢ (((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐹) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐻) ∧ 𝐴 ≠ 𝐵) → {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}:{𝐴, 𝐵}⟶{𝐶, 𝐷}) |
|
Theorem | ftpg 5651 |
A function with a domain of three elements. (Contributed by Alexander van
der Vekens, 4-Dec-2017.)
|
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉}:{𝑋, 𝑌, 𝑍}⟶{𝐴, 𝐵, 𝐶}) |
|
Theorem | ftp 5652 |
A function with a domain of three elements. (Contributed by Stefan
O'Rear, 17-Oct-2014.) (Proof shortened by Alexander van der Vekens,
23-Jan-2018.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝑋 ∈ V & ⊢ 𝑌 ∈ V & ⊢ 𝑍 ∈ V & ⊢ 𝐴 ≠ 𝐵
& ⊢ 𝐴 ≠ 𝐶
& ⊢ 𝐵 ≠ 𝐶 ⇒ ⊢ {〈𝐴, 𝑋〉, 〈𝐵, 𝑌〉, 〈𝐶, 𝑍〉}:{𝐴, 𝐵, 𝐶}⟶{𝑋, 𝑌, 𝑍} |
|
Theorem | fnressn 5653 |
A function restricted to a singleton. (Contributed by NM,
9-Oct-2004.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹 ↾ {𝐵}) = {〈𝐵, (𝐹‘𝐵)〉}) |
|
Theorem | fressnfv 5654 |
The value of a function restricted to a singleton. (Contributed by NM,
9-Oct-2004.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹 ↾ {𝐵}):{𝐵}⟶𝐶 ↔ (𝐹‘𝐵) ∈ 𝐶)) |
|
Theorem | fvconst 5655 |
The value of a constant function. (Contributed by NM, 30-May-1999.)
|
⊢ ((𝐹:𝐴⟶{𝐵} ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) = 𝐵) |
|
Theorem | fmptsn 5656* |
Express a singleton function in maps-to notation. (Contributed by NM,
6-Jun-2006.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Revised
by Stefan O'Rear, 28-Feb-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {〈𝐴, 𝐵〉} = (𝑥 ∈ {𝐴} ↦ 𝐵)) |
|
Theorem | fmptap 5657* |
Append an additional value to a function. (Contributed by NM,
6-Jun-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑅 ∪ {𝐴}) = 𝑆
& ⊢ (𝑥 = 𝐴 → 𝐶 = 𝐵) ⇒ ⊢ ((𝑥 ∈ 𝑅 ↦ 𝐶) ∪ {〈𝐴, 𝐵〉}) = (𝑥 ∈ 𝑆 ↦ 𝐶) |
|
Theorem | fmptapd 5658* |
Append an additional value to a function. (Contributed by Thierry
Arnoux, 3-Jan-2017.)
|
⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → (𝑅 ∪ {𝐴}) = 𝑆)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝑅 ↦ 𝐶) ∪ {〈𝐴, 𝐵〉}) = (𝑥 ∈ 𝑆 ↦ 𝐶)) |
|
Theorem | fmptpr 5659* |
Express a pair function in maps-to notation. (Contributed by Thierry
Arnoux, 3-Jan-2017.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝜑 → 𝐶 ∈ 𝑋)
& ⊢ (𝜑 → 𝐷 ∈ 𝑌)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐸 = 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐸 = 𝐷) ⇒ ⊢ (𝜑 → {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉} = (𝑥 ∈ {𝐴, 𝐵} ↦ 𝐸)) |
|
Theorem | fvresi 5660 |
The value of a restricted identity function. (Contributed by NM,
19-May-2004.)
|
⊢ (𝐵 ∈ 𝐴 → (( I ↾ 𝐴)‘𝐵) = 𝐵) |
|
Theorem | fvunsng 5661 |
Remove an ordered pair not participating in a function value.
(Contributed by Jim Kingdon, 7-Jan-2019.)
|
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷) → ((𝐴 ∪ {〈𝐵, 𝐶〉})‘𝐷) = (𝐴‘𝐷)) |
|
Theorem | fvsn 5662 |
The value of a singleton of an ordered pair is the second member.
(Contributed by NM, 12-Aug-1994.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ({〈𝐴, 𝐵〉}‘𝐴) = 𝐵 |
|
Theorem | fvsng 5663 |
The value of a singleton of an ordered pair is the second member.
(Contributed by NM, 26-Oct-2012.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({〈𝐴, 𝐵〉}‘𝐴) = 𝐵) |
|
Theorem | fvsnun1 5664 |
The value of a function with one of its ordered pairs replaced, at the
replaced ordered pair. See also fvsnun2 5665. (Contributed by NM,
23-Sep-2007.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐺 = ({〈𝐴, 𝐵〉} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) ⇒ ⊢ (𝐺‘𝐴) = 𝐵 |
|
Theorem | fvsnun2 5665 |
The value of a function with one of its ordered pairs replaced, at
arguments other than the replaced one. See also fvsnun1 5664.
(Contributed by NM, 23-Sep-2007.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐺 = ({〈𝐴, 𝐵〉} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) ⇒ ⊢ (𝐷 ∈ (𝐶 ∖ {𝐴}) → (𝐺‘𝐷) = (𝐹‘𝐷)) |
|
Theorem | fnsnsplitss 5666 |
Split a function into a single point and all the rest. (Contributed by
Stefan O'Rear, 27-Feb-2015.) (Revised by Jim Kingdon, 20-Jan-2023.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ↾ (𝐴 ∖ {𝑋})) ∪ {〈𝑋, (𝐹‘𝑋)〉}) ⊆ 𝐹) |
|
Theorem | fsnunf 5667 |
Adjoining a point to a function gives a function. (Contributed by Stefan
O'Rear, 28-Feb-2015.)
|
⊢ ((𝐹:𝑆⟶𝑇 ∧ (𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆) ∧ 𝑌 ∈ 𝑇) → (𝐹 ∪ {〈𝑋, 𝑌〉}):(𝑆 ∪ {𝑋})⟶𝑇) |
|
Theorem | fsnunfv 5668 |
Recover the added point from a point-added function. (Contributed by
Stefan O'Rear, 28-Feb-2015.) (Revised by NM, 18-May-2017.)
|
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ((𝐹 ∪ {〈𝑋, 𝑌〉})‘𝑋) = 𝑌) |
|
Theorem | fsnunres 5669 |
Recover the original function from a point-added function. (Contributed
by Stefan O'Rear, 28-Feb-2015.)
|
⊢ ((𝐹 Fn 𝑆 ∧ ¬ 𝑋 ∈ 𝑆) → ((𝐹 ∪ {〈𝑋, 𝑌〉}) ↾ 𝑆) = 𝐹) |
|
Theorem | funresdfunsnss 5670 |
Restricting a function to a domain without one element of the domain of
the function, and adding a pair of this element and the function value of
the element results in a subset of the function itself. (Contributed by
AV, 2-Dec-2018.) (Revised by Jim Kingdon, 21-Jan-2023.)
|
⊢ ((Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹) → ((𝐹 ↾ (V ∖ {𝑋})) ∪ {〈𝑋, (𝐹‘𝑋)〉}) ⊆ 𝐹) |
|
Theorem | fvpr1 5671 |
The value of a function with a domain of two elements. (Contributed by
Jeff Madsen, 20-Jun-2010.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐶 ∈
V ⇒ ⊢ (𝐴 ≠ 𝐵 → ({〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}‘𝐴) = 𝐶) |
|
Theorem | fvpr2 5672 |
The value of a function with a domain of two elements. (Contributed by
Jeff Madsen, 20-Jun-2010.)
|
⊢ 𝐵 ∈ V & ⊢ 𝐷 ∈
V ⇒ ⊢ (𝐴 ≠ 𝐵 → ({〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}‘𝐵) = 𝐷) |
|
Theorem | fvpr1g 5673 |
The value of a function with a domain of (at most) two elements.
(Contributed by Alexander van der Vekens, 3-Dec-2017.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}‘𝐴) = 𝐶) |
|
Theorem | fvpr2g 5674 |
The value of a function with a domain of (at most) two elements.
(Contributed by Alexander van der Vekens, 3-Dec-2017.)
|
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}‘𝐵) = 𝐷) |
|
Theorem | fvtp1g 5675 |
The value of a function with a domain of (at most) three elements.
(Contributed by Alexander van der Vekens, 4-Dec-2017.)
|
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶)) → ({〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}‘𝐴) = 𝐷) |
|
Theorem | fvtp2g 5676 |
The value of a function with a domain of (at most) three elements.
(Contributed by Alexander van der Vekens, 4-Dec-2017.)
|
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) → ({〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}‘𝐵) = 𝐸) |
|
Theorem | fvtp3g 5677 |
The value of a function with a domain of (at most) three elements.
(Contributed by Alexander van der Vekens, 4-Dec-2017.)
|
⊢ (((𝐶 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ({〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}‘𝐶) = 𝐹) |
|
Theorem | fvtp1 5678 |
The first value of a function with a domain of three elements.
(Contributed by NM, 14-Sep-2011.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐷 ∈
V ⇒ ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) → ({〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}‘𝐴) = 𝐷) |
|
Theorem | fvtp2 5679 |
The second value of a function with a domain of three elements.
(Contributed by NM, 14-Sep-2011.)
|
⊢ 𝐵 ∈ V & ⊢ 𝐸 ∈
V ⇒ ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) → ({〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}‘𝐵) = 𝐸) |
|
Theorem | fvtp3 5680 |
The third value of a function with a domain of three elements.
(Contributed by NM, 14-Sep-2011.)
|
⊢ 𝐶 ∈ V & ⊢ 𝐹 ∈
V ⇒ ⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({〈𝐴, 𝐷〉, 〈𝐵, 𝐸〉, 〈𝐶, 𝐹〉}‘𝐶) = 𝐹) |
|
Theorem | fvconst2g 5681 |
The value of a constant function. (Contributed by NM, 20-Aug-2005.)
|
⊢ ((𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵) |
|
Theorem | fconst2g 5682 |
A constant function expressed as a cross product. (Contributed by NM,
27-Nov-2007.)
|
⊢ (𝐵 ∈ 𝐶 → (𝐹:𝐴⟶{𝐵} ↔ 𝐹 = (𝐴 × {𝐵}))) |
|
Theorem | fvconst2 5683 |
The value of a constant function. (Contributed by NM, 16-Apr-2005.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐶 ∈ 𝐴 → ((𝐴 × {𝐵})‘𝐶) = 𝐵) |
|
Theorem | fconst2 5684 |
A constant function expressed as a cross product. (Contributed by NM,
20-Aug-1999.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹:𝐴⟶{𝐵} ↔ 𝐹 = (𝐴 × {𝐵})) |
|
Theorem | fconstfvm 5685* |
A constant function expressed in terms of its functionality, domain, and
value. See also fconst2 5684. (Contributed by Jim Kingdon,
8-Jan-2019.)
|
⊢ (∃𝑦 𝑦 ∈ 𝐴 → (𝐹:𝐴⟶{𝐵} ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))) |
|
Theorem | fconst3m 5686* |
Two ways to express a constant function. (Contributed by Jim Kingdon,
8-Jan-2019.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐴 → (𝐹:𝐴⟶{𝐵} ↔ (𝐹 Fn 𝐴 ∧ 𝐴 ⊆ (◡𝐹 “ {𝐵})))) |
|
Theorem | fconst4m 5687* |
Two ways to express a constant function. (Contributed by NM,
8-Mar-2007.)
|
⊢ (∃𝑥 𝑥 ∈ 𝐴 → (𝐹:𝐴⟶{𝐵} ↔ (𝐹 Fn 𝐴 ∧ (◡𝐹 “ {𝐵}) = 𝐴))) |
|
Theorem | resfunexg 5688 |
The restriction of a function to a set exists. Compare Proposition 6.17
of [TakeutiZaring] p. 28.
(Contributed by NM, 7-Apr-1995.) (Revised by
Mario Carneiro, 22-Jun-2013.)
|
⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) ∈ V) |
|
Theorem | fnex 5689 |
If the domain of a function is a set, the function is a set. Theorem
6.16(1) of [TakeutiZaring] p. 28.
This theorem is derived using the Axiom
of Replacement in the form of resfunexg 5688. (Contributed by NM,
14-Aug-1994.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵) → 𝐹 ∈ V) |
|
Theorem | funex 5690 |
If the domain of a function exists, so does the function. Part of Theorem
4.15(v) of [Monk1] p. 46. This theorem is
derived using the Axiom of
Replacement in the form of fnex 5689. (Note: Any resemblance between
F.U.N.E.X. and "Have You Any Eggs" is purely a coincidence
originated by
Swedish chefs.) (Contributed by NM, 11-Nov-1995.)
|
⊢ ((Fun 𝐹 ∧ dom 𝐹 ∈ 𝐵) → 𝐹 ∈ V) |
|
Theorem | opabex 5691* |
Existence of a function expressed as class of ordered pairs.
(Contributed by NM, 21-Jul-1996.)
|
⊢ 𝐴 ∈ V & ⊢ (𝑥 ∈ 𝐴 → ∃*𝑦𝜑) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∈ V |
|
Theorem | mptexg 5692* |
If the domain of a function given by maps-to notation is a set, the
function is a set. (Contributed by FL, 6-Jun-2011.) (Revised by Mario
Carneiro, 31-Aug-2015.)
|
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) |
|
Theorem | mptex 5693* |
If the domain of a function given by maps-to notation is a set, the
function is a set. (Contributed by NM, 22-Apr-2005.) (Revised by Mario
Carneiro, 20-Dec-2013.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V |
|
Theorem | mptexd 5694* |
If the domain of a function given by maps-to notation is a set, the
function is a set. Deduction version of mptexg 5692. (Contributed by
Glauco Siliprandi, 24-Dec-2020.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) |
|
Theorem | mptrabex 5695* |
If the domain of a function given by maps-to notation is a class
abstraction based on a set, the function is a set. (Contributed by AV,
16-Jul-2019.) (Revised by AV, 26-Mar-2021.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ↦ 𝐵) ∈ V |
|
Theorem | fex 5696 |
If the domain of a mapping is a set, the function is a set. (Contributed
by NM, 3-Oct-1999.)
|
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ V) |
|
Theorem | eufnfv 5697* |
A function is uniquely determined by its values. (Contributed by NM,
31-Aug-2011.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ∃!𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 𝐵) |
|
Theorem | funfvima 5698 |
A function's value in a preimage belongs to the image. (Contributed by
NM, 23-Sep-2003.)
|
⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴))) |
|
Theorem | funfvima2 5699 |
A function's value in an included preimage belongs to the image.
(Contributed by NM, 3-Feb-1997.)
|
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴))) |
|
Theorem | funfvima3 5700 |
A class including a function contains the function's value in the image
of the singleton of the argument. (Contributed by NM, 23-Mar-2004.)
|
⊢ ((Fun 𝐹 ∧ 𝐹 ⊆ 𝐺) → (𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) ∈ (𝐺 “ {𝐴}))) |