mmtheorems38 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17411

Statement List for Metamath Proof Explorer - 3701-3800 - Page 38 of 175

Type	Label	Description
Statement
Theorem	orddisj 3701	An ordinal class and its singleton are disjoint.
|- (Ord A -> (A i^i {A}) = (/))
Theorem	onfr 3702	The ordinal class is founded. This lemma is needed for ordon 3863 in order to eliminate the need for the Axiom of Regularity.
|- _E Fr On
Theorem	onelpss 3703	Relationship between membership and proper subset of an ordinal number.
|- ((A e. On /\ B e. On) -> (A e. B <-> (A C_ B /\ A =/= B)))
Theorem	onsseleq 3704	Relationship between subset and membership of an ordinal number.
|- ((A e. On /\ B e. On) -> (A C_ B <-> (A e. B \/ A = B)))
Theorem	onelss 3705	An element of an ordinal number is a subset of the number. (The proof was shortened by Andrew Salmon, 25-Jul-2011.)
|- (A e. On -> (B e. A -> B C_ A))
Theorem	onelssOLD 3706	An element of an ordinal number is a subset of the number.
|- (A e. On -> (B e. A -> B C_ A))
Theorem	ordtr1 3707	Transitive law for ordinal classes.
|- (Ord C -> ((A e. B /\ B e. C) -> A e. C))
Theorem	ordtr2 3708	Transitive law for ordinal classes. (The proof was shortened by Andrew Salmon, 25-Jul-2011.)
|- ((Ord A /\ Ord C) -> ((A C_ B /\ B e. C) -> A e. C))
Theorem	ordtr2OLD 3709	Transitive law for ordinal classes.
|- ((Ord A /\ Ord C) -> ((A C_ B /\ B e. C) -> A e. C))
Theorem	ontr1 3710	Transitive law for ordinal numbers. Theorem 7M(b) of [Enderton] p. 192.
|- (C e. On -> ((A e. B /\ B e. C) -> A e. C))
Theorem	ontr2 3711	Transitive law for ordinal numbers. Exercise 3 of [TakeutiZaring] p. 40.
|- ((A e. On /\ C e. On) -> ((A C_ B /\ B e. C) -> A e. C))
Theorem	ordunidif 3712	The union of an ordinal stays the same if a subset equal to one of its elements is removed.
|- ((Ord A /\ B e. A) -> U.(A \ B) = U.A)
Theorem	onintss 3713	If a property is true for an ordinal number, then the minimum ordinal number for which it is true is smaller or equal. Theorem Schema 61 of [Suppes] p. 228.
|- (x = A -> (ph <-> ps))   =>   |- (A e. On -> (ps -> |^|{x e. On | ph} C_ A))
Theorem	oneqmini 3714	A way to show that an ordinal number equals the minimum of a collection of ordinal numbers: it must be in the collection, and it must not be larger than any member of the collection.
|- (B C_ On -> ((A e. B /\ A.x e. A -. x e. B) -> A = |^|B))
Theorem	ord0 3715	The empty set is an ordinal class.
|- Ord (/)
Theorem	0elon 3716	The empty set is an ordinal number. Corollary 7N(b) of [Enderton] p. 193.
|- (/) e. On
Theorem	ord0eln0 3717	A non-empty ordinal contains the empty set.
|- (Ord A -> ((/) e. A <-> A =/= (/)))
Theorem	on0eln0 3718	An ordinal number contains zero iff it is nonzero.
|- (A e. On -> ((/) e. A <-> A =/= (/)))
Theorem	dflim2 3719	An alternate definition of a limit ordinal.
|- (Lim A <-> (Ord A /\ (/) e. A /\ A = U.A))
Theorem	inton 3720	The intersection of the class of ordinal numbers is the empty set.
|- |^|On = (/)
Theorem	nlim0 3721	The empty set is not a limit ordinal. (The proof was shortened by Andrew Salmon, 25-Jul-2011.)
|- -. Lim (/)
Theorem	nlim0OLD 3722	The empty set is not a limit ordinal.
|- -. Lim (/)
Theorem	limord 3723	A limit ordinal is ordinal.
|- (Lim A -> Ord A)
Theorem	limuni 3724	A limit ordinal is its own supremum (union).
|- (Lim A -> A = U.A)
Theorem	limuni2 3725	The union of a limit ordinal is a limit ordinal.
|- (Lim A -> Lim U.A)
Theorem	0ellim 3726	A limit ordinal contains the empty set.
|- (Lim A -> (/) e. A)
Theorem	limelon 3727	A limit ordinal class that is also a set is an ordinal number.
|- ((A e. B /\ Lim A) -> A e. On)
Theorem	onn0 3728	The class of all ordinal numbers in not empty.
|- On =/= (/)
Theorem	suceq 3729	Equality of successors. (The proof was shortened by Andrew Salmon, 25-Jul-2011.)
|- (A = B -> suc A = suc B)
Theorem	suceqOLD 3730	Equality of successors.
|- (A = B -> suc A = suc B)
Theorem	elsuci 3731	Membership in a successor. This one-way implication does not require that either A or B be sets.
|- (A e. suc B -> (A e. B \/ A = B))
Theorem	elsucg 3732	Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17.
|- (A e. C -> (A e. suc B <-> (A e. B \/ A = B)))
Theorem	elsuc2g 3733	Variant of membership in a successor, requiring that B rather than A be a set.
|- (B e. C -> (A e. suc B <-> (A e. B \/ A = B)))
Theorem	elsuc 3734	Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17.
|- A e. _V   =>   |- (A e. suc B <-> (A e. B \/ A = B))
Theorem	elsuc2 3735	Membership in a successor.
|- A e. _V   =>   |- (B e. suc A <-> (B e. A \/ B = A))
Theorem	hbsuc 3736	Bound-variable hypothesis builder for successor.
|- (y e. A -> A.x y e. A)   =>   |- (y e. suc A -> A.x y e. suc A)
Theorem	elelsuc 3737	Membership in a successor.
|- (A e. B -> A e. suc B)
Theorem	sucel 3738	Membership of a successor in another class.
|- (suc A e. B <-> E.x e. B A.y(y e. x <-> (y e. A \/ y = A)))
Theorem	suc0 3739	The successor of the empty set.
|- suc (/) = {(/)}
Theorem	sucprc 3740	A proper class is its own successor.
|- (-. A e. _V -> suc A = A)
Theorem	unisuc 3741	A transitive class is equal to the union of its successor. Combines Theorem 4E of [Enderton] p. 72 and Exercise 6 of [Enderton] p. 73.
|- A e. _V   =>   |- (Tr A <-> U.suc A = A)
Theorem	sssucid 3742	A class is included in its own successor. Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized to arbitrary classes).
|- A C_ suc A
Theorem	sucidg 3743	Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized). (The proof was shortened by Scott Fenton, 20-Feb-2012.)
|- (A e. B -> A e. suc A)
Theorem	sucid 3744	A set belongs to its successor. (The proof was shortened by Scott Fenton, 18-Feb-2012.)
|- A e. _V   =>   |- A e. suc A
Theorem	sucidOLD 3745	A set belongs to its successor. (The proof was shortened by Alan Sare, 18-Feb-2012.) This proof was automatically generated from sucidVD 16696 using translatewithout_overwriting.cmd and minimizing.
|- A e. _V   =>   |- A e. suc A
Theorem	sucidOLDOLD 3746	A set belongs to its successor. (The proof was shortened by Andrew Salmon, 25-Jul-2011.)
|- A e. _V   =>   |- A e. suc A
Theorem	sucidOLDOLDOLD 3747	A set belongs to its successor.
|- A e. _V   =>   |- A e. suc A
Theorem	sucidgOLD 3748	Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized).
|- (A e. B -> A e. suc A)
Theorem	nsuceq0 3749	No successor is empty.
|- suc A =/= (/)
Theorem	eqelsuc 3750	A set belongs to the successor of an equal set.
|- A e. _V   =>   |- (A = B -> A e. suc B)
Theorem	suctr 3751	The successor of a transtive class is transitive. (Contributed by Alan Sare, 11-Apr-2009.)
|- (Tr A -> Tr suc A)
Theorem	trsuc 3752	A set whose successor belongs to a transitive class also belongs. (The proof was shortened by Andrew Salmon, 12-Aug-2011.)
|- ((Tr A /\ suc B e. A) -> B e. A)
Theorem	trsucOLD 3753	A set whose successor belongs to a transitive class also belongs.
|- ((Tr A /\ suc B e. A) -> B e. A)
Theorem	trsuc2 3754	The successor of a transitive set is transitive. (Contributed by Scott Fenton, 21-Feb-2011.)
|- (Tr A -> Tr suc A)
Theorem	trsucss 3755	A member of the successor of a transitive class is a subclass of it.
|- (Tr A -> (B e. suc A -> B C_ A))
Theorem	ordsssuc 3756	A subset of an ordinal belongs to its successor.
|- ((A e. On /\ Ord B) -> (A C_ B <-> A e. suc B))
Theorem	onsssuc 3757	A subset of an ordinal number belongs to its successor.
|- ((A e. On /\ B e. On) -> (A C_ B <-> A e. suc B))
Theorem	ordsssuc2 3758	An ordinal subset of an ordinal number belongs to its successor. (The proof was shortened by Andrew Salmon, 12-Aug-2011.)
|- ((Ord A /\ B e. On) -> (A C_ B <-> A e. suc B))
Theorem	ordsssuc2OLD 3759	An ordinal subset of an ordinal number belongs to its successor.
|- ((Ord A /\ B e. On) -> (A C_ B <-> A e. suc B))
Theorem	onmindif 3760	When its successor is subtracted from a class of ordinal numbers, an ordinal number is less than the minimum of the resulting subclass.
|- ((A C_ On /\ B e. On) -> B e. |^|(A \ suc B))
Theorem	ordnbtwn 3761	There is no set between an ordinal class and its successor. Generalized Proposition 7.25 of [TakeutiZaring] p. 41.
|- (Ord A -> -. (A e. B /\ B e. suc A))
Theorem	onnbtwn 3762	There is no set between an ordinal number and its successor. Proposition 7.25 of [TakeutiZaring] p. 41.
|- (A e. On -> -. (A e. B /\ B e. suc A))
Theorem	sucssel 3763	A set whose successor is a subset of another class is a member of that class.
|- (A e. C -> (suc A C_ B -> A e. B))
Theorem	orddif 3764	Ordinal derived from its successor.
|- (Ord A -> A = (suc A \ {A}))
Theorem	orduniss 3765	An ordinal class includes its union.
|- (Ord A -> U.A C_ A)
Theorem	ordtri2or 3766	A trichotomy law for ordinal classes. (The proof was shortened by Andrew Salmon, 12-Aug-2011.)
|- ((Ord A /\ Ord B) -> (A e. B \/ B C_ A))
Theorem	ordtri2orOLD 3767	A trichotomy law for ordinal classes.
|- ((Ord A /\ Ord B) -> (A e. B \/ B C_ A))
Theorem	ordtri2or2 3768	A trichotomy law for ordinal classes.
|- ((Ord A /\ Ord B) -> (A C_ B \/ B C_ A))
Theorem	ordssun 3769	Property of a subclass of the maximum (i.e. union) of two ordinals.
|- ((Ord B /\ Ord C) -> (A C_ (B u. C) <-> (A C_ B \/ A C_ C)))
Theorem	ordequn 3770	The maximum (i.e. union) of two ordinals is either one or the other. Similar to Exercise 14 of [TakeutiZaring] p. 40.
|- ((Ord B /\ Ord C) -> (A = (B u. C) -> (A = B \/ A = C)))
Theorem	ordun 3771	The maximum (i.e. union) of two ordinals is ordinal. Exercise 12 of [TakeutiZaring] p. 40.
|- ((Ord A /\ Ord B) -> Ord (A u. B))
Theorem	ordunisssuc 3772	A subclass relationship for union and successor of ordinal classes.
|- ((A C_ On /\ Ord B) -> (U.A C_ B <-> A C_ suc B))
Theorem	suc11 3773	The successor operation behaves like a one-to-one function. Compare Exercise 16 of [Enderton] p. 194.
|- ((A e. On /\ B e. On) -> (suc A = suc B <-> A = B))
Theorem	onordi 3774	An ordinal number is an ordinal class.
|- A e. On   =>   |- Ord A
Theorem	ontrci 3775	An ordinal number is a transitive class.
|- A e. On   =>   |- Tr A
Theorem	onirri 3776	An ordinal number is not a member of itself. Theorem 7M(c) of [Enderton] p. 192.
|- A e. On   =>   |- -. A e. A
Theorem	oneli 3777	A member of an ordinal number is an ordinal number. Theorem 7M(a) of [Enderton] p. 192.
|- A e. On   =>   |- (B e. A -> B e. On)
Theorem	onelssi 3778	A member of an ordinal number is a subset of it.
|- A e. On   =>   |- (B e. A -> B C_ A)
Theorem	onssneli 3779	An ordering law for ordinal numbers.
|- A e. On   =>   |- (A C_ B -> -. B e. A)
Theorem	onssnel2i 3780	An ordering law for ordinal numbers.
|- A e. On   =>   |- (B C_ A -> -. A e. B)
Theorem	onelini 3781	An element of an ordinal number equals the intersection with it.
|- A e. On   =>   |- (B e. A -> B = (B i^i A))
Theorem	oneluni 3782	An ordinal number equals its union with any element.
|- A e. On   =>   |- (B e. A -> (A u. B) = A)
Theorem	onunisuci 3783	An ordinal number is equal to the union of its successor.
|- A e. On   =>   |- U.suc A = A
Theorem	onsseli 3784	Subset is equivalent to membership or equality for ordinal numbers.
|- A e. On   &   |- B e. On   =>   |- (A C_ B <-> (A e. B \/ A = B))
Theorem	onun2i 3785	The union of two ordinal numbers is an ordinal number.
|- A e. On   &   |- B e. On   =>   |- (A u. B) e. On
Theorem	unizlim 3786	An ordinal equal to its own union is either zero or a limit ordinal.
|- (Ord A -> (A = U.A <-> (A = (/) \/ Lim A)))
Theorem	on0eqel 3787	An ordinal number either equals zero or contains zero.
|- (A e. On -> (A = (/) \/ (/) e. A))
Theorem	snsn0non 3788	The singleton of the singleton of the empty set is not an ordinal (nor a natural number by omsson 3954). It can be used to represent an "undefined" value for a partial operation on natural or ordinal numbers. See also onxpdisj 4068. (The proof was shortened by Andrew Salmon, 12-Aug-2011.)
|- -. {{(/)}} e. On
Theorem	snsn0nonOLD 3789	The singleton of the singleton of the empty set is not an ordinal (nor a natural number by omsson 3954). It can be used to represent an "undefined" value for a partial operation on natural or ordinal numbers. See also onxpdisj 4068.
|- -. {{(/)}} e. On
ZF Set Theory - add the Axiom of Union
Introduce the Axiom of Union
Axiom	ax-un 3790	Axiom of Union. An axiom of Zermelo-Fraenkel set theory. It states that a set y exists that includes the union of a given set x i.e. the collection of all members of the members of x. The variant axun2 3792 states that the union itself exists. A version with the standard abbreviation for union is uniex2 3793. A version using class notation is uniex 3794. The union of a class df-uni 3178 should not be confused with the union of two classes df-un 2600. Their relationship is shown in unipr 3191.
|- E.yA.z(E.w(z e. w /\ w e. x) -> z e. y)
Theorem	zfun 3791	Axiom of Union expressed with fewest number of different variables.
|- E.xA.y(E.x(y e. x /\ x e. z) -> y e. x)
Theorem	axun2 3792	A variant of the Axiom of Union ax-un 3790. For any set x, there exists a set y whose members are exactly the members of the members of x i.e. the union of x. Axiom Union of [BellMachover] p. 466.
|- E.yA.z(z e. y <-> E.w(z e. w /\ w e. x))
Theorem	uniex2 3793	The Axiom of Union using the standard abbreviation for union. Given any set x, its union y exists.
|- E.y y = U.x
Theorem	uniex 3794	The Axiom of Union in class notation. This says that if A is a set i.e. A e. _V (see isset 2296), then the union of A is also a set. Same as Axiom 3 of [TakeutiZaring] p. 16.
|- A e. _V   =>   |- U.A e. _V
Theorem	uniexg 3795	The ZF Axiom of Union in class notation, in the form of a theorem instead of an inference. We use the antecedent A e. B instead of A e. _V to make the theorem more general and thus shorten some proofs; obviously _V is one possibility for B.
|- (A e. B -> U.A e. _V)
Theorem	unex 3796	The union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16.
|- A e. _V   &   |- B e. _V   =>   |- (A u. B) e. _V
Theorem	unexb 3797	Existence of union is equivalent to existence of its components.
|- ((A e. _V /\ B e. _V) <-> (A u. B) e. _V)
Theorem	unexg 3798	A union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16.
|- ((A e. C /\ B e. D) -> (A u. B) e. _V)
Theorem	unisn2 3799	A version of unisn 3193 without the A e. _V hypothesis. (Contributed by Stefan Allan, 14-Mar-2006.)
|- U.{A} e. {(/), A}
Theorem	unisn3 3800	Union of a singleton in the form of a restricted class abstraction.
|- (A e. B -> U.{x e. B | x = A} = A)