| Metamath
Proof Explorer Theorem List (p. 360 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 | fobigcup 35901 | Bigcup maps the universe onto itself. (Contributed by Scott Fenton, 16-Apr-2012.) |
| ⊢ Bigcup :V–onto→V | ||
| Theorem | fnbigcup 35902 | Bigcup is a function over the universal class. (Contributed by Scott Fenton, 11-Apr-2012.) |
| ⊢ Bigcup Fn V | ||
| Theorem | fvbigcup 35903 | For sets, Bigcup yields union. (Contributed by Scott Fenton, 11-Apr-2012.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ ( Bigcup ‘𝐴) = ∪ 𝐴 | ||
| Theorem | elfix 35904 | Membership in the fixpoints of a class. (Contributed by Scott Fenton, 11-Apr-2012.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ Fix 𝑅 ↔ 𝐴𝑅𝐴) | ||
| Theorem | elfix2 35905 | Alternative membership in the fixpoint of a class. (Contributed by Scott Fenton, 11-Apr-2012.) |
| ⊢ Rel 𝑅 ⇒ ⊢ (𝐴 ∈ Fix 𝑅 ↔ 𝐴𝑅𝐴) | ||
| Theorem | dffix2 35906 | The fixpoints of a class in terms of its range. (Contributed by Scott Fenton, 16-Apr-2012.) |
| ⊢ Fix 𝐴 = ran (𝐴 ∩ I ) | ||
| Theorem | fixssdm 35907 | The fixpoints of a class are a subset of its domain. (Contributed by Scott Fenton, 16-Apr-2012.) |
| ⊢ Fix 𝐴 ⊆ dom 𝐴 | ||
| Theorem | fixssrn 35908 | The fixpoints of a class are a subset of its range. (Contributed by Scott Fenton, 16-Apr-2012.) |
| ⊢ Fix 𝐴 ⊆ ran 𝐴 | ||
| Theorem | fixcnv 35909 | The fixpoints of a class are the same as those of its converse. (Contributed by Scott Fenton, 16-Apr-2012.) |
| ⊢ Fix 𝐴 = Fix ◡𝐴 | ||
| Theorem | fixun 35910 | The fixpoint operator distributes over union. (Contributed by Scott Fenton, 16-Apr-2012.) |
| ⊢ Fix (𝐴 ∪ 𝐵) = ( Fix 𝐴 ∪ Fix 𝐵) | ||
| Theorem | ellimits 35911 | Membership in the class of all limit ordinals. (Contributed by Scott Fenton, 11-Apr-2012.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ Limits ↔ Lim 𝐴) | ||
| Theorem | limitssson 35912 | 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 35913 | A quantifier-free definition of ω that does not depend on ax-inf 9678. (Note: label was changed from dfom5 9690 to dfom5b 35913 to prevent naming conflict. NM, 12-Feb-2013.) (Contributed by Scott Fenton, 11-Apr-2012.) |
| ⊢ ω = (On ∩ ∩ Limits ) | ||
| Theorem | sscoid 35914 | A condition for subset and composition with identity. (Contributed by Scott Fenton, 13-Apr-2018.) |
| ⊢ (𝐴 ⊆ ( I ∘ 𝐵) ↔ (Rel 𝐴 ∧ 𝐴 ⊆ 𝐵)) | ||
| Theorem | dffun10 35915 | Another potential definition of functionality. 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 35916 | Membership in the class of all functions. (Contributed by Scott Fenton, 18-Feb-2013.) |
| ⊢ 𝐹 ∈ V ⇒ ⊢ (𝐹 ∈ Funs ↔ Fun 𝐹) | ||
| Theorem | elfunsg 35917 | Closed form of elfuns 35916. (Contributed by Scott Fenton, 2-May-2014.) |
| ⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ Funs ↔ Fun 𝐹)) | ||
| Theorem | brsingle 35918 | 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 35919* | Membership in the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013.) |
| ⊢ (𝐴 ∈ Singletons ↔ ∃𝑥 𝐴 = {𝑥}) | ||
| Theorem | fnsingle 35920 | 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 35921 | 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 35922* | 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 35923 | A singleton is a member of the class of all singletons. (Contributed by Scott Fenton, 19-Feb-2013.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ {𝐴} ∈ Singletons | ||
| Theorem | dfiota3 35924 | A definition of iota using minimal quantifiers. (Contributed by Scott Fenton, 19-Feb-2013.) |
| ⊢ (℩𝑥𝜑) = ∪ ∪ ({{𝑥 ∣ 𝜑}} ∩ Singletons ) | ||
| Theorem | dffv5 35925 | Another quantifier-free definition of function value. (Contributed by Scott Fenton, 19-Feb-2013.) |
| ⊢ (𝐹‘𝐴) = ∪ ∪ ({(𝐹 “ {𝐴})} ∩ Singletons ) | ||
| Theorem | unisnif 35926 | 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 35927 | 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 35928 | Closed form of brimage 35927. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴Image𝑅𝐵 ↔ 𝐵 = (𝑅 “ 𝐴))) | ||
| Theorem | funimage 35929 | Image𝐴 is a function. (Contributed by Scott Fenton, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ Fun Image𝐴 | ||
| Theorem | fnimage 35930* | 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 35931* | 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 35932 | Value of the image functor. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑅 “ 𝐴) ∈ 𝑊) → (Image𝑅‘𝐴) = (𝑅 “ 𝐴)) | ||
| Theorem | brcart 35933 | 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 35934 | 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 35935 | 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 35936 | Closed form of brdomain 35934. (Contributed by Scott Fenton, 2-May-2014.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴Domain𝐵 ↔ 𝐵 = dom 𝐴)) | ||
| Theorem | brrangeg 35937 | Closed form of brrange 35935. (Contributed by Scott Fenton, 3-May-2014.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴Range𝐵 ↔ 𝐵 = ran 𝐴)) | ||
| Theorem | brimg 35938 | 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 35939 | 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 35940 | 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 35941 | 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 35942 | 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 35943* | Lemma for funpartfun 35944. Show membership in the restriction. (Contributed by Scott Fenton, 4-Dec-2017.) |
| ⊢ (𝐴 ∈ dom ((Image𝐹 ∘ Singleton) ∩ (V × Singletons )) ↔ ∃𝑥(𝐹 “ {𝐴}) = {𝑥}) | ||
| Theorem | funpartfun 35944 | 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 35945 | The functional part of 𝐹 is a subset of 𝐹. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ Funpart𝐹 ⊆ 𝐹 | ||
| Theorem | funpartfv 35946 | The function value of the functional part is identical to the original functional value. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ (Funpart𝐹‘𝐴) = (𝐹‘𝐴) | ||
| Theorem | fullfunfnv 35947 | The full functional part of 𝐹 is a function over V. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ FullFun𝐹 Fn V | ||
| Theorem | fullfunfv 35948 | The function value of the full function of 𝐹 agrees with 𝐹. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ (FullFun𝐹‘𝐴) = (𝐹‘𝐴) | ||
| Theorem | brfullfun 35949 | A binary relation form condition for the full function. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴FullFun𝐹𝐵 ↔ 𝐵 = (𝐹‘𝐴)) | ||
| Theorem | brrestrict 35950 | Binary relation form of the Restrict function. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉Restrict𝐶 ↔ 𝐶 = (𝐴 ↾ 𝐵)) | ||
| Theorem | dfrecs2 35951 | A quantifier-free definition of recs. (Contributed by Scott Fenton, 17-Jul-2020.) |
| ⊢ recs(𝐹) = ∪ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (FullFun𝐹 ∘ Restrict)))) | ||
| Theorem | dfrdg4 35952 | A quantifier-free definition of the recursive definition generator. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
| ⊢ rec(𝐹, 𝐴) = ∪ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))) | ||
| Theorem | dfint3 35953 | Quantifier-free definition of class intersection. (Contributed by Scott Fenton, 13-Apr-2018.) |
| ⊢ ∩ 𝐴 = (V ∖ (◡(V ∖ E ) “ 𝐴)) | ||
| Theorem | imagesset 35954 | The Image functor applied to the converse of the subset relationship yields a subset of the subset relationship. (Contributed by Scott Fenton, 14-Apr-2018.) |
| ⊢ Image◡ SSet ⊆ SSet | ||
| Theorem | brub 35955* | Binary relation form of the upper bound functor. (Contributed by Scott Fenton, 3-May-2018.) |
| ⊢ 𝑆 ∈ V & ⊢ 𝐴 ∈ V ⇒ ⊢ (𝑆UB𝑅𝐴 ↔ ∀𝑥 ∈ 𝑆 𝑥𝑅𝐴) | ||
| Theorem | brlb 35956* | Binary relation form of the lower bound functor. (Contributed by Scott Fenton, 3-May-2018.) |
| ⊢ 𝑆 ∈ V & ⊢ 𝐴 ∈ V ⇒ ⊢ (𝑆LB𝑅𝐴 ↔ ∀𝑥 ∈ 𝑆 𝐴𝑅𝑥) | ||
| Syntax | caltop 35957 | Declare the syntax for an alternate ordered pair. |
| class ⟪𝐴, 𝐵⟫ | ||
| Syntax | caltxp 35958 | Declare the syntax for an alternate Cartesian product. |
| class (𝐴 ×× 𝐵) | ||
| Definition | df-altop 35959 | An alternative definition of ordered pairs. This definition removes a hypothesis from its defining theorem (see altopth 35970), making it more convenient in some circumstances. (Contributed by Scott Fenton, 22-Mar-2012.) |
| ⊢ ⟪𝐴, 𝐵⟫ = {{𝐴}, {𝐴, {𝐵}}} | ||
| Definition | df-altxp 35960* | Define Cartesian products of alternative ordered pairs. (Contributed by Scott Fenton, 23-Mar-2012.) |
| ⊢ (𝐴 ×× 𝐵) = {𝑧 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑧 = ⟪𝑥, 𝑦⟫} | ||
| Theorem | altopex 35961 | Alternative ordered pairs always exist. (Contributed by Scott Fenton, 22-Mar-2012.) |
| ⊢ ⟪𝐴, 𝐵⟫ ∈ V | ||
| Theorem | altopthsn 35962 | Two alternate ordered pairs are equal iff the singletons of their respective elements are equal. Note that this holds regardless of sethood of any of the elements. (Contributed by Scott Fenton, 16-Apr-2012.) |
| ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ ({𝐴} = {𝐶} ∧ {𝐵} = {𝐷})) | ||
| Theorem | altopeq12 35963 | Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.) |
| ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → ⟪𝐴, 𝐶⟫ = ⟪𝐵, 𝐷⟫) | ||
| Theorem | altopeq1 35964 | Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.) |
| ⊢ (𝐴 = 𝐵 → ⟪𝐴, 𝐶⟫ = ⟪𝐵, 𝐶⟫) | ||
| Theorem | altopeq2 35965 | Equality for alternate ordered pairs. (Contributed by Scott Fenton, 22-Mar-2012.) |
| ⊢ (𝐴 = 𝐵 → ⟪𝐶, 𝐴⟫ = ⟪𝐶, 𝐵⟫) | ||
| Theorem | altopth1 35966 | Equality of the first members of equal alternate ordered pairs, which holds regardless of the second members' sethood. (Contributed by Scott Fenton, 22-Mar-2012.) |
| ⊢ (𝐴 ∈ 𝑉 → (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ → 𝐴 = 𝐶)) | ||
| Theorem | altopth2 35967 | Equality of the second members of equal alternate ordered pairs, which holds regardless of the first members' sethood. (Contributed by Scott Fenton, 22-Mar-2012.) |
| ⊢ (𝐵 ∈ 𝑉 → (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ → 𝐵 = 𝐷)) | ||
| Theorem | altopthg 35968 | Alternate ordered pair theorem. (Contributed by Scott Fenton, 22-Mar-2012.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
| Theorem | altopthbg 35969 | Alternate ordered pair theorem. (Contributed by Scott Fenton, 14-Apr-2012.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
| Theorem | altopth 35970 | The alternate ordered pair theorem. If two alternate ordered pairs are equal, their first elements are equal and their second elements are equal. Note that 𝐶 and 𝐷 are not required to be a set due to a peculiarity of our specific ordered pair definition, as opposed to the regular ordered pairs used here, which (as in opth 5481), requires 𝐷 to be a set. (Contributed by Scott Fenton, 23-Mar-2012.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
| Theorem | altopthb 35971 | Alternate ordered pair theorem with different sethood requirements. See altopth 35970 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
| Theorem | altopthc 35972 | Alternate ordered pair theorem with different sethood requirements. See altopth 35970 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.) |
| ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
| Theorem | altopthd 35973 | Alternate ordered pair theorem with different sethood requirements. See altopth 35970 for more comments. (Contributed by Scott Fenton, 14-Apr-2012.) |
| ⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ (⟪𝐴, 𝐵⟫ = ⟪𝐶, 𝐷⟫ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
| Theorem | altxpeq1 35974 | Equality for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.) |
| ⊢ (𝐴 = 𝐵 → (𝐴 ×× 𝐶) = (𝐵 ×× 𝐶)) | ||
| Theorem | altxpeq2 35975 | Equality for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.) |
| ⊢ (𝐴 = 𝐵 → (𝐶 ×× 𝐴) = (𝐶 ×× 𝐵)) | ||
| Theorem | elaltxp 35976* | Membership in alternate Cartesian products. (Contributed by Scott Fenton, 23-Mar-2012.) |
| ⊢ (𝑋 ∈ (𝐴 ×× 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑋 = ⟪𝑥, 𝑦⟫) | ||
| Theorem | altopelaltxp 35977 | Alternate ordered pair membership in a Cartesian product. Note that, unlike opelxp 5721, there is no sethood requirement here. (Contributed by Scott Fenton, 22-Mar-2012.) |
| ⊢ (⟪𝑋, 𝑌⟫ ∈ (𝐴 ×× 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵)) | ||
| Theorem | altxpsspw 35978 | An inclusion rule for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012.) |
| ⊢ (𝐴 ×× 𝐵) ⊆ 𝒫 𝒫 (𝐴 ∪ 𝒫 𝐵) | ||
| Theorem | altxpexg 35979 | The alternate Cartesian product of two sets is a set. (Contributed by Scott Fenton, 24-Mar-2012.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ×× 𝐵) ∈ V) | ||
| Theorem | rankaltopb 35980 | Compute the rank of an alternate ordered pair. (Contributed by Scott Fenton, 18-Dec-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) → (rank‘⟪𝐴, 𝐵⟫) = suc suc ((rank‘𝐴) ∪ suc (rank‘𝐵))) | ||
| Theorem | nfaltop 35981 | Bound-variable hypothesis builder for alternate ordered pairs. (Contributed by Scott Fenton, 25-Sep-2015.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥⟪𝐴, 𝐵⟫ | ||
| Theorem | sbcaltop 35982* | Distribution of class substitution over alternate ordered pairs. (Contributed by Scott Fenton, 25-Sep-2015.) |
| ⊢ (𝐴 ∈ V → ⦋𝐴 / 𝑥⦌⟪𝐶, 𝐷⟫ = ⟪⦋𝐴 / 𝑥⦌𝐶, ⦋𝐴 / 𝑥⦌𝐷⟫) | ||
| Syntax | cofs 35983 | Declare the syntax for the outer five segment configuration. |
| class OuterFiveSeg | ||
| Definition | df-ofs 35984* | The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom (ax5seg 28953). See brofs 36006 and 5segofs 36007 for how it is used. Definition 2.10 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 21-Sep-2013.) |
| ⊢ OuterFiveSeg = {〈𝑝, 𝑞〉 ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 Btwn 〈𝑎, 𝑐〉 ∧ 𝑦 Btwn 〈𝑥, 𝑧〉) ∧ (〈𝑎, 𝑏〉Cgr〈𝑥, 𝑦〉 ∧ 〈𝑏, 𝑐〉Cgr〈𝑦, 𝑧〉) ∧ (〈𝑎, 𝑑〉Cgr〈𝑥, 𝑤〉 ∧ 〈𝑏, 𝑑〉Cgr〈𝑦, 𝑤〉)))} | ||
| Theorem | cgrrflx2d 35985 | Deduction form of axcgrrflx 28929. (Contributed by Scott Fenton, 13-Oct-2013.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐵〉Cgr〈𝐵, 𝐴〉) | ||
| Theorem | cgrtr4d 35986 | Deduction form of axcgrtr 28930. (Contributed by Scott Fenton, 13-Oct-2013.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉) & ⊢ (𝜑 → 〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉) ⇒ ⊢ (𝜑 → 〈𝐶, 𝐷〉Cgr〈𝐸, 𝐹〉) | ||
| Theorem | cgrtr4and 35987 | Deduction form of axcgrtr 28930. (Contributed by Scott Fenton, 13-Oct-2013.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 〈𝐶, 𝐷〉Cgr〈𝐸, 𝐹〉) | ||
| Theorem | cgrrflx 35988 | Reflexivity law for congruence. Theorem 2.1 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 12-Jun-2013.) |
| ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 〈𝐴, 𝐵〉Cgr〈𝐴, 𝐵〉) | ||
| Theorem | cgrrflxd 35989 | Deduction form of cgrrflx 35988. (Contributed by Scott Fenton, 13-Oct-2013.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐵〉Cgr〈𝐴, 𝐵〉) | ||
| Theorem | cgrcomim 35990 | Congruence commutes on the two sides. Implication version. Theorem 2.2 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 12-Jun-2013.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 → 〈𝐶, 𝐷〉Cgr〈𝐴, 𝐵〉)) | ||
| Theorem | cgrcom 35991 | Congruence commutes between the two sides. (Contributed by Scott Fenton, 12-Jun-2013.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 ↔ 〈𝐶, 𝐷〉Cgr〈𝐴, 𝐵〉)) | ||
| Theorem | cgrcomand 35992 | Deduction form of cgrcom 35991. (Contributed by Scott Fenton, 13-Oct-2013.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 〈𝐶, 𝐷〉Cgr〈𝐴, 𝐵〉) | ||
| Theorem | cgrtr 35993 | Transitivity law for congruence. Theorem 2.3 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 24-Sep-2013.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝐹〉) → 〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉)) | ||
| Theorem | cgrtrand 35994 | Deduction form of cgrtr 35993. (Contributed by Scott Fenton, 13-Oct-2013.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐶, 𝐷〉Cgr〈𝐸, 𝐹〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉) | ||
| Theorem | cgrtr3 35995 | Transitivity law for congruence. (Contributed by Scott Fenton, 7-Oct-2013.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝐹〉) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉)) | ||
| Theorem | cgrtr3and 35996 | Deduction form of cgrtr3 35995. (Contributed by Scott Fenton, 13-Oct-2013.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐸 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐹 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐶, 𝐷〉Cgr〈𝐸, 𝐹〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉) | ||
| Theorem | cgrcoml 35997 | Congruence commutes on the left. Biconditional version of Theorem 2.4 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 12-Jun-2013.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 ↔ 〈𝐵, 𝐴〉Cgr〈𝐶, 𝐷〉)) | ||
| Theorem | cgrcomr 35998 | Congruence commutes on the right. Biconditional version of Theorem 2.5 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 12-Jun-2013.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 ↔ 〈𝐴, 𝐵〉Cgr〈𝐷, 𝐶〉)) | ||
| Theorem | cgrcomlr 35999 | Congruence commutes on both sides. (Contributed by Scott Fenton, 12-Jun-2013.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉 ↔ 〈𝐵, 𝐴〉Cgr〈𝐷, 𝐶〉)) | ||
| Theorem | cgrcomland 36000 | Deduction form of cgrcoml 35997. (Contributed by Scott Fenton, 14-Oct-2013.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐵 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐶 ∈ (𝔼‘𝑁)) & ⊢ (𝜑 → 𝐷 ∈ (𝔼‘𝑁)) & ⊢ ((𝜑 ∧ 𝜓) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝐷〉) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 〈𝐵, 𝐴〉Cgr〈𝐶, 𝐷〉) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |