![]() |
Intuitionistic Logic Explorer Theorem List (p. 58 of 151) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fsn 5701 | 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 5702 | 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 5703 | 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 5704 | The cross product of two singletons. (Contributed by Mario Carneiro, 30-Apr-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} × {𝐵}) = {⟨𝐴, 𝐵⟩}) | ||
Theorem | xpsn 5705 | The cross product of two singletons. (Contributed by NM, 4-Nov-2006.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ({𝐴} × {𝐵}) = {⟨𝐴, 𝐵⟩} | ||
Theorem | dfmpt 5706 | Alternate definition for the maps-to notation df-mpt 4078 (although it requires that 𝐵 be a set). (Contributed by NM, 24-Aug-2010.) (Revised by Mario Carneiro, 30-Dec-2016.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩} | ||
Theorem | fnasrn 5707 | 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 5708 | Alternate definition for the maps-to notation df-mpt 4078 (which requires that 𝐵 be a set). (Contributed by Jim Kingdon, 9-Jan-2019.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) = ∪ 𝑥 ∈ 𝐴 {⟨𝑥, 𝐵⟩}) | ||
Theorem | fnasrng 5709 | A function expressed as the range of another function. (Contributed by Jim Kingdon, 9-Jan-2019.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → (𝑥 ∈ 𝐴 ↦ 𝐵) = ran (𝑥 ∈ 𝐴 ↦ ⟨𝑥, 𝐵⟩)) | ||
Theorem | ressnop0 5710 | If 𝐴 is not in 𝐶, then the restriction of a singleton of ⟨𝐴, 𝐵⟩ to 𝐶 is null. (Contributed by Scott Fenton, 15-Apr-2011.) |
⊢ (¬ 𝐴 ∈ 𝐶 → ({⟨𝐴, 𝐵⟩} ↾ 𝐶) = ∅) | ||
Theorem | fpr 5711 | 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 5712 | A function with a domain of two elements. (Contributed by FL, 2-Feb-2014.) |
⊢ (((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐹) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐻) ∧ 𝐴 ≠ 𝐵) → {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩}:{𝐴, 𝐵}⟶{𝐶, 𝐷}) | ||
Theorem | ftpg 5713 | A function with a domain of three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.) |
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → {⟨𝑋, 𝐴⟩, ⟨𝑌, 𝐵⟩, ⟨𝑍, 𝐶⟩}:{𝑋, 𝑌, 𝑍}⟶{𝐴, 𝐵, 𝐶}) | ||
Theorem | ftp 5714 | 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 5715 | A function restricted to a singleton. (Contributed by NM, 9-Oct-2004.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹 ↾ {𝐵}) = {⟨𝐵, (𝐹‘𝐵)⟩}) | ||
Theorem | fressnfv 5716 | The value of a function restricted to a singleton. (Contributed by NM, 9-Oct-2004.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹 ↾ {𝐵}):{𝐵}⟶𝐶 ↔ (𝐹‘𝐵) ∈ 𝐶)) | ||
Theorem | fvconst 5717 | The value of a constant function. (Contributed by NM, 30-May-1999.) |
⊢ ((𝐹:𝐴⟶{𝐵} ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) = 𝐵) | ||
Theorem | fmptsn 5718* | 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 5719* | Append an additional value to a function. (Contributed by NM, 6-Jun-2006.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑅 ∪ {𝐴}) = 𝑆 & ⊢ (𝑥 = 𝐴 → 𝐶 = 𝐵) ⇒ ⊢ ((𝑥 ∈ 𝑅 ↦ 𝐶) ∪ {⟨𝐴, 𝐵⟩}) = (𝑥 ∈ 𝑆 ↦ 𝐶) | ||
Theorem | fmptapd 5720* | Append an additional value to a function. (Contributed by Thierry Arnoux, 3-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → (𝑅 ∪ {𝐴}) = 𝑆) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝑅 ↦ 𝐶) ∪ {⟨𝐴, 𝐵⟩}) = (𝑥 ∈ 𝑆 ↦ 𝐶)) | ||
Theorem | fmptpr 5721* | Express a pair function in maps-to notation. (Contributed by Thierry Arnoux, 3-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) & ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐸 = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐸 = 𝐷) ⇒ ⊢ (𝜑 → {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩} = (𝑥 ∈ {𝐴, 𝐵} ↦ 𝐸)) | ||
Theorem | fvresi 5722 | The value of a restricted identity function. (Contributed by NM, 19-May-2004.) |
⊢ (𝐵 ∈ 𝐴 → (( I ↾ 𝐴)‘𝐵) = 𝐵) | ||
Theorem | fvunsng 5723 | Remove an ordered pair not participating in a function value. (Contributed by Jim Kingdon, 7-Jan-2019.) |
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷) → ((𝐴 ∪ {⟨𝐵, 𝐶⟩})‘𝐷) = (𝐴‘𝐷)) | ||
Theorem | fvsn 5724 | The value of a singleton of an ordered pair is the second member. (Contributed by NM, 12-Aug-1994.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ({⟨𝐴, 𝐵⟩}‘𝐴) = 𝐵 | ||
Theorem | fvsng 5725 | The value of a singleton of an ordered pair is the second member. (Contributed by NM, 26-Oct-2012.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({⟨𝐴, 𝐵⟩}‘𝐴) = 𝐵) | ||
Theorem | fvsnun1 5726 | The value of a function with one of its ordered pairs replaced, at the replaced ordered pair. See also fvsnun2 5727. (Contributed by NM, 23-Sep-2007.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐺 = ({⟨𝐴, 𝐵⟩} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) ⇒ ⊢ (𝐺‘𝐴) = 𝐵 | ||
Theorem | fvsnun2 5727 | The value of a function with one of its ordered pairs replaced, at arguments other than the replaced one. See also fvsnun1 5726. (Contributed by NM, 23-Sep-2007.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐺 = ({⟨𝐴, 𝐵⟩} ∪ (𝐹 ↾ (𝐶 ∖ {𝐴}))) ⇒ ⊢ (𝐷 ∈ (𝐶 ∖ {𝐴}) → (𝐺‘𝐷) = (𝐹‘𝐷)) | ||
Theorem | fnsnsplitss 5728 | 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 5729 | Adjoining a point to a function gives a function. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
⊢ ((𝐹:𝑆⟶𝑇 ∧ (𝑋 ∈ 𝑉 ∧ ¬ 𝑋 ∈ 𝑆) ∧ 𝑌 ∈ 𝑇) → (𝐹 ∪ {⟨𝑋, 𝑌⟩}):(𝑆 ∪ {𝑋})⟶𝑇) | ||
Theorem | fsnunfv 5730 | 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 5731 | Recover the original function from a point-added function. (Contributed by Stefan O'Rear, 28-Feb-2015.) |
⊢ ((𝐹 Fn 𝑆 ∧ ¬ 𝑋 ∈ 𝑆) → ((𝐹 ∪ {⟨𝑋, 𝑌⟩}) ↾ 𝑆) = 𝐹) | ||
Theorem | funresdfunsnss 5732 | 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 5733 | The value of a function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.) |
⊢ 𝐴 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 ≠ 𝐵 → ({⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩}‘𝐴) = 𝐶) | ||
Theorem | fvpr2 5734 | The value of a function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.) |
⊢ 𝐵 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (𝐴 ≠ 𝐵 → ({⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩}‘𝐵) = 𝐷) | ||
Theorem | fvpr1g 5735 | The value of a function with a domain of (at most) two elements. (Contributed by Alexander van der Vekens, 3-Dec-2017.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩}‘𝐴) = 𝐶) | ||
Theorem | fvpr2g 5736 | The value of a function with a domain of (at most) two elements. (Contributed by Alexander van der Vekens, 3-Dec-2017.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩}‘𝐵) = 𝐷) | ||
Theorem | fvtp1g 5737 | The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶)) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐴) = 𝐷) | ||
Theorem | fvtp2g 5738 | The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.) |
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐵) = 𝐸) | ||
Theorem | fvtp3g 5739 | The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.) |
⊢ (((𝐶 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐶) = 𝐹) | ||
Theorem | fvtp1 5740 | The first value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐴) = 𝐷) | ||
Theorem | fvtp2 5741 | The second value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011.) |
⊢ 𝐵 ∈ V & ⊢ 𝐸 ∈ V ⇒ ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐵) = 𝐸) | ||
Theorem | fvtp3 5742 | The third value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011.) |
⊢ 𝐶 ∈ V & ⊢ 𝐹 ∈ V ⇒ ⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({⟨𝐴, 𝐷⟩, ⟨𝐵, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐶) = 𝐹) | ||
Theorem | fvconst2g 5743 | The value of a constant function. (Contributed by NM, 20-Aug-2005.) |
⊢ ((𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵) | ||
Theorem | fconst2g 5744 | A constant function expressed as a cross product. (Contributed by NM, 27-Nov-2007.) |
⊢ (𝐵 ∈ 𝐶 → (𝐹:𝐴⟶{𝐵} ↔ 𝐹 = (𝐴 × {𝐵}))) | ||
Theorem | fvconst2 5745 | The value of a constant function. (Contributed by NM, 16-Apr-2005.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐶 ∈ 𝐴 → ((𝐴 × {𝐵})‘𝐶) = 𝐵) | ||
Theorem | fconst2 5746 | A constant function expressed as a cross product. (Contributed by NM, 20-Aug-1999.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹:𝐴⟶{𝐵} ↔ 𝐹 = (𝐴 × {𝐵})) | ||
Theorem | fconstfvm 5747* | A constant function expressed in terms of its functionality, domain, and value. See also fconst2 5746. (Contributed by Jim Kingdon, 8-Jan-2019.) |
⊢ (∃𝑦 𝑦 ∈ 𝐴 → (𝐹:𝐴⟶{𝐵} ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))) | ||
Theorem | fconst3m 5748* | Two ways to express a constant function. (Contributed by Jim Kingdon, 8-Jan-2019.) |
⊢ (∃𝑥 𝑥 ∈ 𝐴 → (𝐹:𝐴⟶{𝐵} ↔ (𝐹 Fn 𝐴 ∧ 𝐴 ⊆ (◡𝐹 “ {𝐵})))) | ||
Theorem | fconst4m 5749* | Two ways to express a constant function. (Contributed by NM, 8-Mar-2007.) |
⊢ (∃𝑥 𝑥 ∈ 𝐴 → (𝐹:𝐴⟶{𝐵} ↔ (𝐹 Fn 𝐴 ∧ (◡𝐹 “ {𝐵}) = 𝐴))) | ||
Theorem | resfunexg 5750 | 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 5751 | 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 5750. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵) → 𝐹 ∈ V) | ||
Theorem | funex 5752 | 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 5751. (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 5753* | Existence of a function expressed as class of ordered pairs. (Contributed by NM, 21-Jul-1996.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 ∈ 𝐴 → ∃*𝑦𝜑) ⇒ ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∈ V | ||
Theorem | mptexg 5754* | 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 5755* | 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 5756* | If the domain of a function given by maps-to notation is a set, the function is a set. Deduction version of mptexg 5754. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) | ||
Theorem | mptrabex 5757* | 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 5758 | If the domain of a mapping is a set, the function is a set. (Contributed by NM, 3-Oct-1999.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ V) | ||
Theorem | fexd 5759 | If the domain of a mapping is a set, the function is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐹 ∈ V) | ||
Theorem | eufnfv 5760* | A function is uniquely determined by its values. (Contributed by NM, 31-Aug-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∃!𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 𝐵) | ||
Theorem | funfvima 5761 | A function's value in a preimage belongs to the image. (Contributed by NM, 23-Sep-2003.) |
⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴))) | ||
Theorem | funfvima2 5762 | A function's value in an included preimage belongs to the image. (Contributed by NM, 3-Feb-1997.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐵 ∈ 𝐴 → (𝐹‘𝐵) ∈ (𝐹 “ 𝐴))) | ||
Theorem | funfvima3 5763 | 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 𝐹 → (𝐹‘𝐴) ∈ (𝐺 “ {𝐴}))) | ||
Theorem | fnfvima 5764 | The function value of an operand in a set is contained in the image of that set, using the Fn abbreviation. (Contributed by Stefan O'Rear, 10-Mar-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆)) | ||
Theorem | foima2 5765* | Given an onto function, an element is in its codomain if and only if it is the image of an element of its domain (see foima 5455). (Contributed by BJ, 6-Jul-2022.) |
⊢ (𝐹:𝐴–onto→𝐵 → (𝑌 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑌 = (𝐹‘𝑥))) | ||
Theorem | foelrn 5766* | Property of a surjective function. (Contributed by Jeff Madsen, 4-Jan-2011.) (Proof shortened by BJ, 6-Jul-2022.) |
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝐶 = (𝐹‘𝑥)) | ||
Theorem | foco2 5767 | If a composition of two functions is surjective, then the function on the left is surjective. (Contributed by Jeff Madsen, 16-Jun-2011.) |
⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵 ∧ (𝐹 ∘ 𝐺):𝐴–onto→𝐶) → 𝐹:𝐵–onto→𝐶) | ||
Theorem | rexima 5768* | Existential quantification under an image in terms of the base set. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∃𝑥 ∈ (𝐹 “ 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | ralima 5769* | Universal quantification under an image in terms of the base set. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∀𝑥 ∈ (𝐹 “ 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | idref 5770* |
TODO: This is the same as issref 5023 (which has a much longer proof).
Should we replace issref 5023 with this one? - NM 9-May-2016.
Two ways to state a relation is reflexive. (Adapted from Tarski.) (Contributed by FL, 15-Jan-2012.) (Proof shortened by Mario Carneiro, 3-Nov-2015.) (Proof modification is discouraged.) |
⊢ (( I ↾ 𝐴) ⊆ 𝑅 ↔ ∀𝑥 ∈ 𝐴 𝑥𝑅𝑥) | ||
Theorem | elabrex 5771* | Elementhood in an image set. (Contributed by Mario Carneiro, 14-Jan-2014.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝑥 ∈ 𝐴 → 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) | ||
Theorem | elabrexg 5772* | Elementhood in an image set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}) | ||
Theorem | abrexco 5773* | Composition of two image maps 𝐶(𝑦) and 𝐵(𝑤). (Contributed by NM, 27-May-2013.) |
⊢ 𝐵 ∈ V & ⊢ (𝑦 = 𝐵 → 𝐶 = 𝐷) ⇒ ⊢ {𝑥 ∣ ∃𝑦 ∈ {𝑧 ∣ ∃𝑤 ∈ 𝐴 𝑧 = 𝐵}𝑥 = 𝐶} = {𝑥 ∣ ∃𝑤 ∈ 𝐴 𝑥 = 𝐷} | ||
Theorem | imaiun 5774* | The image of an indexed union is the indexed union of the images. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝐴 “ ∪ 𝑥 ∈ 𝐵 𝐶) = ∪ 𝑥 ∈ 𝐵 (𝐴 “ 𝐶) | ||
Theorem | imauni 5775* | The image of a union is the indexed union of the images. Theorem 3K(a) of [Enderton] p. 50. (Contributed by NM, 9-Aug-2004.) (Proof shortened by Mario Carneiro, 18-Jun-2014.) |
⊢ (𝐴 “ ∪ 𝐵) = ∪ 𝑥 ∈ 𝐵 (𝐴 “ 𝑥) | ||
Theorem | fniunfv 5776* | The indexed union of a function's values is the union of its range. Compare Definition 5.4 of [Monk1] p. 50. (Contributed by NM, 27-Sep-2004.) |
⊢ (𝐹 Fn 𝐴 → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ ran 𝐹) | ||
Theorem | funiunfvdm 5777* | The indexed union of a function's values is the union of its image under the index class. This theorem is a slight variation of fniunfv 5776. (Contributed by Jim Kingdon, 10-Jan-2019.) |
⊢ (𝐹 Fn 𝐴 → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ (𝐹 “ 𝐴)) | ||
Theorem | funiunfvdmf 5778* | The indexed union of a function's values is the union of its image under the index class. This version of funiunfvdm 5777 uses a bound-variable hypothesis in place of a distinct variable condition. (Contributed by Jim Kingdon, 10-Jan-2019.) |
⊢ Ⅎ𝑥𝐹 ⇒ ⊢ (𝐹 Fn 𝐴 → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ (𝐹 “ 𝐴)) | ||
Theorem | eluniimadm 5779* | Membership in the union of an image of a function. (Contributed by Jim Kingdon, 10-Jan-2019.) |
⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ∪ (𝐹 “ 𝐴) ↔ ∃𝑥 ∈ 𝐴 𝐵 ∈ (𝐹‘𝑥))) | ||
Theorem | elunirn 5780* | Membership in the union of the range of a function. (Contributed by NM, 24-Sep-2006.) |
⊢ (Fun 𝐹 → (𝐴 ∈ ∪ ran 𝐹 ↔ ∃𝑥 ∈ dom 𝐹 𝐴 ∈ (𝐹‘𝑥))) | ||
Theorem | fnunirn 5781* | Membership in a union of some function-defined family of sets. (Contributed by Stefan O'Rear, 30-Jan-2015.) |
⊢ (𝐹 Fn 𝐼 → (𝐴 ∈ ∪ ran 𝐹 ↔ ∃𝑥 ∈ 𝐼 𝐴 ∈ (𝐹‘𝑥))) | ||
Theorem | dff13 5782* | A one-to-one function in terms of function values. Compare Theorem 4.8(iv) of [Monk1] p. 43. (Contributed by NM, 29-Oct-1996.) |
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) | ||
Theorem | f1veqaeq 5783 | If the values of a one-to-one function for two arguments are equal, the arguments themselves must be equal. (Contributed by Alexander van der Vekens, 12-Nov-2017.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐹‘𝐶) = (𝐹‘𝐷) → 𝐶 = 𝐷)) | ||
Theorem | dff13f 5784* | A one-to-one function in terms of function values. Compare Theorem 4.8(iv) of [Monk1] p. 43. (Contributed by NM, 31-Jul-2003.) |
⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑦𝐹 ⇒ ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) | ||
Theorem | f1mpt 5785* | Express injection for a mapping operation. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) ⇒ ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝐶 = 𝐷 → 𝑥 = 𝑦))) | ||
Theorem | f1fveq 5786 | Equality of function values for a one-to-one function. (Contributed by NM, 11-Feb-1997.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐹‘𝐶) = (𝐹‘𝐷) ↔ 𝐶 = 𝐷)) | ||
Theorem | f1elima 5787 | Membership in the image of a 1-1 map. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ⊆ 𝐴) → ((𝐹‘𝑋) ∈ (𝐹 “ 𝑌) ↔ 𝑋 ∈ 𝑌)) | ||
Theorem | f1imass 5788 | Taking images under a one-to-one function preserves subsets. (Contributed by Stefan O'Rear, 30-Oct-2014.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴)) → ((𝐹 “ 𝐶) ⊆ (𝐹 “ 𝐷) ↔ 𝐶 ⊆ 𝐷)) | ||
Theorem | f1imaeq 5789 | Taking images under a one-to-one function preserves equality. (Contributed by Stefan O'Rear, 30-Oct-2014.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴)) → ((𝐹 “ 𝐶) = (𝐹 “ 𝐷) ↔ 𝐶 = 𝐷)) | ||
Theorem | dff1o6 5790* | A one-to-one onto function in terms of function values. (Contributed by NM, 29-Mar-2008.) |
⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) | ||
Theorem | f1ocnvfv1 5791 | The converse value of the value of a one-to-one onto function. (Contributed by NM, 20-May-2004.) |
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴) → (◡𝐹‘(𝐹‘𝐶)) = 𝐶) | ||
Theorem | f1ocnvfv2 5792 | The value of the converse value of a one-to-one onto function. (Contributed by NM, 20-May-2004.) |
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶) | ||
Theorem | f1ocnvfv 5793 | Relationship between the value of a one-to-one onto function and the value of its converse. (Contributed by Raph Levien, 10-Apr-2004.) |
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹‘𝐶) = 𝐷 → (◡𝐹‘𝐷) = 𝐶)) | ||
Theorem | f1ocnvfvb 5794 | Relationship between the value of a one-to-one onto function and the value of its converse. (Contributed by NM, 20-May-2004.) |
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → ((𝐹‘𝐶) = 𝐷 ↔ (◡𝐹‘𝐷) = 𝐶)) | ||
Theorem | f1ocnvdm 5795 | The value of the converse of a one-to-one onto function belongs to its domain. (Contributed by NM, 26-May-2006.) |
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (◡𝐹‘𝐶) ∈ 𝐴) | ||
Theorem | f1ocnvfvrneq 5796 | If the values of a one-to-one function for two arguments from the range of the function are equal, the arguments themselves must be equal. (Contributed by Alexander van der Vekens, 12-Nov-2017.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ∈ ran 𝐹 ∧ 𝐷 ∈ ran 𝐹)) → ((◡𝐹‘𝐶) = (◡𝐹‘𝐷) → 𝐶 = 𝐷)) | ||
Theorem | fcof1 5797 | An application is injective if a retraction exists. Proposition 8 of [BourbakiEns] p. E.II.18. (Contributed by FL, 11-Nov-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝑅 ∘ 𝐹) = ( I ↾ 𝐴)) → 𝐹:𝐴–1-1→𝐵) | ||
Theorem | fcofo 5798 | An application is surjective if a section exists. Proposition 8 of [BourbakiEns] p. E.II.18. (Contributed by FL, 17-Nov-2011.) (Proof shortened by Mario Carneiro, 27-Dec-2014.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑆:𝐵⟶𝐴 ∧ (𝐹 ∘ 𝑆) = ( I ↾ 𝐵)) → 𝐹:𝐴–onto→𝐵) | ||
Theorem | cbvfo 5799* | Change bound variable between domain and range of function. (Contributed by NM, 23-Feb-1997.) (Proof shortened by Mario Carneiro, 21-Mar-2015.) |
⊢ ((𝐹‘𝑥) = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐹:𝐴–onto→𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | cbvexfo 5800* | Change bound variable between domain and range of function. (Contributed by NM, 23-Feb-1997.) |
⊢ ((𝐹‘𝑥) = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐹:𝐴–onto→𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |