| Metamath
Proof Explorer Theorem List (p. 359 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | axextbdist 35801 | axextb 2711 with distinctors instead of distinct variable conditions. (Contributed by Scott Fenton, 13-Dec-2010.) |
| ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (𝑥 = 𝑦 ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))) | ||
| Theorem | 19.12b 35802* | Version of 19.12vv 2349 with not-free hypotheses, instead of distinct variable conditions. (Contributed by Scott Fenton, 13-Dec-2010.) (Revised by Mario Carneiro, 11-Dec-2016.) |
| ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥∀𝑦(𝜑 → 𝜓) ↔ ∀𝑦∃𝑥(𝜑 → 𝜓)) | ||
| Theorem | exnel 35803 | There is always a set not in 𝑦. (Contributed by Scott Fenton, 13-Dec-2010.) |
| ⊢ ∃𝑥 ¬ 𝑥 ∈ 𝑦 | ||
| Theorem | distel 35804 | Distinctors in terms of membership. (NOTE: this only works with relations where we can prove el 5442 and elirrv 9636.) (Contributed by Scott Fenton, 15-Dec-2010.) |
| ⊢ (¬ ∀𝑦 𝑦 = 𝑥 ↔ ¬ ∀𝑦 ¬ 𝑥 ∈ 𝑦) | ||
| Theorem | axextndbi 35805 | axextnd 10631 as a biconditional. (Contributed by Scott Fenton, 14-Dec-2010.) |
| ⊢ ∃𝑧(𝑥 = 𝑦 ↔ (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)) | ||
| Theorem | hbntg 35806 | A more general form of hbnt 2294. (Contributed by Scott Fenton, 13-Dec-2010.) |
| ⊢ (∀𝑥(𝜑 → ∀𝑥𝜓) → (¬ 𝜓 → ∀𝑥 ¬ 𝜑)) | ||
| Theorem | hbimtg 35807 | A more general and closed form of hbim 2299. (Contributed by Scott Fenton, 13-Dec-2010.) |
| ⊢ ((∀𝑥(𝜑 → ∀𝑥𝜒) ∧ (𝜓 → ∀𝑥𝜃)) → ((𝜒 → 𝜓) → ∀𝑥(𝜑 → 𝜃))) | ||
| Theorem | hbaltg 35808 | A more general and closed form of hbal 2167. (Contributed by Scott Fenton, 13-Dec-2010.) |
| ⊢ (∀𝑥(𝜑 → ∀𝑦𝜓) → (∀𝑥𝜑 → ∀𝑦∀𝑥𝜓)) | ||
| Theorem | hbng 35809 | A more general form of hbn 2295. (Contributed by Scott Fenton, 13-Dec-2010.) |
| ⊢ (𝜑 → ∀𝑥𝜓) ⇒ ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜑) | ||
| Theorem | hbimg 35810 | A more general form of hbim 2299. (Contributed by Scott Fenton, 13-Dec-2010.) |
| ⊢ (𝜑 → ∀𝑥𝜓) & ⊢ (𝜒 → ∀𝑥𝜃) ⇒ ⊢ ((𝜓 → 𝜒) → ∀𝑥(𝜑 → 𝜃)) | ||
| Syntax | cwsuc 35811 | Declare the syntax for well-founded successor. |
| class wsuc(𝑅, 𝐴, 𝑋) | ||
| Syntax | cwlim 35812 | Declare the syntax for well-founded limit class. |
| class WLim(𝑅, 𝐴) | ||
| Definition | df-wsuc 35813 | Define the concept of a successor in a well-founded set. (Contributed by Scott Fenton, 13-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
| ⊢ wsuc(𝑅, 𝐴, 𝑋) = inf(Pred(◡𝑅, 𝐴, 𝑋), 𝐴, 𝑅) | ||
| Definition | df-wlim 35814* | Define the class of limit points of a well-founded set. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
| ⊢ WLim(𝑅, 𝐴) = {𝑥 ∈ 𝐴 ∣ (𝑥 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))} | ||
| Theorem | wsuceq123 35815 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
| ⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌) → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑆, 𝐵, 𝑌)) | ||
| Theorem | wsuceq1 35816 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) |
| ⊢ (𝑅 = 𝑆 → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑆, 𝐴, 𝑋)) | ||
| Theorem | wsuceq2 35817 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) |
| ⊢ (𝐴 = 𝐵 → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑅, 𝐵, 𝑋)) | ||
| Theorem | wsuceq3 35818 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) |
| ⊢ (𝑋 = 𝑌 → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑅, 𝐴, 𝑌)) | ||
| Theorem | nfwsuc 35819 | Bound-variable hypothesis builder for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
| ⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝑋 ⇒ ⊢ Ⅎ𝑥wsuc(𝑅, 𝐴, 𝑋) | ||
| Theorem | wlimeq12 35820 | Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
| ⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵) → WLim(𝑅, 𝐴) = WLim(𝑆, 𝐵)) | ||
| Theorem | wlimeq1 35821 | Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) |
| ⊢ (𝑅 = 𝑆 → WLim(𝑅, 𝐴) = WLim(𝑆, 𝐴)) | ||
| Theorem | wlimeq2 35822 | Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) |
| ⊢ (𝐴 = 𝐵 → WLim(𝑅, 𝐴) = WLim(𝑅, 𝐵)) | ||
| Theorem | nfwlim 35823 | Bound-variable hypothesis builder for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
| ⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥WLim(𝑅, 𝐴) | ||
| Theorem | elwlim 35824 | Membership in the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
| ⊢ (𝑋 ∈ WLim(𝑅, 𝐴) ↔ (𝑋 ∈ 𝐴 ∧ 𝑋 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑋 = sup(Pred(𝑅, 𝐴, 𝑋), 𝐴, 𝑅))) | ||
| Theorem | wzel 35825 | The zero of a well-founded set is a member of that set. (Contributed by Scott Fenton, 13-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
| ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐴 ≠ ∅) → inf(𝐴, 𝐴, 𝑅) ∈ 𝐴) | ||
| Theorem | wsuclem 35826* | Lemma for the supremum properties of well-founded successor. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
| ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ∃𝑤 ∈ 𝐴 𝑋𝑅𝑤) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ Pred (◡𝑅, 𝐴, 𝑋) ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ Pred (◡𝑅, 𝐴, 𝑋)𝑧𝑅𝑦))) | ||
| Theorem | wsucex 35827 | Existence theorem for well-founded successor. (Contributed by Scott Fenton, 16-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
| ⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → wsuc(𝑅, 𝐴, 𝑋) ∈ V) | ||
| Theorem | wsuccl 35828* | If 𝑋 is a set with an 𝑅 successor in 𝐴, then its well-founded successor is a member of 𝐴. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
| ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → ∃𝑦 ∈ 𝐴 𝑋𝑅𝑦) ⇒ ⊢ (𝜑 → wsuc(𝑅, 𝐴, 𝑋) ∈ 𝐴) | ||
| Theorem | wsuclb 35829 | A well-founded successor is a lower bound on points after 𝑋. (Contributed by Scott Fenton, 16-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
| ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝑋𝑅𝑌) ⇒ ⊢ (𝜑 → ¬ 𝑌𝑅wsuc(𝑅, 𝐴, 𝑋)) | ||
| Theorem | wlimss 35830 | The class of limit points is a subclass of the base class. (Contributed by Scott Fenton, 16-Jun-2018.) |
| ⊢ WLim(𝑅, 𝐴) ⊆ 𝐴 | ||
| Syntax | ctxp 35831 | Declare the syntax for tail Cartesian product. |
| class (𝐴 ⊗ 𝐵) | ||
| Syntax | cpprod 35832 | Declare the syntax for the parallel product. |
| class pprod(𝑅, 𝑆) | ||
| Syntax | csset 35833 | Declare the subset relationship class. |
| class SSet | ||
| Syntax | ctrans 35834 | Declare the transitive set class. |
| class Trans | ||
| Syntax | cbigcup 35835 | Declare the set union relationship. |
| class Bigcup | ||
| Syntax | cfix 35836 | Declare the syntax for the fixpoints of a class. |
| class Fix 𝐴 | ||
| Syntax | climits 35837 | Declare the class of limit ordinals. |
| class Limits | ||
| Syntax | cfuns 35838 | Declare the syntax for the class of all function. |
| class Funs | ||
| Syntax | csingle 35839 | Declare the syntax for the singleton function. |
| class Singleton | ||
| Syntax | csingles 35840 | Declare the syntax for the class of all singletons. |
| class Singletons | ||
| Syntax | cimage 35841 | Declare the syntax for the image functor. |
| class Image𝐴 | ||
| Syntax | ccart 35842 | Declare the syntax for the cartesian function. |
| class Cart | ||
| Syntax | cimg 35843 | Declare the syntax for the image function. |
| class Img | ||
| Syntax | cdomain 35844 | Declare the syntax for the domain function. |
| class Domain | ||
| Syntax | crange 35845 | Declare the syntax for the range function. |
| class Range | ||
| Syntax | capply 35846 | Declare the syntax for the application function. |
| class Apply | ||
| Syntax | ccup 35847 | Declare the syntax for the cup function. |
| class Cup | ||
| Syntax | ccap 35848 | Declare the syntax for the cap function. |
| class Cap | ||
| Syntax | csuccf 35849 | Declare the syntax for the successor function. |
| class Succ | ||
| Syntax | cfunpart 35850 | Declare the syntax for the functional part functor. |
| class Funpart𝐹 | ||
| Syntax | cfullfn 35851 | Declare the syntax for the full function functor. |
| class FullFun𝐹 | ||
| Syntax | crestrict 35852 | Declare the syntax for the restriction function. |
| class Restrict | ||
| Syntax | cub 35853 | Declare the syntax for the upper bound relationship functor. |
| class UB𝑅 | ||
| Syntax | clb 35854 | Declare the syntax for the lower bound relationship functor. |
| class LB𝑅 | ||
| Definition | df-txp 35855 | Define the tail cross of two classes. Membership in this class is defined by txpss3v 35879 and brtxp 35881. (Contributed by Scott Fenton, 31-Mar-2012.) |
| ⊢ (𝐴 ⊗ 𝐵) = ((◡(1st ↾ (V × V)) ∘ 𝐴) ∩ (◡(2nd ↾ (V × V)) ∘ 𝐵)) | ||
| Definition | df-pprod 35856 | Define the parallel product of two classes. Membership in this class is defined by pprodss4v 35885 and brpprod 35886. (Contributed by Scott Fenton, 11-Apr-2014.) |
| ⊢ pprod(𝐴, 𝐵) = ((𝐴 ∘ (1st ↾ (V × V))) ⊗ (𝐵 ∘ (2nd ↾ (V × V)))) | ||
| Definition | df-sset 35857 | Define the subset class. For the value, see brsset 35890. (Contributed by Scott Fenton, 31-Mar-2012.) |
| ⊢ SSet = ((V × V) ∖ ran ( E ⊗ (V ∖ E ))) | ||
| Definition | df-trans 35858 | Define the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012.) |
| ⊢ Trans = (V ∖ ran (( E ∘ E ) ∖ E )) | ||
| Definition | df-bigcup 35859 | Define the Bigcup function, which, per fvbigcup 35903, 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 35860 | Define the class of all fixpoints of a relationship. (Contributed by Scott Fenton, 11-Apr-2012.) |
| ⊢ Fix 𝐴 = dom (𝐴 ∩ I ) | ||
| Definition | df-limits 35861 | Define the class of all limit ordinals. (Contributed by Scott Fenton, 11-Apr-2012.) |
| ⊢ Limits = ((On ∩ Fix Bigcup ) ∖ {∅}) | ||
| Definition | df-funs 35862 | Define the class of all functions. See elfuns 35916 for membership. (Contributed by Scott Fenton, 18-Feb-2013.) |
| ⊢ Funs = (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))) | ||
| Definition | df-singleton 35863 | Define the singleton function. See brsingle 35918 for its value. (Contributed by Scott Fenton, 4-Apr-2014.) |
| ⊢ Singleton = ((V × V) ∖ ran ((V ⊗ E ) △ ( I ⊗ V))) | ||
| Definition | df-singles 35864 | Define the class of all singletons. See elsingles 35919 for membership. (Contributed by Scott Fenton, 19-Feb-2013.) |
| ⊢ Singletons = ran Singleton | ||
| Definition | df-image 35865 | Define the image functor. This function takes a set 𝐴 to a function 𝑥 ↦ (𝐴 “ 𝑥), providing that the latter exists. See imageval 35931 for the derivation. (Contributed by Scott Fenton, 27-Mar-2014.) |
| ⊢ Image𝐴 = ((V × V) ∖ ran ((V ⊗ E ) △ (( E ∘ ◡𝐴) ⊗ V))) | ||
| Definition | df-cart 35866 | Define the cartesian product function. See brcart 35933 for its value. (Contributed by Scott Fenton, 11-Apr-2014.) |
| ⊢ Cart = (((V × V) × V) ∖ ran ((V ⊗ E ) △ (pprod( E , E ) ⊗ V))) | ||
| Definition | df-img 35867 | Define the image function. See brimg 35938 for its value. (Contributed by Scott Fenton, 12-Apr-2014.) |
| ⊢ Img = (Image((2nd ∘ 1st ) ↾ (1st ↾ (V × V))) ∘ Cart) | ||
| Definition | df-domain 35868 | Define the domain function. See brdomain 35934 for its value. (Contributed by Scott Fenton, 11-Apr-2014.) |
| ⊢ Domain = Image(1st ↾ (V × V)) | ||
| Definition | df-range 35869 | Define the range function. See brrange 35935 for its value. (Contributed by Scott Fenton, 11-Apr-2014.) |
| ⊢ Range = Image(2nd ↾ (V × V)) | ||
| Definition | df-cup 35870 | Define the little cup function. See brcup 35940 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 35871 | Define the little cap function. See brcap 35941 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 35872 | Define the restriction function. See brrestrict 35950 for its value. (Contributed by Scott Fenton, 17-Apr-2014.) |
| ⊢ Restrict = (Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st ))))) | ||
| Definition | df-succf 35873 | Define the successor function. See brsuccf 35942 for its value. (Contributed by Scott Fenton, 14-Apr-2014.) |
| ⊢ Succ = (Cup ∘ ( I ⊗ Singleton)) | ||
| Definition | df-apply 35874 | Define the application function. See brapply 35939 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 35875 | Define the functional part of a class 𝐹. This is the maximal part of 𝐹 that is a function. See funpartfun 35944 and funpartfv 35946 for the meaning of this statement. (Contributed by Scott Fenton, 16-Apr-2014.) |
| ⊢ Funpart𝐹 = (𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons ))) | ||
| Definition | df-fullfun 35876 | 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 35877 | Define the upper bound relationship functor. See brub 35955 for value. (Contributed by Scott Fenton, 3-May-2018.) |
| ⊢ UB𝑅 = ((V × V) ∖ ((V ∖ 𝑅) ∘ ◡ E )) | ||
| Definition | df-lb 35878 | Define the lower bound relationship functor. See brlb 35956 for value. (Contributed by Scott Fenton, 3-May-2018.) |
| ⊢ LB𝑅 = UB◡𝑅 | ||
| Theorem | txpss3v 35879 | 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 35880 | A tail Cartesian product is a relationship. (Contributed by Scott Fenton, 31-Mar-2012.) |
| ⊢ Rel (𝐴 ⊗ 𝐵) | ||
| Theorem | brtxp 35881 | Characterize a ternary relation over a tail Cartesian product. Together with txpss3v 35879, 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 35882* | 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 35883 | 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 35884 | A converse law for parallel product. (Contributed by Scott Fenton, 3-May-2014.) |
| ⊢ pprod(𝑅, 𝑆) = ◡pprod(◡𝑅, ◡𝑆) | ||
| Theorem | pprodss4v 35885 | 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 35886 | Characterize a quaternary relation over a tail Cartesian product. Together with pprodss4v 35885, 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 35887* | 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 35888* | 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 35889 | The subset class is a binary relation. (Contributed by Scott Fenton, 31-Mar-2012.) |
| ⊢ Rel SSet | ||
| Theorem | brsset 35890 | For sets, the SSet binary relation is equivalent to the subset relationship. (Contributed by Scott Fenton, 31-Mar-2012.) |
| ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 SSet 𝐵 ↔ 𝐴 ⊆ 𝐵) | ||
| Theorem | idsset 35891 | I is equal to the intersection of SSet and its converse. (Contributed by Scott Fenton, 31-Mar-2012.) |
| ⊢ I = ( SSet ∩ ◡ SSet ) | ||
| Theorem | eltrans 35892 | Membership in the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ Trans ↔ Tr 𝐴) | ||
| Theorem | dfon3 35893 | A quantifier-free definition of On. (Contributed by Scott Fenton, 5-Apr-2012.) |
| ⊢ On = (V ∖ ran (( SSet ∩ ( Trans × V)) ∖ ( I ∪ E ))) | ||
| Theorem | dfon4 35894 | Another quantifier-free definition of On. (Contributed by Scott Fenton, 4-May-2014.) |
| ⊢ On = (V ∖ (( SSet ∖ ( I ∪ E )) “ Trans )) | ||
| Theorem | brtxpsd 35895* | 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 35896* | Another common abbreviation for quantifier-free definitions. (Contributed by Scott Fenton, 21-Apr-2014.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝑅 = (𝐶 ∖ ran ((V ⊗ E ) △ (𝑆 ⊗ V))) & ⊢ 𝐴𝐶𝐵 ⇒ ⊢ (𝐴𝑅𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥𝑆𝐴)) | ||
| Theorem | brtxpsd3 35897* | A third common abbreviation for quantifier-free definitions. (Contributed by Scott Fenton, 3-May-2014.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝑅 = (𝐶 ∖ ran ((V ⊗ E ) △ (𝑆 ⊗ V))) & ⊢ 𝐴𝐶𝐵 & ⊢ (𝑥 ∈ 𝑋 ↔ 𝑥𝑆𝐴) ⇒ ⊢ (𝐴𝑅𝐵 ↔ 𝐵 = 𝑋) | ||
| Theorem | relbigcup 35898 | The Bigcup relationship is a relationship. (Contributed by Scott Fenton, 11-Apr-2012.) |
| ⊢ Rel Bigcup | ||
| Theorem | brbigcup 35899 | Binary relation over Bigcup . (Contributed by Scott Fenton, 11-Apr-2012.) |
| ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 Bigcup 𝐵 ↔ ∪ 𝐴 = 𝐵) | ||
| Theorem | dfbigcup2 35900 | Bigcup using maps-to notation. (Contributed by Scott Fenton, 16-Apr-2012.) |
| ⊢ Bigcup = (𝑥 ∈ V ↦ ∪ 𝑥) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |