mmtheorems31 - 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-12229

Statement List for Metamath Proof Explorer - 3001-3100 - Page 31 of 123

Type	Label	Description
Statement
Theorem	tz7.7 3001	Proposition 7.7 of [TakeutiZaring] p. 37.
|- ((Ord A /\ Tr B) -> (B e. A <-> (B (_ A /\ B =/= A)))
Theorem	ordelssne 3002	Corollary 7.8 of [TakeutiZaring] p. 37.
|- ((Ord A /\ Ord B) -> (A e. B <-> (A (_ B /\ A =/= B)))
Theorem	ordelpss 3003	Corollary 7.8 of [TakeutiZaring] p. 37.
|- ((Ord A /\ Ord B) -> (A e. B <-> A (. B))
Theorem	ordsseleq 3004	For ordinal classes, subclass is equivalent to membership or equality.
|- ((Ord A /\ Ord B) -> (A (_ B <-> (A e. B \/ A = B)))
Theorem	ordin 3005	The intersection of two ordinal classes is ordinal. Proposition 7.9 of [TakeutiZaring] p. 37.
|- ((Ord A /\ Ord B) -> Ord (A i^i B))
Theorem	onin 3006	The intersection of two ordinal numbers is an ordinal number.
|- ((A e. On /\ B e. On) -> (A i^i B) e. On)
Theorem	ordtri3or 3007	A trichotomy law for ordinals. Proposition 7.10 of [TakeutiZaring] p. 38.
|- ((Ord A /\ Ord B) -> (A e. B \/ A = B \/ B e. A))
Theorem	ordtri1 3008	A trichotomy law for ordinals.
|- ((Ord A /\ Ord B) -> (A (_ B <-> -. B e. A))
Theorem	ontri1 3009	A trichotomy law for ordinal numbers.
|- ((A e. On /\ B e. On) -> (A (_ B <-> -. B e. A))
Theorem	ordtri2 3010	A trichotomy law for ordinals.
|- ((Ord A /\ Ord B) -> (A e. B <-> -. (A = B \/ B e. A)))
Theorem	ordtri3 3011	A trichotomy law for ordinals.
|- ((Ord A /\ Ord B) -> (A = B <-> -. (A e. B \/ B e. A)))
Theorem	ordtri4 3012	A trichotomy law for ordinals.
|- ((Ord A /\ Ord B) -> (A = B <-> (A (_ B /\ -. A e. B)))
Theorem	orddisj 3013	An ordinal class and its singleton are disjoint.
|- (Ord A -> (A i^i {A}) = (/))
Theorem	onfr 3014	The ordinal class is founded. This lemma is needed for ordon 3141 in order to eliminate the need for the Axiom of Regularity.
|- E Fr On
Theorem	onelpss 3015	Relationship between membership and proper subset of an ordinal number.
|- ((A e. On /\ B e. On) -> (A e. B <-> (A (_ B /\ A =/= B)))
Theorem	onsseleq 3016	Relationship between subset and membership of an ordinal number.
|- ((A e. On /\ B e. On) -> (A (_ B <-> (A e. B \/ A = B)))
Theorem	onelss 3017	An element of an ordinal number is a subset of the number.
|- (A e. On -> (B e. A -> B (_ A))
Theorem	ordtr1 3018	Transitive law for ordinal classes.
|- (Ord C -> ((A e. B /\ B e. C) -> A e. C))
Theorem	ordtr2 3019	Transitive law for ordinal classes.
|- ((Ord A /\ Ord C) -> ((A (_ B /\ B e. C) -> A e. C))
Theorem	ontr1 3020	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 3021	Transitive law for ordinal numbers. Exercise 3 of [TakeutiZaring] p. 40.
|- ((A e. On /\ C e. On) -> ((A (_ B /\ B e. C) -> A e. C))
Theorem	ordunidif 3022	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 3023	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} (_ A))
Theorem	oneqmini 3024	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 (_ On -> ((A e. B /\ A.x e. A -. x e. B) -> A = |^|B))
Theorem	ord0 3025	The empty set is an ordinal class.
|- Ord (/)
Theorem	0elon 3026	The empty set is an ordinal number. Corollary 7N(b) of [Enderton] p. 193.
|- (/) e. On
Theorem	ord0eln0 3027	A non-empty ordinal contains the empty set.
|- (Ord A -> ((/) e. A <-> A =/= (/)))
Theorem	on0eln0 3028	An ordinal number contains zero iff it is nonzero.
|- (A e. On -> ((/) e. A <-> A =/= (/)))
Theorem	dflim2 3029	An alternate definition of a limit ordinal.
|- (Lim A <-> (Ord A /\ (/) e. A /\ A = U.A))
Theorem	inton 3030	The intersection of the class of ordinal numbers is the empty set.
|- |^|On = (/)
Theorem	nlim0 3031	The empty set is not a limit ordinal.
|- -. Lim (/)
Theorem	limord 3032	A limit ordinal is ordinal.
|- (Lim A -> Ord A)
Theorem	limuni 3033	A limit ordinal is its own supremum (union).
|- (Lim A -> A = U.A)
Theorem	limuni2 3034	The union of a limit ordinal is a limit ordinal.
|- (Lim A -> Lim U.A)
Theorem	0ellim 3035	A limit ordinal contains the empty set.
|- (Lim A -> (/) e. A)
Theorem	limelon 3036	A limit ordinal class that is also a set is an ordinal number.
|- ((A e. B /\ Lim A) -> A e. On)
Theorem	onn0 3037	The class of all ordinal numbers in not empty.
|- On =/= (/)
Theorem	suceq 3038	Equality of successors.
|- (A = B -> suc A = suc B)
Theorem	elsuci 3039	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 3040	Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17.
|- (A e. C -> (A e. suc B <-> (A e. B \/ A = B)))
Theorem	elsuc2g 3041	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 3042	Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17.
|- A e. V   =>   |- (A e. suc B <-> (A e. B \/ A = B))
Theorem	elsuc2 3043	Membership in a successor.
|- A e. V   =>   |- (B e. suc A <-> (B e. A \/ B = A))
Theorem	hbsuc 3044	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 3045	Membership in a successor.
|- (A e. B -> A e. suc B)
Theorem	sucel 3046	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 3047	The successor of the empty set.
|- suc (/) = {(/)}
Theorem	sucprc 3048	A proper class is its own successor.
|- (-. A e. V -> suc A = A)
Theorem	unisuc 3049	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 3050	A class is included in its own successor. Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized to arbitrary classes).
|- A (_ suc A
Theorem	sucid 3051	A set belongs to its successor.
|- A e. V   =>   |- A e. suc A
Theorem	sucidg 3052	Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized).
|- (A e. B -> A e. suc A)
Theorem	nsuceq0 3053	No successor is empty.
|- suc A =/= (/)
Theorem	eqelsuc 3054	A set belongs to the successor of an equal set.
|- A e. V   =>   |- (A = B -> A e. suc B)
Theorem	suctr 3055	The successor of a transtive class is transitive. (Contributed by Alan Sare, 11-Apr-2009.)
|- (Tr A -> Tr suc A)
Theorem	trsuc 3056	A set whose successor belongs to a transitive class also belongs.
|- ((Tr A /\ suc B e. A) -> B e. A)
Theorem	trsucss 3057	A member of the successor of a transitive class is a subclass of it.
|- (Tr A -> (B e. suc A -> B (_ A))
Theorem	ordsssuc 3058	A subset of an ordinal belongs to its successor.
|- ((A e. On /\ Ord B) -> (A (_ B <-> A e. suc B))
Theorem	onsssuc 3059	A subset of an ordinal number belongs to its successor.
|- ((A e. On /\ B e. On) -> (A (_ B <-> A e. suc B))
Theorem	ordsssuc2 3060	An ordinal subset of an ordinal number belongs to its successor.
|- ((Ord A /\ B e. On) -> (A (_ B <-> A e. suc B))
Theorem	onmindif 3061	When its successor is subtracted from a class of ordinal numbers, an ordinal number is less than the minimum of the resulting subclass.
|- ((A (_ On /\ B e. On) -> B e. |^|(A \ suc B))
Theorem	ordnbtwn 3062	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 3063	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 3064	A set whose successor is a subset of another class is a member of that class.
|- (A e. C -> (suc A (_ B -> A e. B))
Theorem	orddif 3065	Ordinal derived from its successor.
|- (Ord A -> A = (suc A \ {A}))
Theorem	orduniss 3066	An ordinal class includes its union.
|- (Ord A -> U.A (_ A)
Theorem	ordtri2or 3067	A trichotomy law for ordinal classes.
|- ((Ord A /\ Ord B) -> (A e. B \/ B (_ A))
Theorem	ordtri2or2 3068	A trichotomy law for ordinal classes.
|- ((Ord A /\ Ord B) -> (A (_ B \/ B (_ A))
Theorem	ordssun 3069	Property of a subclass of the maximum (i.e. union) of two ordinals.
|- ((Ord B /\ Ord C) -> (A (_ (B u. C) <-> (A (_ B \/ A (_ C)))
Theorem	ordequn 3070	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 3071	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 3072	A subclass relationship for union and successor of ordinal classes.
|- ((A (_ On /\ Ord B) -> (U.A (_ B <-> A (_ suc B))
Theorem	suc11 3073	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 3074	An ordinal number is an ordinal class.
|- A e. On   =>   |- Ord A
Theorem	ontrci 3075	An ordinal number is a transitive class.
|- A e. On   =>   |- Tr A
Theorem	onirri 3076	An ordinal number is not a member of itself. Theorem 7M(c) of [Enderton] p. 192.
|- A e. On   =>   |- -. A e. A
Theorem	oneli 3077	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 3078	A member of an ordinal number is a subset of it.
|- A e. On   =>   |- (B e. A -> B (_ A)
Theorem	onssneli 3079	An ordering law for ordinal numbers.
|- A e. On   =>   |- (A (_ B -> -. B e. A)
Theorem	onssnel2i 3080	An ordering law for ordinal numbers.
|- A e. On   =>   |- (B (_ A -> -. A e. B)
Theorem	onelini 3081	An element of an ordinal number equals the intersection with it.
|- A e. On   =>   |- (B e. A -> B = (B i^i A))
Theorem	oneluni 3082	An ordinal number equals its union with any element.
|- A e. On   =>   |- (B e. A -> (A u. B) = A)
Theorem	onunisuci 3083	An ordinal number is equal to the union of its successor.
|- A e. On   =>   |- U.suc A = A
Theorem	onsseli 3084	Subset is equivalent to membership or equality for ordinal numbers.
|- A e. On   &   |- B e. On   =>   |- (A (_ B <-> (A e. B \/ A = B))
Theorem	onun2i 3085	The union of two ordinal numbers is an ordinal number.
|- A e. On   &   |- B e. On   =>   |- (A u. B) e. On
Theorem	unizlim 3086	An ordinal equal to its own union is either zero or a limit ordinal.
|- (Ord A -> (A = U.A <-> (A = (/) \/ Lim A)))
Theorem	on0eqel 3087	An ordinal number either equals zero or contains zero.
|- (A e. On -> (A = (/) \/ (/) e. A))
Theorem	snsn0non 3088	The singleton of the singleton of the empty set is not an ordinal (nor a natural number by omsson 3223). It can be used to represent an "undefined" value for a partial operation on natural or ordinal numbers. See also onxpdisj 3328.
|- -. {{(/)}} e. On
ZF Set Theory - add the Axiom of Union
Introduce the Axiom of Union
Axiom	ax-un 3089	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 3091 states that the union itself exists. A version with the standard abbreviation for union is uniex2 3092. A version using class notation is uniex 3093. The union of a class df-uni 2570 should not be confused with the union of two classes df-un 2102. Their relationship is shown in unipr 2581.
|- E.yA.z(E.w(z e. w /\ w e. x) -> z e. y)
Theorem	zfun 3090	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 3091	A variant of the Axiom of Union ax-un 3089. 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 3092	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 3093	The Axiom of Union in class notation. This says that if A is a set i.e. A e. V (see isset 1860), 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 3094	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 3095	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 3096	Existence of union is equivalent to existence of its components.
|- ((A e. V /\ B e. V) <-> (A u. B) e. V)
Theorem	unexg 3097	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 3098	A version of unisn 2583 without the A e. V hypothesis. (Contributed by Stefan Allan, 14-Mar-2006.)
|- U.{A} e. {(/), A}
Theorem	unisn3 3099	Union of a singleton in the form of a restricted class abstraction.
|- (A e. B -> U.{x e. B | x = A} = A)
Theorem	snnex 3100	The class of all singletons is a proper class. (Proof shortened by Eric Schmidt, 7-Dec-2008.)
|- {x | E.y x = {y}} e/ V