![]() |
Metamath
Proof Explorer Theorem List (p. 74 of 486) | < 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-30851) |
![]() (30852-32374) |
![]() (32375-48553) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fcof1 7301 | 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 7302 | 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 7303* | 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 7304* | Change bound variable between domain and range of function. (Contributed by NM, 23-Feb-1997.) |
⊢ ((𝐹‘𝑥) = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐹:𝐴–onto→𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | cocan1 7305 | An injection is left-cancelable. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 21-Mar-2015.) |
⊢ ((𝐹:𝐵–1-1→𝐶 ∧ 𝐻:𝐴⟶𝐵 ∧ 𝐾:𝐴⟶𝐵) → ((𝐹 ∘ 𝐻) = (𝐹 ∘ 𝐾) ↔ 𝐻 = 𝐾)) | ||
Theorem | cocan2 7306 | A surjection is right-cancelable. (Contributed by FL, 21-Nov-2011.) (Proof shortened by Mario Carneiro, 21-Mar-2015.) |
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐻 Fn 𝐵 ∧ 𝐾 Fn 𝐵) → ((𝐻 ∘ 𝐹) = (𝐾 ∘ 𝐹) ↔ 𝐻 = 𝐾)) | ||
Theorem | fcof1oinvd 7307 | Show that a function is the inverse of a bijective function if their composition is the identity function. Formerly part of proof of fcof1o 7310. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by AV, 15-Dec-2019.) |
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) & ⊢ (𝜑 → (𝐹 ∘ 𝐺) = ( I ↾ 𝐵)) ⇒ ⊢ (𝜑 → ◡𝐹 = 𝐺) | ||
Theorem | fcof1od 7308 | A function is bijective if a "retraction" and a "section" exist, see comments for fcof1 7301 and fcofo 7302. Formerly part of proof of fcof1o 7310. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by AV, 15-Dec-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) & ⊢ (𝜑 → (𝐺 ∘ 𝐹) = ( I ↾ 𝐴)) & ⊢ (𝜑 → (𝐹 ∘ 𝐺) = ( I ↾ 𝐵)) ⇒ ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) | ||
Theorem | 2fcoidinvd 7309 | Show that a function is the inverse of a function if their compositions are the identity functions. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by AV, 15-Dec-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) & ⊢ (𝜑 → (𝐺 ∘ 𝐹) = ( I ↾ 𝐴)) & ⊢ (𝜑 → (𝐹 ∘ 𝐺) = ( I ↾ 𝐵)) ⇒ ⊢ (𝜑 → ◡𝐹 = 𝐺) | ||
Theorem | fcof1o 7310 | Show that two functions are inverse to each other by computing their compositions. (Contributed by Mario Carneiro, 21-Mar-2015.) (Proof shortened by AV, 15-Dec-2019.) |
⊢ (((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ((𝐹 ∘ 𝐺) = ( I ↾ 𝐵) ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐴))) → (𝐹:𝐴–1-1-onto→𝐵 ∧ ◡𝐹 = 𝐺)) | ||
Theorem | 2fvcoidd 7311* | Show that the composition of two functions is the identity function by applying both functions to each value of the domain of the first function. (Contributed by AV, 15-Dec-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) & ⊢ (𝜑 → ∀𝑎 ∈ 𝐴 (𝐺‘(𝐹‘𝑎)) = 𝑎) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = ( I ↾ 𝐴)) | ||
Theorem | 2fvidf1od 7312* | A function is bijective if it has an inverse function. (Contributed by AV, 15-Dec-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) & ⊢ (𝜑 → ∀𝑎 ∈ 𝐴 (𝐺‘(𝐹‘𝑎)) = 𝑎) & ⊢ (𝜑 → ∀𝑏 ∈ 𝐵 (𝐹‘(𝐺‘𝑏)) = 𝑏) ⇒ ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) | ||
Theorem | 2fvidinvd 7313* | Show that two functions are inverse to each other by applying them twice to each value of their domains. (Contributed by AV, 13-Dec-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) & ⊢ (𝜑 → ∀𝑎 ∈ 𝐴 (𝐺‘(𝐹‘𝑎)) = 𝑎) & ⊢ (𝜑 → ∀𝑏 ∈ 𝐵 (𝐹‘(𝐺‘𝑏)) = 𝑏) ⇒ ⊢ (𝜑 → ◡𝐹 = 𝐺) | ||
Theorem | foeqcnvco 7314 | Condition for function equality in terms of vanishing of the composition with the converse. EDITORIAL: Is there a relation-algebraic proof of this? (Contributed by Stefan O'Rear, 12-Feb-2015.) |
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) → (𝐹 = 𝐺 ↔ (𝐹 ∘ ◡𝐺) = ( I ↾ 𝐵))) | ||
Theorem | f1eqcocnv 7315 | Condition for function equality in terms of vanishing of the composition with the inverse. (Contributed by Stefan O'Rear, 12-Feb-2015.) (Proof shortened by Wolf Lammen, 29-May-2024.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → (𝐹 = 𝐺 ↔ (◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴))) | ||
Theorem | fveqf1o 7316 | Given a bijection 𝐹, produce another bijection 𝐺 which additionally maps two specified points. (Contributed by Mario Carneiro, 30-May-2015.) |
⊢ 𝐺 = (𝐹 ∘ (( I ↾ (𝐴 ∖ {𝐶, (◡𝐹‘𝐷)})) ∪ {〈𝐶, (◡𝐹‘𝐷)〉, 〈(◡𝐹‘𝐷), 𝐶〉})) ⇒ ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐺:𝐴–1-1-onto→𝐵 ∧ (𝐺‘𝐶) = 𝐷)) | ||
Theorem | nf1const 7317 | A constant function from at least two elements is not one-to-one. (Contributed by AV, 30-Mar-2024.) |
⊢ ((𝐹:𝐴⟶{𝐵} ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌)) → ¬ 𝐹:𝐴–1-1→𝐶) | ||
Theorem | nf1oconst 7318 | A constant function from at least two elements is not bijective. (Contributed by AV, 30-Mar-2024.) |
⊢ ((𝐹:𝐴⟶{𝐵} ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌)) → ¬ 𝐹:𝐴–1-1-onto→𝐶) | ||
Theorem | f1ofvswap 7319 | Swapping two values in a bijection between two classes yields another bijection between those classes. (Contributed by BTernaryTau, 31-Aug-2024.) |
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((𝐹 ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, (𝐹‘𝑌)〉, 〈𝑌, (𝐹‘𝑋)〉}):𝐴–1-1-onto→𝐵) | ||
Theorem | fliftrel 7320* | 𝐹, a function lift, is a subset of 𝑅 × 𝑆. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝐹 ⊆ (𝑅 × 𝑆)) | ||
Theorem | fliftel 7321* | Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐶𝐹𝐷 ↔ ∃𝑥 ∈ 𝑋 (𝐶 = 𝐴 ∧ 𝐷 = 𝐵))) | ||
Theorem | fliftel1 7322* | Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴𝐹𝐵) | ||
Theorem | fliftcnv 7323* | Converse of the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → ◡𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐵, 𝐴〉)) | ||
Theorem | fliftfun 7324* | The function 𝐹 is the unique function defined by 𝐹‘𝐴 = 𝐵, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐶) & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (Fun 𝐹 ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐴 = 𝐶 → 𝐵 = 𝐷))) | ||
Theorem | fliftfund 7325* | The function 𝐹 is the unique function defined by 𝐹‘𝐴 = 𝐵, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐶) & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐷) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝐴 = 𝐶)) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → Fun 𝐹) | ||
Theorem | fliftfuns 7326* | The function 𝐹 is the unique function defined by 𝐹‘𝐴 = 𝐵, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → (Fun 𝐹 ↔ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵))) | ||
Theorem | fliftf 7327* | The domain and range of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → (Fun 𝐹 ↔ 𝐹:ran (𝑥 ∈ 𝑋 ↦ 𝐴)⟶𝑆)) | ||
Theorem | fliftval 7328* | The value of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆) & ⊢ (𝑥 = 𝑌 → 𝐴 = 𝐶) & ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷) & ⊢ (𝜑 → Fun 𝐹) ⇒ ⊢ ((𝜑 ∧ 𝑌 ∈ 𝑋) → (𝐹‘𝐶) = 𝐷) | ||
Theorem | isoeq1 7329 | Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.) |
⊢ (𝐻 = 𝐺 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵))) | ||
Theorem | isoeq2 7330 | Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.) |
⊢ (𝑅 = 𝑇 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑇, 𝑆 (𝐴, 𝐵))) | ||
Theorem | isoeq3 7331 | Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.) |
⊢ (𝑆 = 𝑇 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑇 (𝐴, 𝐵))) | ||
Theorem | isoeq4 7332 | Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.) |
⊢ (𝐴 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐶, 𝐵))) | ||
Theorem | isoeq5 7333 | Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.) |
⊢ (𝐵 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐶))) | ||
Theorem | nfiso 7334 | Bound-variable hypothesis builder for an isomorphism. (Contributed by NM, 17-May-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
⊢ Ⅎ𝑥𝐻 & ⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝑆 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) | ||
Theorem | isof1o 7335 | An isomorphism is a one-to-one onto function. (Contributed by NM, 27-Apr-2004.) |
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵) | ||
Theorem | isof1oidb 7336 | A function is a bijection iff it is an isomorphism regarding the identity relation. (Contributed by AV, 9-May-2021.) |
⊢ (𝐻:𝐴–1-1-onto→𝐵 ↔ 𝐻 Isom I , I (𝐴, 𝐵)) | ||
Theorem | isof1oopb 7337 | A function is a bijection iff it is an isomorphism regarding the universal class of ordered pairs as relations. (Contributed by AV, 9-May-2021.) |
⊢ (𝐻:𝐴–1-1-onto→𝐵 ↔ 𝐻 Isom (V × V), (V × V)(𝐴, 𝐵)) | ||
Theorem | isorel 7338 | An isomorphism connects binary relations via its function values. (Contributed by NM, 27-Apr-2004.) |
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶𝑅𝐷 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝐷))) | ||
Theorem | soisores 7339* | Express the condition of isomorphism on two strict orders for a function's restriction. (Contributed by Mario Carneiro, 22-Jan-2015.) |
⊢ (((𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶) ∧ (𝐹:𝐵⟶𝐶 ∧ 𝐴 ⊆ 𝐵)) → ((𝐹 ↾ 𝐴) Isom 𝑅, 𝑆 (𝐴, (𝐹 “ 𝐴)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐹‘𝑥)𝑆(𝐹‘𝑦)))) | ||
Theorem | soisoi 7340* | Infer isomorphism from one direction of an order proof for isomorphisms between strict orders. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)) | ||
Theorem | isoid 7341 | Identity law for isomorphism. Proposition 6.30(1) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.) |
⊢ ( I ↾ 𝐴) Isom 𝑅, 𝑅 (𝐴, 𝐴) | ||
Theorem | isocnv 7342 | Converse law for isomorphism. Proposition 6.30(2) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.) |
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → ◡𝐻 Isom 𝑆, 𝑅 (𝐵, 𝐴)) | ||
Theorem | isocnv2 7343 | Converse law for isomorphism. (Contributed by Mario Carneiro, 30-Jan-2014.) |
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom ◡𝑅, ◡𝑆(𝐴, 𝐵)) | ||
Theorem | isocnv3 7344 | Complementation law for isomorphism. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ 𝐶 = ((𝐴 × 𝐴) ∖ 𝑅) & ⊢ 𝐷 = ((𝐵 × 𝐵) ∖ 𝑆) ⇒ ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝐶, 𝐷 (𝐴, 𝐵)) | ||
Theorem | isores2 7345 | An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013.) |
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, (𝑆 ∩ (𝐵 × 𝐵))(𝐴, 𝐵)) | ||
Theorem | isores1 7346 | An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013.) |
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom (𝑅 ∩ (𝐴 × 𝐴)), 𝑆(𝐴, 𝐵)) | ||
Theorem | isores3 7347 | Induced isomorphism on a subset. (Contributed by Stefan O'Rear, 5-Nov-2014.) |
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐾 ⊆ 𝐴 ∧ 𝑋 = (𝐻 “ 𝐾)) → (𝐻 ↾ 𝐾) Isom 𝑅, 𝑆 (𝐾, 𝑋)) | ||
Theorem | isotr 7348 | Composition (transitive) law for isomorphism. Proposition 6.30(3) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.) (Proof shortened by Mario Carneiro, 5-Dec-2016.) |
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐺 Isom 𝑆, 𝑇 (𝐵, 𝐶)) → (𝐺 ∘ 𝐻) Isom 𝑅, 𝑇 (𝐴, 𝐶)) | ||
Theorem | isomin 7349 | Isomorphisms preserve minimal elements. Note that (◡𝑅 “ {𝐷}) is Takeuti and Zaring's idiom for the initial segment {𝑥 ∣ 𝑥𝑅𝐷}. Proposition 6.31(1) of [TakeutiZaring] p. 33. (Contributed by NM, 19-Apr-2004.) |
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐶 ∩ (◡𝑅 “ {𝐷})) = ∅ ↔ ((𝐻 “ 𝐶) ∩ (◡𝑆 “ {(𝐻‘𝐷)})) = ∅)) | ||
Theorem | isoini 7350 | Isomorphisms preserve initial segments. Proposition 6.31(2) of [TakeutiZaring] p. 33. (Contributed by NM, 20-Apr-2004.) |
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐷 ∈ 𝐴) → (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝐷}))) = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝐷)}))) | ||
Theorem | isoini2 7351 | Isomorphisms are isomorphisms on their initial segments. (Contributed by Mario Carneiro, 29-Mar-2014.) |
⊢ 𝐶 = (𝐴 ∩ (◡𝑅 “ {𝑋})) & ⊢ 𝐷 = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑋)})) ⇒ ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → (𝐻 ↾ 𝐶) Isom 𝑅, 𝑆 (𝐶, 𝐷)) | ||
Theorem | isofrlem 7352* | Lemma for isofr 7354. (Contributed by NM, 29-Apr-2004.) (Revised by Mario Carneiro, 18-Nov-2014.) |
⊢ (𝜑 → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → (𝐻 “ 𝑥) ∈ V) ⇒ ⊢ (𝜑 → (𝑆 Fr 𝐵 → 𝑅 Fr 𝐴)) | ||
Theorem | isoselem 7353* | Lemma for isose 7355. (Contributed by Mario Carneiro, 23-Jun-2015.) |
⊢ (𝜑 → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → (𝐻 “ 𝑥) ∈ V) ⇒ ⊢ (𝜑 → (𝑅 Se 𝐴 → 𝑆 Se 𝐵)) | ||
Theorem | isofr 7354 | An isomorphism preserves well-foundedness. Proposition 6.32(1) of [TakeutiZaring] p. 33. (Contributed by NM, 30-Apr-2004.) (Revised by Mario Carneiro, 18-Nov-2014.) |
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐵)) | ||
Theorem | isose 7355 | An isomorphism preserves set-like relations. (Contributed by Mario Carneiro, 23-Jun-2015.) |
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Se 𝐴 ↔ 𝑆 Se 𝐵)) | ||
Theorem | isofr2 7356 | A weak form of isofr 7354 that does not need Replacement. (Contributed by Mario Carneiro, 18-Nov-2014.) |
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐵 ∈ 𝑉) → (𝑆 Fr 𝐵 → 𝑅 Fr 𝐴)) | ||
Theorem | isopolem 7357 | Lemma for isopo 7358. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑆 Po 𝐵 → 𝑅 Po 𝐴)) | ||
Theorem | isopo 7358 | An isomorphism preserves the property of being a partial order. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Po 𝐴 ↔ 𝑆 Po 𝐵)) | ||
Theorem | isosolem 7359 | Lemma for isoso 7360. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑆 Or 𝐵 → 𝑅 Or 𝐴)) | ||
Theorem | isoso 7360 | An isomorphism preserves the property of being a strict total order. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐵)) | ||
Theorem | isowe 7361 | An isomorphism preserves the property of being a well-ordering. Proposition 6.32(3) of [TakeutiZaring] p. 33. (Contributed by NM, 30-Apr-2004.) (Revised by Mario Carneiro, 18-Nov-2014.) |
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 We 𝐴 ↔ 𝑆 We 𝐵)) | ||
Theorem | isowe2 7362* | A weak form of isowe 7361 that does not need Replacement. (Contributed by Mario Carneiro, 18-Nov-2014.) |
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ ∀𝑥(𝐻 “ 𝑥) ∈ V) → (𝑆 We 𝐵 → 𝑅 We 𝐴)) | ||
Theorem | f1oiso 7363* | Any one-to-one onto function determines an isomorphism with an induced relation 𝑆. Proposition 6.33 of [TakeutiZaring] p. 34. (Contributed by NM, 30-Apr-2004.) |
⊢ ((𝐻:𝐴–1-1-onto→𝐵 ∧ 𝑆 = {〈𝑧, 𝑤〉 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑧 = (𝐻‘𝑥) ∧ 𝑤 = (𝐻‘𝑦)) ∧ 𝑥𝑅𝑦)}) → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)) | ||
Theorem | f1oiso2 7364* | Any one-to-one onto function determines an isomorphism with an induced relation 𝑆. (Contributed by Mario Carneiro, 9-Mar-2013.) |
⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (◡𝐻‘𝑥)𝑅(◡𝐻‘𝑦))} ⇒ ⊢ (𝐻:𝐴–1-1-onto→𝐵 → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)) | ||
Theorem | f1owe 7365* | Well-ordering of isomorphic relations. (Contributed by NM, 4-Mar-1997.) |
⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ (𝐹‘𝑥)𝑆(𝐹‘𝑦)} ⇒ ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝑆 We 𝐵 → 𝑅 We 𝐴)) | ||
Theorem | weniso 7366 | A set-like well-ordering has no nontrivial automorphisms. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Mario Carneiro, 25-Jun-2015.) |
⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹 = ( I ↾ 𝐴)) | ||
Theorem | weisoeq 7367 | Thus, there is at most one isomorphism between any two set-like well-ordered classes. Class version of wemoiso 7987. (Contributed by Mario Carneiro, 25-Jun-2015.) |
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵))) → 𝐹 = 𝐺) | ||
Theorem | weisoeq2 7368 | Thus, there is at most one isomorphism between any two set-like well-ordered classes. Class version of wemoiso2 7988. (Contributed by Mario Carneiro, 25-Jun-2015.) |
⊢ (((𝑆 We 𝐵 ∧ 𝑆 Se 𝐵) ∧ (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵))) → 𝐹 = 𝐺) | ||
Theorem | knatar 7369* | The Knaster-Tarski theorem says that every monotone function over a complete lattice has a (least) fixpoint. Here we specialize this theorem to the case when the lattice is the powerset lattice 𝒫 𝐴. (Contributed by Mario Carneiro, 11-Jun-2015.) |
⊢ 𝑋 = ∩ {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹‘𝑧) ⊆ 𝑧} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → (𝑋 ⊆ 𝐴 ∧ (𝐹‘𝑋) = 𝑋)) | ||
Theorem | fvresval 7370 | The value of a restricted function at a class is either the empty set or the value of the unrestricted function at that class. (Contributed by Scott Fenton, 4-Sep-2011.) |
⊢ (((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴) ∨ ((𝐹 ↾ 𝐵)‘𝐴) = ∅) | ||
Theorem | funeldmb 7371 | If ∅ is not part of the range of a function 𝐹, then 𝐴 is in the domain of 𝐹 iff (𝐹‘𝐴) ≠ ∅. (Contributed by Scott Fenton, 7-Dec-2021.) |
⊢ ((Fun 𝐹 ∧ ¬ ∅ ∈ ran 𝐹) → (𝐴 ∈ dom 𝐹 ↔ (𝐹‘𝐴) ≠ ∅)) | ||
Theorem | eqfunresadj 7372 | Law for adjoining an element to restrictions of functions. (Contributed by Scott Fenton, 6-Dec-2021.) |
⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (𝐹 ↾ 𝑋) = (𝐺 ↾ 𝑋) ∧ (𝑌 ∈ dom 𝐹 ∧ 𝑌 ∈ dom 𝐺 ∧ (𝐹‘𝑌) = (𝐺‘𝑌))) → (𝐹 ↾ (𝑋 ∪ {𝑌})) = (𝐺 ↾ (𝑋 ∪ {𝑌}))) | ||
Theorem | eqfunressuc 7373 | Law for equality of restriction to successors. This is primarily useful when 𝑋 is an ordinal, but it does not require that. (Contributed by Scott Fenton, 6-Dec-2021.) |
⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (𝐹 ↾ 𝑋) = (𝐺 ↾ 𝑋) ∧ (𝑋 ∈ dom 𝐹 ∧ 𝑋 ∈ dom 𝐺 ∧ (𝐹‘𝑋) = (𝐺‘𝑋))) → (𝐹 ↾ suc 𝑋) = (𝐺 ↾ suc 𝑋)) | ||
Theorem | fnssintima 7374* | Condition for subset of an intersection of an image. (Contributed by Scott Fenton, 16-Aug-2024.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ⊆ ∩ (𝐹 “ 𝐵) ↔ ∀𝑥 ∈ 𝐵 𝐶 ⊆ (𝐹‘𝑥))) | ||
Theorem | imaeqsexv 7375* | Substitute a function value into an existential quantifier over an image. (Contributed by Scott Fenton, 27-Sep-2024.) |
⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∃𝑥 ∈ (𝐹 “ 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | imaeqsalv 7376* | Substitute a function value into a universal quantifier over an image. (Contributed by Scott Fenton, 27-Sep-2024.) |
⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∀𝑥 ∈ (𝐹 “ 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | canth 7377 | No set 𝐴 is equinumerous to its power set (Cantor's theorem), i.e., no function can map 𝐴 onto its power set. Compare Theorem 6B(b) of [Enderton] p. 132. For the equinumerosity version, see canth2 9168. Note that 𝐴 must be a set: this theorem does not hold when 𝐴 is too large to be a set; see ncanth 7378 for a counterexample. (Use nex 1795 if you want the form ¬ ∃𝑓𝑓:𝐴–onto→𝒫 𝐴.) (Contributed by NM, 7-Aug-1994.) (Proof shortened by Mario Carneiro, 7-Jun-2016.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ¬ 𝐹:𝐴–onto→𝒫 𝐴 | ||
Theorem | ncanth 7378 |
Cantor's theorem fails for the universal class (which is not a set but a
proper class by vprc 5320). Specifically, the identity function maps
the
universe onto its power class. Compare canth 7377 that works for sets.
This failure comes from a limitation of the collection principle (which is necessary to avoid Russell's paradox ru 3774): 𝒫 V, being a class, cannot contain proper classes, so it is no larger than V, which is why the identity function "succeeds" in being surjective onto 𝒫 V (see pwv 4910). See also the remark in ru 3774 about NF, in which Cantor's theorem fails for sets that are "too large". This theorem gives some intuition behind that failure: in NF the universal class is a set, and it equals its own power set. (Contributed by NM, 29-Jun-2004.) (Proof shortened by BJ, 29-Dec-2023.) |
⊢ I :V–onto→𝒫 V | ||
Syntax | crio 7379 | Extend class notation with restricted description binder. |
class (℩𝑥 ∈ 𝐴 𝜑) | ||
Definition | df-riota 7380 | Define restricted description binder. In case there is no unique 𝑥 such that (𝑥 ∈ 𝐴 ∧ 𝜑) holds, it evaluates to the empty set. See also comments for df-iota 6506. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 2-Sep-2018.) |
⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Theorem | riotaeqdv 7381* | Formula-building deduction for iota. (Contributed by NM, 15-Sep-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | riotabidv 7382* | Formula-building deduction for restricted iota. (Contributed by NM, 15-Sep-2011.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | riotaeqbidv 7383* | Equality deduction for restricted universal quantifier. (Contributed by NM, 15-Sep-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | riotaex 7384 | Restricted iota is a set. (Contributed by NM, 15-Sep-2011.) |
⊢ (℩𝑥 ∈ 𝐴 𝜓) ∈ V | ||
Theorem | riotav 7385 | An iota restricted to the universe is unrestricted. (Contributed by NM, 18-Sep-2011.) |
⊢ (℩𝑥 ∈ V 𝜑) = (℩𝑥𝜑) | ||
Theorem | riotauni 7386 | Restricted iota in terms of class union. (Contributed by NM, 11-Oct-2011.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) = ∪ {𝑥 ∈ 𝐴 ∣ 𝜑}) | ||
Theorem | nfriota1 7387* | The abstraction variable in a restricted iota descriptor isn't free. (Contributed by NM, 12-Oct-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥(℩𝑥 ∈ 𝐴 𝜑) | ||
Theorem | nfriotadw 7388* | Deduction version of nfriota 7393 with a disjoint variable condition, which contrary to nfriotad 7392 does not require ax-13 2366. (Contributed by NM, 18-Feb-2013.) Avoid ax-13 2366. (Revised by GG, 26-Jan-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜓)) | ||
Theorem | cbvriotaw 7389* | Change bound variable in a restricted description binder. Version of cbvriota 7394 with a disjoint variable condition, which does not require ax-13 2366. (Contributed by NM, 18-Mar-2013.) Avoid ax-13 2366. (Revised by GG, 26-Jan-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvriotavw 7390* | Change bound variable in a restricted description binder. Version of cbvriotav 7395 with a disjoint variable condition, which requires fewer axioms . (Contributed by NM, 18-Mar-2013.) (Revised by GG, 30-Sep-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvriotavwOLD 7391* | Obsolete version of cbvriotavw 7390 as of 30-Sep-2024. (Contributed by NM, 18-Mar-2013.) (Revised by GG, 26-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓) | ||
Theorem | nfriotad 7392 | Deduction version of nfriota 7393. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker nfriotadw 7388 when possible. (Contributed by NM, 18-Feb-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜓)) | ||
Theorem | nfriota 7393* | A variable not free in a wff remains so in a restricted iota descriptor. (Contributed by NM, 12-Oct-2011.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜑) | ||
Theorem | cbvriota 7394* | Change bound variable in a restricted description binder. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker cbvriotaw 7389 when possible. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvriotav 7395* | Change bound variable in a restricted description binder. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker cbvriotavw 7390 when possible. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓) | ||
Theorem | csbriota 7396* | Interchange class substitution and restricted description binder. (Contributed by NM, 24-Feb-2013.) (Revised by NM, 2-Sep-2018.) |
⊢ ⦋𝐴 / 𝑥⦌(℩𝑦 ∈ 𝐵 𝜑) = (℩𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑) | ||
Theorem | riotacl2 7397 | Membership law for "the unique element in 𝐴 such that 𝜑". (Contributed by NM, 21-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑}) | ||
Theorem | riotacl 7398* | Closure of restricted iota. (Contributed by NM, 21-Aug-2011.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴) | ||
Theorem | riotasbc 7399 | Substitution law for descriptions. Compare iotasbc 44093. (Contributed by NM, 23-Aug-2011.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → [(℩𝑥 ∈ 𝐴 𝜑) / 𝑥]𝜑) | ||
Theorem | riotabidva 7400* | Equivalent wff's yield equal restricted class abstractions (deduction form). (rabbidva 3426 analog.) (Contributed by NM, 17-Jan-2012.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |