Home | New
Foundations Explorer Theorem List (p. 44 of 64) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > NFE Home Page > Theorem List Contents This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dfpw12 4301 | Alternate expression for unit power classes. (Contributed by SF, 26-Jan-2015.) |
⊢ ℘_{1}A = ( SI_{k} (A ×_{k} A) “_{k} V) | ||
Theorem | pw1exg 4302 | The unit power class preserves sethood. (Contributed by SF, 14-Jan-2015.) |
⊢ (A ∈ V → ℘_{1}A ∈ V) | ||
Theorem | pw1ex 4303 | The unit power class preserves sethood. (Contributed by SF, 14-Jan-2015.) |
⊢ A ∈ V ⇒ ⊢ ℘_{1}A ∈ V | ||
Theorem | insklem 4304* | Lemma for ins2kexg 4305 and ins3kexg 4306. Equality for subsets of (℘_{1}1_{c} ×_{k} (V ×_{k} V)). (Contributed by SF, 14-Jan-2015.) |
⊢ A ⊆ (℘_{1}1_{c} ×_{k} (V ×_{k} V)) & ⊢ B ⊆ (℘_{1}1_{c} ×_{k} (V ×_{k} V)) ⇒ ⊢ (A = B ↔ ∀x∀y∀z(⟪{{x}}, ⟪y, z⟫⟫ ∈ A ↔ ⟪{{x}}, ⟪y, z⟫⟫ ∈ B)) | ||
Theorem | ins2kexg 4305 | Ins2_{k} preserves sethood. (Contributed by SF, 14-Jan-2015.) |
⊢ (A ∈ V → Ins2_{k} A ∈ V) | ||
Theorem | ins3kexg 4306 | Ins3_{k} preserves sethood. (Contributed by SF, 14-Jan-2015.) |
⊢ (A ∈ V → Ins3_{k} A ∈ V) | ||
Theorem | ins2kex 4307 | Ins2_{k} preserves sethood. (Contributed by SF, 14-Jan-2015.) |
⊢ A ∈ V ⇒ ⊢ Ins2_{k} A ∈ V | ||
Theorem | ins3kex 4308 | Ins3_{k} preserves sethood. (Contributed by SF, 14-Jan-2015.) |
⊢ A ∈ V ⇒ ⊢ Ins3_{k} A ∈ V | ||
Theorem | cokexg 4309 | The Kuratowski composition of two sets is a set. (Contributed by SF, 14-Jan-2015.) |
⊢ ((A ∈ V ∧ B ∈ W) → (A ∘_{k} B) ∈ V) | ||
Theorem | cokex 4310 | The Kuratowski composition of two sets is a set. (Contributed by SF, 14-Jan-2015.) |
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (A ∘_{k} B) ∈ V | ||
Theorem | imagekexg 4311 | The Kuratowski image functor preserves sethood. (Contributed by SF, 14-Jan-2015.) |
⊢ (A ∈ V → Image_{k}A ∈ V) | ||
Theorem | imagekex 4312 | The Kuratowski image functor preserves sethood. (Contributed by SF, 14-Jan-2015.) |
⊢ A ∈ V ⇒ ⊢ Image_{k}A ∈ V | ||
Theorem | dfidk2 4313 | Definition of I_{k} in terms of S_{k}. (Contributed by SF, 14-Jan-2015.) |
⊢ I_{k} = ( S_{k} ∩ ^{◡}_{k} S_{k} ) | ||
Theorem | idkex 4314 | The Kuratowski identity relationship is a set. (Contributed by SF, 14-Jan-2015.) |
⊢ I_{k} ∈ V | ||
Theorem | dfuni3 4315 | Alternate definition of class union for existence proof. (Contributed by SF, 14-Jan-2015.) |
⊢ ∪A = ⋃_{1}(^{◡}_{k} S_{k} “_{k} A) | ||
Theorem | uniexg 4316 | The sum class of a set is a set. (Contributed by SF, 14-Jan-2015.) |
⊢ (A ∈ V → ∪A ∈ V) | ||
Theorem | uniex 4317 | The sum class of a set is a set. (Contributed by SF, 14-Jan-2015.) |
⊢ A ∈ V ⇒ ⊢ ∪A ∈ V | ||
Theorem | dfint3 4318 | Alternate definition of class intersection for the existence proof. (Contributed by SF, 14-Jan-2015.) |
⊢ ∩A = ∼ ⋃_{1}(^{◡}_{k} ∼ S_{k} “_{k} A) | ||
Theorem | intexg 4319 | The intersection of a set is a set. (Contributed by SF, 14-Jan-2015.) |
⊢ (A ∈ V → ∩A ∈ V) | ||
Theorem | intex 4320 | The intersection of a set is a set. (Contributed by SF, 14-Jan-2015.) |
⊢ A ∈ V ⇒ ⊢ ∩A ∈ V | ||
Theorem | setswith 4321* | Two ways to express the class of all sets that contain A. (Contributed by SF, 14-Jan-2015.) |
⊢ {x ∣ A ∈ x} = if(A ∈ V, ( S_{k} “_{k} {{A}}), ∅) | ||
Theorem | setswithex 4322* | The class of all sets that contain A exist. (Contributed by SF, 14-Jan-2015.) |
⊢ {x ∣ A ∈ x} ∈ V | ||
Theorem | ndisjrelk 4323 | Membership in a particular Kuratowski relationship is equivalent to non-disjointedness. (Contributed by SF, 15-Jan-2015.) |
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (⟪A, B⟫ ∈ (( Ins3_{k} S_{k} ∩ Ins2_{k} S_{k} ) “_{k} ℘_{1}℘_{1}1_{c}) ↔ (A ∩ B) ≠ ∅) | ||
Theorem | abexv 4324* | When x does not occur in φ, {x ∣ φ} is a set. (Contributed by SF, 17-Jan-2015.) |
⊢ {x ∣ φ} ∈ V | ||
Theorem | unipw1 4325 | The union of a unit power class is the original set. (Contributed by SF, 20-Jan-2015.) |
⊢ ∪℘_{1}A = A | ||
Theorem | pw1exb 4326 | Biconditional existence for unit power class. (Contributed by SF, 20-Jan-2015.) |
⊢ (℘_{1}A ∈ V ↔ A ∈ V) | ||
Theorem | dfpw2 4327 | Definition of power set for existence proof. (Contributed by SF, 21-Jan-2015.) |
⊢ ℘A = ∼ (( S_{k} ∖ (℘_{1}A ×_{k} V)) “_{k} 1_{c}) | ||
Theorem | pwexg 4328 | The power class of a set is a set. (Contributed by SF, 21-Jan-2015.) |
⊢ (A ∈ V → ℘A ∈ V) | ||
Theorem | pwex 4329 | The power class of a set is a set. (Contributed by SF, 21-Jan-2015.) |
⊢ A ∈ V ⇒ ⊢ ℘A ∈ V | ||
Theorem | eqpw1uni 4330 | A class of singletons is equal to the unit power class of its union. (Contributed by SF, 26-Jan-2015.) |
⊢ (A ⊆ 1_{c} → A = ℘_{1}∪A) | ||
Theorem | pw1equn 4331* | A condition for a unit power class to equal a union. (Contributed by SF, 26-Jan-2015.) |
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (℘_{1}C = (A ∪ B) ↔ ∃x∃y(C = (x ∪ y) ∧ A = ℘_{1}x ∧ B = ℘_{1}y)) | ||
Theorem | pw1eqadj 4332* | A condition for a unit power class to work out to an adjunction. (Contributed by SF, 26-Jan-2015.) |
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (℘_{1}C = (A ∪ {B}) ↔ ∃x∃y(C = (x ∪ {y}) ∧ A = ℘_{1}x ∧ B = {y})) | ||
Theorem | dfeu2 4333 | Alternate definition of existential uniqueness in terms of abstraction. (Contributed by SF, 29-Jan-2015.) |
⊢ (∃!xφ ↔ {x ∣ φ} ∈ 1_{c}) | ||
Theorem | euabex 4334 | If there is a unique object satisfying a property φ, then the set of all elements that satisfy φ exists. (Contributed by SF, 16-Jan-2015.) |
⊢ (∃!xφ → {x ∣ φ} ∈ V) | ||
Theorem | sspw1 4335* | A condition for being a subclass of a unit power class. Corollary 2 of theorem IX.6.14 of [Rosser] p. 255. (Contributed by SF, 3-Feb-2015.) |
⊢ A ∈ V ⇒ ⊢ (A ⊆ ℘_{1}B ↔ ∃x(x ⊆ B ∧ A = ℘_{1}x)) | ||
Theorem | sspw12 4336* | A set is a subset of cardinal one iff it is the unit power class of some other set. (Contributed by SF, 17-Mar-2015.) |
⊢ A ∈ V ⇒ ⊢ (A ⊆ 1_{c} ↔ ∃x A = ℘_{1}x) | ||
Syntax | cio 4337 | Extend class notation with Russell's definition description binder (inverted iota). |
class (℩xφ) | ||
Theorem | iotajust 4338* | Soundness justification theorem for df-iota 4339. (Contributed by Andrew Salmon, 29-Jun-2011.) |
⊢ ∪{y ∣ {x ∣ φ} = {y}} = ∪{z ∣ {x ∣ φ} = {z}} | ||
Definition | df-iota 4339* | Define Russell's definition description binder, which can be read as "the unique x such that φ," where φ ordinarily contains x as a free variable. Our definition is meaningful only when there is exactly one x such that φ is true (see iotaval 4350); otherwise, it evaluates to the empty set (see iotanul 4354). Russell used the inverted iota symbol ℩ to represent the binder. (Contributed by SF, 12-Jan-2015.) |
⊢ (℩xφ) = ∪{y ∣ {x ∣ φ} = {y}} | ||
Theorem | dfiota2 4340* | Alternate definition for descriptions. Definition 8.18 in [Quine] p. 56. (Contributed by Andrew Salmon, 30-Jun-2011.) |
⊢ (℩xφ) = ∪{y ∣ ∀x(φ ↔ x = y)} | ||
Theorem | nfiota1 4341 | Bound-variable hypothesis builder for the ℩ class. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎx(℩xφ) | ||
Theorem | nfiotad 4342 | Deduction version of nfiota 4343. (Contributed by NM, 18-Feb-2013.) |
⊢ Ⅎyφ & ⊢ (φ → Ⅎxψ) ⇒ ⊢ (φ → Ⅎx(℩yψ)) | ||
Theorem | nfiota 4343 | Bound-variable hypothesis builder for the ℩ class. (Contributed by NM, 23-Aug-2011.) |
⊢ Ⅎxφ ⇒ ⊢ Ⅎx(℩yφ) | ||
Theorem | cbviota 4344 | Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.) |
⊢ (x = y → (φ ↔ ψ)) & ⊢ Ⅎyφ & ⊢ Ⅎxψ ⇒ ⊢ (℩xφ) = (℩yψ) | ||
Theorem | cbviotav 4345* | Change bound variables in a description binder. (Contributed by Andrew Salmon, 1-Aug-2011.) |
⊢ (x = y → (φ ↔ ψ)) ⇒ ⊢ (℩xφ) = (℩yψ) | ||
Theorem | sb8iota 4346 | Variable substitution in description binder. Compare sb8eu 2222. (Contributed by NM, 18-Mar-2013.) |
⊢ Ⅎyφ ⇒ ⊢ (℩xφ) = (℩y[y / x]φ) | ||
Theorem | iotaeq 4347 | Equality theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.) |
⊢ (∀x x = y → (℩xφ) = (℩yφ)) | ||
Theorem | iotabi 4348 | Equivalence theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011.) |
⊢ (∀x(φ ↔ ψ) → (℩xφ) = (℩xψ)) | ||
Theorem | uniabio 4349* | Part of Theorem 8.17 in [Quine] p. 56. This theorem serves as a lemma for the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011.) |
⊢ (∀x(φ ↔ x = y) → ∪{x ∣ φ} = y) | ||
Theorem | iotaval 4350* | Theorem 8.19 in [Quine] p. 57. This theorem is the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011.) |
⊢ (∀x(φ ↔ x = y) → (℩xφ) = y) | ||
Theorem | iotauni 4351 | Equivalence between two different forms of ℩. (Contributed by Andrew Salmon, 12-Jul-2011.) |
⊢ (∃!xφ → (℩xφ) = ∪{x ∣ φ}) | ||
Theorem | iotaint 4352 | Equivalence between two different forms of ℩. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (∃!xφ → (℩xφ) = ∩{x ∣ φ}) | ||
Theorem | iota1 4353 | Property of iota. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.) |
⊢ (∃!xφ → (φ ↔ (℩xφ) = x)) | ||
Theorem | iotanul 4354 | Theorem 8.22 in [Quine] p. 57. This theorem is the result if there isn't exactly one x that satisfies φ. (Contributed by Andrew Salmon, 11-Jul-2011.) |
⊢ (¬ ∃!xφ → (℩xφ) = ∅) | ||
Theorem | iotassuni 4355 | The ℩ class is a subset of the union of all elements satisfying φ. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (℩xφ) ⊆ ∪{x ∣ φ} | ||
Theorem | iotaex 4356 | Theorem 8.23 in [Quine] p. 58. This theorem proves the existence of the ℩ class under our definition. (Contributed by Andrew Salmon, 11-Jul-2011.) |
⊢ (℩xφ) ∈ V | ||
Theorem | iota4 4357 | Theorem *14.22 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 12-Jul-2011.) |
⊢ (∃!xφ → [̣(℩xφ) / x]̣φ) | ||
Theorem | iota4an 4358 | Theorem *14.23 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.) |
⊢ (∃!x(φ ∧ ψ) → [̣(℩x(φ ∧ ψ)) / x]̣φ) | ||
Theorem | iota5 4359* | A method for computing iota. (Contributed by NM, 17-Sep-2013.) |
⊢ ((φ ∧ A ∈ V) → (ψ ↔ x = A)) ⇒ ⊢ ((φ ∧ A ∈ V) → (℩xψ) = A) | ||
Theorem | iotabidv 4360* | Formula-building deduction rule for iota. (Contributed by NM, 20-Aug-2011.) |
⊢ (φ → (ψ ↔ χ)) ⇒ ⊢ (φ → (℩xψ) = (℩xχ)) | ||
Theorem | iotabii 4361 | Formula-building deduction rule for iota. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ (φ ↔ ψ) ⇒ ⊢ (℩xφ) = (℩xψ) | ||
Theorem | iotacl 4362 |
Membership law for descriptions.
This can useful for expanding an unbounded iota-based definition (see df-iota 4339). If you have a bounded iota-based definition, riotacl2 in set.mm may be useful. (Contributed by Andrew Salmon, 1-Aug-2011.) |
⊢ (∃!xφ → (℩xφ) ∈ {x ∣ φ}) | ||
Theorem | reiotacl2 4363 | Membership law for descriptions. (Contributed by SF, 21-Aug-2011.) |
⊢ (∃!x ∈ A φ → (℩x(x ∈ A ∧ φ)) ∈ {x ∈ A ∣ φ}) | ||
Theorem | reiotacl 4364* | Membership law for descriptions. (Contributed by SF, 21-Aug-2011.) |
⊢ (∃!x ∈ A φ → (℩x(x ∈ A ∧ φ)) ∈ A) | ||
Theorem | iota2df 4365 | A condition that allows us to represent "the unique element such that φ " with a class expression A. (Contributed by NM, 30-Dec-2014.) |
⊢ (φ → B ∈ V) & ⊢ (φ → ∃!xψ) & ⊢ ((φ ∧ x = B) → (ψ ↔ χ)) & ⊢ Ⅎxφ & ⊢ (φ → Ⅎxχ) & ⊢ (φ → ℲxB) ⇒ ⊢ (φ → (χ ↔ (℩xψ) = B)) | ||
Theorem | iota2d 4366* | A condition that allows us to represent "the unique element such that φ " with a class expression A. (Contributed by NM, 30-Dec-2014.) |
⊢ (φ → B ∈ V) & ⊢ (φ → ∃!xψ) & ⊢ ((φ ∧ x = B) → (ψ ↔ χ)) ⇒ ⊢ (φ → (χ ↔ (℩xψ) = B)) | ||
Theorem | iota2 4367* | The unique element such that φ. (Contributed by Jeff Madsen, 1-Jun-2011.) (Revised by Mario Carneiro, 23-Dec-2016.) |
⊢ (x = A → (φ ↔ ψ)) ⇒ ⊢ ((A ∈ B ∧ ∃!xφ) → (ψ ↔ (℩xφ) = A)) | ||
Theorem | reiota2 4368* | A condition allowing us to represent "the unique element in A such that φ " with a class expression B. (Contributed by Scott Fenton, 7-Jan-2018.) |
⊢ (x = B → (φ ↔ ψ)) ⇒ ⊢ ((B ∈ A ∧ ∃!x ∈ A φ) → (ψ ↔ (℩x(x ∈ A ∧ φ)) = B)) | ||
Theorem | sniota 4369 | A class abstraction with a unique member can be expressed as a singleton. (Contributed by Mario Carneiro, 23-Dec-2016.) |
⊢ (∃!xφ → {x ∣ φ} = {(℩xφ)}) | ||
Theorem | dfiota3 4370 | The ℩ operation using the if operator. (Contributed by Scott Fenton, 6-Oct-2017.) |
⊢ (℩xφ) = if(∃!xφ, ∪{x ∣ φ}, ∅) | ||
Theorem | csbiotag 4371* | Class substitution within a description binder. (Contributed by Scott Fenton, 6-Oct-2017.) |
⊢ (A ∈ V → [A / x](℩yφ) = (℩y[̣A / x]̣φ)) | ||
Theorem | dfiota4 4372 | Alternate definition of iota in terms of 1_{c}. (Contributed by SF, 29-Jan-2015.) |
⊢ (℩xφ) = ∪∪(1_{c} ∩ {{x ∣ φ}}) | ||
Syntax | cnnc 4373 | Extend the definition of a class to include the set of finite cardinals. |
class Nn | ||
Syntax | c0c 4374 | Extend the definition of a class to include cardinal zero. |
class 0_{c} | ||
Syntax | cplc 4375 | Extend the definition of a class to include cardinal addition. |
class (A +_{c} B) | ||
Syntax | cfin 4376 | Extend the definition of a class to include the set of all finite sets. |
class Fin | ||
Definition | df-0c 4377 | Define cardinal zero. (Contributed by SF, 12-Jan-2015.) |
⊢ 0_{c} = {∅} | ||
Definition | df-addc 4378* | Define cardinal addition. Definition from [Rosser] p. 275. (Contributed by SF, 12-Jan-2015.) |
⊢ (A +_{c} B) = {x ∣ ∃y ∈ A ∃z ∈ B ((y ∩ z) = ∅ ∧ x = (y ∪ z))} | ||
Definition | df-nnc 4379* | Define the finite cardinals. Definition from [Rosser] p. 275. (Contributed by SF, 12-Jan-2015.) |
⊢ Nn = ∩{b ∣ (0_{c} ∈ b ∧ ∀y ∈ b (y +_{c} 1_{c}) ∈ b)} | ||
Definition | df-fin 4380 | Define the set of all finite sets. Definition from [Rosser], p. 417. (Contributed by SF, 12-Jan-2015.) |
⊢ Fin = ∪ Nn | ||
Theorem | dfaddc2 4381 | Alternate definition of cardinal addition to establish stratification. (Contributed by SF, 15-Jan-2015.) |
⊢ (A +_{c} B) = ((( Ins3_{k} ∼ (( Ins3_{k} S_{k} ∩ Ins2_{k} S_{k} ) “_{k} ℘_{1}℘_{1}1_{c}) ∖ (( Ins2_{k} Ins2_{k} S_{k} ⊕ ( Ins2_{k} Ins3_{k} S_{k} ∪ Ins3_{k} SI_{k} SI_{k} S_{k} )) “_{k} ℘_{1}℘_{1}℘_{1}℘_{1}1_{c})) “_{k} ℘_{1}℘_{1}B) “_{k} A) | ||
Theorem | addcexlem 4382 | The expression at the heart of dfaddc2 4381 is a set. (Contributed by SF, 17-Jan-2015.) |
⊢ ( Ins3_{k} ∼ (( Ins3_{k} S_{k} ∩ Ins2_{k} S_{k} ) “_{k} ℘_{1}℘_{1}1_{c}) ∖ (( Ins2_{k} Ins2_{k} S_{k} ⊕ ( Ins2_{k} Ins3_{k} S_{k} ∪ Ins3_{k} SI_{k} SI_{k} S_{k} )) “_{k} ℘_{1}℘_{1}℘_{1}℘_{1}1_{c})) ∈ V | ||
Theorem | addceq1 4383 | Equality law for cardinal addition. (Contributed by SF, 15-Jan-2015.) |
⊢ (A = B → (A +_{c} C) = (B +_{c} C)) | ||
Theorem | addceq2 4384 | Equality law for cardinal addition. (Contributed by SF, 15-Jan-2015.) |
⊢ (A = B → (C +_{c} A) = (C +_{c} B)) | ||
Theorem | addceq12 4385 | Equality law for cardinal addition. (Contributed by SF, 15-Jan-2015.) |
⊢ ((A = C ∧ B = D) → (A +_{c} B) = (C +_{c} D)) | ||
Theorem | addceq1i 4386 | Equality inference for cardinal addition. (Contributed by SF, 3-Feb-2015.) |
⊢ A = B ⇒ ⊢ (A +_{c} C) = (B +_{c} C) | ||
Theorem | addceq2i 4387 | Equality inference for cardinal addition. (Contributed by SF, 3-Feb-2015.) |
⊢ A = B ⇒ ⊢ (C +_{c} A) = (C +_{c} B) | ||
Theorem | addceq12i 4388 | Equality inference for cardinal addition. (Contributed by SF, 3-Feb-2015.) |
⊢ A = B & ⊢ C = D ⇒ ⊢ (A +_{c} C) = (B +_{c} D) | ||
Theorem | addceq1d 4389 | Equality deduction for cardinal addition. (Contributed by SF, 3-Feb-2015.) |
⊢ (φ → A = B) ⇒ ⊢ (φ → (A +_{c} C) = (B +_{c} C)) | ||
Theorem | addceq2d 4390 | Equality deduction for cardinal addition. (Contributed by SF, 3-Feb-2015.) |
⊢ (φ → A = B) ⇒ ⊢ (φ → (C +_{c} A) = (C +_{c} B)) | ||
Theorem | addceq12d 4391 | Equality deduction for cardinal addition. (Contributed by SF, 3-Feb-2015.) |
⊢ (φ → A = B) & ⊢ (φ → C = D) ⇒ ⊢ (φ → (A +_{c} C) = (B +_{c} D)) | ||
Theorem | 0cex 4392 | Cardinal zero is a set. (Contributed by SF, 14-Jan-2015.) |
⊢ 0_{c} ∈ V | ||
Theorem | addcexg 4393 | The cardinal sum of two sets is a set. (Contributed by SF, 15-Jan-2015.) |
⊢ ((A ∈ V ∧ B ∈ W) → (A +_{c} B) ∈ V) | ||
Theorem | addcex 4394 | The cardinal sum of two sets is a set. (Contributed by SF, 25-Jan-2015.) |
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (A +_{c} B) ∈ V | ||
Theorem | dfnnc2 4395 | Definition of the finite cardinals for existence theorem. (Contributed by SF, 14-Jan-2015.) |
⊢ Nn = ∩({x ∣ 0_{c} ∈ x} ∖ (( S_{k} ∖ ( S_{k} ∘_{k} SI_{k} Image_{k}(( Ins3_{k} ∼ (( Ins3_{k} S_{k} ∩ Ins2_{k} S_{k} ) “_{k} ℘_{1}℘_{1}1_{c}) ∖ (( Ins2_{k} Ins2_{k} S_{k} ⊕ ( Ins2_{k} Ins3_{k} S_{k} ∪ Ins3_{k} SI_{k} SI_{k} S_{k} )) “_{k} ℘_{1}℘_{1}℘_{1}℘_{1}1_{c})) “_{k} ℘_{1}℘_{1}1_{c}))) “_{k} 1_{c})) | ||
Theorem | nncex 4396 | The class of all finite cardinals is a set. (Contributed by SF, 14-Jan-2015.) |
⊢ Nn ∈ V | ||
Theorem | finex 4397 | The class of all finite sets is a set. (Contributed by SF, 19-Jan-2015.) |
⊢ Fin ∈ V | ||
Theorem | eladdc 4398* | Membership in cardinal addition. Theorem X.1.1 of [Rosser] p. 275. (Contributed by SF, 16-Jan-2015.) |
⊢ (A ∈ (M +_{c} N) ↔ ∃b ∈ M ∃c ∈ N ((b ∩ c) = ∅ ∧ A = (b ∪ c))) | ||
Theorem | eladdci 4399 | Inference form of membership in cardinal addition. (Contributed by SF, 26-Jan-2015.) |
⊢ ((A ∈ M ∧ B ∈ N ∧ (A ∩ B) = ∅) → (A ∪ B) ∈ (M +_{c} N)) | ||
Theorem | 0nelsuc 4400 | The empty class is not a member of a successor. (Contributed by SF, 14-Jan-2015.) |
⊢ ¬ ∅ ∈ (A +_{c} 1_{c}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |