Theorem List for Intuitionistic Logic Explorer - 5601-5700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | fndmdif 5601* |
Two ways to express the locus of differences between two functions.
(Contributed by Stefan O'Rear, 17-Jan-2015.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → dom (𝐹 ∖ 𝐺) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ (𝐺‘𝑥)}) |
|
Theorem | fndmdifcom 5602 |
The difference set between two functions is commutative. (Contributed
by Stefan O'Rear, 17-Jan-2015.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → dom (𝐹 ∖ 𝐺) = dom (𝐺 ∖ 𝐹)) |
|
Theorem | fndmin 5603* |
Two ways to express the locus of equality between two functions.
(Contributed by Stefan O'Rear, 17-Jan-2015.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → dom (𝐹 ∩ 𝐺) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = (𝐺‘𝑥)}) |
|
Theorem | fneqeql 5604 |
Two functions are equal iff their equalizer is the whole domain.
(Contributed by Stefan O'Rear, 7-Mar-2015.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ dom (𝐹 ∩ 𝐺) = 𝐴)) |
|
Theorem | fneqeql2 5605 |
Two functions are equal iff their equalizer contains the whole domain.
(Contributed by Stefan O'Rear, 9-Mar-2015.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ 𝐴 ⊆ dom (𝐹 ∩ 𝐺))) |
|
Theorem | fnreseql 5606 |
Two functions are equal on a subset iff their equalizer contains that
subset. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴) → ((𝐹 ↾ 𝑋) = (𝐺 ↾ 𝑋) ↔ 𝑋 ⊆ dom (𝐹 ∩ 𝐺))) |
|
Theorem | chfnrn 5607* |
The range of a choice function (a function that chooses an element from
each member of its domain) is included in the union of its domain.
(Contributed by NM, 31-Aug-1999.)
|
⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝑥) → ran 𝐹 ⊆ ∪ 𝐴) |
|
Theorem | funfvop 5608 |
Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1]
p. 41. (Contributed by NM, 14-Oct-1996.)
|
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → 〈𝐴, (𝐹‘𝐴)〉 ∈ 𝐹) |
|
Theorem | funfvbrb 5609 |
Two ways to say that 𝐴 is in the domain of 𝐹.
(Contributed by
Mario Carneiro, 1-May-2014.)
|
⊢ (Fun 𝐹 → (𝐴 ∈ dom 𝐹 ↔ 𝐴𝐹(𝐹‘𝐴))) |
|
Theorem | fvimacnvi 5610 |
A member of a preimage is a function value argument. (Contributed by NM,
4-May-2007.)
|
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ (◡𝐹 “ 𝐵)) → (𝐹‘𝐴) ∈ 𝐵) |
|
Theorem | fvimacnv 5611 |
The argument of a function value belongs to the preimage of any class
containing the function value. Raph Levien remarks: "This proof is
unsatisfying, because it seems to me that funimass2 5276 could probably be
strengthened to a biconditional." (Contributed by Raph Levien,
20-Nov-2006.)
|
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → ((𝐹‘𝐴) ∈ 𝐵 ↔ 𝐴 ∈ (◡𝐹 “ 𝐵))) |
|
Theorem | funimass3 5612 |
A kind of contraposition law that infers an image subclass from a
subclass of a preimage. Raph Levien remarks: "Likely this could
be
proved directly, and fvimacnv 5611 would be the special case of 𝐴 being
a singleton, but it works this way round too." (Contributed by
Raph
Levien, 20-Nov-2006.)
|
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → ((𝐹 “ 𝐴) ⊆ 𝐵 ↔ 𝐴 ⊆ (◡𝐹 “ 𝐵))) |
|
Theorem | funimass5 5613* |
A subclass of a preimage in terms of function values. (Contributed by
NM, 15-May-2007.)
|
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐴 ⊆ (◡𝐹 “ 𝐵) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
|
Theorem | funconstss 5614* |
Two ways of specifying that a function is constant on a subdomain.
(Contributed by NM, 8-Mar-2007.)
|
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 ↔ 𝐴 ⊆ (◡𝐹 “ {𝐵}))) |
|
Theorem | elpreima 5615 |
Membership in the preimage of a set under a function. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶))) |
|
Theorem | fniniseg 5616 |
Membership in the preimage of a singleton, under a function. (Contributed
by Mario Carneiro, 12-May-2014.) (Proof shortened by Mario Carneiro,
28-Apr-2015.)
|
⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵))) |
|
Theorem | fncnvima2 5617* |
Inverse images under functions expressed as abstractions. (Contributed
by Stefan O'Rear, 1-Feb-2015.)
|
⊢ (𝐹 Fn 𝐴 → (◡𝐹 “ 𝐵) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ∈ 𝐵}) |
|
Theorem | fniniseg2 5618* |
Inverse point images under functions expressed as abstractions.
(Contributed by Stefan O'Rear, 1-Feb-2015.)
|
⊢ (𝐹 Fn 𝐴 → (◡𝐹 “ {𝐵}) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = 𝐵}) |
|
Theorem | fnniniseg2 5619* |
Support sets of functions expressed as abstractions. (Contributed by
Stefan O'Rear, 1-Feb-2015.)
|
⊢ (𝐹 Fn 𝐴 → (◡𝐹 “ (V ∖ {𝐵})) = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ 𝐵}) |
|
Theorem | rexsupp 5620* |
Existential quantification restricted to a support. (Contributed by
Stefan O'Rear, 23-Mar-2015.)
|
⊢ (𝐹 Fn 𝐴 → (∃𝑥 ∈ (◡𝐹 “ (V ∖ {𝑍}))𝜑 ↔ ∃𝑥 ∈ 𝐴 ((𝐹‘𝑥) ≠ 𝑍 ∧ 𝜑))) |
|
Theorem | unpreima 5621 |
Preimage of a union. (Contributed by Jeff Madsen, 2-Sep-2009.)
|
⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∪ 𝐵)) = ((◡𝐹 “ 𝐴) ∪ (◡𝐹 “ 𝐵))) |
|
Theorem | inpreima 5622 |
Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009.)
(Proof shortened by Mario Carneiro, 14-Jun-2016.)
|
⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∩ 𝐵)) = ((◡𝐹 “ 𝐴) ∩ (◡𝐹 “ 𝐵))) |
|
Theorem | difpreima 5623 |
Preimage of a difference. (Contributed by Mario Carneiro,
14-Jun-2016.)
|
⊢ (Fun 𝐹 → (◡𝐹 “ (𝐴 ∖ 𝐵)) = ((◡𝐹 “ 𝐴) ∖ (◡𝐹 “ 𝐵))) |
|
Theorem | respreima 5624 |
The preimage of a restricted function. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
⊢ (Fun 𝐹 → (◡(𝐹 ↾ 𝐵) “ 𝐴) = ((◡𝐹 “ 𝐴) ∩ 𝐵)) |
|
Theorem | fimacnv 5625 |
The preimage of the codomain of a mapping is the mapping's domain.
(Contributed by FL, 25-Jan-2007.)
|
⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴) |
|
Theorem | fnopfv 5626 |
Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1]
p. 41. (Contributed by NM, 30-Sep-2004.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → 〈𝐵, (𝐹‘𝐵)〉 ∈ 𝐹) |
|
Theorem | fvelrn 5627 |
A function's value belongs to its range. (Contributed by NM,
14-Oct-1996.)
|
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ ran 𝐹) |
|
Theorem | fnfvelrn 5628 |
A function's value belongs to its range. (Contributed by NM,
15-Oct-1996.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹‘𝐵) ∈ ran 𝐹) |
|
Theorem | ffvelrn 5629 |
A function's value belongs to its codomain. (Contributed by NM,
12-Aug-1999.)
|
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵) |
|
Theorem | ffvelrni 5630 |
A function's value belongs to its codomain. (Contributed by NM,
6-Apr-2005.)
|
⊢ 𝐹:𝐴⟶𝐵 ⇒ ⊢ (𝐶 ∈ 𝐴 → (𝐹‘𝐶) ∈ 𝐵) |
|
Theorem | ffvelrnda 5631 |
A function's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵) |
|
Theorem | ffvelrnd 5632 |
A function's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
& ⊢ (𝜑 → 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐹‘𝐶) ∈ 𝐵) |
|
Theorem | rexrn 5633* |
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 5634* |
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 5635* |
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 5636* |
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 5637* |
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 5638* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
& ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | rexrnmpt 5639* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
& ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (∃𝑦 ∈ ran 𝐹𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) |
|
Theorem | dff2 5640 |
Alternate definition of a mapping. (Contributed by NM, 14-Nov-2007.)
|
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ 𝐹 ⊆ (𝐴 × 𝐵))) |
|
Theorem | dff3im 5641* |
Property of a mapping. (Contributed by Jim Kingdon, 4-Jan-2019.)
|
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦)) |
|
Theorem | dff4im 5642* |
Property of a mapping. (Contributed by Jim Kingdon, 4-Jan-2019.)
|
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥𝐹𝑦)) |
|
Theorem | dffo3 5643* |
An onto mapping expressed in terms of function values. (Contributed by
NM, 29-Oct-2006.)
|
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) |
|
Theorem | dffo4 5644* |
Alternate definition of an onto mapping. (Contributed by NM,
20-Mar-2007.)
|
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑥𝐹𝑦)) |
|
Theorem | dffo5 5645* |
Alternate definition of an onto mapping. (Contributed by NM,
20-Mar-2007.)
|
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 𝑥𝐹𝑦)) |
|
Theorem | fmpt 5646* |
Functionality of the mapping operation. (Contributed by Mario Carneiro,
26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵) |
|
Theorem | f1ompt 5647* |
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 5648* |
Functionality of the mapping operation. (Contributed by NM,
19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)
& ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵) ⇒ ⊢ 𝐹:𝐴⟶𝐵 |
|
Theorem | fvmptelrn 5649* |
The value of a function at a point of its domain belongs to its
codomain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) |
|
Theorem | fmptd 5650* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by Mario Carneiro, 13-Jan-2013.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)
& ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) |
|
Theorem | fmpttd 5651* |
Version of fmptd 5650 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 5652* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by Thierry Arnoux, 4-Jun-2017.)
|
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) |
|
Theorem | fmptdf 5653* |
A version of fmptd 5650 using bound-variable hypothesis instead of a
distinct variable condition for 𝜑. (Contributed by Glauco
Siliprandi, 29-Jun-2017.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)
& ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) |
|
Theorem | ffnfv 5654* |
A function maps to a class to which all values belong. (Contributed by
NM, 3-Dec-2003.)
|
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
|
Theorem | ffnfvf 5655 |
A function maps to a class to which all values belong. This version of
ffnfv 5654 uses bound-variable hypotheses instead of
distinct variable
conditions. (Contributed by NM, 28-Sep-2006.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵
& ⊢ Ⅎ𝑥𝐹 ⇒ ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
|
Theorem | fnfvrnss 5656* |
An upper bound for range determined by function values. (Contributed by
NM, 8-Oct-2004.)
|
⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵) |
|
Theorem | rnmptss 5657* |
The range of an operation given by the maps-to notation as a subset.
(Contributed by Thierry Arnoux, 24-Sep-2017.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶) |
|
Theorem | fmpt2d 5658* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by NM, 27-Dec-2014.)
|
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)
& ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) |
|
Theorem | ffvresb 5659* |
A necessary and sufficient condition for a restricted function.
(Contributed by Mario Carneiro, 14-Nov-2013.)
|
⊢ (Fun 𝐹 → ((𝐹 ↾ 𝐴):𝐴⟶𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) ∈ 𝐵))) |
|
Theorem | resflem 5660* |
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 5660 where (𝑋 ∩ 𝑌) is
substituted for 𝑌 (in both the conclusion and the
third hypothesis).
(Contributed by BJ, 4-Jul-2022.)
|
⊢ (𝜑 → 𝐹:𝑉⟶𝑋)
& ⊢ (𝜑 → 𝐴 ⊆ 𝑉)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝑌) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴⟶𝑌) |
|
Theorem | f1oresrab 5661* |
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 5662* |
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 5663* |
Version of fmptco 5662 where 𝜑 needn't be distinct from 𝑥.
(Contributed by NM, 27-Dec-2014.)
|
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ 𝐵)
& ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅)) & ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆)) & ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝑇)) |
|
Theorem | fmptcos 5664* |
Composition of two functions expressed as mapping abstractions.
(Contributed by NM, 22-May-2006.) (Revised by Mario Carneiro,
31-Aug-2015.)
|
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ 𝐵)
& ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅)) & ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆)) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ ⦋𝑅 / 𝑦⦌𝑆)) |
|
Theorem | cofmpt 5665* |
Express composition of a maps-to function with another function in a
maps-to notation. (Contributed by Thierry Arnoux, 29-Jun-2017.)
|
⊢ (𝜑 → 𝐹:𝐶⟶𝐷)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵))) |
|
Theorem | fcompt 5666* |
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 5667 |
Composition with a constant function. (Contributed by Stefan O'Rear,
11-Mar-2015.)
|
⊢ ((𝐹 Fn 𝑋 ∧ 𝑌 ∈ 𝑋) → (𝐹 ∘ (𝐼 × {𝑌})) = (𝐼 × {(𝐹‘𝑌)})) |
|
Theorem | fsn 5668 |
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 5669 |
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 5670 |
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 5671 |
The cross product of two singletons. (Contributed by Mario Carneiro,
30-Apr-2015.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} × {𝐵}) = {〈𝐴, 𝐵〉}) |
|
Theorem | xpsn 5672 |
The cross product of two singletons. (Contributed by NM,
4-Nov-2006.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ({𝐴} × {𝐵}) = {〈𝐴, 𝐵〉} |
|
Theorem | dfmpt 5673 |
Alternate definition for the maps-to notation df-mpt 4052 (although it
requires that 𝐵 be a set). (Contributed by NM,
24-Aug-2010.)
(Revised by Mario Carneiro, 30-Dec-2016.)
|
⊢ 𝐵 ∈ V ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = ∪
𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉} |
|
Theorem | fnasrn 5674 |
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 5675 |
Alternate definition for the maps-to notation df-mpt 4052 (which requires
that 𝐵 be a set). (Contributed by Jim
Kingdon, 9-Jan-2019.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) = ∪
𝑥 ∈ 𝐴 {〈𝑥, 𝐵〉}) |
|
Theorem | fnasrng 5676 |
A function expressed as the range of another function. (Contributed by
Jim Kingdon, 9-Jan-2019.)
|
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) = ran (𝑥 ∈ 𝐴 ↦ 〈𝑥, 𝐵〉)) |
|
Theorem | ressnop0 5677 |
If 𝐴 is not in 𝐶, then the restriction of
a singleton of
〈𝐴, 𝐵〉 to 𝐶 is null. (Contributed
by Scott Fenton,
15-Apr-2011.)
|
⊢ (¬ 𝐴 ∈ 𝐶 → ({〈𝐴, 𝐵〉} ↾ 𝐶) = ∅) |
|
Theorem | fpr 5678 |
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 5679 |
A function with a domain of two elements. (Contributed by FL,
2-Feb-2014.)
|
⊢ (((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐹) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐻) ∧ 𝐴 ≠ 𝐵) → {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}:{𝐴, 𝐵}⟶{𝐶, 𝐷}) |
|
Theorem | ftpg 5680 |
A function with a domain of three elements. (Contributed by Alexander van
der Vekens, 4-Dec-2017.)
|
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉}:{𝑋, 𝑌, 𝑍}⟶{𝐴, 𝐵, 𝐶}) |
|
Theorem | ftp 5681 |
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 5682 |
A function restricted to a singleton. (Contributed by NM,
9-Oct-2004.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹 ↾ {𝐵}) = {〈𝐵, (𝐹‘𝐵)〉}) |
|
Theorem | fressnfv 5683 |
The value of a function restricted to a singleton. (Contributed by NM,
9-Oct-2004.)
|
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹 ↾ {𝐵}):{𝐵}⟶𝐶 ↔ (𝐹‘𝐵) ∈ 𝐶)) |
|
Theorem | fvconst 5684 |
The value of a constant function. (Contributed by NM, 30-May-1999.)
|
⊢ ((𝐹:𝐴⟶{𝐵} ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) = 𝐵) |
|
Theorem | fmptsn 5685* |
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 5686* |
Append an additional value to a function. (Contributed by NM,
6-Jun-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑅 ∪ {𝐴}) = 𝑆
& ⊢ (𝑥 = 𝐴 → 𝐶 = 𝐵) ⇒ ⊢ ((𝑥 ∈ 𝑅 ↦ 𝐶) ∪ {〈𝐴, 𝐵〉}) = (𝑥 ∈ 𝑆 ↦ 𝐶) |
|
Theorem | fmptapd 5687* |
Append an additional value to a function. (Contributed by Thierry
Arnoux, 3-Jan-2017.)
|
⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → (𝑅 ∪ {𝐴}) = 𝑆)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝑅 ↦ 𝐶) ∪ {〈𝐴, 𝐵〉}) = (𝑥 ∈ 𝑆 ↦ 𝐶)) |
|
Theorem | fmptpr 5688* |
Express a pair function in maps-to notation. (Contributed by Thierry
Arnoux, 3-Jan-2017.)
|
⊢ (𝜑 → 𝐴 ∈ 𝑉)
& ⊢ (𝜑 → 𝐵 ∈ 𝑊)
& ⊢ (𝜑 → 𝐶 ∈ 𝑋)
& ⊢ (𝜑 → 𝐷 ∈ 𝑌)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐸 = 𝐶)
& ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐸 = 𝐷) ⇒ ⊢ (𝜑 → {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉} = (𝑥 ∈ {𝐴, 𝐵} ↦ 𝐸)) |
|
Theorem | fvresi 5689 |
The value of a restricted identity function. (Contributed by NM,
19-May-2004.)
|
⊢ (𝐵 ∈ 𝐴 → (( I ↾ 𝐴)‘𝐵) = 𝐵) |
|
Theorem | fvunsng 5690 |
Remove an ordered pair not participating in a function value.
(Contributed by Jim Kingdon, 7-Jan-2019.)
|
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷) → ((𝐴 ∪ {〈𝐵, 𝐶〉})‘𝐷) = (𝐴‘𝐷)) |
|
Theorem | fvsn 5691 |
The value of a singleton of an ordered pair is the second member.
(Contributed by NM, 12-Aug-1994.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ ({〈𝐴, 𝐵〉}‘𝐴) = 𝐵 |
|
Theorem | fvsng 5692 |
The value of a singleton of an ordered pair is the second member.
(Contributed by NM, 26-Oct-2012.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({〈𝐴, 𝐵〉}‘𝐴) = 𝐵) |
|
Theorem | fvsnun1 5693 |
The value of a function with one of its ordered pairs replaced, at the
replaced ordered pair. See also fvsnun2 5694. (Contributed by NM,
23-Sep-2007.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐺 = ({〈𝐴, 𝐵〉} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) ⇒ ⊢ (𝐺‘𝐴) = 𝐵 |
|
Theorem | fvsnun2 5694 |
The value of a function with one of its ordered pairs replaced, at
arguments other than the replaced one. See also fvsnun1 5693.
(Contributed by NM, 23-Sep-2007.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐺 = ({〈𝐴, 𝐵〉} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) ⇒ ⊢ (𝐷 ∈ (𝐶 ∖ {𝐴}) → (𝐺‘𝐷) = (𝐹‘𝐷)) |
|
Theorem | fnsnsplitss 5695 |
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 5696 |
Adjoining a point to a function gives a function. (Contributed by Stefan
O'Rear, 28-Feb-2015.)
|
⊢ ((𝐹:𝑆⟶𝑇 ∧ (𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆) ∧ 𝑌 ∈ 𝑇) → (𝐹 ∪ {〈𝑋, 𝑌〉}):(𝑆 ∪ {𝑋})⟶𝑇) |
|
Theorem | fsnunfv 5697 |
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 5698 |
Recover the original function from a point-added function. (Contributed
by Stefan O'Rear, 28-Feb-2015.)
|
⊢ ((𝐹 Fn 𝑆 ∧ ¬ 𝑋 ∈ 𝑆) → ((𝐹 ∪ {〈𝑋, 𝑌〉}) ↾ 𝑆) = 𝐹) |
|
Theorem | funresdfunsnss 5699 |
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 5700 |
The value of a function with a domain of two elements. (Contributed by
Jeff Madsen, 20-Jun-2010.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐶 ∈
V ⇒ ⊢ (𝐴 ≠ 𝐵 → ({〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉}‘𝐴) = 𝐶) |