Home | Metamath
Proof Explorer Theorem List (p. 334 of 449) | < 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: | Metamath Proof Explorer
(1-28689) |
Hilbert Space Explorer
(28690-30212) |
Users' Mathboxes
(30213-44900) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | capply 33301 | Declare the syntax for the application function. |
class Apply | ||
Syntax | ccup 33302 | Declare the syntax for the cup function. |
class Cup | ||
Syntax | ccap 33303 | Declare the syntax for the cap function. |
class Cap | ||
Syntax | csuccf 33304 | Declare the syntax for the successor function. |
class Succ | ||
Syntax | cfunpart 33305 | Declare the syntax for the functional part functor. |
class Funpart𝐹 | ||
Syntax | cfullfn 33306 | Declare the syntax for the full function functor. |
class FullFun𝐹 | ||
Syntax | crestrict 33307 | Declare the syntax for the restriction function. |
class Restrict | ||
Syntax | cub 33308 | Declare the syntax for the upper bound relationship functor. |
class UB𝑅 | ||
Syntax | clb 33309 | Declare the syntax for the lower bound relationship functor. |
class LB𝑅 | ||
Definition | df-txp 33310 | Define the tail cross of two classes. Membership in this class is defined by txpss3v 33334 and brtxp 33336. (Contributed by Scott Fenton, 31-Mar-2012.) |
⊢ (𝐴 ⊗ 𝐵) = ((◡(1st ↾ (V × V)) ∘ 𝐴) ∩ (◡(2nd ↾ (V × V)) ∘ 𝐵)) | ||
Definition | df-pprod 33311 | Define the parallel product of two classes. Membership in this class is defined by pprodss4v 33340 and brpprod 33341. (Contributed by Scott Fenton, 11-Apr-2014.) |
⊢ pprod(𝐴, 𝐵) = ((𝐴 ∘ (1st ↾ (V × V))) ⊗ (𝐵 ∘ (2nd ↾ (V × V)))) | ||
Definition | df-sset 33312 | Define the subset class. For the value, see brsset 33345. (Contributed by Scott Fenton, 31-Mar-2012.) |
⊢ SSet = ((V × V) ∖ ran ( E ⊗ (V ∖ E ))) | ||
Definition | df-trans 33313 | Define the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012.) |
⊢ Trans = (V ∖ ran (( E ∘ E ) ∖ E )) | ||
Definition | df-bigcup 33314 | Define the Bigcup function, which, per fvbigcup 33358, 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 33315 | Define the class of all fixpoints of a relationship. (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ Fix 𝐴 = dom (𝐴 ∩ I ) | ||
Definition | df-limits 33316 | Define the class of all limit ordinals. (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ Limits = ((On ∩ Fix Bigcup ) ∖ {∅}) | ||
Definition | df-funs 33317 | Define the class of all functions. See elfuns 33371 for membership. (Contributed by Scott Fenton, 18-Feb-2013.) |
⊢ Funs = (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E ))) | ||
Definition | df-singleton 33318 | Define the singleton function. See brsingle 33373 for its value. (Contributed by Scott Fenton, 4-Apr-2014.) |
⊢ Singleton = ((V × V) ∖ ran ((V ⊗ E ) △ ( I ⊗ V))) | ||
Definition | df-singles 33319 | Define the class of all singletons. See elsingles 33374 for membership. (Contributed by Scott Fenton, 19-Feb-2013.) |
⊢ Singletons = ran Singleton | ||
Definition | df-image 33320 | Define the image functor. This function takes a set 𝐴 to a function 𝑥 ↦ (𝐴 “ 𝑥), providing that the latter exists. See imageval 33386 for the derivation. (Contributed by Scott Fenton, 27-Mar-2014.) |
⊢ Image𝐴 = ((V × V) ∖ ran ((V ⊗ E ) △ (( E ∘ ◡𝐴) ⊗ V))) | ||
Definition | df-cart 33321 | Define the cartesian product function. See brcart 33388 for its value. (Contributed by Scott Fenton, 11-Apr-2014.) |
⊢ Cart = (((V × V) × V) ∖ ran ((V ⊗ E ) △ (pprod( E , E ) ⊗ V))) | ||
Definition | df-img 33322 | Define the image function. See brimg 33393 for its value. (Contributed by Scott Fenton, 12-Apr-2014.) |
⊢ Img = (Image((2nd ∘ 1st ) ↾ (1st ↾ (V × V))) ∘ Cart) | ||
Definition | df-domain 33323 | Define the domain function. See brdomain 33389 for its value. (Contributed by Scott Fenton, 11-Apr-2014.) |
⊢ Domain = Image(1st ↾ (V × V)) | ||
Definition | df-range 33324 | Define the range function. See brrange 33390 for its value. (Contributed by Scott Fenton, 11-Apr-2014.) |
⊢ Range = Image(2nd ↾ (V × V)) | ||
Definition | df-cup 33325 | Define the little cup function. See brcup 33395 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 33326 | Define the little cap function. See brcap 33396 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 33327 | Define the restriction function. See brrestrict 33405 for its value. (Contributed by Scott Fenton, 17-Apr-2014.) |
⊢ Restrict = (Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st ))))) | ||
Definition | df-succf 33328 | Define the successor function. See brsuccf 33397 for its value. (Contributed by Scott Fenton, 14-Apr-2014.) |
⊢ Succ = (Cup ∘ ( I ⊗ Singleton)) | ||
Definition | df-apply 33329 | Define the application function. See brapply 33394 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 33330 | Define the functional part of a class 𝐹. This is the maximal part of 𝐹 that is a function. See funpartfun 33399 and funpartfv 33401 for the meaning of this statement. (Contributed by Scott Fenton, 16-Apr-2014.) |
⊢ Funpart𝐹 = (𝐹 ↾ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons ))) | ||
Definition | df-fullfun 33331 | 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 33332 | Define the upper bound relationship functor. See brub 33410 for value. (Contributed by Scott Fenton, 3-May-2018.) |
⊢ UB𝑅 = ((V × V) ∖ ((V ∖ 𝑅) ∘ ◡ E )) | ||
Definition | df-lb 33333 | Define the lower bound relationship functor. See brlb 33411 for value. (Contributed by Scott Fenton, 3-May-2018.) |
⊢ LB𝑅 = UB◡𝑅 | ||
Theorem | txpss3v 33334 | 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 33335 | A tail Cartesian product is a relationship. (Contributed by Scott Fenton, 31-Mar-2012.) |
⊢ Rel (𝐴 ⊗ 𝐵) | ||
Theorem | brtxp 33336 | Characterize a ternary relation over a tail Cartesian product. Together with txpss3v 33334, 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 33337* | 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 33338 | 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 33339 | A converse law for parallel product. (Contributed by Scott Fenton, 3-May-2014.) |
⊢ pprod(𝑅, 𝑆) = ◡pprod(◡𝑅, ◡𝑆) | ||
Theorem | pprodss4v 33340 | 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 33341 | Characterize a quaternary relation over a tail Cartesian product. Together with pprodss4v 33340, 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 33342* | 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 33343* | 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 33344 | The subset class is a binary relation. (Contributed by Scott Fenton, 31-Mar-2012.) |
⊢ Rel SSet | ||
Theorem | brsset 33345 | For sets, the SSet binary relation is equivalent to the subset relationship. (Contributed by Scott Fenton, 31-Mar-2012.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 SSet 𝐵 ↔ 𝐴 ⊆ 𝐵) | ||
Theorem | idsset 33346 | I is equal to the intersection of SSet and its converse. (Contributed by Scott Fenton, 31-Mar-2012.) |
⊢ I = ( SSet ∩ ◡ SSet ) | ||
Theorem | eltrans 33347 | Membership in the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ Trans ↔ Tr 𝐴) | ||
Theorem | dfon3 33348 | A quantifier-free definition of On. (Contributed by Scott Fenton, 5-Apr-2012.) |
⊢ On = (V ∖ ran (( SSet ∩ ( Trans × V)) ∖ ( I ∪ E ))) | ||
Theorem | dfon4 33349 | Another quantifier-free definition of On. (Contributed by Scott Fenton, 4-May-2014.) |
⊢ On = (V ∖ (( SSet ∖ ( I ∪ E )) “ Trans )) | ||
Theorem | brtxpsd 33350* | 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 33351* | Another common abbreviation for quantifier-free definitions. (Contributed by Scott Fenton, 21-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝑅 = (𝐶 ∖ ran ((V ⊗ E ) △ (𝑆 ⊗ V))) & ⊢ 𝐴𝐶𝐵 ⇒ ⊢ (𝐴𝑅𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥𝑆𝐴)) | ||
Theorem | brtxpsd3 33352* | A third common abbreviation for quantifier-free definitions. (Contributed by Scott Fenton, 3-May-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝑅 = (𝐶 ∖ ran ((V ⊗ E ) △ (𝑆 ⊗ V))) & ⊢ 𝐴𝐶𝐵 & ⊢ (𝑥 ∈ 𝑋 ↔ 𝑥𝑆𝐴) ⇒ ⊢ (𝐴𝑅𝐵 ↔ 𝐵 = 𝑋) | ||
Theorem | relbigcup 33353 | The Bigcup relationship is a relationship. (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ Rel Bigcup | ||
Theorem | brbigcup 33354 | Binary relation over Bigcup . (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 Bigcup 𝐵 ↔ ∪ 𝐴 = 𝐵) | ||
Theorem | dfbigcup2 33355 | Bigcup using maps-to notation. (Contributed by Scott Fenton, 16-Apr-2012.) |
⊢ Bigcup = (𝑥 ∈ V ↦ ∪ 𝑥) | ||
Theorem | fobigcup 33356 | Bigcup maps the universe onto itself. (Contributed by Scott Fenton, 16-Apr-2012.) |
⊢ Bigcup :V–onto→V | ||
Theorem | fnbigcup 33357 | Bigcup is a function over the universal class. (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ Bigcup Fn V | ||
Theorem | fvbigcup 33358 | For sets, Bigcup yields union. (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ( Bigcup ‘𝐴) = ∪ 𝐴 | ||
Theorem | elfix 33359 | Membership in the fixpoints of a class. (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ Fix 𝑅 ↔ 𝐴𝑅𝐴) | ||
Theorem | elfix2 33360 | Alternative membership in the fixpoint of a class. (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ Rel 𝑅 ⇒ ⊢ (𝐴 ∈ Fix 𝑅 ↔ 𝐴𝑅𝐴) | ||
Theorem | dffix2 33361 | The fixpoints of a class in terms of its range. (Contributed by Scott Fenton, 16-Apr-2012.) |
⊢ Fix 𝐴 = ran (𝐴 ∩ I ) | ||
Theorem | fixssdm 33362 | The fixpoints of a class are a subset of its domain. (Contributed by Scott Fenton, 16-Apr-2012.) |
⊢ Fix 𝐴 ⊆ dom 𝐴 | ||
Theorem | fixssrn 33363 | The fixpoints of a class are a subset of its range. (Contributed by Scott Fenton, 16-Apr-2012.) |
⊢ Fix 𝐴 ⊆ ran 𝐴 | ||
Theorem | fixcnv 33364 | The fixpoints of a class are the same as those of its converse. (Contributed by Scott Fenton, 16-Apr-2012.) |
⊢ Fix 𝐴 = Fix ◡𝐴 | ||
Theorem | fixun 33365 | The fixpoint operator distributes over union. (Contributed by Scott Fenton, 16-Apr-2012.) |
⊢ Fix (𝐴 ∪ 𝐵) = ( Fix 𝐴 ∪ Fix 𝐵) | ||
Theorem | ellimits 33366 | Membership in the class of all limit ordinals. (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ Limits ↔ Lim 𝐴) | ||
Theorem | limitssson 33367 | The class of all limit ordinals is a subclass of the class of all ordinals. (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ Limits ⊆ On | ||
Theorem | dfom5b 33368 | A quantifier-free definition of ω that does not depend on ax-inf 9095. (Note: label was changed from dfom5 9107 to dfom5b 33368 to prevent naming conflict. NM, 12-Feb-2013.) (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ ω = (On ∩ ∩ Limits ) | ||
Theorem | sscoid 33369 | A condition for subset and composition with identity. (Contributed by Scott Fenton, 13-Apr-2018.) |
⊢ (𝐴 ⊆ ( I ∘ 𝐵) ↔ (Rel 𝐴 ∧ 𝐴 ⊆ 𝐵)) | ||
Theorem | dffun10 33370 | Another potential definition of functionhood. Based on statements in http://people.math.gatech.edu/~belinfan/research/autoreas/otter/sum/fs/. (Contributed by Scott Fenton, 30-Aug-2017.) |
⊢ (Fun 𝐹 ↔ 𝐹 ⊆ ( I ∘ (V ∖ ((V ∖ I ) ∘ 𝐹)))) | ||
Theorem | elfuns 33371 | Membership in the class of all functions. (Contributed by Scott Fenton, 18-Feb-2013.) |
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐹 ∈ Funs ↔ Fun 𝐹) | ||
Theorem | elfunsg 33372 | Closed form of elfuns 33371. (Contributed by Scott Fenton, 2-May-2014.) |
⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ Funs ↔ Fun 𝐹)) | ||
Theorem | brsingle 33373 | The binary relation form of the singleton function. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴Singleton𝐵 ↔ 𝐵 = {𝐴}) | ||
Theorem | elsingles 33374* | Membership in the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013.) |
⊢ (𝐴 ∈ Singletons ↔ ∃𝑥 𝐴 = {𝑥}) | ||
Theorem | fnsingle 33375 | The singleton relationship is a function over the universe. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ Singleton Fn V | ||
Theorem | fvsingle 33376 | The value of the singleton function. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Revised by Scott Fenton, 13-Apr-2018.) |
⊢ (Singleton‘𝐴) = {𝐴} | ||
Theorem | dfsingles2 33377* | Alternate definition of the class of all singletons. (Contributed by Scott Fenton, 20-Nov-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ Singletons = {𝑥 ∣ ∃𝑦 𝑥 = {𝑦}} | ||
Theorem | snelsingles 33378 | A singleton is a member of the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ {𝐴} ∈ Singletons | ||
Theorem | dfiota3 33379 | A definition of iota using minimal quantifiers. (Contributed by Scott Fenton, 19-Feb-2013.) |
⊢ (℩𝑥𝜑) = ∪ ∪ ({{𝑥 ∣ 𝜑}} ∩ Singletons ) | ||
Theorem | dffv5 33380 | Another quantifier free definition of function value. (Contributed by Scott Fenton, 19-Feb-2013.) |
⊢ (𝐹‘𝐴) = ∪ ∪ ({(𝐹 “ {𝐴})} ∩ Singletons ) | ||
Theorem | unisnif 33381 | Express union of singleton in terms of if. (Contributed by Scott Fenton, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ∪ {𝐴} = if(𝐴 ∈ V, 𝐴, ∅) | ||
Theorem | brimage 33382 | Binary relation form of the Image functor. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴Image𝑅𝐵 ↔ 𝐵 = (𝑅 “ 𝐴)) | ||
Theorem | brimageg 33383 | Closed form of brimage 33382. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴Image𝑅𝐵 ↔ 𝐵 = (𝑅 “ 𝐴))) | ||
Theorem | funimage 33384 | Image𝐴 is a function. (Contributed by Scott Fenton, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ Fun Image𝐴 | ||
Theorem | fnimage 33385* | Image𝑅 is a function over the set-like portion of 𝑅. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ Image𝑅 Fn {𝑥 ∣ (𝑅 “ 𝑥) ∈ V} | ||
Theorem | imageval 33386* | The image functor in maps-to notation. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ Image𝑅 = (𝑥 ∈ V ↦ (𝑅 “ 𝑥)) | ||
Theorem | fvimage 33387 | Value of the image functor. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅 “ 𝐴) ∈ 𝑊) → (Image𝑅‘𝐴) = (𝑅 “ 𝐴)) | ||
Theorem | brcart 33388 | Binary relation form of the cartesian product operator. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉Cart𝐶 ↔ 𝐶 = (𝐴 × 𝐵)) | ||
Theorem | brdomain 33389 | Binary relation form of the domain function. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴Domain𝐵 ↔ 𝐵 = dom 𝐴) | ||
Theorem | brrange 33390 | Binary relation form of the range function. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴Range𝐵 ↔ 𝐵 = ran 𝐴) | ||
Theorem | brdomaing 33391 | Closed form of brdomain 33389. (Contributed by Scott Fenton, 2-May-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴Domain𝐵 ↔ 𝐵 = dom 𝐴)) | ||
Theorem | brrangeg 33392 | Closed form of brrange 33390. (Contributed by Scott Fenton, 3-May-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴Range𝐵 ↔ 𝐵 = ran 𝐴)) | ||
Theorem | brimg 33393 | Binary relation form of the Img function. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉Img𝐶 ↔ 𝐶 = (𝐴 “ 𝐵)) | ||
Theorem | brapply 33394 | Binary relation form of the Apply function. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉Apply𝐶 ↔ 𝐶 = (𝐴‘𝐵)) | ||
Theorem | brcup 33395 | Binary relation form of the Cup function. (Contributed by Scott Fenton, 14-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉Cup𝐶 ↔ 𝐶 = (𝐴 ∪ 𝐵)) | ||
Theorem | brcap 33396 | Binary relation form of the Cap function. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉Cap𝐶 ↔ 𝐶 = (𝐴 ∩ 𝐵)) | ||
Theorem | brsuccf 33397 | Binary relation form of the Succ function. (Contributed by Scott Fenton, 14-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴Succ𝐵 ↔ 𝐵 = suc 𝐴) | ||
Theorem | funpartlem 33398* | Lemma for funpartfun 33399. Show membership in the restriction. (Contributed by Scott Fenton, 4-Dec-2017.) |
⊢ (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )) ↔ ∃𝑥(𝐹 “ {𝐴}) = {𝑥}) | ||
Theorem | funpartfun 33399 | The functional part of 𝐹 is a function. (Contributed by Scott Fenton, 16-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ Fun Funpart𝐹 | ||
Theorem | funpartss 33400 | The functional part of 𝐹 is a subset of 𝐹. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ Funpart𝐹 ⊆ 𝐹 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |