Theorem List for Intuitionistic Logic Explorer - 5201-5300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | fvmptdf 5201* |
Alternate deduction version of fvmpt 5192, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
⊢ (φ
→ A ∈ 𝐷)
& ⊢ ((φ
∧ x =
A) → B ∈ 𝑉) & ⊢ ((φ ∧
x = A)
→ ((𝐹‘A) = B →
ψ)) & ⊢
Ⅎx𝐹
& ⊢ Ⅎxψ ⇒ ⊢ (φ → (𝐹 = (x
∈ 𝐷 ↦ B) → ψ)) |
|
Theorem | fvmptdv 5202* |
Alternate deduction version of fvmpt 5192, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
⊢ (φ
→ A ∈ 𝐷)
& ⊢ ((φ
∧ x =
A) → B ∈ 𝑉) & ⊢ ((φ ∧
x = A)
→ ((𝐹‘A) = B →
ψ)) ⇒ ⊢ (φ → (𝐹 = (x
∈ 𝐷 ↦ B) → ψ)) |
|
Theorem | fvmptdv2 5203* |
Alternate deduction version of fvmpt 5192, suitable for iteration.
(Contributed by Mario Carneiro, 7-Jan-2017.)
|
⊢ (φ
→ A ∈ 𝐷)
& ⊢ ((φ
∧ x =
A) → B ∈ 𝑉) & ⊢ ((φ ∧
x = A)
→ B = 𝐶) ⇒ ⊢ (φ → (𝐹 = (x
∈ 𝐷 ↦ B) → (𝐹‘A) = 𝐶)) |
|
Theorem | mpteqb 5204* |
Bidirectional equality theorem for a mapping abstraction. Equivalent to
eqfnfv 5208. (Contributed by Mario Carneiro,
14-Nov-2014.)
|
⊢ (∀x ∈ A B ∈ 𝑉 → ((x ∈ A ↦ B) =
(x ∈
A ↦ 𝐶) ↔ ∀x ∈ A B = 𝐶)) |
|
Theorem | fvmptt 5205* |
Closed theorem form of fvmpt 5192. (Contributed by Scott Fenton,
21-Feb-2013.) (Revised by Mario Carneiro, 11-Sep-2015.)
|
⊢ ((∀x(x = A → B =
𝐶) ∧ 𝐹 = (x
∈ 𝐷 ↦ B) ∧ (A ∈ 𝐷 ∧ 𝐶 ∈ 𝑉)) → (𝐹‘A) = 𝐶) |
|
Theorem | fvmptf 5206* |
Value of a function given by an ordered-pair class abstraction. This
version of fvmptg 5191 uses bound-variable hypotheses instead of
distinct
variable conditions. (Contributed by NM, 8-Nov-2005.) (Revised by
Mario Carneiro, 15-Oct-2016.)
|
⊢ ℲxA & ⊢
Ⅎx𝐶
& ⊢ (x =
A → B = 𝐶)
& ⊢ 𝐹 = (x
∈ 𝐷 ↦ B) ⇒ ⊢ ((A ∈ 𝐷 ∧ 𝐶 ∈ 𝑉) → (𝐹‘A) = 𝐶) |
|
Theorem | fvopab6 5207* |
Value of a function given by ordered-pair class abstraction.
(Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro,
11-Sep-2015.)
|
⊢ 𝐹 = {〈x, y〉
∣ (φ ∧ y = B)}
& ⊢ (x =
A → (φ ↔ ψ)) & ⊢ (x = A →
B = 𝐶) ⇒ ⊢ ((A ∈ 𝐷 ∧ 𝐶 ∈ 𝑅 ∧ ψ) →
(𝐹‘A) = 𝐶) |
|
Theorem | eqfnfv 5208* |
Equality of functions is determined by their values. Special case of
Exercise 4 of [TakeutiZaring] p.
28 (with domain equality omitted).
(Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew Salmon,
22-Oct-2011.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
|
⊢ ((𝐹 Fn A
∧ 𝐺 Fn A)
→ (𝐹 = 𝐺 ↔ ∀x ∈ A (𝐹‘x) = (𝐺‘x))) |
|
Theorem | eqfnfv2 5209* |
Equality of functions is determined by their values. Exercise 4 of
[TakeutiZaring] p. 28.
(Contributed by NM, 3-Aug-1994.) (Revised by
Mario Carneiro, 31-Aug-2015.)
|
⊢ ((𝐹 Fn A
∧ 𝐺 Fn B)
→ (𝐹 = 𝐺 ↔ (A = B ∧ ∀x ∈ A (𝐹‘x) = (𝐺‘x)))) |
|
Theorem | eqfnfv3 5210* |
Derive equality of functions from equality of their values.
(Contributed by Jeff Madsen, 2-Sep-2009.)
|
⊢ ((𝐹 Fn A
∧ 𝐺 Fn B)
→ (𝐹 = 𝐺 ↔ (B ⊆ A
∧ ∀x ∈ A (x ∈ B ∧ (𝐹‘x) = (𝐺‘x))))) |
|
Theorem | eqfnfvd 5211* |
Deduction for equality of functions. (Contributed by Mario Carneiro,
24-Jul-2014.)
|
⊢ (φ
→ 𝐹 Fn A)
& ⊢ (φ
→ 𝐺 Fn A)
& ⊢ ((φ
∧ x ∈ A) →
(𝐹‘x) = (𝐺‘x)) ⇒ ⊢ (φ → 𝐹 = 𝐺) |
|
Theorem | eqfnfv2f 5212* |
Equality of functions is determined by their values. Special case of
Exercise 4 of [TakeutiZaring] p.
28 (with domain equality omitted).
This version of eqfnfv 5208 uses bound-variable hypotheses instead of
distinct variable conditions. (Contributed by NM, 29-Jan-2004.)
|
⊢ Ⅎx𝐹
& ⊢ Ⅎx𝐺 ⇒ ⊢ ((𝐹 Fn A
∧ 𝐺 Fn A)
→ (𝐹 = 𝐺 ↔ ∀x ∈ A (𝐹‘x) = (𝐺‘x))) |
|
Theorem | eqfunfv 5213* |
Equality of functions is determined by their values. (Contributed by
Scott Fenton, 19-Jun-2011.)
|
⊢ ((Fun 𝐹 ∧ Fun
𝐺) → (𝐹 = 𝐺 ↔ (dom 𝐹 = dom 𝐺 ∧ ∀x ∈ dom 𝐹(𝐹‘x) = (𝐺‘x)))) |
|
Theorem | fvreseq 5214* |
Equality of restricted functions is determined by their values.
(Contributed by NM, 3-Aug-1994.)
|
⊢ (((𝐹 Fn A
∧ 𝐺 Fn A)
∧ B
⊆ A) → ((𝐹 ↾ B) = (𝐺 ↾ B) ↔ ∀x ∈ B (𝐹‘x) = (𝐺‘x))) |
|
Theorem | fndmdif 5215* |
Two ways to express the locus of differences between two functions.
(Contributed by Stefan O'Rear, 17-Jan-2015.)
|
⊢ ((𝐹 Fn A
∧ 𝐺 Fn A)
→ dom (𝐹 ∖
𝐺) = {x ∈ A ∣ (𝐹‘x) ≠ (𝐺‘x)}) |
|
Theorem | fndmdifcom 5216 |
The difference set between two functions is commutative. (Contributed
by Stefan O'Rear, 17-Jan-2015.)
|
⊢ ((𝐹 Fn A
∧ 𝐺 Fn A)
→ dom (𝐹 ∖
𝐺) = dom (𝐺 ∖ 𝐹)) |
|
Theorem | fndmin 5217* |
Two ways to express the locus of equality between two functions.
(Contributed by Stefan O'Rear, 17-Jan-2015.)
|
⊢ ((𝐹 Fn A
∧ 𝐺 Fn A)
→ dom (𝐹 ∩ 𝐺) = {x ∈ A ∣ (𝐹‘x) = (𝐺‘x)}) |
|
Theorem | fneqeql 5218 |
Two functions are equal iff their equalizer is the whole domain.
(Contributed by Stefan O'Rear, 7-Mar-2015.)
|
⊢ ((𝐹 Fn A
∧ 𝐺 Fn A)
→ (𝐹 = 𝐺 ↔ dom (𝐹 ∩ 𝐺) = A)) |
|
Theorem | fneqeql2 5219 |
Two functions are equal iff their equalizer contains the whole domain.
(Contributed by Stefan O'Rear, 9-Mar-2015.)
|
⊢ ((𝐹 Fn A
∧ 𝐺 Fn A)
→ (𝐹 = 𝐺 ↔ A ⊆ dom (𝐹 ∩ 𝐺))) |
|
Theorem | fnreseql 5220 |
Two functions are equal on a subset iff their equalizer contains that
subset. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|
⊢ ((𝐹 Fn A
∧ 𝐺 Fn A
∧ 𝑋 ⊆ A) → ((𝐹 ↾ 𝑋) = (𝐺 ↾ 𝑋) ↔ 𝑋 ⊆ dom (𝐹 ∩ 𝐺))) |
|
Theorem | chfnrn 5221* |
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 A
∧ ∀x ∈ A (𝐹‘x) ∈ x) → ran 𝐹 ⊆ ∪
A) |
|
Theorem | funfvop 5222 |
Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1]
p. 41. (Contributed by NM, 14-Oct-1996.)
|
⊢ ((Fun 𝐹 ∧
A ∈ dom
𝐹) → 〈A, (𝐹‘A)〉 ∈ 𝐹) |
|
Theorem | funfvbrb 5223 |
Two ways to say that A is in the domain of 𝐹. (Contributed by
Mario Carneiro, 1-May-2014.)
|
⊢ (Fun 𝐹 → (A ∈ dom 𝐹 ↔ A𝐹(𝐹‘A))) |
|
Theorem | fvimacnvi 5224 |
A member of a preimage is a function value argument. (Contributed by NM,
4-May-2007.)
|
⊢ ((Fun 𝐹 ∧
A ∈
(◡𝐹 “ B)) → (𝐹‘A) ∈ B) |
|
Theorem | fvimacnv 5225 |
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 4920 could probably be
strengthened to a biconditional." (Contributed by Raph Levien,
20-Nov-2006.)
|
⊢ ((Fun 𝐹 ∧
A ∈ dom
𝐹) → ((𝐹‘A) ∈ B ↔ A
∈ (◡𝐹 “ B))) |
|
Theorem | funimass3 5226 |
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 5225 would be the special case of A being
a singleton, but it works this way round too." (Contributed by
Raph
Levien, 20-Nov-2006.)
|
⊢ ((Fun 𝐹 ∧
A ⊆ dom 𝐹) → ((𝐹 “ A) ⊆ B
↔ A ⊆ (◡𝐹 “ B))) |
|
Theorem | funimass5 5227* |
A subclass of a preimage in terms of function values. (Contributed by
NM, 15-May-2007.)
|
⊢ ((Fun 𝐹 ∧
A ⊆ dom 𝐹) → (A ⊆ (◡𝐹 “ B) ↔ ∀x ∈ A (𝐹‘x) ∈ B)) |
|
Theorem | funconstss 5228* |
Two ways of specifying that a function is constant on a subdomain.
(Contributed by NM, 8-Mar-2007.)
|
⊢ ((Fun 𝐹 ∧
A ⊆ dom 𝐹) → (∀x ∈ A (𝐹‘x) = B ↔
A ⊆ (◡𝐹 “ {B}))) |
|
Theorem | elpreima 5229 |
Membership in the preimage of a set under a function. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
⊢ (𝐹 Fn A
→ (B ∈ (◡𝐹 “ 𝐶) ↔ (B ∈ A ∧ (𝐹‘B) ∈ 𝐶))) |
|
Theorem | fniniseg 5230 |
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 A
→ (𝐶 ∈ (◡𝐹 “ {B}) ↔ (𝐶 ∈
A ∧
(𝐹‘𝐶) = B))) |
|
Theorem | fncnvima2 5231* |
Inverse images under functions expressed as abstractions. (Contributed
by Stefan O'Rear, 1-Feb-2015.)
|
⊢ (𝐹 Fn A
→ (◡𝐹 “ B) = {x ∈ A ∣
(𝐹‘x) ∈ B}) |
|
Theorem | fniniseg2 5232* |
Inverse point images under functions expressed as abstractions.
(Contributed by Stefan O'Rear, 1-Feb-2015.)
|
⊢ (𝐹 Fn A
→ (◡𝐹 “ {B}) = {x ∈ A ∣
(𝐹‘x) = B}) |
|
Theorem | fnniniseg2 5233* |
Support sets of functions expressed as abstractions. (Contributed by
Stefan O'Rear, 1-Feb-2015.)
|
⊢ (𝐹 Fn A
→ (◡𝐹 “ (V ∖ {B})) = {x ∈ A ∣
(𝐹‘x) ≠ B}) |
|
Theorem | rexsupp 5234* |
Existential quantification restricted to a support. (Contributed by
Stefan O'Rear, 23-Mar-2015.)
|
⊢ (𝐹 Fn A
→ (∃x ∈ (◡𝐹 “ (V ∖ {𝑍}))φ ↔ ∃x ∈ A ((𝐹‘x) ≠ 𝑍 ∧ φ))) |
|
Theorem | unpreima 5235 |
Preimage of a union. (Contributed by Jeff Madsen, 2-Sep-2009.)
|
⊢ (Fun 𝐹 → (◡𝐹 “ (A ∪ B)) =
((◡𝐹 “ A) ∪ (◡𝐹 “ B))) |
|
Theorem | inpreima 5236 |
Preimage of an intersection. (Contributed by Jeff Madsen, 2-Sep-2009.)
(Proof shortened by Mario Carneiro, 14-Jun-2016.)
|
⊢ (Fun 𝐹 → (◡𝐹 “ (A ∩ B)) =
((◡𝐹 “ A) ∩ (◡𝐹 “ B))) |
|
Theorem | difpreima 5237 |
Preimage of a difference. (Contributed by Mario Carneiro,
14-Jun-2016.)
|
⊢ (Fun 𝐹 → (◡𝐹 “ (A ∖ B)) =
((◡𝐹 “ A) ∖ (◡𝐹 “ B))) |
|
Theorem | respreima 5238 |
The preimage of a restricted function. (Contributed by Jeff Madsen,
2-Sep-2009.)
|
⊢ (Fun 𝐹 → (◡(𝐹 ↾ B) “ A) =
((◡𝐹 “ A) ∩ B)) |
|
Theorem | fimacnv 5239 |
The preimage of the codomain of a mapping is the mapping's domain.
(Contributed by FL, 25-Jan-2007.)
|
⊢ (𝐹:A⟶B
→ (◡𝐹 “ B) = A) |
|
Theorem | fnopfv 5240 |
Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1]
p. 41. (Contributed by NM, 30-Sep-2004.)
|
⊢ ((𝐹 Fn A
∧ B ∈ A) →
〈B, (𝐹‘B)〉 ∈ 𝐹) |
|
Theorem | fvelrn 5241 |
A function's value belongs to its range. (Contributed by NM,
14-Oct-1996.)
|
⊢ ((Fun 𝐹 ∧
A ∈ dom
𝐹) → (𝐹‘A) ∈ ran 𝐹) |
|
Theorem | fnfvelrn 5242 |
A function's value belongs to its range. (Contributed by NM,
15-Oct-1996.)
|
⊢ ((𝐹 Fn A
∧ B ∈ A) →
(𝐹‘B) ∈ ran 𝐹) |
|
Theorem | ffvelrn 5243 |
A function's value belongs to its codomain. (Contributed by NM,
12-Aug-1999.)
|
⊢ ((𝐹:A⟶B
∧ 𝐶 ∈
A) → (𝐹‘𝐶) ∈
B) |
|
Theorem | ffvelrni 5244 |
A function's value belongs to its codomain. (Contributed by NM,
6-Apr-2005.)
|
⊢ 𝐹:A⟶B ⇒ ⊢ (𝐶 ∈
A → (𝐹‘𝐶) ∈
B) |
|
Theorem | ffvelrnda 5245 |
A function's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
⊢ (φ
→ 𝐹:A⟶B) ⇒ ⊢ ((φ ∧ 𝐶 ∈ A) →
(𝐹‘𝐶) ∈
B) |
|
Theorem | ffvelrnd 5246 |
A function's value belongs to its codomain. (Contributed by Mario
Carneiro, 29-Dec-2016.)
|
⊢ (φ
→ 𝐹:A⟶B)
& ⊢ (φ
→ 𝐶 ∈ A) ⇒ ⊢ (φ → (𝐹‘𝐶) ∈
B) |
|
Theorem | rexrn 5247* |
Restricted existential quantification over the range of a function.
(Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario
Carneiro, 20-Aug-2014.)
|
⊢ (x = (𝐹‘y) → (φ ↔ ψ)) ⇒ ⊢ (𝐹 Fn A
→ (∃x ∈ ran 𝐹φ ↔ ∃y ∈ A ψ)) |
|
Theorem | ralrn 5248* |
Restricted universal quantification over the range of a function.
(Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario
Carneiro, 20-Aug-2014.)
|
⊢ (x = (𝐹‘y) → (φ ↔ ψ)) ⇒ ⊢ (𝐹 Fn A
→ (∀x ∈ ran 𝐹φ ↔ ∀y ∈ A ψ)) |
|
Theorem | elrnrexdm 5249* |
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
𝐹 → ∃x ∈ dom 𝐹 𝑌 = (𝐹‘x))) |
|
Theorem | elrnrexdmb 5250* |
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
𝐹 ↔ ∃x ∈ dom 𝐹 𝑌 = (𝐹‘x))) |
|
Theorem | eldmrexrn 5251* |
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
𝐹 → ∃x ∈ ran 𝐹 x =
(𝐹‘𝑌))) |
|
Theorem | ralrnmpt 5252* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
⊢ 𝐹 = (x
∈ A
↦ B) & ⊢ (y = B →
(ψ ↔ χ)) ⇒ ⊢ (∀x ∈ A B ∈ 𝑉 → (∀y ∈ ran 𝐹ψ
↔ ∀x ∈ A χ)) |
|
Theorem | rexrnmpt 5253* |
A restricted quantifier over an image set. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
⊢ 𝐹 = (x
∈ A
↦ B) & ⊢ (y = B →
(ψ ↔ χ)) ⇒ ⊢ (∀x ∈ A B ∈ 𝑉 → (∃y ∈ ran 𝐹ψ
↔ ∃x ∈ A χ)) |
|
Theorem | dff2 5254 |
Alternate definition of a mapping. (Contributed by NM, 14-Nov-2007.)
|
⊢ (𝐹:A⟶B
↔ (𝐹 Fn A ∧ 𝐹 ⊆ (A × B))) |
|
Theorem | dff3im 5255* |
Property of a mapping. (Contributed by Jim Kingdon, 4-Jan-2019.)
|
⊢ (𝐹:A⟶B
→ (𝐹 ⊆
(A × B) ∧ ∀x ∈ A ∃!y x𝐹y)) |
|
Theorem | dff4im 5256* |
Property of a mapping. (Contributed by Jim Kingdon, 4-Jan-2019.)
|
⊢ (𝐹:A⟶B
→ (𝐹 ⊆
(A × B) ∧ ∀x ∈ A ∃!y ∈ B x𝐹y)) |
|
Theorem | dffo3 5257* |
An onto mapping expressed in terms of function values. (Contributed by
NM, 29-Oct-2006.)
|
⊢ (𝐹:A–onto→B ↔
(𝐹:A⟶B
∧ ∀y ∈ B ∃x ∈ A y = (𝐹‘x))) |
|
Theorem | dffo4 5258* |
Alternate definition of an onto mapping. (Contributed by NM,
20-Mar-2007.)
|
⊢ (𝐹:A–onto→B ↔
(𝐹:A⟶B
∧ ∀y ∈ B ∃x ∈ A x𝐹y)) |
|
Theorem | dffo5 5259* |
Alternate definition of an onto mapping. (Contributed by NM,
20-Mar-2007.)
|
⊢ (𝐹:A–onto→B ↔
(𝐹:A⟶B
∧ ∀y ∈ B ∃x x𝐹y)) |
|
Theorem | foelrn 5260* |
Property of a surjective function. (Contributed by Jeff Madsen,
4-Jan-2011.)
|
⊢ ((𝐹:A–onto→B ∧ 𝐶 ∈
B) → ∃x ∈ A 𝐶 = (𝐹‘x)) |
|
Theorem | foco2 5261 |
If a composition of two functions is surjective, then the function on
the left is surjective. (Contributed by Jeff Madsen, 16-Jun-2011.)
|
⊢ ((𝐹:B⟶𝐶 ∧ 𝐺:A⟶B
∧ (𝐹 ∘ 𝐺):A–onto→𝐶) → 𝐹:B–onto→𝐶) |
|
Theorem | fmpt 5262* |
Functionality of the mapping operation. (Contributed by Mario Carneiro,
26-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
⊢ 𝐹 = (x
∈ A
↦ 𝐶) ⇒ ⊢ (∀x ∈ A 𝐶 ∈ B ↔
𝐹:A⟶B) |
|
Theorem | f1ompt 5263* |
Express bijection for a mapping operation. (Contributed by Mario
Carneiro, 30-May-2015.) (Revised by Mario Carneiro, 4-Dec-2016.)
|
⊢ 𝐹 = (x
∈ A
↦ 𝐶) ⇒ ⊢ (𝐹:A–1-1-onto→B ↔
(∀x
∈ A
𝐶 ∈ B ∧ ∀y ∈ B ∃!x ∈ A y = 𝐶)) |
|
Theorem | fmpti 5264* |
Functionality of the mapping operation. (Contributed by NM,
19-Mar-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)
|
⊢ 𝐹 = (x
∈ A
↦ 𝐶) & ⊢ (x ∈ A → 𝐶 ∈
B) ⇒ ⊢ 𝐹:A⟶B |
|
Theorem | fmptd 5265* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by Mario Carneiro, 13-Jan-2013.)
|
⊢ ((φ
∧ x ∈ A) →
B ∈
𝐶) & ⊢ 𝐹 = (x ∈ A ↦ B) ⇒ ⊢ (φ → 𝐹:A⟶𝐶) |
|
Theorem | ffnfv 5266* |
A function maps to a class to which all values belong. (Contributed by
NM, 3-Dec-2003.)
|
⊢ (𝐹:A⟶B
↔ (𝐹 Fn A ∧ ∀x ∈ A (𝐹‘x) ∈ B)) |
|
Theorem | ffnfvf 5267 |
A function maps to a class to which all values belong. This version of
ffnfv 5266 uses bound-variable hypotheses instead of
distinct variable
conditions. (Contributed by NM, 28-Sep-2006.)
|
⊢ ℲxA & ⊢
ℲxB
& ⊢ Ⅎx𝐹 ⇒ ⊢ (𝐹:A⟶B
↔ (𝐹 Fn A ∧ ∀x ∈ A (𝐹‘x) ∈ B)) |
|
Theorem | fnfvrnss 5268* |
An upper bound for range determined by function values. (Contributed by
NM, 8-Oct-2004.)
|
⊢ ((𝐹 Fn A
∧ ∀x ∈ A (𝐹‘x) ∈ B) → ran 𝐹 ⊆ B) |
|
Theorem | rnmptss 5269* |
The range of an operation given by the "maps to" notation as a
subset.
(Contributed by Thierry Arnoux, 24-Sep-2017.)
|
⊢ 𝐹 = (x
∈ A
↦ B) ⇒ ⊢ (∀x ∈ A B ∈ 𝐶 → ran 𝐹 ⊆ 𝐶) |
|
Theorem | fmpt2d 5270* |
Domain and codomain of the mapping operation; deduction form.
(Contributed by NM, 27-Dec-2014.)
|
⊢ ((φ
∧ x ∈ A) →
B ∈
𝑉) & ⊢ (φ → 𝐹 = (x
∈ A
↦ B)) & ⊢ ((φ ∧
y ∈
A) → (𝐹‘y) ∈ 𝐶)
⇒ ⊢ (φ → 𝐹:A⟶𝐶) |
|
Theorem | ffvresb 5271* |
A necessary and sufficient condition for a restricted function.
(Contributed by Mario Carneiro, 14-Nov-2013.)
|
⊢ (Fun 𝐹 → ((𝐹 ↾ A):A⟶B
↔ ∀x ∈ A (x ∈ dom 𝐹 ∧ (𝐹‘x) ∈ B))) |
|
Theorem | f1oresrab 5272* |
Build a bijection between restricted abstract builders, given a
bijection between the base classes, deduction version. (Contributed by
Thierry Arnoux, 17-Aug-2018.)
|
⊢ 𝐹 = (x
∈ A
↦ 𝐶) & ⊢ (φ → 𝐹:A–1-1-onto→B)
& ⊢ ((φ
∧ x ∈ A ∧ y = 𝐶) → (χ ↔ ψ)) ⇒ ⊢ (φ → (𝐹 ↾ {x ∈ A ∣ ψ}):{x
∈ A
∣ ψ}–1-1-onto→{y ∈ B ∣
χ}) |
|
Theorem | fmptco 5273* |
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.)
|
⊢ ((φ
∧ x ∈ A) →
𝑅 ∈ B)
& ⊢ (φ
→ 𝐹 = (x ∈ A ↦ 𝑅)) & ⊢ (φ → 𝐺 = (y
∈ B
↦ 𝑆)) & ⊢ (y = 𝑅 → 𝑆 = 𝑇) ⇒ ⊢ (φ → (𝐺 ∘ 𝐹) = (x
∈ A
↦ 𝑇)) |
|
Theorem | fmptcof 5274* |
Version of fmptco 5273 where φ needn't be distinct from x.
(Contributed by NM, 27-Dec-2014.)
|
⊢ (φ
→ ∀x ∈ A 𝑅 ∈
B) & ⊢ (φ → 𝐹 = (x
∈ A
↦ 𝑅)) & ⊢ (φ → 𝐺 = (y
∈ B
↦ 𝑆)) & ⊢ (y = 𝑅 → 𝑆 = 𝑇) ⇒ ⊢ (φ → (𝐺 ∘ 𝐹) = (x
∈ A
↦ 𝑇)) |
|
Theorem | fmptcos 5275* |
Composition of two functions expressed as mapping abstractions.
(Contributed by NM, 22-May-2006.) (Revised by Mario Carneiro,
31-Aug-2015.)
|
⊢ (φ
→ ∀x ∈ A 𝑅 ∈
B) & ⊢ (φ → 𝐹 = (x
∈ A
↦ 𝑅)) & ⊢ (φ → 𝐺 = (y
∈ B
↦ 𝑆)) ⇒ ⊢ (φ → (𝐺 ∘ 𝐹) = (x
∈ A
↦ ⦋𝑅 /
y⦌𝑆)) |
|
Theorem | fcompt 5276* |
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.)
|
⊢ ((A:𝐷⟶𝐸 ∧
B:𝐶⟶𝐷) → (A ∘ B) =
(x ∈
𝐶 ↦ (A‘(B‘x)))) |
|
Theorem | fcoconst 5277 |
Composition with a constant function. (Contributed by Stefan O'Rear,
11-Mar-2015.)
|
⊢ ((𝐹 Fn 𝑋 ∧ 𝑌 ∈ 𝑋) → (𝐹 ∘ (𝐼 × {𝑌})) = (𝐼 × {(𝐹‘𝑌)})) |
|
Theorem | fsn 5278 |
A function maps a singleton to a singleton iff it is the singleton of an
ordered pair. (Contributed by NM, 10-Dec-2003.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (𝐹:{A}⟶{B}
↔ 𝐹 = {〈A, B〉}) |
|
Theorem | fsng 5279 |
A function maps a singleton to a singleton iff it is the singleton of an
ordered pair. (Contributed by NM, 26-Oct-2012.)
|
⊢ ((A ∈ 𝐶 ∧
B ∈
𝐷) → (𝐹:{A}⟶{B}
↔ 𝐹 = {〈A, B〉})) |
|
Theorem | fsn2 5280 |
A function that maps a singleton to a class is the singleton of an
ordered pair. (Contributed by NM, 19-May-2004.)
|
⊢ A ∈ V ⇒ ⊢ (𝐹:{A}⟶B
↔ ((𝐹‘A) ∈ B ∧ 𝐹 = {〈A, (𝐹‘A)〉})) |
|
Theorem | xpsng 5281 |
The cross product of two singletons. (Contributed by Mario Carneiro,
30-Apr-2015.)
|
⊢ ((A ∈ 𝑉 ∧
B ∈
𝑊) → ({A} × {B})
= {〈A, B〉}) |
|
Theorem | xpsn 5282 |
The cross product of two singletons. (Contributed by NM,
4-Nov-2006.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ ({A} × {B})
= {〈A, B〉} |
|
Theorem | dfmpt 5283 |
Alternate definition for the "maps to" notation df-mpt 3811 (although it
requires that B be a set). (Contributed by NM,
24-Aug-2010.)
(Revised by Mario Carneiro, 30-Dec-2016.)
|
⊢ B ∈ V ⇒ ⊢ (x ∈ A ↦ B) =
∪ x
∈ A
{〈x, B〉} |
|
Theorem | fnasrn 5284 |
A function expressed as the range of another function. (Contributed by
Mario Carneiro, 22-Jun-2013.) (Proof shortened by Mario Carneiro,
31-Aug-2015.)
|
⊢ B ∈ V ⇒ ⊢ (x ∈ A ↦ B) =
ran (x ∈
A ↦ 〈x, B〉) |
|
Theorem | dfmptg 5285 |
Alternate definition for the "maps to" notation df-mpt 3811 (which requires
that B be a
set). (Contributed by Jim Kingdon, 9-Jan-2019.)
|
⊢ (∀x ∈ A B ∈ 𝑉 → (x ∈ A ↦ B) =
∪ x
∈ A
{〈x, B〉}) |
|
Theorem | fnasrng 5286 |
A function expressed as the range of another function. (Contributed by
Jim Kingdon, 9-Jan-2019.)
|
⊢ (∀x ∈ A B ∈ 𝑉 → (x ∈ A ↦ B) =
ran (x ∈
A ↦ 〈x, B〉)) |
|
Theorem | ressnop0 5287 |
If A is not in
𝐶,
then the restriction of a singleton of
〈A, B〉 to 𝐶 is null. (Contributed by Scott
Fenton,
15-Apr-2011.)
|
⊢ (¬ A
∈ 𝐶 → ({〈A, B〉}
↾ 𝐶) =
∅) |
|
Theorem | fpr 5288 |
A function with a domain of two elements. (Contributed by Jeff Madsen,
20-Jun-2010.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|
⊢ A ∈ V
& ⊢ B ∈ V
& ⊢ 𝐶 ∈
V
& ⊢ 𝐷 ∈
V ⇒ ⊢ (A ≠ B →
{〈A, 𝐶〉, 〈B, 𝐷〉}:{A, B}⟶{𝐶, 𝐷}) |
|
Theorem | fprg 5289 |
A function with a domain of two elements. (Contributed by FL,
2-Feb-2014.)
|
⊢ (((A ∈ 𝐸 ∧
B ∈
𝐹) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐻) ∧ A ≠
B) → {〈A, 𝐶〉, 〈B, 𝐷〉}:{A, B}⟶{𝐶, 𝐷}) |
|
Theorem | ftpg 5290 |
A function with a domain of three elements. (Contributed by Alexander van
der Vekens, 4-Dec-2017.)
|
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (A ∈ 𝐹 ∧
B ∈
𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → {〈𝑋, A〉, 〈𝑌, B〉, 〈𝑍, 𝐶〉}:{𝑋, 𝑌, 𝑍}⟶{A, B, 𝐶}) |
|
Theorem | ftp 5291 |
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.)
|
⊢ A ∈ V
& ⊢ B ∈ V
& ⊢ 𝐶 ∈
V
& ⊢ 𝑋 ∈
V
& ⊢ 𝑌 ∈
V
& ⊢ 𝑍 ∈
V
& ⊢ A ≠
B & ⊢ A ≠ 𝐶
& ⊢ B ≠
𝐶
⇒ ⊢ {〈A, 𝑋〉, 〈B, 𝑌〉, 〈𝐶, 𝑍〉}:{A, B, 𝐶}⟶{𝑋, 𝑌, 𝑍} |
|
Theorem | fnressn 5292 |
A function restricted to a singleton. (Contributed by NM,
9-Oct-2004.)
|
⊢ ((𝐹 Fn A
∧ B ∈ A) →
(𝐹 ↾ {B}) = {〈B,
(𝐹‘B)〉}) |
|
Theorem | fressnfv 5293 |
The value of a function restricted to a singleton. (Contributed by NM,
9-Oct-2004.)
|
⊢ ((𝐹 Fn A
∧ B ∈ A) →
((𝐹 ↾ {B}):{B}⟶𝐶 ↔ (𝐹‘B) ∈ 𝐶)) |
|
Theorem | fvconst 5294 |
The value of a constant function. (Contributed by NM, 30-May-1999.)
|
⊢ ((𝐹:A⟶{B}
∧ 𝐶 ∈
A) → (𝐹‘𝐶) = B) |
|
Theorem | fmptsn 5295* |
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.)
|
⊢ ((A ∈ 𝑉 ∧
B ∈
𝑊) → {〈A, B〉} =
(x ∈
{A} ↦ B)) |
|
Theorem | fmptap 5296* |
Append an additional value to a function. (Contributed by NM,
6-Jun-2006.) (Revised by Mario Carneiro, 31-Aug-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V
& ⊢ (𝑅 ∪ {A}) = 𝑆
& ⊢ (x =
A → 𝐶 = B) ⇒ ⊢ ((x ∈ 𝑅 ↦ 𝐶) ∪ {〈A, B〉}) =
(x ∈
𝑆 ↦ 𝐶) |
|
Theorem | fmptapd 5297* |
Append an additional value to a function. (Contributed by Thierry
Arnoux, 3-Jan-2017.)
|
⊢ (φ
→ A ∈ V)
& ⊢ (φ
→ B ∈ V)
& ⊢ (φ
→ (𝑅 ∪ {A}) = 𝑆)
& ⊢ ((φ
∧ x =
A) → 𝐶 = B) ⇒ ⊢ (φ → ((x ∈ 𝑅 ↦ 𝐶) ∪ {〈A, B〉}) =
(x ∈
𝑆 ↦ 𝐶)) |
|
Theorem | fmptpr 5298* |
Express a pair function in maps-to notation. (Contributed by Thierry
Arnoux, 3-Jan-2017.)
|
⊢ (φ
→ A ∈ 𝑉)
& ⊢ (φ
→ B ∈ 𝑊)
& ⊢ (φ
→ 𝐶 ∈ 𝑋)
& ⊢ (φ
→ 𝐷 ∈ 𝑌)
& ⊢ ((φ
∧ x =
A) → 𝐸 = 𝐶)
& ⊢ ((φ
∧ x =
B) → 𝐸 = 𝐷) ⇒ ⊢ (φ → {〈A, 𝐶〉, 〈B, 𝐷〉} = (x ∈ {A, B} ↦
𝐸)) |
|
Theorem | fvresi 5299 |
The value of a restricted identity function. (Contributed by NM,
19-May-2004.)
|
⊢ (B ∈ A → ((
I ↾ A)‘B) = B) |
|
Theorem | fvunsng 5300 |
Remove an ordered pair not participating in a function value.
(Contributed by Jim Kingdon, 7-Jan-2019.)
|
⊢ ((𝐷 ∈ 𝑉 ∧ B ≠ 𝐷) → ((A ∪ {〈B, 𝐶〉})‘𝐷) = (A‘𝐷)) |