![]() |
Metamath
Proof Explorer Theorem List (p. 326 of 437) | < 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-28347) |
![]() (28348-29872) |
![]() (29873-43657) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | scutcut 32501 | Cut properties of the surreal cut operation. (Contributed by Scott Fenton, 8-Dec-2021.) |
⊢ (𝐴 <<s 𝐵 → ((𝐴 |s 𝐵) ∈ No ∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵)) | ||
Theorem | scutbday 32502* | The birthday of the surreal cut is equal to the minimum birthday in the gap. (Contributed by Scott Fenton, 8-Dec-2021.) |
⊢ (𝐴 <<s 𝐵 → ( bday ‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑥 ∈ No ∣ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)})) | ||
Theorem | sslttr 32503 | Transitive law for surreal set less than. (Contributed by Scott Fenton, 9-Dec-2021.) |
⊢ ((𝐴 <<s 𝐵 ∧ 𝐵 <<s 𝐶 ∧ 𝐵 ≠ ∅) → 𝐴 <<s 𝐶) | ||
Theorem | ssltun1 32504 | Union law for surreal set less than. (Contributed by Scott Fenton, 9-Dec-2021.) |
⊢ ((𝐴 <<s 𝐶 ∧ 𝐵 <<s 𝐶) → (𝐴 ∪ 𝐵) <<s 𝐶) | ||
Theorem | ssltun2 32505 | Union law for surreal set less than. (Contributed by Scott Fenton, 9-Dec-2021.) |
⊢ ((𝐴 <<s 𝐵 ∧ 𝐴 <<s 𝐶) → 𝐴 <<s (𝐵 ∪ 𝐶)) | ||
Theorem | scutun12 32506 | Union law for surreal cuts. (Contributed by Scott Fenton, 9-Dec-2021.) |
⊢ ((𝐴 <<s 𝐵 ∧ 𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → ((𝐴 ∪ 𝐶) |s (𝐵 ∪ 𝐷)) = (𝐴 |s 𝐵)) | ||
Theorem | dmscut 32507 | The domain of the surreal cut operation is all separated surreal sets. (Contributed by Scott Fenton, 8-Dec-2021.) |
⊢ dom |s = <<s | ||
Theorem | scutf 32508 | Functionhood statement for the surreal cut operator. (Contributed by Scott Fenton, 15-Dec-2021.) |
⊢ |s : <<s ⟶ No | ||
Theorem | etasslt 32509* | A restatement of noeta 32457 using set less than. (Contributed by Scott Fenton, 10-Dec-2021.) |
⊢ (𝐴 <<s 𝐵 → ∃𝑥 ∈ No (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday ‘𝑥) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵)))) | ||
Theorem | scutbdaybnd 32510 | An upper bound on the birthday of a surreal cut. (Contributed by Scott Fenton, 10-Dec-2021.) |
⊢ (𝐴 <<s 𝐵 → ( bday ‘(𝐴 |s 𝐵)) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵))) | ||
Theorem | scutbdaylt 32511 | If a surreal lies in a gap and is not equal to the cut, its birthday is greater than the cut's. (Contributed by Scott Fenton, 11-Dec-2021.) |
⊢ ((𝑋 ∈ No ∧ (𝐴 <<s {𝑋} ∧ {𝑋} <<s 𝐵) ∧ 𝑋 ≠ (𝐴 |s 𝐵)) → ( bday ‘(𝐴 |s 𝐵)) ∈ ( bday ‘𝑋)) | ||
Theorem | slerec 32512* | A comparison law for surreals considered as cuts of sets of surreals. In Conway's treatment, this is the definition of less than or equal. (Contributed by Scott Fenton, 11-Dec-2021.) |
⊢ (((𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷) ∧ (𝑋 = (𝐴 |s 𝐵) ∧ 𝑌 = (𝐶 |s 𝐷))) → (𝑋 ≤s 𝑌 ↔ (∀𝑑 ∈ 𝐷 𝑋 <s 𝑑 ∧ ∀𝑎 ∈ 𝐴 𝑎 <s 𝑌))) | ||
Theorem | sltrec 32513* | A comparison law for surreals considered as cuts of sets of surreals. (Contributed by Scott Fenton, 11-Dec-2021.) |
⊢ (((𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷) ∧ (𝑋 = (𝐴 |s 𝐵) ∧ 𝑌 = (𝐶 |s 𝐷))) → (𝑋 <s 𝑌 ↔ (∃𝑐 ∈ 𝐶 𝑋 ≤s 𝑐 ∨ ∃𝑏 ∈ 𝐵 𝑏 ≤s 𝑌))) | ||
Syntax | cmade 32514 | Declare the symbol for the made by function. |
class M | ||
Syntax | cold 32515 | Declare the symbol for the older than function. |
class O | ||
Syntax | cnew 32516 | Declare the symbol for the new on function. |
class N | ||
Syntax | cleft 32517 | Declare the symbol for the left option function. |
class L | ||
Syntax | cright 32518 | Declare the symbol for the right option function. |
class R | ||
Definition | df-made 32519 | Define the made by function. This function carries an ordinal to all surreals made by sections of surreals older than it. (Contributed by Scott Fenton, 17-Dec-2021.) |
⊢ M = recs((𝑓 ∈ V ↦ ( |s “ (𝒫 ∪ ran 𝑓 × 𝒫 ∪ ran 𝑓)))) | ||
Definition | df-old 32520 | Define the older than function. This function carries an ordinal to all surreals made by a previous ordinal. (Contributed by Scott Fenton, 17-Dec-2021.) |
⊢ O = (𝑥 ∈ On ↦ ∪ ( M “ 𝑥)) | ||
Definition | df-new 32521 | Define the newer than function. This function carries an ordinal to all surreals made on that day. (Contributed by Scott Fenton, 17-Dec-2021.) |
⊢ N = (𝑥 ∈ On ↦ (( O ‘𝑥) ∖ ( M ‘𝑥))) | ||
Definition | df-left 32522* | Define the left options of a surreal. This is the set of surreals that are "closest" on the left to the given surreal. (Contributed by Scott Fenton, 17-Dec-2021.) |
⊢ L = (𝑥 ∈ No ↦ {𝑦 ∈ ( O ‘( bday ‘𝑥)) ∣ ∀𝑧 ∈ No ((𝑦 <s 𝑧 ∧ 𝑧 <s 𝑥) → ( bday ‘𝑦) ∈ ( bday ‘𝑧))}) | ||
Definition | df-right 32523* | Define the left options of a surreal. This is the set of surreals that are "closest" on the right to the given surreal. (Contributed by Scott Fenton, 17-Dec-2021.) |
⊢ R = (𝑥 ∈ No ↦ {𝑦 ∈ ( O ‘( bday ‘𝑥)) ∣ ∀𝑧 ∈ No ((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → ( bday ‘𝑦) ∈ ( bday ‘𝑧))}) | ||
Theorem | madeval 32524 | The value of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.) |
⊢ (𝐴 ∈ On → ( M ‘𝐴) = ( |s “ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)))) | ||
Theorem | madeval2 32525* | Alternative characterization of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.) |
⊢ (𝐴 ∈ On → ( M ‘𝐴) = {𝑥 ∈ No ∣ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)}) | ||
Syntax | ctxp 32526 | Declare the syntax for tail Cartesian product. |
class (𝐴 ⊗ 𝐵) | ||
Syntax | cpprod 32527 | Declare the syntax for the parallel product. |
class pprod(𝑅, 𝑆) | ||
Syntax | csset 32528 | Declare the subset relationship class. |
class SSet | ||
Syntax | ctrans 32529 | Declare the transitive set class. |
class Trans | ||
Syntax | cbigcup 32530 | Declare the set union relationship. |
class Bigcup | ||
Syntax | cfix 32531 | Declare the syntax for the fixpoints of a class. |
class Fix 𝐴 | ||
Syntax | climits 32532 | Declare the class of limit ordinals. |
class Limits | ||
Syntax | cfuns 32533 | Declare the syntax for the class of all function. |
class Funs | ||
Syntax | csingle 32534 | Declare the syntax for the singleton function. |
class Singleton | ||
Syntax | csingles 32535 | Declare the syntax for the class of all singletons. |
class Singletons | ||
Syntax | cimage 32536 | Declare the syntax for the image functor. |
class Image𝐴 | ||
Syntax | ccart 32537 | Declare the syntax for the cartesian function. |
class Cart | ||
Syntax | cimg 32538 | Declare the syntax for the image function. |
class Img | ||
Syntax | cdomain 32539 | Declare the syntax for the domain function. |
class Domain | ||
Syntax | crange 32540 | Declare the syntax for the range function. |
class Range | ||
Syntax | capply 32541 | Declare the syntax for the application function. |
class Apply | ||
Syntax | ccup 32542 | Declare the syntax for the cup function. |
class Cup | ||
Syntax | ccap 32543 | Declare the syntax for the cap function. |
class Cap | ||
Syntax | csuccf 32544 | Declare the syntax for the successor function. |
class Succ | ||
Syntax | cfunpart 32545 | Declare the syntax for the functional part functor. |
class Funpart𝐹 | ||
Syntax | cfullfn 32546 | Declare the syntax for the full function functor. |
class FullFun𝐹 | ||
Syntax | crestrict 32547 | Declare the syntax for the restriction function. |
class Restrict | ||
Syntax | cub 32548 | Declare the syntax for the upper bound relationship functor. |
class UB𝑅 | ||
Syntax | clb 32549 | Declare the syntax for the lower bound relationship functor. |
class LB𝑅 | ||
Definition | df-txp 32550 | Define the tail cross of two classes. Membership in this class is defined by txpss3v 32574 and brtxp 32576. (Contributed by Scott Fenton, 31-Mar-2012.) |
⊢ (𝐴 ⊗ 𝐵) = ((◡(1st ↾ (V × V)) ∘ 𝐴) ∩ (◡(2nd ↾ (V × V)) ∘ 𝐵)) | ||
Definition | df-pprod 32551 | Define the parallel product of two classes. Membership in this class is defined by pprodss4v 32580 and brpprod 32581. (Contributed by Scott Fenton, 11-Apr-2014.) |
⊢ pprod(𝐴, 𝐵) = ((𝐴 ∘ (1st ↾ (V × V))) ⊗ (𝐵 ∘ (2nd ↾ (V × V)))) | ||
Definition | df-sset 32552 | Define the subset class. For the value, see brsset 32585. (Contributed by Scott Fenton, 31-Mar-2012.) |
⊢ SSet = ((V × V) ∖ ran ( E ⊗ (V ∖ E ))) | ||
Definition | df-trans 32553 | Define the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012.) |
⊢ Trans = (V ∖ ran (( E ∘ E ) ∖ E )) | ||
Definition | df-bigcup 32554 | Define the Bigcup function, which, per fvbigcup 32598, carries a set to its union. (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ Bigcup = ((V × V) ∖ ran ((V ⊗ E ) △ (( E ∘ E ) ⊗ V))) | ||
Definition | df-fix 32555 | Define the class of all fixpoints of a relationship. (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ Fix 𝐴 = dom (𝐴 ∩ I ) | ||
Definition | df-limits 32556 | Define the class of all limit ordinals. (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ Limits = ((On ∩ Fix Bigcup ) ∖ {∅}) | ||
Definition | df-funs 32557 | Define the class of all functions. See elfuns 32611 for membership. (Contributed by Scott Fenton, 18-Feb-2013.) |
⊢ Funs = (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))) | ||
Definition | df-singleton 32558 | Define the singleton function. See brsingle 32613 for its value. (Contributed by Scott Fenton, 4-Apr-2014.) |
⊢ Singleton = ((V × V) ∖ ran ((V ⊗ E ) △ ( I ⊗ V))) | ||
Definition | df-singles 32559 | Define the class of all singletons. See elsingles 32614 for membership. (Contributed by Scott Fenton, 19-Feb-2013.) |
⊢ Singletons = ran Singleton | ||
Definition | df-image 32560 | Define the image functor. This function takes a set 𝐴 to a function 𝑥 ↦ (𝐴 “ 𝑥), providing that the latter exists. See imageval 32626 for the derivation. (Contributed by Scott Fenton, 27-Mar-2014.) |
⊢ Image𝐴 = ((V × V) ∖ ran ((V ⊗ E ) △ (( E ∘ ◡𝐴) ⊗ V))) | ||
Definition | df-cart 32561 | Define the cartesian product function. See brcart 32628 for its value. (Contributed by Scott Fenton, 11-Apr-2014.) |
⊢ Cart = (((V × V) × V) ∖ ran ((V ⊗ E ) △ (pprod( E , E ) ⊗ V))) | ||
Definition | df-img 32562 | Define the image function. See brimg 32633 for its value. (Contributed by Scott Fenton, 12-Apr-2014.) |
⊢ Img = (Image((2nd ∘ 1st ) ↾ (1st ↾ (V × V))) ∘ Cart) | ||
Definition | df-domain 32563 | Define the domain function. See brdomain 32629 for its value. (Contributed by Scott Fenton, 11-Apr-2014.) |
⊢ Domain = Image(1st ↾ (V × V)) | ||
Definition | df-range 32564 | Define the range function. See brrange 32630 for its value. (Contributed by Scott Fenton, 11-Apr-2014.) |
⊢ Range = Image(2nd ↾ (V × V)) | ||
Definition | df-cup 32565 | Define the little cup function. See brcup 32635 for its value. (Contributed by Scott Fenton, 14-Apr-2014.) |
⊢ Cup = (((V × V) × V) ∖ ran ((V ⊗ E ) △ (((◡1st ∘ E ) ∪ (◡2nd ∘ E )) ⊗ V))) | ||
Definition | df-cap 32566 | Define the little cap function. See brcap 32636 for its value. (Contributed by Scott Fenton, 17-Apr-2014.) |
⊢ Cap = (((V × V) × V) ∖ ran ((V ⊗ E ) △ (((◡1st ∘ E ) ∩ (◡2nd ∘ E )) ⊗ V))) | ||
Definition | df-restrict 32567 | Define the restriction function. See brrestrict 32645 for its value. (Contributed by Scott Fenton, 17-Apr-2014.) |
⊢ Restrict = (Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st ))))) | ||
Definition | df-succf 32568 | Define the successor function. See brsuccf 32637 for its value. (Contributed by Scott Fenton, 14-Apr-2014.) |
⊢ Succ = (Cup ∘ ( I ⊗ Singleton)) | ||
Definition | df-apply 32569 | Define the application function. See brapply 32634 for its value. (Contributed by Scott Fenton, 12-Apr-2014.) |
⊢ Apply = (( Bigcup ∘ Bigcup ) ∘ (((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I , Singleton)))) | ||
Definition | df-funpart 32570 | Define the functional part of a class 𝐹. This is the maximal part of 𝐹 that is a function. See funpartfun 32639 and funpartfv 32641 for the meaning of this statement. (Contributed by Scott Fenton, 16-Apr-2014.) |
⊢ Funpart𝐹 = (𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons ))) | ||
Definition | df-fullfun 32571 | Define the full function over 𝐹. This is a function with domain V that always agrees with 𝐹 for its value. (Contributed by Scott Fenton, 17-Apr-2014.) |
⊢ FullFun𝐹 = (Funpart𝐹 ∪ ((V ∖ dom Funpart𝐹) × {∅})) | ||
Definition | df-ub 32572 | Define the upper bound relationship functor. See brub 32650 for value. (Contributed by Scott Fenton, 3-May-2018.) |
⊢ UB𝑅 = ((V × V) ∖ ((V ∖ 𝑅) ∘ ◡ E )) | ||
Definition | df-lb 32573 | Define the lower bound relationship functor. See brlb 32651 for value. (Contributed by Scott Fenton, 3-May-2018.) |
⊢ LB𝑅 = UB◡𝑅 | ||
Theorem | txpss3v 32574 | A tail Cartesian product is a subset of the class of ordered triples. (Contributed by Scott Fenton, 31-Mar-2012.) |
⊢ (𝐴 ⊗ 𝐵) ⊆ (V × (V × V)) | ||
Theorem | txprel 32575 | A tail Cartesian product is a relationship. (Contributed by Scott Fenton, 31-Mar-2012.) |
⊢ Rel (𝐴 ⊗ 𝐵) | ||
Theorem | brtxp 32576 | Characterize a ternary relation over a tail Cartesian product. Together with txpss3v 32574, this completely defines membership in a tail cross. (Contributed by Scott Fenton, 31-Mar-2012.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ 𝑋 ∈ V & ⊢ 𝑌 ∈ V & ⊢ 𝑍 ∈ V ⇒ ⊢ (𝑋(𝐴 ⊗ 𝐵)〈𝑌, 𝑍〉 ↔ (𝑋𝐴𝑌 ∧ 𝑋𝐵𝑍)) | ||
Theorem | brtxp2 32577* | The binary relation over a tail cross when the second argument is not an ordered pair. (Contributed by Scott Fenton, 14-Apr-2014.) (Revised by Mario Carneiro, 3-May-2015.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴(𝑅 ⊗ 𝑆)𝐵 ↔ ∃𝑥∃𝑦(𝐵 = 〈𝑥, 𝑦〉 ∧ 𝐴𝑅𝑥 ∧ 𝐴𝑆𝑦)) | ||
Theorem | dfpprod2 32578 | Expanded definition of parallel product. (Contributed by Scott Fenton, 3-May-2014.) |
⊢ pprod(𝐴, 𝐵) = ((◡(1st ↾ (V × V)) ∘ (𝐴 ∘ (1st ↾ (V × V)))) ∩ (◡(2nd ↾ (V × V)) ∘ (𝐵 ∘ (2nd ↾ (V × V))))) | ||
Theorem | pprodcnveq 32579 | A converse law for parallel product. (Contributed by Scott Fenton, 3-May-2014.) |
⊢ pprod(𝑅, 𝑆) = ◡pprod(◡𝑅, ◡𝑆) | ||
Theorem | pprodss4v 32580 | The parallel product is a subclass of ((V × V) × (V × V)). (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ pprod(𝐴, 𝐵) ⊆ ((V × V) × (V × V)) | ||
Theorem | brpprod 32581 | Characterize a quaternary relation over a tail Cartesian product. Together with pprodss4v 32580, this completely defines membership in a parallel product. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝑋 ∈ V & ⊢ 𝑌 ∈ V & ⊢ 𝑍 ∈ V & ⊢ 𝑊 ∈ V ⇒ ⊢ (〈𝑋, 𝑌〉pprod(𝐴, 𝐵)〈𝑍, 𝑊〉 ↔ (𝑋𝐴𝑍 ∧ 𝑌𝐵𝑊)) | ||
Theorem | brpprod3a 32582* | Condition for parallel product when the last argument is not an ordered pair. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝑋 ∈ V & ⊢ 𝑌 ∈ V & ⊢ 𝑍 ∈ V ⇒ ⊢ (〈𝑋, 𝑌〉pprod(𝑅, 𝑆)𝑍 ↔ ∃𝑧∃𝑤(𝑍 = 〈𝑧, 𝑤〉 ∧ 𝑋𝑅𝑧 ∧ 𝑌𝑆𝑤)) | ||
Theorem | brpprod3b 32583* | Condition for parallel product when the first argument is not an ordered pair. (Contributed by Scott Fenton, 3-May-2014.) |
⊢ 𝑋 ∈ V & ⊢ 𝑌 ∈ V & ⊢ 𝑍 ∈ V ⇒ ⊢ (𝑋pprod(𝑅, 𝑆)〈𝑌, 𝑍〉 ↔ ∃𝑧∃𝑤(𝑋 = 〈𝑧, 𝑤〉 ∧ 𝑧𝑅𝑌 ∧ 𝑤𝑆𝑍)) | ||
Theorem | relsset 32584 | The subset class is a binary relation. (Contributed by Scott Fenton, 31-Mar-2012.) |
⊢ Rel SSet | ||
Theorem | brsset 32585 | For sets, the SSet binary relation is equivalent to the subset relationship. (Contributed by Scott Fenton, 31-Mar-2012.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 SSet 𝐵 ↔ 𝐴 ⊆ 𝐵) | ||
Theorem | idsset 32586 | I is equal to the intersection of SSet and its converse. (Contributed by Scott Fenton, 31-Mar-2012.) |
⊢ I = ( SSet ∩ ◡ SSet ) | ||
Theorem | eltrans 32587 | Membership in the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ Trans ↔ Tr 𝐴) | ||
Theorem | dfon3 32588 | A quantifier-free definition of On. (Contributed by Scott Fenton, 5-Apr-2012.) |
⊢ On = (V ∖ ran (( SSet ∩ ( Trans × V)) ∖ ( I ∪ E ))) | ||
Theorem | dfon4 32589 | Another quantifier-free definition of On. (Contributed by Scott Fenton, 4-May-2014.) |
⊢ On = (V ∖ (( SSet ∖ ( I ∪ E )) “ Trans )) | ||
Theorem | brtxpsd 32590* | Expansion of a common form used in quantifier-free definitions. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (¬ 𝐴ran ((V ⊗ E ) △ (𝑅 ⊗ V))𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥𝑅𝐴)) | ||
Theorem | brtxpsd2 32591* | Another common abbreviation for quantifier-free definitions. (Contributed by Scott Fenton, 21-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝑅 = (𝐶 ∖ ran ((V ⊗ E ) △ (𝑆 ⊗ V))) & ⊢ 𝐴𝐶𝐵 ⇒ ⊢ (𝐴𝑅𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥𝑆𝐴)) | ||
Theorem | brtxpsd3 32592* | A third common abbreviation for quantifier-free definitions. (Contributed by Scott Fenton, 3-May-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝑅 = (𝐶 ∖ ran ((V ⊗ E ) △ (𝑆 ⊗ V))) & ⊢ 𝐴𝐶𝐵 & ⊢ (𝑥 ∈ 𝑋 ↔ 𝑥𝑆𝐴) ⇒ ⊢ (𝐴𝑅𝐵 ↔ 𝐵 = 𝑋) | ||
Theorem | relbigcup 32593 | The Bigcup relationship is a relationship. (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ Rel Bigcup | ||
Theorem | brbigcup 32594 | Binary relation over Bigcup . (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 Bigcup 𝐵 ↔ ∪ 𝐴 = 𝐵) | ||
Theorem | dfbigcup2 32595 | Bigcup using maps-to notation. (Contributed by Scott Fenton, 16-Apr-2012.) |
⊢ Bigcup = (𝑥 ∈ V ↦ ∪ 𝑥) | ||
Theorem | fobigcup 32596 | Bigcup maps the universe onto itself. (Contributed by Scott Fenton, 16-Apr-2012.) |
⊢ Bigcup :V–onto→V | ||
Theorem | fnbigcup 32597 | Bigcup is a function over the universal class. (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ Bigcup Fn V | ||
Theorem | fvbigcup 32598 | For sets, Bigcup yields union. (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ( Bigcup ‘𝐴) = ∪ 𝐴 | ||
Theorem | elfix 32599 | Membership in the fixpoints of a class. (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ Fix 𝑅 ↔ 𝐴𝑅𝐴) | ||
Theorem | elfix2 32600 | Alternative membership in the fixpoint of a class. (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ Rel 𝑅 ⇒ ⊢ (𝐴 ∈ Fix 𝑅 ↔ 𝐴𝑅𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |