![]() |
Metamath
Proof Explorer Theorem List (p. 326 of 485) | < 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: | ![]() (1-30800) |
![]() (30801-32323) |
![]() (32324-48424) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | f1mptrn 32501* | Express injection for a mapping operation. (Contributed by Thierry Arnoux, 3-May-2020.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ∃!𝑥 ∈ 𝐴 𝑦 = 𝐵) ⇒ ⊢ (𝜑 → Fun ◡(𝑥 ∈ 𝐴 ↦ 𝐵)) | ||
Theorem | dfimafnf 32502* | 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 32503 | Membership relation for the values of a function whose image is a subclass. (Contributed by Thierry Arnoux, 24-Apr-2017.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝐹 ⇒ ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → ((𝐹 “ 𝐴) ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) | ||
Theorem | elimampt 32504* | Membership in the image of a mapping. (Contributed by Thierry Arnoux, 3-Jan-2022.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) & ⊢ (𝜑 → 𝐷 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝐶 ∈ (𝐹 “ 𝐷) ↔ ∃𝑥 ∈ 𝐷 𝐶 = 𝐵)) | ||
Theorem | suppss2f 32505* | 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 | ofrn 32506 | The range of the function operation. (Contributed by Thierry Arnoux, 8-Jan-2017.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐵) & ⊢ (𝜑 → + :(𝐵 × 𝐵)⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ran (𝐹 ∘f + 𝐺) ⊆ 𝐶) | ||
Theorem | ofrn2 32507 | The range of the function operation. (Contributed by Thierry Arnoux, 21-Mar-2017.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐵) & ⊢ (𝜑 → + :(𝐵 × 𝐵)⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ran (𝐹 ∘f + 𝐺) ⊆ ( + “ (ran 𝐹 × ran 𝐺))) | ||
Theorem | off2 32508* | The function operation produces a function - alternative form with all antecedents as deduction. (Contributed by Thierry Arnoux, 17-Feb-2017.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐺:𝐵⟶𝑇) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = 𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺):𝐶⟶𝑈) | ||
Theorem | ofresid 32509 | 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 32510* | Expressing the image of a set as a restricted abstract builder. (Contributed by Thierry Arnoux, 27-Jan-2020.) |
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑋 ⊆ 𝐴) → (𝐹 “ 𝑋) = {𝑦 ∈ 𝐵 ∣ ∃𝑥 ∈ 𝑋 (𝐹‘𝑥) = 𝑦}) | ||
Theorem | unipreima 32511* | Preimage of a class union. (Contributed by Thierry Arnoux, 7-Feb-2017.) |
⊢ (Fun 𝐹 → (◡𝐹 “ ∪ 𝐴) = ∪ 𝑥 ∈ 𝐴 (◡𝐹 “ 𝑥)) | ||
Theorem | opfv 32512 | Value of a function producing ordered pairs. (Contributed by Thierry Arnoux, 3-Jan-2017.) |
⊢ (((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) = 〈((1st ∘ 𝐹)‘𝑥), ((2nd ∘ 𝐹)‘𝑥)〉) | ||
Theorem | xppreima 32513 | 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 32514 | Image of a cartesian product by 2nd. (Contributed by Thierry Arnoux, 23-Jun-2024.) |
⊢ (𝐴 ≠ ∅ → (2nd “ (𝐴 × 𝐵)) = 𝐵) | ||
Theorem | djussxp2 32515* | Stronger version of djussxp 5848. (Contributed by Thierry Arnoux, 23-Jun-2024.) |
⊢ ∪ 𝑘 ∈ 𝐴 ({𝑘} × 𝐵) ⊆ (𝐴 × ∪ 𝑘 ∈ 𝐴 𝐵) | ||
Theorem | 2ndresdju 32516* | The 2nd function restricted to a disjoint union is injective. (Contributed by Thierry Arnoux, 23-Jun-2024.) |
⊢ 𝑈 = ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑊) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝑋 𝐶) & ⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴) ⇒ ⊢ (𝜑 → (2nd ↾ 𝑈):𝑈–1-1→𝐴) | ||
Theorem | 2ndresdjuf1o 32517* | The 2nd function restricted to a disjoint union is a bijection. See also e.g. 2ndconst 8106. (Contributed by Thierry Arnoux, 23-Jun-2024.) |
⊢ 𝑈 = ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑊) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝑋 𝐶) & ⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴) ⇒ ⊢ (𝜑 → (2nd ↾ 𝑈):𝑈–1-1-onto→𝐴) | ||
Theorem | xppreima2 32518* | The preimage of a Cartesian product is the intersection of the preimages of each component function. (Contributed by Thierry Arnoux, 7-Jun-2017.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐶) & ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ⇒ ⊢ (𝜑 → (◡𝐻 “ (𝑌 × 𝑍)) = ((◡𝐹 “ 𝑌) ∩ (◡𝐺 “ 𝑍))) | ||
Theorem | abfmpunirn 32519* | Membership in a union of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 28-Sep-2016.) |
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∣ 𝜑}) & ⊢ {𝑦 ∣ 𝜑} ∈ V & ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐵 ∈ ∪ ran 𝐹 ↔ (𝐵 ∈ V ∧ ∃𝑥 ∈ 𝑉 𝜓)) | ||
Theorem | rabfmpunirn 32520* | Membership in a union of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 30-Sep-2016.) |
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ 𝑊 ∣ 𝜑}) & ⊢ 𝑊 ∈ V & ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐵 ∈ ∪ ran 𝐹 ↔ ∃𝑥 ∈ 𝑉 (𝐵 ∈ 𝑊 ∧ 𝜓)) | ||
Theorem | abfmpeld 32521* | Membership in an element of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 19-Oct-2016.) |
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∣ 𝜓}) & ⊢ (𝜑 → {𝑦 ∣ 𝜓} ∈ V) & ⊢ (𝜑 → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∈ (𝐹‘𝐴) ↔ 𝜒))) | ||
Theorem | abfmpel 32522* | Membership in an element of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 19-Oct-2016.) |
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∣ 𝜑}) & ⊢ {𝑦 ∣ 𝜑} ∈ V & ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐵 ∈ (𝐹‘𝐴) ↔ 𝜓)) | ||
Theorem | fmptdF 32523 | Domain and codomain of the mapping operation; deduction form. This version of fmptd 7123 uses bound-variable hypothesis instead of distinct variable conditions. (Contributed by Thierry Arnoux, 28-Mar-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐶 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) | ||
Theorem | fmptcof2 32524* | 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 32525* | Express composition of two functions as a maps-to applying both in sequence. This version has one less distinct variable restriction compared to fcompt 7142. (Contributed by Thierry Arnoux, 30-Jun-2017.) |
⊢ Ⅎ𝑥𝐵 ⇒ ⊢ ((𝐴:𝐷⟶𝐸 ∧ 𝐵:𝐶⟶𝐷) → (𝐴 ∘ 𝐵) = (𝑥 ∈ 𝐶 ↦ (𝐴‘(𝐵‘𝑥)))) | ||
Theorem | acunirnmpt 32526* | Axiom of choice for the union of the range of a mapping to function. (Contributed by Thierry Arnoux, 6-Nov-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅) & ⊢ 𝐶 = ran (𝑗 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:𝐶⟶∪ 𝐶 ∧ ∀𝑦 ∈ 𝐶 ∃𝑗 ∈ 𝐴 (𝑓‘𝑦) ∈ 𝐵)) | ||
Theorem | acunirnmpt2 32527* | Axiom of choice for the union of the range of a mapping to function. (Contributed by Thierry Arnoux, 7-Nov-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅) & ⊢ 𝐶 = ∪ ran (𝑗 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝑗 = (𝑓‘𝑥) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷)) | ||
Theorem | acunirnmpt2f 32528* | Axiom of choice for the union of the range of a mapping to function. (Contributed by Thierry Arnoux, 7-Nov-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅) & ⊢ Ⅎ𝑗𝐴 & ⊢ Ⅎ𝑗𝐶 & ⊢ Ⅎ𝑗𝐷 & ⊢ 𝐶 = ∪ 𝑗 ∈ 𝐴 𝐵 & ⊢ (𝑗 = (𝑓‘𝑥) → 𝐵 = 𝐷) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷)) | ||
Theorem | aciunf1lem 32529* | Choice in an index union. (Contributed by Thierry Arnoux, 8-Nov-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅) & ⊢ Ⅎ𝑗𝐴 & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑥)) = 𝑥)) | ||
Theorem | aciunf1 32530* | Choice in an index union. (Contributed by Thierry Arnoux, 4-May-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑘)) = 𝑘)) | ||
Theorem | ofoprabco 32531* | Function operation as a composition with an operation. (Contributed by Thierry Arnoux, 4-Jun-2017.) |
⊢ Ⅎ𝑎𝑀 & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 = (𝑎 ∈ 𝐴 ↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉)) & ⊢ (𝜑 → 𝑁 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦))) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑁 ∘ 𝑀)) | ||
Theorem | ofpreima 32532* | 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 32533* | Express the preimage of a function operation as a union of preimages. This version of ofpreima 32532 iterates the union over a smaller set. (Contributed by Thierry Arnoux, 8-Mar-2018.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 Fn (𝐵 × 𝐶)) ⇒ ⊢ (𝜑 → (◡(𝐹 ∘f 𝑅𝐺) “ 𝐷) = ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) | ||
Theorem | funcnvmpt 32534* | Condition for a function in maps-to notation to be single-rooted. (Contributed by Thierry Arnoux, 28-Feb-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (Fun ◡𝐹 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 = 𝐵)) | ||
Theorem | funcnv5mpt 32535* | Two ways to say that a function in maps-to notation is single-rooted. (Contributed by Thierry Arnoux, 1-Mar-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝑥 = 𝑧 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (Fun ◡𝐹 ↔ ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥 = 𝑧 ∨ 𝐵 ≠ 𝐶))) | ||
Theorem | funcnv4mpt 32536* | Two ways to say that a function in maps-to notation is single-rooted. (Contributed by Thierry Arnoux, 2-Mar-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (Fun ◡𝐹 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑗 / 𝑥⦌𝐵))) | ||
Theorem | preimane 32537 | Different elements have different preimages. (Contributed by Thierry Arnoux, 7-May-2023.) |
⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐹) & ⊢ (𝜑 → 𝑌 ∈ ran 𝐹) ⇒ ⊢ (𝜑 → (◡𝐹 “ {𝑋}) ≠ (◡𝐹 “ {𝑌})) | ||
Theorem | fnpreimac 32538* | Choose a set 𝑥 containing a preimage of each element of a given set 𝐵. (Contributed by Thierry Arnoux, 7-May-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵)) | ||
Theorem | fgreu 32539* | Exactly one point of a function's graph has a given first element. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
⊢ ((Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹) → ∃!𝑝 ∈ 𝐹 𝑋 = (1st ‘𝑝)) | ||
Theorem | fcnvgreu 32540* | If the converse of a relation 𝐴 is a function, exactly one point of its graph has a given second element (that is, function value). (Contributed by Thierry Arnoux, 1-Apr-2018.) |
⊢ (((Rel 𝐴 ∧ Fun ◡𝐴) ∧ 𝑌 ∈ ran 𝐴) → ∃!𝑝 ∈ 𝐴 𝑌 = (2nd ‘𝑝)) | ||
Theorem | rnmposs 32541* | The range of an operation given by the maps-to notation as a subset. (Contributed by Thierry Arnoux, 23-May-2017.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 → ran 𝐹 ⊆ 𝐷) | ||
Theorem | mptssALT 32542* | Deduce subset relation of mapping-to function graphs from a subset relation of domains. Alternative proof of mptss 6047. (Contributed by Thierry Arnoux, 30-May-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⊆ (𝑥 ∈ 𝐵 ↦ 𝐶)) | ||
Theorem | dfcnv2 32543* | Alternative definition of the converse of a relation. (Contributed by Thierry Arnoux, 31-Mar-2018.) |
⊢ (ran 𝑅 ⊆ 𝐴 → ◡𝑅 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (◡𝑅 “ {𝑥}))) | ||
Theorem | fnimatp 32544 | The image of an unordered triple under a function. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
⊢ (𝜑 → 𝐹 Fn 𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝐹 “ {𝐴, 𝐵, 𝐶}) = {(𝐹‘𝐴), (𝐹‘𝐵), (𝐹‘𝐶)}) | ||
Theorem | mpomptxf 32545* | Express a two-argument function as a one-argument function, or vice-versa. In this version 𝐵(𝑥) is not assumed to be constant w.r.t 𝑥. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by Thierry Arnoux, 31-Mar-2018.) |
⊢ Ⅎ𝑥𝐶 & ⊢ Ⅎ𝑦𝐶 & ⊢ (𝑧 = 〈𝑥, 𝑦〉 → 𝐶 = 𝐷) ⇒ ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) | ||
Theorem | of0r 32546 | Function operation with the empty function. (Contributed by Thierry Arnoux, 27-May-2025.) |
⊢ (𝐹 ∘f 𝑅∅) = ∅ | ||
Theorem | suppovss 32547* | A bound for the support of an operation. (Contributed by Thierry Arnoux, 19-Jul-2023.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ 𝐶)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝑍 ∈ 𝐷) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ ((𝐺 supp (𝐵 × {𝑍})) × ∪ 𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))) | ||
Theorem | suppiniseg 32548 | Relation between the support (𝐹 supp 𝑍) and the initial segment (◡𝐹 “ {𝑍}). (Contributed by Thierry Arnoux, 25-Jun-2024.) |
⊢ ((Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (dom 𝐹 ∖ (𝐹 supp 𝑍)) = (◡𝐹 “ {𝑍})) | ||
Theorem | fsuppinisegfi 32549 | The initial segment (◡𝐹 “ {𝑌}) of a nonzero 𝑌 is finite if 𝐹 has finite support. (Contributed by Thierry Arnoux, 21-Jun-2024.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 0 ∈ 𝑊) & ⊢ (𝜑 → 𝑌 ∈ (V ∖ { 0 })) & ⊢ (𝜑 → 𝐹 finSupp 0 ) ⇒ ⊢ (𝜑 → (◡𝐹 “ {𝑌}) ∈ Fin) | ||
Theorem | fressupp 32550 | The restriction of a function to its support. (Contributed by Thierry Arnoux, 25-Jun-2024.) |
⊢ ((Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 ↾ (𝐹 supp 𝑍)) = (𝐹 ∖ (V × {𝑍}))) | ||
Theorem | fdifsuppconst 32551 | A function is a zero constant outside of its support. (Contributed by Thierry Arnoux, 22-Jun-2024.) |
⊢ 𝐴 = (dom 𝐹 ∖ (𝐹 supp 𝑍)) ⇒ ⊢ ((Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 ↾ 𝐴) = (𝐴 × {𝑍})) | ||
Theorem | ressupprn 32552 | The range of a function restricted to its support. (Contributed by Thierry Arnoux, 25-Jun-2024.) |
⊢ ((Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 0 ∈ 𝑊) → ran (𝐹 ↾ (𝐹 supp 0 )) = (ran 𝐹 ∖ { 0 })) | ||
Theorem | supppreima 32553 | Express the support of a function as the preimage of its range except zero. (Contributed by Thierry Arnoux, 24-Jun-2024.) |
⊢ ((Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 supp 𝑍) = (◡𝐹 “ (ran 𝐹 ∖ {𝑍}))) | ||
Theorem | fsupprnfi 32554 | Finite support implies finite range. (Contributed by Thierry Arnoux, 24-Jun-2024.) |
⊢ (((Fun 𝐹 ∧ 𝐹 ∈ 𝑉) ∧ ( 0 ∈ 𝑊 ∧ 𝐹 finSupp 0 )) → ran 𝐹 ∈ Fin) | ||
Theorem | mptiffisupp 32555* | Conditions for a mapping function defined with a conditional to have finite support. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ if(𝑥 ∈ 𝐵, 𝐶, 𝑍)) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐹 finSupp 𝑍) | ||
Theorem | cosnopne 32556 | Composition of two ordered pair singletons with non-matching domain and range. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐴 ≠ 𝐷) ⇒ ⊢ (𝜑 → ({〈𝐴, 𝐵〉} ∘ {〈𝐶, 𝐷〉}) = ∅) | ||
Theorem | cosnop 32557 | Composition of two ordered pair singletons with matching domain and range. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) ⇒ ⊢ (𝜑 → ({〈𝐴, 𝐵〉} ∘ {〈𝐶, 𝐴〉}) = {〈𝐶, 𝐵〉}) | ||
Theorem | cnvprop 32558 | Converse of a pair of ordered pairs. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊)) → ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {〈𝐵, 𝐴〉, 〈𝐷, 𝐶〉}) | ||
Theorem | brprop 32559 | Binary relation for a pair of ordered pairs. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝑋{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉}𝑌 ↔ ((𝑋 = 𝐴 ∧ 𝑌 = 𝐵) ∨ (𝑋 = 𝐶 ∧ 𝑌 = 𝐷)))) | ||
Theorem | mptprop 32560* | Rewrite pairs of ordered pairs as mapping to functions. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) ⇒ ⊢ (𝜑 → {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = (𝑥 ∈ {𝐴, 𝐶} ↦ if(𝑥 = 𝐴, 𝐵, 𝐷))) | ||
Theorem | coprprop 32561 | Composition of two pairs of ordered pairs with matching domain and range. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) & ⊢ (𝜑 → 𝐸 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 ∈ 𝑋) & ⊢ (𝜑 → 𝐸 ≠ 𝐹) ⇒ ⊢ (𝜑 → ({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∘ {〈𝐸, 𝐴〉, 〈𝐹, 𝐶〉}) = {〈𝐸, 𝐵〉, 〈𝐹, 𝐷〉}) | ||
Theorem | gtiso 32562 | Two ways to write a strictly decreasing function on the reals. (Contributed by Thierry Arnoux, 6-Apr-2017.) |
⊢ ((𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ*) → (𝐹 Isom < , ◡ < (𝐴, 𝐵) ↔ 𝐹 Isom ≤ , ◡ ≤ (𝐴, 𝐵))) | ||
Theorem | isoun 32563* | Infer an isomorphism from a union of two isomorphisms. (Contributed by Thierry Arnoux, 30-Mar-2017.) |
⊢ (𝜑 → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → 𝐺 Isom 𝑅, 𝑆 (𝐶, 𝐷)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) → 𝑥𝑅𝑦) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐷) → 𝑧𝑆𝑤) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴) → ¬ 𝑥𝑅𝑦) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐵) → ¬ 𝑧𝑆𝑤) & ⊢ (𝜑 → (𝐴 ∩ 𝐶) = ∅) & ⊢ (𝜑 → (𝐵 ∩ 𝐷) = ∅) ⇒ ⊢ (𝜑 → (𝐻 ∪ 𝐺) Isom 𝑅, 𝑆 ((𝐴 ∪ 𝐶), (𝐵 ∪ 𝐷))) | ||
Theorem | disjdsct 32564* | A disjoint collection is distinct, i.e. each set in this collection is different of all others, provided that it does not contain the empty set This can be expressed as "the converse of the mapping function is a function", or "the mapping function is single-rooted". (Cf. funcnv 6623) (Contributed by Thierry Arnoux, 28-Feb-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (𝑉 ∖ {∅})) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) ⇒ ⊢ (𝜑 → Fun ◡(𝑥 ∈ 𝐴 ↦ 𝐵)) | ||
Theorem | df1stres 32565* | Definition for a restriction of the 1st (first member of an ordered pair) function. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
⊢ (1st ↾ (𝐴 × 𝐵)) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑥) | ||
Theorem | df2ndres 32566* | Definition for a restriction of the 2nd (second member of an ordered pair) function. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
⊢ (2nd ↾ (𝐴 × 𝐵)) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑦) | ||
Theorem | 1stpreimas 32567 | The preimage of a singleton. (Contributed by Thierry Arnoux, 27-Apr-2020.) |
⊢ ((Rel 𝐴 ∧ 𝑋 ∈ 𝑉) → (◡(1st ↾ 𝐴) “ {𝑋}) = ({𝑋} × (𝐴 “ {𝑋}))) | ||
Theorem | 1stpreima 32568 | The preimage by 1st is a 'vertical band'. (Contributed by Thierry Arnoux, 13-Oct-2017.) |
⊢ (𝐴 ⊆ 𝐵 → (◡(1st ↾ (𝐵 × 𝐶)) “ 𝐴) = (𝐴 × 𝐶)) | ||
Theorem | 2ndpreima 32569 | The preimage by 2nd is an 'horizontal band'. (Contributed by Thierry Arnoux, 13-Oct-2017.) |
⊢ (𝐴 ⊆ 𝐶 → (◡(2nd ↾ (𝐵 × 𝐶)) “ 𝐴) = (𝐵 × 𝐴)) | ||
Theorem | curry2ima 32570* | The image of a curried function with a constant second argument. (Contributed by Thierry Arnoux, 25-Sep-2017.) |
⊢ 𝐺 = (𝐹 ∘ ◡(1st ↾ (V × {𝐶}))) ⇒ ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵 ∧ 𝐷 ⊆ 𝐴) → (𝐺 “ 𝐷) = {𝑦 ∣ ∃𝑥 ∈ 𝐷 𝑦 = (𝑥𝐹𝐶)}) | ||
Theorem | preiman0 32571 | The preimage of a nonempty set is nonempty. (Contributed by Thierry Arnoux, 9-Jun-2024.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ≠ ∅) → (◡𝐹 “ 𝐴) ≠ ∅) | ||
Theorem | intimafv 32572* | The intersection of an image set, as an indexed intersection of function values. (Contributed by Thierry Arnoux, 15-Jun-2024.) |
⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → ∩ (𝐹 “ 𝐴) = ∩ 𝑥 ∈ 𝐴 (𝐹‘𝑥)) | ||
Theorem | supssd 32573* | Inequality deduction for supremum of a subset. (Contributed by Thierry Arnoux, 21-Mar-2017.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → ¬ sup(𝐶, 𝐴, 𝑅)𝑅sup(𝐵, 𝐴, 𝑅)) | ||
Theorem | infssd 32574* | Inequality deduction for infimum of a subset. (Contributed by AV, 4-Oct-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝐶 ⊆ 𝐵) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐶 𝑧𝑅𝑦))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → ¬ inf(𝐶, 𝐴, 𝑅)𝑅inf(𝐵, 𝐴, 𝑅)) | ||
Theorem | imafi2 32575 | The image by a finite set is finite. See also imafi 9200. (Contributed by Thierry Arnoux, 25-Apr-2020.) |
⊢ (𝐴 ∈ Fin → (𝐴 “ 𝐵) ∈ Fin) | ||
Theorem | unifi3 32576 | If a union is finite, then all its elements are finite. See unifi 9367. (Contributed by Thierry Arnoux, 27-Aug-2017.) |
⊢ (∪ 𝐴 ∈ Fin → 𝐴 ⊆ Fin) | ||
Theorem | snct 32577 | A singleton is countable. (Contributed by Thierry Arnoux, 16-Sep-2016.) |
⊢ (𝐴 ∈ 𝑉 → {𝐴} ≼ ω) | ||
Theorem | prct 32578 | An unordered pair is countable. (Contributed by Thierry Arnoux, 16-Sep-2016.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ≼ ω) | ||
Theorem | mpocti 32579* | An operation is countable if both its domains are countable. (Contributed by Thierry Arnoux, 17-Sep-2017.) |
⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 ⇒ ⊢ ((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ≼ ω) | ||
Theorem | abrexct 32580* | An image set of a countable set is countable. (Contributed by Thierry Arnoux, 29-Dec-2016.) |
⊢ (𝐴 ≼ ω → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ≼ ω) | ||
Theorem | mptctf 32581 | A countable mapping set is countable, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 ≼ ω → (𝑥 ∈ 𝐴 ↦ 𝐵) ≼ ω) | ||
Theorem | abrexctf 32582* | An image set of a countable set is countable, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 ≼ ω → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ≼ ω) | ||
Theorem | padct 32583* | Index a countable set with integers and pad with 𝑍. (Contributed by Thierry Arnoux, 1-Jun-2020.) |
⊢ ((𝐴 ≼ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) | ||
Theorem | cnvoprabOLD 32584* | The converse of a class abstraction of nested ordered pairs. Obsolete version of cnvoprab 8065 as of 16-Oct-2022, which has nonfreeness hypotheses instead of disjoint variable conditions. (Contributed by Thierry Arnoux, 17-Aug-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑎 = 〈𝑥, 𝑦〉 → (𝜓 ↔ 𝜑)) & ⊢ (𝜓 → 𝑎 ∈ (V × V)) ⇒ ⊢ ◡{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈𝑧, 𝑎〉 ∣ 𝜓} | ||
Theorem | f1od2 32585* | Sufficient condition for a binary function expressed in maps-to notation to be bijective. (Contributed by Thierry Arnoux, 17-Aug-2017.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → (𝐼 ∈ 𝑋 ∧ 𝐽 ∈ 𝑌)) & ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ (𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽)))) ⇒ ⊢ (𝜑 → 𝐹:(𝐴 × 𝐵)–1-1-onto→𝐷) | ||
Theorem | fcobij 32586* | Composing functions with a bijection yields a bijection between sets of functions. (Contributed by Thierry Arnoux, 25-Aug-2017.) |
⊢ (𝜑 → 𝐺:𝑆–1-1-onto→𝑇) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝑓 ∈ (𝑆 ↑m 𝑅) ↦ (𝐺 ∘ 𝑓)):(𝑆 ↑m 𝑅)–1-1-onto→(𝑇 ↑m 𝑅)) | ||
Theorem | fcobijfs 32587* | Composing finitely supported functions with a bijection yields a bijection between sets of finitely supported functions. See also mapfien 9433. (Contributed by Thierry Arnoux, 25-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
⊢ (𝜑 → 𝐺:𝑆–1-1-onto→𝑇) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ 𝑊) & ⊢ (𝜑 → 𝑂 ∈ 𝑆) & ⊢ 𝑄 = (𝐺‘𝑂) & ⊢ 𝑋 = {𝑔 ∈ (𝑆 ↑m 𝑅) ∣ 𝑔 finSupp 𝑂} & ⊢ 𝑌 = {ℎ ∈ (𝑇 ↑m 𝑅) ∣ ℎ finSupp 𝑄} ⇒ ⊢ (𝜑 → (𝑓 ∈ 𝑋 ↦ (𝐺 ∘ 𝑓)):𝑋–1-1-onto→𝑌) | ||
Theorem | suppss3 32588* | Deduce a function's support's inclusion in another function's support. (Contributed by Thierry Arnoux, 7-Sep-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝑍) → 𝐵 = 𝑍) ⇒ ⊢ (𝜑 → (𝐺 supp 𝑍) ⊆ (𝐹 supp 𝑍)) | ||
Theorem | fsuppcurry1 32589* | Finite support of a curried function with a constant first argument. (Contributed by Thierry Arnoux, 7-Jul-2023.) |
⊢ 𝐺 = (𝑥 ∈ 𝐵 ↦ (𝐶𝐹𝑥)) & ⊢ (𝜑 → 𝑍 ∈ 𝑈) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 Fn (𝐴 × 𝐵)) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐹 finSupp 𝑍) ⇒ ⊢ (𝜑 → 𝐺 finSupp 𝑍) | ||
Theorem | fsuppcurry2 32590* | Finite support of a curried function with a constant second argument. (Contributed by Thierry Arnoux, 7-Jul-2023.) |
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝑥𝐹𝐶)) & ⊢ (𝜑 → 𝑍 ∈ 𝑈) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 Fn (𝐴 × 𝐵)) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 finSupp 𝑍) ⇒ ⊢ (𝜑 → 𝐺 finSupp 𝑍) | ||
Theorem | offinsupp1 32591* | Finite support for a function operation. (Contributed by Thierry Arnoux, 8-Jul-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑇) & ⊢ (𝜑 → 𝐹 finSupp 𝑌) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝑌𝑅𝑥) = 𝑍) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) finSupp 𝑍) | ||
Theorem | ffs2 32592 | Rewrite a function's support based with its codomain rather than the universal class. See also fsuppeq 8180. (Contributed by Thierry Arnoux, 27-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
⊢ 𝐶 = (𝐵 ∖ {𝑍}) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 supp 𝑍) = (◡𝐹 “ 𝐶)) | ||
Theorem | ffsrn 32593 | The range of a finitely supported function is finite. (Contributed by Thierry Arnoux, 27-Aug-2017.) |
⊢ (𝜑 → 𝑍 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin) ⇒ ⊢ (𝜑 → ran 𝐹 ∈ Fin) | ||
Theorem | resf1o 32594* | Restriction of functions to a superset of their support creates a bijection. (Contributed by Thierry Arnoux, 12-Sep-2017.) |
⊢ 𝑋 = {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶} & ⊢ 𝐹 = (𝑓 ∈ 𝑋 ↦ (𝑓 ↾ 𝐶)) ⇒ ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) → 𝐹:𝑋–1-1-onto→(𝐵 ↑m 𝐶)) | ||
Theorem | maprnin 32595* | Restricting the range of the mapping operator. (Contributed by Thierry Arnoux, 30-Aug-2017.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐵 ∩ 𝐶) ↑m 𝐴) = {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ ran 𝑓 ⊆ 𝐶} | ||
Theorem | fpwrelmapffslem 32596* | Lemma for fpwrelmapffs 32598. For this theorem, the sets 𝐴 and 𝐵 could be infinite, but the relation 𝑅 itself is finite. (Contributed by Thierry Arnoux, 1-Sep-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝜑 → 𝐹:𝐴⟶𝒫 𝐵) & ⊢ (𝜑 → 𝑅 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}) ⇒ ⊢ (𝜑 → (𝑅 ∈ Fin ↔ (ran 𝐹 ⊆ Fin ∧ (𝐹 supp ∅) ∈ Fin))) | ||
Theorem | fpwrelmap 32597* | Define a canonical mapping between functions from 𝐴 into subsets of 𝐵 and the relations with domain 𝐴 and range within 𝐵. Note that the same relation is used in axdc2lem 10473 and marypha2lem1 9460. (Contributed by Thierry Arnoux, 28-Aug-2017.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝑀 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ⇒ ⊢ 𝑀:(𝒫 𝐵 ↑m 𝐴)–1-1-onto→𝒫 (𝐴 × 𝐵) | ||
Theorem | fpwrelmapffs 32598* | Define a canonical mapping between finite relations (finite subsets of a cartesian product) and functions with finite support into finite subsets. (Contributed by Thierry Arnoux, 28-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝑀 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) & ⊢ 𝑆 = {𝑓 ∈ ((𝒫 𝐵 ∩ Fin) ↑m 𝐴) ∣ (𝑓 supp ∅) ∈ Fin} ⇒ ⊢ (𝑀 ↾ 𝑆):𝑆–1-1-onto→(𝒫 (𝐴 × 𝐵) ∩ Fin) | ||
Theorem | creq0 32599 | The real representation of complex numbers is zero iff both its terms are zero. Cf. crne0 12238. (Contributed by Thierry Arnoux, 20-Aug-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 = 0 ∧ 𝐵 = 0) ↔ (𝐴 + (i · 𝐵)) = 0)) | ||
Theorem | 1nei 32600 | The imaginary unit i is not one. (Contributed by Thierry Arnoux, 20-Aug-2023.) |
⊢ 1 ≠ i |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |