![]() |
Metamath
Proof Explorer Theorem List (p. 78 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | caofref 7701* | Transfer a reflexive law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥𝑅𝑥) ⇒ ⊢ (𝜑 → 𝐹 ∘r 𝑅𝐹) | ||
Theorem | caofinvl 7702* | Transfer a left inverse law to the function operation. (Contributed by NM, 22-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝑁:𝑆⟶𝑆) & ⊢ (𝜑 → 𝐺 = (𝑣 ∈ 𝐴 ↦ (𝑁‘(𝐹‘𝑣)))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝑁‘𝑥)𝑅𝑥) = 𝐵) ⇒ ⊢ (𝜑 → (𝐺 ∘f 𝑅𝐹) = (𝐴 × {𝐵})) | ||
Theorem | caofid0l 7703* | Transfer a left identity law to the function operation. (Contributed by NM, 21-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐵𝑅𝑥) = 𝑥) ⇒ ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘f 𝑅𝐹) = 𝐹) | ||
Theorem | caofid0r 7704* | Transfer a right identity law to the function operation. (Contributed by NM, 21-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥𝑅𝐵) = 𝑥) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅(𝐴 × {𝐵})) = 𝐹) | ||
Theorem | caofid1 7705* | Transfer a right absorption law to the function operation. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥𝑅𝐵) = 𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅(𝐴 × {𝐵})) = (𝐴 × {𝐶})) | ||
Theorem | caofid2 7706* | Transfer a right absorption law to the function operation. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐵𝑅𝑥) = 𝐶) ⇒ ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘f 𝑅𝐹) = (𝐴 × {𝐶})) | ||
Theorem | caofcom 7707* | Transfer a commutative law to the function operation. (Contributed by Mario Carneiro, 26-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑅𝑦) = (𝑦𝑅𝑥)) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝐺 ∘f 𝑅𝐹)) | ||
Theorem | caofrss 7708* | Transfer a relation subset law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑅𝑦 → 𝑥𝑇𝑦)) ⇒ ⊢ (𝜑 → (𝐹 ∘r 𝑅𝐺 → 𝐹 ∘r 𝑇𝐺)) | ||
Theorem | caofass 7709* | Transfer an associative law to the function operation. (Contributed by Mario Carneiro, 26-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐻:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝑅𝑦)𝑇𝑧) = (𝑥𝑂(𝑦𝑃𝑧))) ⇒ ⊢ (𝜑 → ((𝐹 ∘f 𝑅𝐺) ∘f 𝑇𝐻) = (𝐹 ∘f 𝑂(𝐺 ∘f 𝑃𝐻))) | ||
Theorem | caoftrn 7710* | Transfer a transitivity law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐻:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝑅𝑦 ∧ 𝑦𝑇𝑧) → 𝑥𝑈𝑧)) ⇒ ⊢ (𝜑 → ((𝐹 ∘r 𝑅𝐺 ∧ 𝐺 ∘r 𝑇𝐻) → 𝐹 ∘r 𝑈𝐻)) | ||
Theorem | caofdi 7711* | Transfer a distributive law to the function operation. (Contributed by Mario Carneiro, 26-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐾) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐻:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑇(𝑦𝑅𝑧)) = ((𝑥𝑇𝑦)𝑂(𝑥𝑇𝑧))) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑇(𝐺 ∘f 𝑅𝐻)) = ((𝐹 ∘f 𝑇𝐺) ∘f 𝑂(𝐹 ∘f 𝑇𝐻))) | ||
Theorem | caofdir 7712* | Transfer a reverse distributive law to the function operation. (Contributed by NM, 19-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐾) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐻:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝐾)) → ((𝑥𝑅𝑦)𝑇𝑧) = ((𝑥𝑇𝑧)𝑂(𝑦𝑇𝑧))) ⇒ ⊢ (𝜑 → ((𝐺 ∘f 𝑅𝐻) ∘f 𝑇𝐹) = ((𝐺 ∘f 𝑇𝐹) ∘f 𝑂(𝐻 ∘f 𝑇𝐹))) | ||
Theorem | caonncan 7713* | Transfer nncan 11493-shaped laws to vectors of numbers. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐴:𝐼⟶𝑆) & ⊢ (𝜑 → 𝐵:𝐼⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑀(𝑥𝑀𝑦)) = 𝑦) ⇒ ⊢ (𝜑 → (𝐴 ∘f 𝑀(𝐴 ∘f 𝑀𝐵)) = 𝐵) | ||
Syntax | crpss 7714 | Extend class notation to include the reified proper subset relation. |
class [⊊] | ||
Definition | df-rpss 7715* | Define a relation which corresponds to proper subsethood df-pss 3966 on sets. This allows to use proper subsethood with general concepts that require relations, such as strict ordering, see sorpss 7720. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ [⊊] = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ⊊ 𝑦} | ||
Theorem | relrpss 7716 | The proper subset relation is a relation. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ Rel [⊊] | ||
Theorem | brrpssg 7717 | The proper subset relation on sets is the same as class proper subsethood. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 [⊊] 𝐵 ↔ 𝐴 ⊊ 𝐵)) | ||
Theorem | brrpss 7718 | The proper subset relation on sets is the same as class proper subsethood. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 [⊊] 𝐵 ↔ 𝐴 ⊊ 𝐵) | ||
Theorem | porpss 7719 | Every class is partially ordered by proper subsets. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ [⊊] Po 𝐴 | ||
Theorem | sorpss 7720* | Express strict ordering under proper subsets, i.e. the notion of a chain of sets. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ ( [⊊] Or 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥)) | ||
Theorem | sorpssi 7721 | Property of a chain of sets. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ (( [⊊] Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) | ||
Theorem | sorpssun 7722 | A chain of sets is closed under binary union. (Contributed by Mario Carneiro, 16-May-2015.) |
⊢ (( [⊊] Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 ∪ 𝐶) ∈ 𝐴) | ||
Theorem | sorpssin 7723 | A chain of sets is closed under binary intersection. (Contributed by Mario Carneiro, 16-May-2015.) |
⊢ (( [⊊] Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 ∩ 𝐶) ∈ 𝐴) | ||
Theorem | sorpssuni 7724* | In a chain of sets, a maximal element is the union of the chain. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ ( [⊊] Or 𝑌 → (∃𝑢 ∈ 𝑌 ∀𝑣 ∈ 𝑌 ¬ 𝑢 ⊊ 𝑣 ↔ ∪ 𝑌 ∈ 𝑌)) | ||
Theorem | sorpssint 7725* | In a chain of sets, a minimal element is the intersection of the chain. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ ( [⊊] Or 𝑌 → (∃𝑢 ∈ 𝑌 ∀𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢 ↔ ∩ 𝑌 ∈ 𝑌)) | ||
Theorem | sorpsscmpl 7726* | The componentwise complement of a chain of sets is also a chain of sets. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ ( [⊊] Or 𝑌 → [⊊] Or {𝑢 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑢) ∈ 𝑌}) | ||
Axiom | ax-un 7727* |
Axiom of Union. An axiom of Zermelo-Fraenkel set theory. It states
that a set 𝑦 exists that includes the union of a
given set 𝑥
i.e. the collection of all members of the members of 𝑥. The
variant axun2 7729 states that the union itself exists. A
version with the
standard abbreviation for union is uniex2 7730. A version using class
notation is uniex 7733.
The union of a class df-uni 4908 should not be confused with the union of two classes df-un 3952. Their relationship is shown in unipr 4925. (Contributed by NM, 23-Dec-1993.) |
⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) | ||
Theorem | zfun 7728* | Axiom of Union expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.) Use ax-un 7727 instead. (New usage is discouraged.) |
⊢ ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) | ||
Theorem | axun2 7729* | A variant of the Axiom of Union ax-un 7727. For any set 𝑥, there exists a set 𝑦 whose members are exactly the members of the members of 𝑥 i.e. the union of 𝑥. Axiom Union of [BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.) |
⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) | ||
Theorem | uniex2 7730* | The Axiom of Union using the standard abbreviation for union. Given any set 𝑥, its union 𝑦 exists. (Contributed by NM, 4-Jun-2006.) |
⊢ ∃𝑦 𝑦 = ∪ 𝑥 | ||
Theorem | vuniex 7731 | The union of a setvar is a set. (Contributed by BJ, 3-May-2021.) (Revised by BJ, 6-Apr-2024.) |
⊢ ∪ 𝑥 ∈ V | ||
Theorem | uniexg 7732 | The ZF Axiom of Union in class notation, in the form of a theorem instead of an inference. We use the antecedent 𝐴 ∈ 𝑉 instead of 𝐴 ∈ V to make the theorem more general and thus shorten some proofs; obviously the universal class constant V is one possible substitution for class variable 𝑉. (Contributed by NM, 25-Nov-1994.) |
⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) | ||
Theorem | uniex 7733 | The Axiom of Union in class notation. This says that if 𝐴 is a set i.e. 𝐴 ∈ V (see isset 3485), then the union of 𝐴 is also a set. Same as Axiom 3 of [TakeutiZaring] p. 16. (Contributed by NM, 11-Aug-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ∪ 𝐴 ∈ V | ||
Theorem | uniexd 7734 | Deduction version of the ZF Axiom of Union in class notation. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∪ 𝐴 ∈ V) | ||
Theorem | unex 7735 | The union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 1-Jul-1994.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∪ 𝐵) ∈ V | ||
Theorem | tpex 7736 | An unordered triple of classes exists. (Contributed by NM, 10-Apr-1994.) |
⊢ {𝐴, 𝐵, 𝐶} ∈ V | ||
Theorem | unexb 7737 | Existence of union is equivalent to existence of its components. (Contributed by NM, 11-Jun-1998.) |
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ∪ 𝐵) ∈ V) | ||
Theorem | unexg 7738 | A union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 18-Sep-2006.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) | ||
Theorem | xpexg 7739 | The Cartesian product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. See also xpexgALT 7970. (Contributed by NM, 14-Aug-1994.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) | ||
Theorem | xpexd 7740 | The Cartesian product of two sets is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐴 × 𝐵) ∈ V) | ||
Theorem | 3xpexg 7741 | The Cartesian product of three sets is a set. (Contributed by Alexander van der Vekens, 21-Feb-2018.) |
⊢ (𝑉 ∈ 𝑊 → ((𝑉 × 𝑉) × 𝑉) ∈ V) | ||
Theorem | xpex 7742 | The Cartesian product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. (Contributed by NM, 14-Aug-1994.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 × 𝐵) ∈ V | ||
Theorem | unexd 7743 | The union of two sets is a set. (Contributed by SN, 16-Jul-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ V) | ||
Theorem | sqxpexg 7744 | The Cartesian square of a set is a set. (Contributed by AV, 13-Jan-2020.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 × 𝐴) ∈ V) | ||
Theorem | abnexg 7745* | Sufficient condition for a class abstraction to be a proper class. The class 𝐹 can be thought of as an expression in 𝑥 and the abstraction appearing in the statement as the class of values 𝐹 as 𝑥 varies through 𝐴. Assuming the antecedents, if that class is a set, then so is the "domain" 𝐴. The converse holds without antecedent, see abrexexg 7949. Note that the second antecedent ∀𝑥 ∈ 𝐴𝑥 ∈ 𝐹 cannot be translated to 𝐴 ⊆ 𝐹 since 𝐹 may depend on 𝑥. In applications, one may take 𝐹 = {𝑥} or 𝐹 = 𝒫 𝑥 (see snnex 7747 and pwnex 7748 respectively, proved from abnex 7746, which is a consequence of abnexg 7745 with 𝐴 = V). (Contributed by BJ, 2-Dec-2021.) |
⊢ (∀𝑥 ∈ 𝐴 (𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹) → ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐹} ∈ 𝑊 → 𝐴 ∈ V)) | ||
Theorem | abnex 7746* | Sufficient condition for a class abstraction to be a proper class. Lemma for snnex 7747 and pwnex 7748. See the comment of abnexg 7745. (Contributed by BJ, 2-May-2021.) |
⊢ (∀𝑥(𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹) → ¬ {𝑦 ∣ ∃𝑥 𝑦 = 𝐹} ∈ V) | ||
Theorem | snnex 7747* | The class of all singletons is a proper class. See also pwnex 7748. (Contributed by NM, 10-Oct-2008.) (Proof shortened by Eric Schmidt, 7-Dec-2008.) (Proof shortened by BJ, 5-Dec-2021.) |
⊢ {𝑥 ∣ ∃𝑦 𝑥 = {𝑦}} ∉ V | ||
Theorem | pwnex 7748* | The class of all power sets is a proper class. See also snnex 7747. (Contributed by BJ, 2-May-2021.) |
⊢ {𝑥 ∣ ∃𝑦 𝑥 = 𝒫 𝑦} ∉ V | ||
Theorem | difex2 7749 | If the subtrahend of a class difference exists, then the minuend exists iff the difference exists. (Contributed by NM, 12-Nov-2003.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ (𝐵 ∈ 𝐶 → (𝐴 ∈ V ↔ (𝐴 ∖ 𝐵) ∈ V)) | ||
Theorem | difsnexi 7750 | If the difference of a class and a singleton is a set, the class itself is a set. (Contributed by AV, 15-Jan-2019.) |
⊢ ((𝑁 ∖ {𝐾}) ∈ V → 𝑁 ∈ V) | ||
Theorem | uniuni 7751* | Expression for double union that moves union into a class abstraction. (Contributed by FL, 28-May-2007.) |
⊢ ∪ ∪ 𝐴 = ∪ {𝑥 ∣ ∃𝑦(𝑥 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴)} | ||
Theorem | uniexr 7752 | Converse of the Axiom of Union. Note that it does not require ax-un 7727. (Contributed by NM, 11-Nov-2003.) |
⊢ (∪ 𝐴 ∈ 𝑉 → 𝐴 ∈ V) | ||
Theorem | uniexb 7753 | The Axiom of Union and its converse. A class is a set iff its union is a set. (Contributed by NM, 11-Nov-2003.) |
⊢ (𝐴 ∈ V ↔ ∪ 𝐴 ∈ V) | ||
Theorem | pwexr 7754 | Converse of the Axiom of Power Sets. Note that it does not require ax-pow 5362. (Contributed by NM, 11-Nov-2003.) |
⊢ (𝒫 𝐴 ∈ 𝑉 → 𝐴 ∈ V) | ||
Theorem | pwexb 7755 | The Axiom of Power Sets and its converse. A class is a set iff its power class is a set. (Contributed by NM, 11-Nov-2003.) |
⊢ (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V) | ||
Theorem | elpwpwel 7756 | A class belongs to a double power class if and only if its union belongs to the power class. (Contributed by BJ, 22-Jan-2023.) |
⊢ (𝐴 ∈ 𝒫 𝒫 𝐵 ↔ ∪ 𝐴 ∈ 𝒫 𝐵) | ||
Theorem | eldifpw 7757 | Membership in a power class difference. (Contributed by NM, 25-Mar-2007.) |
⊢ 𝐶 ∈ V ⇒ ⊢ ((𝐴 ∈ 𝒫 𝐵 ∧ ¬ 𝐶 ⊆ 𝐵) → (𝐴 ∪ 𝐶) ∈ (𝒫 (𝐵 ∪ 𝐶) ∖ 𝒫 𝐵)) | ||
Theorem | elpwun 7758 | Membership in the power class of a union. (Contributed by NM, 26-Mar-2007.) |
⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 ∈ 𝒫 (𝐵 ∪ 𝐶) ↔ (𝐴 ∖ 𝐶) ∈ 𝒫 𝐵) | ||
Theorem | pwuncl 7759 | Power classes are closed under union. (Contributed by AV, 27-Feb-2024.) |
⊢ ((𝐴 ∈ 𝒫 𝑋 ∧ 𝐵 ∈ 𝒫 𝑋) → (𝐴 ∪ 𝐵) ∈ 𝒫 𝑋) | ||
Theorem | iunpw 7760* | An indexed union of a power class in terms of the power class of the union of its index. Part of Exercise 24(b) of [Enderton] p. 33. (Contributed by NM, 29-Nov-2003.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝑥 = ∪ 𝐴 ↔ 𝒫 ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝒫 𝑥) | ||
Theorem | fr3nr 7761 | A well-founded relation has no 3-cycle loops. Special case of Proposition 6.23 of [TakeutiZaring] p. 30. (Contributed by NM, 10-Apr-1994.) (Revised by Mario Carneiro, 22-Jun-2015.) |
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵)) | ||
Theorem | epne3 7762 | A well-founded class contains no 3-cycle loops. (Contributed by NM, 19-Apr-1994.) (Revised by Mario Carneiro, 22-Jun-2015.) |
⊢ (( E Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐷 ∧ 𝐷 ∈ 𝐵)) | ||
Theorem | dfwe2 7763* | Alternate definition of well-ordering. Definition 6.24(2) of [TakeutiZaring] p. 30. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) | ||
Theorem | epweon 7764 | The membership relation well-orders the class of ordinal numbers. This proof does not require the axiom of regularity. Proposition 4.8(g) of [Mendelson] p. 244. For a shorter proof requiring ax-un 7727, see epweonALT 7765. (Contributed by NM, 1-Nov-2003.) Avoid ax-un 7727. (Revised by BTernaryTau, 30-Nov-2024.) |
⊢ E We On | ||
Theorem | epweonALT 7765 | Alternate proof of epweon 7764, shorter but requiring ax-un 7727. (Contributed by NM, 1-Nov-2003.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ E We On | ||
Theorem | ordon 7766 | The class of all ordinal numbers is ordinal. Proposition 7.12 of [TakeutiZaring] p. 38, but without using the Axiom of Regularity. (Contributed by NM, 17-May-1994.) |
⊢ Ord On | ||
Theorem | onprc 7767 | No set contains all ordinal numbers. Proposition 7.13 of [TakeutiZaring] p. 38, but without using the Axiom of Regularity. This is also known as the Burali-Forti paradox (remark in [Enderton] p. 194). In 1897, Cesare Burali-Forti noticed that since the "set" of all ordinal numbers is an ordinal class (ordon 7766), it must be both an element of the set of all ordinal numbers yet greater than every such element. ZF set theory resolves this paradox by not allowing the class of all ordinal numbers to be a set (so instead it is a proper class). Here we prove the denial of its existence. (Contributed by NM, 18-May-1994.) |
⊢ ¬ On ∈ V | ||
Theorem | ssorduni 7768 | The union of a class of ordinal numbers is ordinal. Proposition 7.19 of [TakeutiZaring] p. 40. Lemma 2.7 of [Schloeder] p. 4. (Contributed by NM, 30-May-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ (𝐴 ⊆ On → Ord ∪ 𝐴) | ||
Theorem | ssonuni 7769 | The union of a set of ordinal numbers is an ordinal number. Theorem 9 of [Suppes] p. 132. Lemma 2.7 of [Schloeder] p. 4. (Contributed by NM, 1-Nov-2003.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ⊆ On → ∪ 𝐴 ∈ On)) | ||
Theorem | ssonunii 7770 | The union of a set of ordinal numbers is an ordinal number. Corollary 7N(d) of [Enderton] p. 193. (Contributed by NM, 20-Sep-2003.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ⊆ On → ∪ 𝐴 ∈ On) | ||
Theorem | ordeleqon 7771 | A way to express the ordinal property of a class in terms of the class of ordinal numbers. Corollary 7.14 of [TakeutiZaring] p. 38 and its converse. (Contributed by NM, 1-Jun-2003.) |
⊢ (Ord 𝐴 ↔ (𝐴 ∈ On ∨ 𝐴 = On)) | ||
Theorem | ordsson 7772 | Any ordinal class is a subclass of the class of ordinal numbers. Corollary 7.15 of [TakeutiZaring] p. 38. (Contributed by NM, 18-May-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ (Ord 𝐴 → 𝐴 ⊆ On) | ||
Theorem | dford5 7773 | A class is ordinal iff it is a subclass of On and transitive. (Contributed by Scott Fenton, 21-Nov-2021.) |
⊢ (Ord 𝐴 ↔ (𝐴 ⊆ On ∧ Tr 𝐴)) | ||
Theorem | onss 7774 | An ordinal number is a subset of the class of ordinal numbers. (Contributed by NM, 5-Jun-1994.) |
⊢ (𝐴 ∈ On → 𝐴 ⊆ On) | ||
Theorem | predon 7775 | The predecessor of an ordinal under E and On is itself. (Contributed by Scott Fenton, 27-Mar-2011.) (Proof shortened by BJ, 16-Oct-2024.) |
⊢ (𝐴 ∈ On → Pred( E , On, 𝐴) = 𝐴) | ||
Theorem | predonOLD 7776 | Obsolete version of predon 7775 as of 16-Oct-2024. (Contributed by Scott Fenton, 27-Mar-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ On → Pred( E , On, 𝐴) = 𝐴) | ||
Theorem | ssonprc 7777 | Two ways of saying a class of ordinals is unbounded. (Contributed by Mario Carneiro, 8-Jun-2013.) |
⊢ (𝐴 ⊆ On → (𝐴 ∉ V ↔ ∪ 𝐴 = On)) | ||
Theorem | onuni 7778 | The union of an ordinal number is an ordinal number. (Contributed by NM, 29-Sep-2006.) |
⊢ (𝐴 ∈ On → ∪ 𝐴 ∈ On) | ||
Theorem | orduni 7779 | The union of an ordinal class is ordinal. (Contributed by NM, 12-Sep-2003.) |
⊢ (Ord 𝐴 → Ord ∪ 𝐴) | ||
Theorem | onint 7780 | The intersection (infimum) of a nonempty class of ordinal numbers belongs to the class. Compare Exercise 4 of [TakeutiZaring] p. 45. (Contributed by NM, 31-Jan-1997.) |
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ 𝐴) | ||
Theorem | onint0 7781 | The intersection of a class of ordinal numbers is zero iff the class contains zero. (Contributed by NM, 24-Apr-2004.) |
⊢ (𝐴 ⊆ On → (∩ 𝐴 = ∅ ↔ ∅ ∈ 𝐴)) | ||
Theorem | onssmin 7782* | A nonempty class of ordinal numbers has the smallest member. Exercise 9 of [TakeutiZaring] p. 40. (Contributed by NM, 3-Oct-2003.) |
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦) | ||
Theorem | onminesb 7783 | If a property is true for some ordinal number, it is true for a minimal ordinal number. This version uses explicit substitution. Theorem Schema 62 of [Suppes] p. 228. (Contributed by NM, 29-Sep-2003.) |
⊢ (∃𝑥 ∈ On 𝜑 → [∩ {𝑥 ∈ On ∣ 𝜑} / 𝑥]𝜑) | ||
Theorem | onminsb 7784 | If a property is true for some ordinal number, it is true for a minimal ordinal number. This version uses implicit substitution. Theorem Schema 62 of [Suppes] p. 228. (Contributed by NM, 3-Oct-2003.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = ∩ {𝑥 ∈ On ∣ 𝜑} → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ On 𝜑 → 𝜓) | ||
Theorem | oninton 7785 | The intersection of a nonempty collection of ordinal numbers is an ordinal number. Compare Exercise 6 of [TakeutiZaring] p. 44. (Contributed by NM, 29-Jan-1997.) |
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ On) | ||
Theorem | onintrab 7786 | The intersection of a class of ordinal numbers exists iff it is an ordinal number. (Contributed by NM, 6-Nov-2003.) |
⊢ (∩ {𝑥 ∈ On ∣ 𝜑} ∈ V ↔ ∩ {𝑥 ∈ On ∣ 𝜑} ∈ On) | ||
Theorem | onintrab2 7787 | An existence condition equivalent to an intersection's being an ordinal number. (Contributed by NM, 6-Nov-2003.) |
⊢ (∃𝑥 ∈ On 𝜑 ↔ ∩ {𝑥 ∈ On ∣ 𝜑} ∈ On) | ||
Theorem | onnmin 7788 | No member of a set of ordinal numbers belongs to its minimum. (Contributed by NM, 2-Feb-1997.) |
⊢ ((𝐴 ⊆ On ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵 ∈ ∩ 𝐴) | ||
Theorem | onnminsb 7789* | An ordinal number smaller than the minimum of a set of ordinal numbers does not have the property determining that set. 𝜓 is the wff resulting from the substitution of 𝐴 for 𝑥 in wff 𝜑. (Contributed by NM, 9-Nov-2003.) |
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 ∈ On → (𝐴 ∈ ∩ {𝑥 ∈ On ∣ 𝜑} → ¬ 𝜓)) | ||
Theorem | oneqmin 7790* | A way to show that an ordinal number equals the minimum of a nonempty collection of ordinal numbers: it must be in the collection, and it must not be larger than any member of the collection. (Contributed by NM, 14-Nov-2003.) |
⊢ ((𝐵 ⊆ On ∧ 𝐵 ≠ ∅) → (𝐴 = ∩ 𝐵 ↔ (𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵))) | ||
Theorem | uniordint 7791* | The union of a set of ordinals is equal to the intersection of its upper bounds. Problem 2.5(ii) of [BellMachover] p. 471. (Contributed by NM, 20-Sep-2003.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ⊆ On → ∪ 𝐴 = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥}) | ||
Theorem | onminex 7792* | If a wff is true for an ordinal number, then there is the smallest ordinal number for which it is true. (Contributed by NM, 2-Feb-1997.) (Proof shortened by Mario Carneiro, 20-Nov-2016.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ On 𝜑 → ∃𝑥 ∈ On (𝜑 ∧ ∀𝑦 ∈ 𝑥 ¬ 𝜓)) | ||
Theorem | sucon 7793 | The class of all ordinal numbers is its own successor. (Contributed by NM, 12-Sep-2003.) |
⊢ suc On = On | ||
Theorem | sucexb 7794 | A successor exists iff its class argument exists. (Contributed by NM, 22-Jun-1998.) |
⊢ (𝐴 ∈ V ↔ suc 𝐴 ∈ V) | ||
Theorem | sucexg 7795 | The successor of a set is a set (generalization). (Contributed by NM, 5-Jun-1994.) |
⊢ (𝐴 ∈ 𝑉 → suc 𝐴 ∈ V) | ||
Theorem | sucex 7796 | The successor of a set is a set. (Contributed by NM, 30-Aug-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ suc 𝐴 ∈ V | ||
Theorem | onmindif2 7797 | The minimum of a class of ordinal numbers is less than the minimum of that class with its minimum removed. (Contributed by NM, 20-Nov-2003.) |
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ ∩ (𝐴 ∖ {∩ 𝐴})) | ||
Theorem | ordsuci 7798 | The successor of an ordinal class is an ordinal class. Remark 1.5 of [Schloeder] p. 1. (Contributed by NM, 6-Jun-1994.) Extract and adapt from a subproof of onsuc 7801. (Revised by BTernaryTau, 6-Jan-2025.) (Proof shortened by BJ, 11-Jan-2025.) |
⊢ (Ord 𝐴 → Ord suc 𝐴) | ||
Theorem | sucexeloni 7799 | If the successor of an ordinal number exists, it is an ordinal number. This variation of onsuc 7801 does not require ax-un 7727. (Contributed by BTernaryTau, 30-Nov-2024.) (Proof shortened by BJ, 11-Jan-2025.) |
⊢ ((𝐴 ∈ On ∧ suc 𝐴 ∈ 𝑉) → suc 𝐴 ∈ On) | ||
Theorem | sucexeloniOLD 7800 | Obsolete version of sucexeloni 7799 as of 6-Jan-2025. (Contributed by BTernaryTau, 30-Nov-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ On ∧ suc 𝐴 ∈ 𝑉) → suc 𝐴 ∈ On) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |