![]() |
Intuitionistic Logic Explorer Theorem List (p. 59 of 145) | < 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 | nfiso 5801 | Bound-variable hypothesis builder for an isomorphism. (Contributed by NM, 17-May-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
⊢ Ⅎ𝑥𝐻 & ⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝑆 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) | ||
Theorem | isof1o 5802 | An isomorphism is a one-to-one onto function. (Contributed by NM, 27-Apr-2004.) |
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵) | ||
Theorem | isorel 5803 | An isomorphism connects binary relations via its function values. (Contributed by NM, 27-Apr-2004.) |
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶𝑅𝐷 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝐷))) | ||
Theorem | isoresbr 5804* | A consequence of isomorphism on two relations for a function's restriction. (Contributed by Jim Kingdon, 11-Jan-2019.) |
⊢ ((𝐹 ↾ 𝐴) Isom 𝑅, 𝑆 (𝐴, (𝐹 “ 𝐴)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐹‘𝑥)𝑆(𝐹‘𝑦))) | ||
Theorem | isoid 5805 | Identity law for isomorphism. Proposition 6.30(1) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.) |
⊢ ( I ↾ 𝐴) Isom 𝑅, 𝑅 (𝐴, 𝐴) | ||
Theorem | isocnv 5806 | Converse law for isomorphism. Proposition 6.30(2) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.) |
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → ◡𝐻 Isom 𝑆, 𝑅 (𝐵, 𝐴)) | ||
Theorem | isocnv2 5807 | Converse law for isomorphism. (Contributed by Mario Carneiro, 30-Jan-2014.) |
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom ◡𝑅, ◡𝑆(𝐴, 𝐵)) | ||
Theorem | isores2 5808 | 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 5809 | 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 5810 | Induced isomorphism on a subset. (Contributed by Stefan O'Rear, 5-Nov-2014.) |
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐾 ⊆ 𝐴 ∧ 𝑋 = (𝐻 “ 𝐾)) → (𝐻 ↾ 𝐾) Isom 𝑅, 𝑆 (𝐾, 𝑋)) | ||
Theorem | isotr 5811 | 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 | iso0 5812 | The empty set is an 𝑅, 𝑆 isomorphism from the empty set to the empty set. (Contributed by Steve Rodriguez, 24-Oct-2015.) |
⊢ ∅ Isom 𝑅, 𝑆 (∅, ∅) | ||
Theorem | isoini 5813 | Isomorphisms preserve initial segments. Proposition 6.31(2) of [TakeutiZaring] p. 33. (Contributed by NM, 20-Apr-2004.) |
⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐷 ∈ 𝐴) → (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝐷}))) = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝐷)}))) | ||
Theorem | isoini2 5814 | Isomorphisms are isomorphisms on their initial segments. (Contributed by Mario Carneiro, 29-Mar-2014.) |
⊢ 𝐶 = (𝐴 ∩ (◡𝑅 “ {𝑋})) & ⊢ 𝐷 = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑋)})) ⇒ ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → (𝐻 ↾ 𝐶) Isom 𝑅, 𝑆 (𝐶, 𝐷)) | ||
Theorem | isoselem 5815* | Lemma for isose 5816. (Contributed by Mario Carneiro, 23-Jun-2015.) |
⊢ (𝜑 → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → (𝐻 “ 𝑥) ∈ V) ⇒ ⊢ (𝜑 → (𝑅 Se 𝐴 → 𝑆 Se 𝐵)) | ||
Theorem | isose 5816 | An isomorphism preserves set-like relations. (Contributed by Mario Carneiro, 23-Jun-2015.) |
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Se 𝐴 ↔ 𝑆 Se 𝐵)) | ||
Theorem | isopolem 5817 | Lemma for isopo 5818. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑆 Po 𝐵 → 𝑅 Po 𝐴)) | ||
Theorem | isopo 5818 | An isomorphism preserves partial ordering. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Po 𝐴 ↔ 𝑆 Po 𝐵)) | ||
Theorem | isosolem 5819 | Lemma for isoso 5820. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑆 Or 𝐵 → 𝑅 Or 𝐴)) | ||
Theorem | isoso 5820 | An isomorphism preserves strict ordering. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐵)) | ||
Theorem | f1oiso 5821* | 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 5822* | 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 | canth 5823 | 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. (Use nex 1500 if you want the form ¬ ∃𝑓𝑓:𝐴–onto→𝒫 𝐴.) (Contributed by NM, 7-Aug-1994.) (Revised by Noah R Kingdon, 23-Jul-2024.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ¬ 𝐹:𝐴–onto→𝒫 𝐴 | ||
Syntax | crio 5824 | Extend class notation with restricted description binder. |
class (℩𝑥 ∈ 𝐴 𝜑) | ||
Definition | df-riota 5825 | 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 5174. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 2-Sep-2018.) |
⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Theorem | riotaeqdv 5826* | Formula-building deduction for iota. (Contributed by NM, 15-Sep-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | riotabidv 5827* | Formula-building deduction for restricted iota. (Contributed by NM, 15-Sep-2011.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | riotaeqbidv 5828* | Equality deduction for restricted universal quantifier. (Contributed by NM, 15-Sep-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | riotaexg 5829* | Restricted iota is a set. (Contributed by Jim Kingdon, 15-Jun-2020.) |
⊢ (𝐴 ∈ 𝑉 → (℩𝑥 ∈ 𝐴 𝜓) ∈ V) | ||
Theorem | riotav 5830 | An iota restricted to the universe is unrestricted. (Contributed by NM, 18-Sep-2011.) |
⊢ (℩𝑥 ∈ V 𝜑) = (℩𝑥𝜑) | ||
Theorem | riotauni 5831 | Restricted iota in terms of class union. (Contributed by NM, 11-Oct-2011.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) = ∪ {𝑥 ∈ 𝐴 ∣ 𝜑}) | ||
Theorem | nfriota1 5832* | 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 | nfriotadxy 5833* | Deduction version of nfriota 5834. (Contributed by Jim Kingdon, 12-Jan-2019.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜓)) | ||
Theorem | nfriota 5834* | A variable not free in a wff remains so in a restricted iota descriptor. (Contributed by NM, 12-Oct-2011.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜑) | ||
Theorem | cbvriota 5835* | Change bound variable in a restricted description binder. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓) | ||
Theorem | cbvriotav 5836* | Change bound variable in a restricted description binder. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓) | ||
Theorem | csbriotag 5837* | Interchange class substitution and restricted description binder. (Contributed by NM, 24-Feb-2013.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(℩𝑦 ∈ 𝐵 𝜑) = (℩𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) | ||
Theorem | riotacl2 5838 |
Membership law for "the unique element in 𝐴 such that 𝜑."
(Contributed by NM, 21-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑}) | ||
Theorem | riotacl 5839* | Closure of restricted iota. (Contributed by NM, 21-Aug-2011.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴) | ||
Theorem | riotasbc 5840 | Substitution law for descriptions. (Contributed by NM, 23-Aug-2011.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → [(℩𝑥 ∈ 𝐴 𝜑) / 𝑥]𝜑) | ||
Theorem | riotabidva 5841* | Equivalent wff's yield equal restricted class abstractions (deduction form). (rabbidva 2725 analog.) (Contributed by NM, 17-Jan-2012.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | riotabiia 5842 | Equivalent wff's yield equal restricted iotas (inference form). (rabbiia 2722 analog.) (Contributed by NM, 16-Jan-2012.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐴 𝜓) | ||
Theorem | riota1 5843* | Property of restricted iota. Compare iota1 5188. (Contributed by Mario Carneiro, 15-Oct-2016.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝑥)) | ||
Theorem | riota1a 5844 | Property of iota. (Contributed by NM, 23-Aug-2011.) |
⊢ ((𝑥 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜑 ↔ (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) = 𝑥)) | ||
Theorem | riota2df 5845* | A deduction version of riota2f 5846. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝐵) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝜑 ∧ ∃!𝑥 ∈ 𝐴 𝜓) → (𝜒 ↔ (℩𝑥 ∈ 𝐴 𝜓) = 𝐵)) | ||
Theorem | riota2f 5846* | This theorem shows a condition that allows us to represent a descriptor with a class expression 𝐵. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐵 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜓 ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝐵)) | ||
Theorem | riota2 5847* | This theorem shows a condition that allows us to represent a descriptor with a class expression 𝐵. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 10-Dec-2016.) |
⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐵 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜓 ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝐵)) | ||
Theorem | riotaprop 5848* | Properties of a restricted definite description operator. Todo (df-riota 5825 update): can some uses of riota2f 5846 be shortened with this? (Contributed by NM, 23-Nov-2013.) |
⊢ Ⅎ𝑥𝜓 & ⊢ 𝐵 = (℩𝑥 ∈ 𝐴 𝜑) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (𝐵 ∈ 𝐴 ∧ 𝜓)) | ||
Theorem | riota5f 5849* | A method for computing restricted iota. (Contributed by NM, 16-Apr-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐵) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝑥 = 𝐵)) ⇒ ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = 𝐵) | ||
Theorem | riota5 5850* | A method for computing restricted iota. (Contributed by NM, 20-Oct-2011.) (Revised by Mario Carneiro, 6-Dec-2016.) |
⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝑥 = 𝐵)) ⇒ ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = 𝐵) | ||
Theorem | riotass2 5851* | Restriction of a unique element to a smaller class. (Contributed by NM, 21-Aug-2011.) (Revised by NM, 22-Mar-2013.) |
⊢ (((𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)) ∧ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜓)) → (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜓)) | ||
Theorem | riotass 5852* | Restriction of a unique element to a smaller class. (Contributed by NM, 19-Oct-2005.) (Revised by Mario Carneiro, 24-Dec-2016.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐵 𝜑) → (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | moriotass 5853* | Restriction of a unique element to a smaller class. (Contributed by NM, 19-Feb-2006.) (Revised by NM, 16-Jun-2017.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐵 𝜑) → (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜑)) | ||
Theorem | snriota 5854 | A restricted class abstraction with a unique member can be expressed as a singleton. (Contributed by NM, 30-May-2006.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜑} = {(℩𝑥 ∈ 𝐴 𝜑)}) | ||
Theorem | eusvobj2 5855* | Specify the same property in two ways when class 𝐵(𝑦) is single-valued. (Contributed by NM, 1-Nov-2010.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 → (∃𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∀𝑦 ∈ 𝐴 𝑥 = 𝐵)) | ||
Theorem | eusvobj1 5856* | Specify the same object in two ways when class 𝐵(𝑦) is single-valued. (Contributed by NM, 1-Nov-2010.) (Proof shortened by Mario Carneiro, 19-Nov-2016.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (∃!𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵 → (℩𝑥∃𝑦 ∈ 𝐴 𝑥 = 𝐵) = (℩𝑥∀𝑦 ∈ 𝐴 𝑥 = 𝐵)) | ||
Theorem | f1ofveu 5857* | There is one domain element for each value of a one-to-one onto function. (Contributed by NM, 26-May-2006.) |
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ∃!𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐶) | ||
Theorem | f1ocnvfv3 5858* | Value of the converse of a one-to-one onto function. (Contributed by NM, 26-May-2006.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (◡𝐹‘𝐶) = (℩𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐶)) | ||
Theorem | riotaund 5859* | Restricted iota equals the empty set when not meaningful. (Contributed by NM, 16-Jan-2012.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 13-Sep-2018.) |
⊢ (¬ ∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) = ∅) | ||
Theorem | acexmidlema 5860* | Lemma for acexmid 5868. (Contributed by Jim Kingdon, 6-Aug-2019.) |
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)} & ⊢ 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)} & ⊢ 𝐶 = {𝐴, 𝐵} ⇒ ⊢ ({∅} ∈ 𝐴 → 𝜑) | ||
Theorem | acexmidlemb 5861* | Lemma for acexmid 5868. (Contributed by Jim Kingdon, 6-Aug-2019.) |
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)} & ⊢ 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)} & ⊢ 𝐶 = {𝐴, 𝐵} ⇒ ⊢ (∅ ∈ 𝐵 → 𝜑) | ||
Theorem | acexmidlemph 5862* | Lemma for acexmid 5868. (Contributed by Jim Kingdon, 6-Aug-2019.) |
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)} & ⊢ 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)} & ⊢ 𝐶 = {𝐴, 𝐵} ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | acexmidlemab 5863* | Lemma for acexmid 5868. (Contributed by Jim Kingdon, 6-Aug-2019.) |
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)} & ⊢ 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)} & ⊢ 𝐶 = {𝐴, 𝐵} ⇒ ⊢ (((℩𝑣 ∈ 𝐴 ∃𝑢 ∈ 𝑦 (𝐴 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)) = ∅ ∧ (℩𝑣 ∈ 𝐵 ∃𝑢 ∈ 𝑦 (𝐵 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)) = {∅}) → ¬ 𝜑) | ||
Theorem | acexmidlemcase 5864* |
Lemma for acexmid 5868. Here we divide the proof into cases (based
on the
disjunction implicit in an unordered pair, not the sort of case
elimination which relies on excluded middle).
The cases are (1) the choice function evaluated at 𝐴 equals {∅}, (2) the choice function evaluated at 𝐵 equals ∅, and (3) the choice function evaluated at 𝐴 equals ∅ and the choice function evaluated at 𝐵 equals {∅}. Because of the way we represent the choice function 𝑦, the choice function evaluated at 𝐴 is (℩𝑣 ∈ 𝐴∃𝑢 ∈ 𝑦(𝐴 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)) and the choice function evaluated at 𝐵 is (℩𝑣 ∈ 𝐵∃𝑢 ∈ 𝑦(𝐵 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)). Other than the difference in notation these work just as (𝑦‘𝐴) and (𝑦‘𝐵) would if 𝑦 were a function as defined by df-fun 5214. Although it isn't exactly about the division into cases, it is also convenient for this lemma to also include the step that if the choice function evaluated at 𝐴 equals {∅}, then {∅} ∈ 𝐴 and likewise for 𝐵. (Contributed by Jim Kingdon, 7-Aug-2019.) |
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)} & ⊢ 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)} & ⊢ 𝐶 = {𝐴, 𝐵} ⇒ ⊢ (∀𝑧 ∈ 𝐶 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) → ({∅} ∈ 𝐴 ∨ ∅ ∈ 𝐵 ∨ ((℩𝑣 ∈ 𝐴 ∃𝑢 ∈ 𝑦 (𝐴 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)) = ∅ ∧ (℩𝑣 ∈ 𝐵 ∃𝑢 ∈ 𝑦 (𝐵 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)) = {∅}))) | ||
Theorem | acexmidlem1 5865* | Lemma for acexmid 5868. List the cases identified in acexmidlemcase 5864 and hook them up to the lemmas which handle each case. (Contributed by Jim Kingdon, 7-Aug-2019.) |
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)} & ⊢ 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)} & ⊢ 𝐶 = {𝐴, 𝐵} ⇒ ⊢ (∀𝑧 ∈ 𝐶 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) → (𝜑 ∨ ¬ 𝜑)) | ||
Theorem | acexmidlem2 5866* |
Lemma for acexmid 5868. This builds on acexmidlem1 5865 by noting that every
element of 𝐶 is inhabited.
(Note that 𝑦 is not quite a function in the df-fun 5214 sense because it uses ordered pairs as described in opthreg 4552 rather than df-op 3600). The set 𝐴 is also found in onsucelsucexmidlem 4525. (Contributed by Jim Kingdon, 5-Aug-2019.) |
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝜑)} & ⊢ 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝜑)} & ⊢ 𝐶 = {𝐴, 𝐵} ⇒ ⊢ (∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) → (𝜑 ∨ ¬ 𝜑)) | ||
Theorem | acexmidlemv 5867* |
Lemma for acexmid 5868.
This is acexmid 5868 with additional disjoint variable conditions, most notably between 𝜑 and 𝑥. (Contributed by Jim Kingdon, 6-Aug-2019.) |
⊢ ∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ⇒ ⊢ (𝜑 ∨ ¬ 𝜑) | ||
Theorem | acexmid 5868* |
The axiom of choice implies excluded middle. Theorem 1.3 in [Bauer]
p. 483.
The statement of the axiom of choice given here is ac2 in the Metamath Proof Explorer (version of 3-Aug-2019). In particular, note that the choice function 𝑦 provides a value when 𝑧 is inhabited (as opposed to nonempty as in some statements of the axiom of choice). Essentially the same proof can also be found at "The axiom of choice implies instances of EM", [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic". Often referred to as Diaconescu's theorem, or Diaconescu-Goodman-Myhill theorem, after Radu Diaconescu who discovered it in 1975 in the framework of topos theory and N. D. Goodman and John Myhill in 1978 in the framework of set theory (although it already appeared as an exercise in Errett Bishop's book Foundations of Constructive Analysis from 1967). For this theorem stated using the df-ac 7199 and df-exmid 4192 syntaxes, see exmidac 7202. (Contributed by Jim Kingdon, 4-Aug-2019.) |
⊢ ∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ⇒ ⊢ (𝜑 ∨ ¬ 𝜑) | ||
Syntax | co 5869 | Extend class notation to include the value of an operation 𝐹 (such as + ) for two arguments 𝐴 and 𝐵. Note that the syntax is simply three class symbols in a row surrounded by parentheses. Since operation values are the only possible class expressions consisting of three class expressions in a row surrounded by parentheses, the syntax is unambiguous. |
class (𝐴𝐹𝐵) | ||
Syntax | coprab 5870 | Extend class notation to include class abstraction (class builder) of nested ordered pairs. |
class {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} | ||
Syntax | cmpo 5871 | Extend the definition of a class to include maps-to notation for defining an operation via a rule. |
class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | ||
Definition | df-ov 5872 | Define the value of an operation. Definition of operation value in [Enderton] p. 79. Note that the syntax is simply three class expressions in a row bracketed by parentheses. There are no restrictions of any kind on what those class expressions may be, although only certain kinds of class expressions - a binary operation 𝐹 and its arguments 𝐴 and 𝐵- will be useful for proving meaningful theorems. For example, if class 𝐹 is the operation + and arguments 𝐴 and 𝐵 are 3 and 2 , the expression ( 3 + 2 ) can be proved to equal 5 . This definition is well-defined, although not very meaningful, when classes 𝐴 and/or 𝐵 are proper classes (i.e. are not sets); see ovprc1 5905 and ovprc2 5906. On the other hand, we often find uses for this definition when 𝐹 is a proper class. 𝐹 is normally equal to a class of nested ordered pairs of the form defined by df-oprab 5873. (Contributed by NM, 28-Feb-1995.) |
⊢ (𝐴𝐹𝐵) = (𝐹‘〈𝐴, 𝐵〉) | ||
Definition | df-oprab 5873* | Define the class abstraction (class builder) of a collection of nested ordered pairs (for use in defining operations). This is a special case of Definition 4.16 of [TakeutiZaring] p. 14. Normally 𝑥, 𝑦, and 𝑧 are distinct, although the definition doesn't strictly require it. See df-ov 5872 for the value of an operation. The brace notation is called "class abstraction" by Quine; it is also called a "class builder" in the literature. The value of the most common operation class builder is given by ovmpo 6004. (Contributed by NM, 12-Mar-1995.) |
⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = 〈〈𝑥, 𝑦〉, 𝑧〉 ∧ 𝜑)} | ||
Definition | df-mpo 5874* | Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from 𝑥, 𝑦 (in 𝐴 × 𝐵) to 𝐵(𝑥, 𝑦)". An extension of df-mpt 4063 for two arguments. (Contributed by NM, 17-Feb-2008.) |
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} | ||
Theorem | oveq 5875 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
⊢ (𝐹 = 𝐺 → (𝐴𝐹𝐵) = (𝐴𝐺𝐵)) | ||
Theorem | oveq1 5876 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶)) | ||
Theorem | oveq2 5877 | Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.) |
⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵)) | ||
Theorem | oveq12 5878 | Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) | ||
Theorem | oveq1i 5879 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐶) | ||
Theorem | oveq2i 5880 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶𝐹𝐴) = (𝐶𝐹𝐵) | ||
Theorem | oveq12i 5881 | Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐷) | ||
Theorem | oveqi 5882 | Equality inference for operation value. (Contributed by NM, 24-Nov-2007.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶𝐴𝐷) = (𝐶𝐵𝐷) | ||
Theorem | oveq123i 5883 | Equality inference for operation value. (Contributed by FL, 11-Jul-2010.) |
⊢ 𝐴 = 𝐶 & ⊢ 𝐵 = 𝐷 & ⊢ 𝐹 = 𝐺 ⇒ ⊢ (𝐴𝐹𝐵) = (𝐶𝐺𝐷) | ||
Theorem | oveq1d 5884 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶)) | ||
Theorem | oveq2d 5885 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵)) | ||
Theorem | oveqd 5886 | Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷)) | ||
Theorem | oveq12d 5887 | Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) | ||
Theorem | oveqan12d 5888 | Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜓 → 𝐶 = 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) | ||
Theorem | oveqan12rd 5889 | Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜓 → 𝐶 = 𝐷) ⇒ ⊢ ((𝜓 ∧ 𝜑) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) | ||
Theorem | oveq123d 5890 | Equality deduction for operation value. (Contributed by FL, 22-Dec-2008.) |
⊢ (𝜑 → 𝐹 = 𝐺) & ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐺𝐷)) | ||
Theorem | fvoveq1d 5891 | Equality deduction for nested function and operation value. (Contributed by AV, 23-Jul-2022.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶))) | ||
Theorem | fvoveq1 5892 | Equality theorem for nested function and operation value. Closed form of fvoveq1d 5891. (Contributed by AV, 23-Jul-2022.) |
⊢ (𝐴 = 𝐵 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶))) | ||
Theorem | ovanraleqv 5893* | Equality theorem for a conjunction with an operation values within a restricted universal quantification. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 13-Aug-2022.) |
⊢ (𝐵 = 𝑋 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐵 = 𝑋 → (∀𝑥 ∈ 𝑉 (𝜑 ∧ (𝐴 · 𝐵) = 𝐶) ↔ ∀𝑥 ∈ 𝑉 (𝜓 ∧ (𝐴 · 𝑋) = 𝐶))) | ||
Theorem | imbrov2fvoveq 5894 | Equality theorem for nested function and operation value in an implication for a binary relation. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 17-Aug-2022.) |
⊢ (𝑋 = 𝑌 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝑋 = 𝑌 → ((𝜑 → (𝐹‘((𝐺‘𝑋) · 𝑂))𝑅𝐴) ↔ (𝜓 → (𝐹‘((𝐺‘𝑌) · 𝑂))𝑅𝐴))) | ||
Theorem | ovrspc2v 5895* | If an operation value is element of a class for all operands of two classes, then the operation value is an element of the class for specific operands of the two classes. (Contributed by Mario Carneiro, 6-Dec-2014.) |
⊢ (((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐹𝑦) ∈ 𝐶) → (𝑋𝐹𝑌) ∈ 𝐶) | ||
Theorem | oveqrspc2v 5896* | Restricted specialization of operands, using implicit substitution. (Contributed by Mario Carneiro, 6-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦)) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐹𝑌) = (𝑋𝐺𝑌)) | ||
Theorem | oveqdr 5897 | Equality of two operations for any two operands. Useful in proofs using *propd theorems. (Contributed by Mario Carneiro, 29-Jun-2015.) |
⊢ (𝜑 → 𝐹 = 𝐺) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦)) | ||
Theorem | nfovd 5898 | Deduction version of bound-variable hypothesis builder nfov 5899. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐹) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥(𝐴𝐹𝐵)) | ||
Theorem | nfov 5899 | Bound-variable hypothesis builder for operation value. (Contributed by NM, 4-May-2004.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴𝐹𝐵) | ||
Theorem | oprabidlem 5900* | Slight elaboration of exdistrfor 1800. A lemma for oprabid 5901. (Contributed by Jim Kingdon, 15-Jan-2019.) |
⊢ (∃𝑥∃𝑦(𝑥 = 𝑧 ∧ 𝜓) → ∃𝑥(𝑥 = 𝑧 ∧ ∃𝑦𝜓)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |