Home | Metamath
Proof Explorer Theorem List (p. 307 of 462) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28971) |
Hilbert Space Explorer
(28972-30494) |
Users' Mathboxes
(30495-46134) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cbvdisjf 30601* | Change bound variables in a disjoint collection. (Contributed by Thierry Arnoux, 6-Apr-2017.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶) | ||
Theorem | disjss1f 30602 | A subset of a disjoint collection is disjoint. (Contributed by Thierry Arnoux, 6-Apr-2017.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 ⊆ 𝐵 → (Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐴 𝐶)) | ||
Theorem | disjeq1f 30603 | Equality theorem for disjoint collection. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶)) | ||
Theorem | disjxun0 30604* | Simplify a disjoint union. (Contributed by Thierry Arnoux, 27-Nov-2023.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 = ∅) ⇒ ⊢ (𝜑 → (Disj 𝑥 ∈ (𝐴 ∪ 𝐵)𝐶 ↔ Disj 𝑥 ∈ 𝐴 𝐶)) | ||
Theorem | disjdifprg 30605* | A trivial partition into a subset and its complement. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → Disj 𝑥 ∈ {(𝐵 ∖ 𝐴), 𝐴}𝑥) | ||
Theorem | disjdifprg2 30606* | A trivial partition of a set into its difference and intersection with another set. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
⊢ (𝐴 ∈ 𝑉 → Disj 𝑥 ∈ {(𝐴 ∖ 𝐵), (𝐴 ∩ 𝐵)}𝑥) | ||
Theorem | disji2f 30607* | Property of a disjoint collection: if 𝐵(𝑥) = 𝐶 and 𝐵(𝑌) = 𝐷, and 𝑥 ≠ 𝑌, then 𝐵 and 𝐶 are disjoint. (Contributed by Thierry Arnoux, 30-Dec-2016.) |
⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐶) ⇒ ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ 𝑥 ≠ 𝑌) → (𝐵 ∩ 𝐶) = ∅) | ||
Theorem | disjif 30608* | Property of a disjoint collection: if 𝐵(𝑥) and 𝐵(𝑌) = 𝐷 have a common element 𝑍, then 𝑥 = 𝑌. (Contributed by Thierry Arnoux, 30-Dec-2016.) |
⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐶) ⇒ ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (𝑍 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶)) → 𝑥 = 𝑌) | ||
Theorem | disjorf 30609* | Two ways to say that a collection 𝐵(𝑖) for 𝑖 ∈ 𝐴 is disjoint. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
⊢ Ⅎ𝑖𝐴 & ⊢ Ⅎ𝑗𝐴 & ⊢ (𝑖 = 𝑗 → 𝐵 = 𝐶) ⇒ ⊢ (Disj 𝑖 ∈ 𝐴 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (𝐵 ∩ 𝐶) = ∅)) | ||
Theorem | disjorsf 30610* | Two ways to say that a collection 𝐵(𝑖) for 𝑖 ∈ 𝐴 is disjoint. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) | ||
Theorem | disjif2 30611* | Property of a disjoint collection: if 𝐵(𝑥) and 𝐵(𝑌) = 𝐷 have a common element 𝑍, then 𝑥 = 𝑌. (Contributed by Thierry Arnoux, 6-Apr-2017.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐶) ⇒ ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (𝑍 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶)) → 𝑥 = 𝑌) | ||
Theorem | disjabrex 30612* | Rewriting a disjoint collection into a partition of its image set. (Contributed by Thierry Arnoux, 30-Dec-2016.) |
⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}𝑦) | ||
Theorem | disjabrexf 30613* | Rewriting a disjoint collection into a partition of its image set. (Contributed by Thierry Arnoux, 30-Dec-2016.) (Revised by Thierry Arnoux, 9-Mar-2017.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}𝑦) | ||
Theorem | disjpreima 30614* | A preimage of a disjoint set is disjoint. (Contributed by Thierry Arnoux, 7-Feb-2017.) |
⊢ ((Fun 𝐹 ∧ Disj 𝑥 ∈ 𝐴 𝐵) → Disj 𝑥 ∈ 𝐴 (◡𝐹 “ 𝐵)) | ||
Theorem | disjrnmpt 30615* | Rewriting a disjoint collection using the range of a mapping. (Contributed by Thierry Arnoux, 27-May-2020.) |
⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑦) | ||
Theorem | disjin 30616 | If a collection is disjoint, so is the collection of the intersections with a given set. (Contributed by Thierry Arnoux, 14-Feb-2017.) |
⊢ (Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐵 (𝐶 ∩ 𝐴)) | ||
Theorem | disjin2 30617 | If a collection is disjoint, so is the collection of the intersections with a given set. (Contributed by Thierry Arnoux, 21-Jun-2020.) |
⊢ (Disj 𝑥 ∈ 𝐵 𝐶 → Disj 𝑥 ∈ 𝐵 (𝐴 ∩ 𝐶)) | ||
Theorem | disjxpin 30618* | Derive a disjunction over a Cartesian product from the disjunctions over its first and second elements. (Contributed by Thierry Arnoux, 9-Mar-2018.) |
⊢ (𝑥 = (1st ‘𝑝) → 𝐶 = 𝐸) & ⊢ (𝑦 = (2nd ‘𝑝) → 𝐷 = 𝐹) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐶) & ⊢ (𝜑 → Disj 𝑦 ∈ 𝐵 𝐷) ⇒ ⊢ (𝜑 → Disj 𝑝 ∈ (𝐴 × 𝐵)(𝐸 ∩ 𝐹)) | ||
Theorem | iundisjf 30619* | Rewrite a countable union as a disjoint union. Cf. iundisj 24417. (Contributed by Thierry Arnoux, 31-Dec-2016.) |
⊢ Ⅎ𝑘𝐴 & ⊢ Ⅎ𝑛𝐵 & ⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵) ⇒ ⊢ ∪ 𝑛 ∈ ℕ 𝐴 = ∪ 𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) | ||
Theorem | iundisj2f 30620* | A disjoint union is disjoint. Cf. iundisj2 24418. (Contributed by Thierry Arnoux, 30-Dec-2016.) |
⊢ Ⅎ𝑘𝐴 & ⊢ Ⅎ𝑛𝐵 & ⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵) ⇒ ⊢ Disj 𝑛 ∈ ℕ (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵) | ||
Theorem | disjrdx 30621* | Re-index a disjunct collection statement. (Contributed by Thierry Arnoux, 7-Apr-2017.) |
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐶) & ⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑥)) → 𝐷 = 𝐵) ⇒ ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐶 𝐷)) | ||
Theorem | disjex 30622* | Two ways to say that two classes are disjoint (or equal). (Contributed by Thierry Arnoux, 4-Oct-2016.) |
⊢ ((∃𝑧(𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → 𝐴 = 𝐵) ↔ (𝐴 = 𝐵 ∨ (𝐴 ∩ 𝐵) = ∅)) | ||
Theorem | disjexc 30623* | A variant of disjex 30622, applicable for more generic families. (Contributed by Thierry Arnoux, 4-Oct-2016.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ ((∃𝑧(𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → 𝑥 = 𝑦) → (𝐴 = 𝐵 ∨ (𝐴 ∩ 𝐵) = ∅)) | ||
Theorem | disjunsn 30624* | Append an element to a disjoint collection. Similar to ralunsn 4795, gsumunsn 19317, etc. (Contributed by Thierry Arnoux, 28-Mar-2018.) |
⊢ (𝑥 = 𝑀 → 𝐵 = 𝐶) ⇒ ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅))) | ||
Theorem | disjun0 30625* | Adding the empty element preserves disjointness. (Contributed by Thierry Arnoux, 30-May-2020.) |
⊢ (Disj 𝑥 ∈ 𝐴 𝑥 → Disj 𝑥 ∈ (𝐴 ∪ {∅})𝑥) | ||
Theorem | disjiunel 30626* | A set of elements B of a disjoint set A is disjoint with another element of that set. (Contributed by Thierry Arnoux, 24-May-2020.) |
⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) & ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷) & ⊢ (𝜑 → 𝐸 ⊆ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ (𝐴 ∖ 𝐸)) ⇒ ⊢ (𝜑 → (∪ 𝑥 ∈ 𝐸 𝐵 ∩ 𝐷) = ∅) | ||
Theorem | disjuniel 30627* | A set of elements B of a disjoint set A is disjoint with another element of that set. (Contributed by Thierry Arnoux, 24-May-2020.) |
⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝑥) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐶 ∈ (𝐴 ∖ 𝐵)) ⇒ ⊢ (𝜑 → (∪ 𝐵 ∩ 𝐶) = ∅) | ||
Theorem | xpdisjres 30628 | Restriction of a constant function (or other Cartesian product) outside of its domain. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ ((𝐴 ∩ 𝐶) = ∅ → ((𝐴 × 𝐵) ↾ 𝐶) = ∅) | ||
Theorem | opeldifid 30629 | Ordered pair elementhood outside of the diagonal. (Contributed by Thierry Arnoux, 1-Jan-2020.) |
⊢ (Rel 𝐴 → (〈𝑋, 𝑌〉 ∈ (𝐴 ∖ I ) ↔ (〈𝑋, 𝑌〉 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌))) | ||
Theorem | difres 30630 | Case when class difference in unaffected by restriction. (Contributed by Thierry Arnoux, 1-Jan-2020.) |
⊢ (𝐴 ⊆ (𝐵 × V) → (𝐴 ∖ (𝐶 ↾ 𝐵)) = (𝐴 ∖ 𝐶)) | ||
Theorem | imadifxp 30631 | Image of the difference with a Cartesian product. (Contributed by Thierry Arnoux, 13-Dec-2017.) |
⊢ (𝐶 ⊆ 𝐴 → ((𝑅 ∖ (𝐴 × 𝐵)) “ 𝐶) = ((𝑅 “ 𝐶) ∖ 𝐵)) | ||
Theorem | relfi 30632 | A relation (set) is finite if and only if both its domain and range are finite. (Contributed by Thierry Arnoux, 27-Aug-2017.) |
⊢ (Rel 𝐴 → (𝐴 ∈ Fin ↔ (dom 𝐴 ∈ Fin ∧ ran 𝐴 ∈ Fin))) | ||
Theorem | reldisjun 30633 | Split a relation into two disjoint parts based on its domain. (Contributed by Thierry Arnoux, 9-Oct-2023.) |
⊢ ((Rel 𝑅 ∧ dom 𝑅 = (𝐴 ∪ 𝐵) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝑅 = ((𝑅 ↾ 𝐴) ∪ (𝑅 ↾ 𝐵))) | ||
Theorem | 0res 30634 | Restriction of the empty function. (Contributed by Thierry Arnoux, 20-Nov-2023.) |
⊢ (∅ ↾ 𝐴) = ∅ | ||
Theorem | funresdm1 30635 | Restriction of a disjoint union to the domain of the first term. (Contributed by Thierry Arnoux, 9-Dec-2021.) |
⊢ ((Rel 𝐴 ∧ (dom 𝐴 ∩ dom 𝐵) = ∅) → ((𝐴 ∪ 𝐵) ↾ dom 𝐴) = 𝐴) | ||
Theorem | fnunres1 30636 | Restriction of a disjoint union to the domain of the first function. (Contributed by Thierry Arnoux, 9-Dec-2021.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐹 ∪ 𝐺) ↾ 𝐴) = 𝐹) | ||
Theorem | fcoinver 30637 | Build an equivalence relation from a function. Two values are equivalent if they have the same image by the function. See also fcoinvbr 30638. (Contributed by Thierry Arnoux, 3-Jan-2020.) |
⊢ (𝐹 Fn 𝑋 → (◡𝐹 ∘ 𝐹) Er 𝑋) | ||
Theorem | fcoinvbr 30638 | Binary relation for the equivalence relation from fcoinver 30637. (Contributed by Thierry Arnoux, 3-Jan-2020.) |
⊢ ∼ = (◡𝐹 ∘ 𝐹) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∼ 𝑌 ↔ (𝐹‘𝑋) = (𝐹‘𝑌))) | ||
Theorem | brabgaf 30639* | The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013.) (Revised by Thierry Arnoux, 17-May-2020.) |
⊢ Ⅎ𝑥𝜓 & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴𝑅𝐵 ↔ 𝜓)) | ||
Theorem | brelg 30640 | Two things in a binary relation belong to the relation's domain. (Contributed by Thierry Arnoux, 29-Aug-2017.) |
⊢ ((𝑅 ⊆ (𝐶 × 𝐷) ∧ 𝐴𝑅𝐵) → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) | ||
Theorem | br8d 30641* | Substitution for an eight-place predicate. (Contributed by Scott Fenton, 26-Sep-2013.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by Thierry Arnoux, 21-Mar-2019.) |
⊢ (𝑎 = 𝐴 → (𝜓 ↔ 𝜒)) & ⊢ (𝑏 = 𝐵 → (𝜒 ↔ 𝜃)) & ⊢ (𝑐 = 𝐶 → (𝜃 ↔ 𝜏)) & ⊢ (𝑑 = 𝐷 → (𝜏 ↔ 𝜂)) & ⊢ (𝑒 = 𝐸 → (𝜂 ↔ 𝜁)) & ⊢ (𝑓 = 𝐹 → (𝜁 ↔ 𝜎)) & ⊢ (𝑔 = 𝐺 → (𝜎 ↔ 𝜌)) & ⊢ (ℎ = 𝐻 → (𝜌 ↔ 𝜇)) & ⊢ (𝜑 → 𝑅 = {〈𝑝, 𝑞〉 ∣ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜓)}) & ⊢ (𝜑 → 𝐴 ∈ 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑃) & ⊢ (𝜑 → 𝐶 ∈ 𝑃) & ⊢ (𝜑 → 𝐷 ∈ 𝑃) & ⊢ (𝜑 → 𝐸 ∈ 𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝑃) & ⊢ (𝜑 → 𝐺 ∈ 𝑃) & ⊢ (𝜑 → 𝐻 ∈ 𝑃) ⇒ ⊢ (𝜑 → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉𝑅〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ↔ 𝜇)) | ||
Theorem | opabdm 30642* | Domain of an ordered-pair class abstraction. (Contributed by Thierry Arnoux, 31-Aug-2017.) |
⊢ (𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} → dom 𝑅 = {𝑥 ∣ ∃𝑦𝜑}) | ||
Theorem | opabrn 30643* | Range of an ordered-pair class abstraction. (Contributed by Thierry Arnoux, 31-Aug-2017.) |
⊢ (𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} → ran 𝑅 = {𝑦 ∣ ∃𝑥𝜑}) | ||
Theorem | opabssi 30644* | Sufficient condition for a collection of ordered pairs to be a subclass of a relation. (Contributed by Peter Mazsa, 21-Oct-2019.) (Revised by Thierry Arnoux, 18-Feb-2022.) |
⊢ (𝜑 → 〈𝑥, 𝑦〉 ∈ 𝐴) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ 𝐴 | ||
Theorem | opabid2ss 30645* | One direction of opabid2 5687 which holds without a Rel 𝐴 requirement. (Contributed by Thierry Arnoux, 18-Feb-2022.) |
⊢ {〈𝑥, 𝑦〉 ∣ 〈𝑥, 𝑦〉 ∈ 𝐴} ⊆ 𝐴 | ||
Theorem | ssrelf 30646* | A subclass relationship depends only on a relation's ordered pairs. Theorem 3.2(i) of [Monk1] p. 33. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Revised by Thierry Arnoux, 6-Nov-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵))) | ||
Theorem | eqrelrd2 30647* | A version of eqrelrdv2 5654 with explicit nonfree declarations. (Contributed by Thierry Arnoux, 28-Aug-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑦𝐵 & ⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ 𝐵)) ⇒ ⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → 𝐴 = 𝐵) | ||
Theorem | erbr3b 30648 | Biconditional for equivalent elements. (Contributed by Thierry Arnoux, 6-Jan-2020.) |
⊢ ((𝑅 Er 𝑋 ∧ 𝐴𝑅𝐵) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)) | ||
Theorem | iunsnima 30649 | Image of a singleton by an indexed union involving that singleton. (Contributed by Thierry Arnoux, 10-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) “ {𝑥}) = 𝐵) | ||
Theorem | iunsnima2 30650* | Version of iunsnima 30649 with different variables. (Contributed by Thierry Arnoux, 22-Jun-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐶) ⇒ ⊢ ((𝜑 ∧ 𝑌 ∈ 𝐴) → (∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) “ {𝑌}) = 𝐶) | ||
Theorem | ac6sf2 30651* | Alternate version of ac6 10077 with bound-variable hypothesis. (Contributed by NM, 2-Mar-2008.) (Revised by Thierry Arnoux, 17-May-2020.) |
⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑦𝜓 & ⊢ 𝐴 ∈ V & ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | fnresin 30652 | Restriction of a function with a subclass of its domain. (Contributed by Thierry Arnoux, 10-Oct-2017.) |
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐵) Fn (𝐴 ∩ 𝐵)) | ||
Theorem | f1o3d 30653* | Describe an implicit one-to-one onto function. (Contributed by Thierry Arnoux, 23-Apr-2017.) |
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝐴) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥 = 𝐷 ↔ 𝑦 = 𝐶)) ⇒ ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐵 ∧ ◡𝐹 = (𝑦 ∈ 𝐵 ↦ 𝐷))) | ||
Theorem | eldmne0 30654 | A function of nonempty domain is not empty. (Contributed by Thierry Arnoux, 20-Nov-2023.) |
⊢ (𝑋 ∈ dom 𝐹 → 𝐹 ≠ ∅) | ||
Theorem | f1rnen 30655 | Equinumerosity of the range of an injective function. (Contributed by Thierry Arnoux, 7-Jul-2023.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉) → ran 𝐹 ≈ 𝐴) | ||
Theorem | rinvf1o 30656 | Sufficient conditions for the restriction of an involution to be a bijection. (Contributed by Thierry Arnoux, 7-Dec-2016.) |
⊢ Fun 𝐹 & ⊢ ◡𝐹 = 𝐹 & ⊢ (𝐹 “ 𝐴) ⊆ 𝐵 & ⊢ (𝐹 “ 𝐵) ⊆ 𝐴 & ⊢ 𝐴 ⊆ dom 𝐹 & ⊢ 𝐵 ⊆ dom 𝐹 ⇒ ⊢ (𝐹 ↾ 𝐴):𝐴–1-1-onto→𝐵 | ||
Theorem | fresf1o 30657 | Conditions for a restriction to be a one-to-one onto function. (Contributed by Thierry Arnoux, 7-Dec-2016.) |
⊢ ((Fun 𝐹 ∧ 𝐶 ⊆ ran 𝐹 ∧ Fun (◡𝐹 ↾ 𝐶)) → (𝐹 ↾ (◡𝐹 “ 𝐶)):(◡𝐹 “ 𝐶)–1-1-onto→𝐶) | ||
Theorem | nfpconfp 30658 | The set of fixed points of 𝐹 is the complement of the set of points moved by 𝐹. (Contributed by Thierry Arnoux, 17-Nov-2023.) |
⊢ (𝐹 Fn 𝐴 → (𝐴 ∖ dom (𝐹 ∖ I )) = dom (𝐹 ∩ I )) | ||
Theorem | fmptco1f1o 30659* | The action of composing (to the right) with a bijection is itself a bijection of functions. (Contributed by Thierry Arnoux, 3-Jan-2021.) |
⊢ 𝐴 = (𝑅 ↑m 𝐸) & ⊢ 𝐵 = (𝑅 ↑m 𝐷) & ⊢ 𝐹 = (𝑓 ∈ 𝐴 ↦ (𝑓 ∘ 𝑇)) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ 𝑋) & ⊢ (𝜑 → 𝑇:𝐷–1-1-onto→𝐸) ⇒ ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) | ||
Theorem | cofmpt2 30660* | Express composition of a maps-to function with another function in a maps-to notation. (Contributed by Thierry Arnoux, 15-Jul-2023.) |
⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑥)) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ 𝐸) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝐶) ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝐷)) | ||
Theorem | f1mptrn 30661* | Express injection for a mapping operation. (Contributed by Thierry Arnoux, 3-May-2020.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ∃!𝑥 ∈ 𝐴 𝑦 = 𝐵) ⇒ ⊢ (𝜑 → Fun ◡(𝑥 ∈ 𝐴 ↦ 𝐵)) | ||
Theorem | dfimafnf 30662* | Alternate definition of the image of a function. (Contributed by Raph Levien, 20-Nov-2006.) (Revised by Thierry Arnoux, 24-Apr-2017.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 ⇒ ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 “ 𝐴) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}) | ||
Theorem | funimass4f 30663 | Membership relation for the values of a function whose image is a subclass. (Contributed by Thierry Arnoux, 24-Apr-2017.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝐹 ⇒ ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → ((𝐹 “ 𝐴) ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) | ||
Theorem | elimampt 30664* | Membership in the image of a mapping. (Contributed by Thierry Arnoux, 3-Jan-2022.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) & ⊢ (𝜑 → 𝐷 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝐶 ∈ (𝐹 “ 𝐷) ↔ ∃𝑥 ∈ 𝐷 𝐶 = 𝐵)) | ||
Theorem | suppss2f 30665* | Show that the support of a function is contained in a set. (Contributed by Thierry Arnoux, 22-Jun-2017.) (Revised by AV, 1-Sep-2020.) |
⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐴 & ⊢ Ⅎ𝑘𝑊 & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → 𝐵 = 𝑍) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 𝑍) ⊆ 𝑊) | ||
Theorem | fovcld 30666 | Closure law for an operation. (Contributed by NM, 19-Apr-2007.) (Revised by Thierry Arnoux, 17-Feb-2017.) |
⊢ (𝜑 → 𝐹:(𝑅 × 𝑆)⟶𝐶) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶) | ||
Theorem | ofrn 30667 | The range of the function operation. (Contributed by Thierry Arnoux, 8-Jan-2017.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐵) & ⊢ (𝜑 → + :(𝐵 × 𝐵)⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ran (𝐹 ∘f + 𝐺) ⊆ 𝐶) | ||
Theorem | ofrn2 30668 | The range of the function operation. (Contributed by Thierry Arnoux, 21-Mar-2017.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐵) & ⊢ (𝜑 → + :(𝐵 × 𝐵)⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ran (𝐹 ∘f + 𝐺) ⊆ ( + “ (ran 𝐹 × ran 𝐺))) | ||
Theorem | off2 30669* | The function operation produces a function - alternative form with all antecedents as deduction. (Contributed by Thierry Arnoux, 17-Feb-2017.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐺:𝐵⟶𝑇) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = 𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺):𝐶⟶𝑈) | ||
Theorem | ofresid 30670 | Applying an operation restricted to the range of the functions does not change the function operation. (Contributed by Thierry Arnoux, 14-Feb-2018.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝐹 ∘f (𝑅 ↾ (𝐵 × 𝐵))𝐺)) | ||
Theorem | fimarab 30671* | Expressing the image of a set as a restricted abstract builder. (Contributed by Thierry Arnoux, 27-Jan-2020.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑋 ⊆ 𝐴) → (𝐹 “ 𝑋) = {𝑦 ∈ 𝐵 ∣ ∃𝑥 ∈ 𝑋 (𝐹‘𝑥) = 𝑦}) | ||
Theorem | unipreima 30672* | Preimage of a class union. (Contributed by Thierry Arnoux, 7-Feb-2017.) |
⊢ (Fun 𝐹 → (◡𝐹 “ ∪ 𝐴) = ∪ 𝑥 ∈ 𝐴 (◡𝐹 “ 𝑥)) | ||
Theorem | opfv 30673 | Value of a function producing ordered pairs. (Contributed by Thierry Arnoux, 3-Jan-2017.) |
⊢ (((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) = 〈((1st ∘ 𝐹)‘𝑥), ((2nd ∘ 𝐹)‘𝑥)〉) | ||
Theorem | xppreima 30674 | The preimage of a Cartesian product is the intersection of the preimages of each component function. (Contributed by Thierry Arnoux, 6-Jun-2017.) |
⊢ ((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) → (◡𝐹 “ (𝑌 × 𝑍)) = ((◡(1st ∘ 𝐹) “ 𝑌) ∩ (◡(2nd ∘ 𝐹) “ 𝑍))) | ||
Theorem | 2ndimaxp 30675 | Image of a cartesian product by 2nd. (Contributed by Thierry Arnoux, 23-Jun-2024.) |
⊢ (𝐴 ≠ ∅ → (2nd “ (𝐴 × 𝐵)) = 𝐵) | ||
Theorem | djussxp2 30676* | Stronger version of djussxp 5703. (Contributed by Thierry Arnoux, 23-Jun-2024.) |
⊢ ∪ 𝑘 ∈ 𝐴 ({𝑘} × 𝐵) ⊆ (𝐴 × ∪ 𝑘 ∈ 𝐴 𝐵) | ||
Theorem | 2ndresdju 30677* | The 2nd function restricted to a disjoint union is injective. (Contributed by Thierry Arnoux, 23-Jun-2024.) |
⊢ 𝑈 = ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑊) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝑋 𝐶) & ⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴) ⇒ ⊢ (𝜑 → (2nd ↾ 𝑈):𝑈–1-1→𝐴) | ||
Theorem | 2ndresdjuf1o 30678* | The 2nd function restricted to a disjoint union is a bijection. See also e.g. 2ndconst 7858. (Contributed by Thierry Arnoux, 23-Jun-2024.) |
⊢ 𝑈 = ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑊) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝑋 𝐶) & ⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴) ⇒ ⊢ (𝜑 → (2nd ↾ 𝑈):𝑈–1-1-onto→𝐴) | ||
Theorem | xppreima2 30679* | The preimage of a Cartesian product is the intersection of the preimages of each component function. (Contributed by Thierry Arnoux, 7-Jun-2017.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐶) & ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ⇒ ⊢ (𝜑 → (◡𝐻 “ (𝑌 × 𝑍)) = ((◡𝐹 “ 𝑌) ∩ (◡𝐺 “ 𝑍))) | ||
Theorem | elunirn2 30680 | Condition for the membership in the union of the range of a function. (Contributed by Thierry Arnoux, 13-Nov-2016.) |
⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (𝐹‘𝐴)) → 𝐵 ∈ ∪ ran 𝐹) | ||
Theorem | abfmpunirn 30681* | Membership in a union of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 28-Sep-2016.) |
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∣ 𝜑}) & ⊢ {𝑦 ∣ 𝜑} ∈ V & ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐵 ∈ ∪ ran 𝐹 ↔ (𝐵 ∈ V ∧ ∃𝑥 ∈ 𝑉 𝜓)) | ||
Theorem | rabfmpunirn 30682* | Membership in a union of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 30-Sep-2016.) |
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ 𝑊 ∣ 𝜑}) & ⊢ 𝑊 ∈ V & ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐵 ∈ ∪ ran 𝐹 ↔ ∃𝑥 ∈ 𝑉 (𝐵 ∈ 𝑊 ∧ 𝜓)) | ||
Theorem | abfmpeld 30683* | Membership in an element of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 19-Oct-2016.) |
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∣ 𝜓}) & ⊢ (𝜑 → {𝑦 ∣ 𝜓} ∈ V) & ⊢ (𝜑 → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∈ (𝐹‘𝐴) ↔ 𝜒))) | ||
Theorem | abfmpel 30684* | Membership in an element of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 19-Oct-2016.) |
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∣ 𝜑}) & ⊢ {𝑦 ∣ 𝜑} ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∈ (𝐹‘𝐴) ↔ 𝜓)) | ||
Theorem | fmptdF 30685 | Domain and codomain of the mapping operation; deduction form. This version of fmptd 6920 uses bound-variable hypothesis instead of distinct variable conditions. (Contributed by Thierry Arnoux, 28-Mar-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) | ||
Theorem | fmptcof2 30686* | Composition of two functions expressed as ordered-pair class abstractions. (Contributed by FL, 21-Jun-2012.) (Revised by Mario Carneiro, 24-Jul-2014.) (Revised by Thierry Arnoux, 10-May-2017.) |
⊢ Ⅎ𝑥𝑆 & ⊢ Ⅎ𝑦𝑇 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑅)) & ⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐵 ↦ 𝑆)) & ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴 ↦ 𝑇)) | ||
Theorem | fcomptf 30687* | Express composition of two functions as a maps-to applying both in sequence. This version has one less distinct variable restriction compared to fcompt 6937. (Contributed by Thierry Arnoux, 30-Jun-2017.) |
⊢ Ⅎ𝑥𝐵 ⇒ ⊢ ((𝐴:𝐷⟶𝐸 ∧ 𝐵:𝐶⟶𝐷) → (𝐴 ∘ 𝐵) = (𝑥 ∈ 𝐶 ↦ (𝐴‘(𝐵‘𝑥)))) | ||
Theorem | acunirnmpt 30688* | Axiom of choice for the union of the range of a mapping to function. (Contributed by Thierry Arnoux, 6-Nov-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅) & ⊢ 𝐶 = ran (𝑗 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:𝐶⟶∪ 𝐶 ∧ ∀𝑦 ∈ 𝐶 ∃𝑗 ∈ 𝐴 (𝑓‘𝑦) ∈ 𝐵)) | ||
Theorem | acunirnmpt2 30689* | Axiom of choice for the union of the range of a mapping to function. (Contributed by Thierry Arnoux, 7-Nov-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅) & ⊢ 𝐶 = ∪ ran (𝑗 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝑗 = (𝑓‘𝑥) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷)) | ||
Theorem | acunirnmpt2f 30690* | Axiom of choice for the union of the range of a mapping to function. (Contributed by Thierry Arnoux, 7-Nov-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅) & ⊢ Ⅎ𝑗𝐴 & ⊢ Ⅎ𝑗𝐶 & ⊢ Ⅎ𝑗𝐷 & ⊢ 𝐶 = ∪ 𝑗 ∈ 𝐴 𝐵 & ⊢ (𝑗 = (𝑓‘𝑥) → 𝐵 = 𝐷) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷)) | ||
Theorem | aciunf1lem 30691* | Choice in an index union. (Contributed by Thierry Arnoux, 8-Nov-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅) & ⊢ Ⅎ𝑗𝐴 & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑥)) = 𝑥)) | ||
Theorem | aciunf1 30692* | Choice in an index union. (Contributed by Thierry Arnoux, 4-May-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑘)) = 𝑘)) | ||
Theorem | ofoprabco 30693* | Function operation as a composition with an operation. (Contributed by Thierry Arnoux, 4-Jun-2017.) |
⊢ Ⅎ𝑎𝑀 & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 = (𝑎 ∈ 𝐴 ↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉)) & ⊢ (𝜑 → 𝑁 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦))) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑁 ∘ 𝑀)) | ||
Theorem | ofpreima 30694* | Express the preimage of a function operation as a union of preimages. (Contributed by Thierry Arnoux, 8-Mar-2018.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 Fn (𝐵 × 𝐶)) ⇒ ⊢ (𝜑 → (◡(𝐹 ∘f 𝑅𝐺) “ 𝐷) = ∪ 𝑝 ∈ (◡𝑅 “ 𝐷)((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) | ||
Theorem | ofpreima2 30695* | Express the preimage of a function operation as a union of preimages. This version of ofpreima 30694 iterates the union over a smaller set. (Contributed by Thierry Arnoux, 8-Mar-2018.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 Fn (𝐵 × 𝐶)) ⇒ ⊢ (𝜑 → (◡(𝐹 ∘f 𝑅𝐺) “ 𝐷) = ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) | ||
Theorem | funcnvmpt 30696* | Condition for a function in maps-to notation to be single-rooted. (Contributed by Thierry Arnoux, 28-Feb-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (Fun ◡𝐹 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 = 𝐵)) | ||
Theorem | funcnv5mpt 30697* | Two ways to say that a function in maps-to notation is single-rooted. (Contributed by Thierry Arnoux, 1-Mar-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝑥 = 𝑧 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (Fun ◡𝐹 ↔ ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥 = 𝑧 ∨ 𝐵 ≠ 𝐶))) | ||
Theorem | funcnv4mpt 30698* | Two ways to say that a function in maps-to notation is single-rooted. (Contributed by Thierry Arnoux, 2-Mar-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (Fun ◡𝐹 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑗 / 𝑥⦌𝐵))) | ||
Theorem | preimane 30699 | Different elements have different preimages. (Contributed by Thierry Arnoux, 7-May-2023.) |
⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐹) & ⊢ (𝜑 → 𝑌 ∈ ran 𝐹) ⇒ ⊢ (𝜑 → (◡𝐹 “ {𝑋}) ≠ (◡𝐹 “ {𝑌})) | ||
Theorem | fnpreimac 30700* | Choose a set 𝑥 containing a preimage of each element of a given set 𝐵. (Contributed by Thierry Arnoux, 7-May-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |