P. 361 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36001-36100   *Has distinct variable group(s)

Type	Label	Description
Statement
21.11.10  Properties of functions and mappings
Theorem	funpsstri 36001	A condition for subset trichotomy for functions. (Contributed by Scott Fenton, 19-Apr-2011.)
⊢ ((Fun 𝐻 ∧ (𝐹 ⊆ 𝐻 ∧ 𝐺 ⊆ 𝐻) ∧ (dom 𝐹 ⊆ dom 𝐺 ∨ dom 𝐺 ⊆ dom 𝐹)) → (𝐹 ⊊ 𝐺 ∨ 𝐹 = 𝐺 ∨ 𝐺 ⊊ 𝐹))
Theorem	fundmpss 36002	If a class 𝐹 is a proper subset of a function 𝐺, then dom 𝐹 ⊊ dom 𝐺. (Contributed by Scott Fenton, 20-Apr-2011.)
⊢ (Fun 𝐺 → (𝐹 ⊊ 𝐺 → dom 𝐹 ⊊ dom 𝐺))
Theorem	funsseq 36003	Given two functions with equal domains, equality only requires one direction of the subset relationship. (Contributed by Scott Fenton, 24-Apr-2012.) (Proof shortened by Mario Carneiro, 3-May-2015.)
⊢ ((Fun 𝐹 ∧ Fun 𝐺 ∧ dom 𝐹 = dom 𝐺) → (𝐹 = 𝐺 ↔ 𝐹 ⊆ 𝐺))
Theorem	fununiq 36004	The uniqueness condition of functions. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (Fun 𝐹 → ((𝐴𝐹𝐵 ∧ 𝐴𝐹𝐶) → 𝐵 = 𝐶))
Theorem	funbreq 36005	An equality condition for functions. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ ((Fun 𝐹 ∧ 𝐴𝐹𝐵) → (𝐴𝐹𝐶 ↔ 𝐵 = 𝐶))
Theorem	br1steq 36006	Uniqueness condition for the binary relation 1st. (Contributed by Scott Fenton, 11-Apr-2014.) (Proof shortened by Mario Carneiro, 3-May-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩1st 𝐶 ↔ 𝐶 = 𝐴)
Theorem	br2ndeq 36007	Uniqueness condition for the binary relation 2nd. (Contributed by Scott Fenton, 11-Apr-2014.) (Proof shortened by Mario Carneiro, 3-May-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (⟨𝐴, 𝐵⟩2nd 𝐶 ↔ 𝐶 = 𝐵)
Theorem	dfdm5 36008	Definition of domain in terms of 1st and image. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ dom 𝐴 = ((1st ↾ (V × V)) “ 𝐴)
Theorem	dfrn5 36009	Definition of range in terms of 2nd and image. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ ran 𝐴 = ((2nd ↾ (V × V)) “ 𝐴)
Theorem	opelco3 36010	Alternate way of saying that an ordered pair is in a composition. (Contributed by Scott Fenton, 6-May-2018.)
⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 ∘ 𝐷) ↔ 𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})))
Theorem	elima4 36011	Quantifier-free expression saying that a class is a member of an image. (Contributed by Scott Fenton, 8-May-2018.)
⊢ (𝐴 ∈ (𝑅 “ 𝐵) ↔ (𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅)
Theorem	fv1stcnv 36012	The value of the converse of 1st restricted to a singleton. (Contributed by Scott Fenton, 2-Jul-2020.)
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → (◡(1st ↾ (𝐴 × {𝑌}))‘𝑋) = ⟨𝑋, 𝑌⟩)
Theorem	fv2ndcnv 36013	The value of the converse of 2nd restricted to a singleton. (Contributed by Scott Fenton, 2-Jul-2020.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → (◡(2nd ↾ ({𝑋} × 𝐴))‘𝑌) = ⟨𝑋, 𝑌⟩)
21.11.11  Ordinal numbers
Theorem	elpotr 36014*	A class of transitive sets is partially ordered by E. (Contributed by Scott Fenton, 15-Oct-2010.)
⊢ (∀𝑧 ∈ 𝐴 Tr 𝑧 → E Po 𝐴)
Theorem	dford5reg 36015	Given ax-reg 9504, an ordinal is a transitive class totally ordered by the membership relation. (Contributed by Scott Fenton, 28-Jan-2011.)
⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E Or 𝐴))
Theorem	dfon2lem1 36016	Lemma for dfon2 36025. (Contributed by Scott Fenton, 28-Feb-2011.)
⊢ Tr ∪ {𝑥 ∣ (𝜑 ∧ Tr 𝑥 ∧ 𝜓)}
Theorem	dfon2lem2 36017*	Lemma for dfon2 36025. (Contributed by Scott Fenton, 28-Feb-2011.)
⊢ ∪ {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝜑 ∧ 𝜓)} ⊆ 𝐴
Theorem	dfon2lem3 36018*	Lemma for dfon2 36025. All sets satisfying the new definition are transitive and untangled. (Contributed by Scott Fenton, 25-Feb-2011.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) → (Tr 𝐴 ∧ ∀𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑧)))
Theorem	dfon2lem4 36019*	Lemma for dfon2 36025. If two sets satisfy the new definition, then one is a subset of the other. (Contributed by Scott Fenton, 25-Feb-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) ∧ ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴))
Theorem	dfon2lem5 36020*	Lemma for dfon2 36025. Two sets satisfying the new definition also satisfy trichotomy with respect to ∈. (Contributed by Scott Fenton, 25-Feb-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) ∧ ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))
Theorem	dfon2lem6 36021*	Lemma for dfon2 36025. A transitive class of sets satisfying the new definition satisfies the new definition. (Contributed by Scott Fenton, 25-Feb-2011.)
⊢ ((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) → ∀𝑦((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → 𝑦 ∈ 𝑆))
Theorem	dfon2lem7 36022*	Lemma for dfon2 36025. All elements of a new ordinal are new ordinals. (Contributed by Scott Fenton, 25-Feb-2011.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) → (𝐵 ∈ 𝐴 → ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)))
Theorem	dfon2lem8 36023*	Lemma for dfon2 36025. The intersection of a nonempty class 𝐴 of new ordinals is itself a new ordinal and is contained within 𝐴 (Contributed by Scott Fenton, 26-Feb-2011.)
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) ∧ ∩ 𝐴 ∈ 𝐴))
Theorem	dfon2lem9 36024*	Lemma for dfon2 36025. A class of new ordinals is well-founded by E. (Contributed by Scott Fenton, 3-Mar-2011.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → E Fr 𝐴)
Theorem	dfon2 36025*	On consists of all sets that contain all its transitive proper subsets. This definition comes from J. R. Isbell, "A Definition of Ordinal Numbers", American Mathematical Monthly, vol 67 (1960), pp. 51-52. (Contributed by Scott Fenton, 20-Feb-2011.)
⊢ On = {𝑥 ∣ ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)}
Theorem	rdgprc0 36026	The value of the recursive definition generator at ∅ when the base value is a proper class. (Contributed by Scott Fenton, 26-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (¬ 𝐼 ∈ V → (rec(𝐹, 𝐼)‘∅) = ∅)
Theorem	rdgprc 36027	The value of the recursive definition generator when 𝐼 is a proper class. (Contributed by Scott Fenton, 26-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (¬ 𝐼 ∈ V → rec(𝐹, 𝐼) = rec(𝐹, ∅))
Theorem	dfrdg2 36028*	Alternate definition of the recursive function generator when 𝐼 is a set. (Contributed by Scott Fenton, 26-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (𝐼 ∈ 𝑉 → rec(𝐹, 𝐼) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))})
Theorem	dfrdg3 36029*	Generalization of dfrdg2 36028 to remove sethood requirement. (Contributed by Scott Fenton, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ rec(𝐹, 𝐼) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐼 ∈ V, 𝐼, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))}
21.11.12  Defined equality axioms
Theorem	axextdfeq 36030	A version of ax-ext 2712 for use with defined equality. (Contributed by Scott Fenton, 12-Dec-2010.)
⊢ ∃𝑧((𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦) → ((𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥) → (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤)))
Theorem	ax8dfeq 36031	A version of ax-8 2121 for use with defined equality. (Contributed by Scott Fenton, 12-Dec-2010.)
⊢ ∃𝑧((𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦) → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑦))
Theorem	axextdist 36032	ax-ext 2712 with distinctors instead of distinct variable conditions. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦))
Theorem	axextbdist 36033	axextb 2715 with distinctors instead of distinct variable conditions. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (𝑥 = 𝑦 ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)))
Theorem	19.12b 36034*	Version of 19.12vv 2355 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 36035	There is always a set not in 𝑦. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ ∃𝑥 ¬ 𝑥 ∈ 𝑦
Theorem	distel 36036	Distinctors in terms of membership. (NOTE: this only works with relations where we can prove el 5384 and elirrv 9509.) (Contributed by Scott Fenton, 15-Dec-2010.)
⊢ (¬ ∀𝑦 𝑦 = 𝑥 ↔ ¬ ∀𝑦 ¬ 𝑥 ∈ 𝑦)
Theorem	axextndbi 36037	axextnd 10512 as a biconditional. (Contributed by Scott Fenton, 14-Dec-2010.)
⊢ ∃𝑧(𝑥 = 𝑦 ↔ (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
21.11.13  Hypothesis builders
Theorem	hbntg 36038	A more general form of hbnt 2305. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜓) → (¬ 𝜓 → ∀𝑥 ¬ 𝜑))
Theorem	hbimtg 36039	A more general and closed form of hbim 2310. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ ((∀𝑥(𝜑 → ∀𝑥𝜒) ∧ (𝜓 → ∀𝑥𝜃)) → ((𝜒 → 𝜓) → ∀𝑥(𝜑 → 𝜃)))
Theorem	hbaltg 36040	A more general and closed form of hbal 2178. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ (∀𝑥(𝜑 → ∀𝑦𝜓) → (∀𝑥𝜑 → ∀𝑦∀𝑥𝜓))
Theorem	hbng 36041	A more general form of hbn 2306. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ (𝜑 → ∀𝑥𝜓)    ⇒   ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜑)
Theorem	hbimg 36042	A more general form of hbim 2310. (Contributed by Scott Fenton, 13-Dec-2010.)
⊢ (𝜑 → ∀𝑥𝜓)    &   ⊢ (𝜒 → ∀𝑥𝜃)    ⇒   ⊢ ((𝜓 → 𝜒) → ∀𝑥(𝜑 → 𝜃))
21.11.14  Well-founded zero, successor, and limits
Syntax	cwsuc 36043	Declare the syntax for well-founded successor.
class wsuc(𝑅, 𝐴, 𝑋)
Syntax	cwlim 36044	Declare the syntax for well-founded limit class.
class WLim(𝑅, 𝐴)
Definition	df-wsuc 36045	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 36046*	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 36047	Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌) → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑆, 𝐵, 𝑌))
Theorem	wsuceq1 36048	Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ (𝑅 = 𝑆 → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑆, 𝐴, 𝑋))
Theorem	wsuceq2 36049	Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ (𝐴 = 𝐵 → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑅, 𝐵, 𝑋))
Theorem	wsuceq3 36050	Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.)
⊢ (𝑋 = 𝑌 → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑅, 𝐴, 𝑌))
Theorem	nfwsuc 36051	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 36052	Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵) → WLim(𝑅, 𝐴) = WLim(𝑆, 𝐵))
Theorem	wlimeq1 36053	Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.)
⊢ (𝑅 = 𝑆 → WLim(𝑅, 𝐴) = WLim(𝑆, 𝐴))
Theorem	wlimeq2 36054	Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.)
⊢ (𝐴 = 𝐵 → WLim(𝑅, 𝐴) = WLim(𝑅, 𝐵))
Theorem	nfwlim 36055	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 36056	Membership in the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.)
⊢ (𝑋 ∈ WLim(𝑅, 𝐴) ↔ (𝑋 ∈ 𝐴 ∧ 𝑋 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑋 = sup(Pred(𝑅, 𝐴, 𝑋), 𝐴, 𝑅)))
Theorem	wzel 36057	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 36058*	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 36059	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 36060*	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 36061	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 36062	The class of limit points is a subclass of the base class. (Contributed by Scott Fenton, 16-Jun-2018.)
⊢ WLim(𝑅, 𝐴) ⊆ 𝐴
21.11.15  Quantifier-free definitions
Syntax	ctxp 36063	Declare the syntax for tail Cartesian product.
class (𝐴 ⊗ 𝐵)
Syntax	cpprod 36064	Declare the syntax for the parallel product.
class pprod(𝑅, 𝑆)
Syntax	csset 36065	Declare the subset relationship class.
class SSet
Syntax	ctrans 36066	Declare the transitive set class.
class Trans
Syntax	cbigcup 36067	Declare the set union relationship.
class Bigcup
Syntax	cfix 36068	Declare the syntax for the fixpoints of a class.
class Fix 𝐴
Syntax	climits 36069	Declare the class of limit ordinals.
class Limits
Syntax	cfuns 36070	Declare the syntax for the class of all function.
class Funs
Syntax	csingle 36071	Declare the syntax for the singleton function.
class Singleton
Syntax	csingles 36072	Declare the syntax for the class of all singletons.
class Singletons
Syntax	cimage 36073	Declare the syntax for the image functor.
class Image𝐴
Syntax	ccart 36074	Declare the syntax for the cartesian function.
class Cart
Syntax	cimg 36075	Declare the syntax for the image function.
class Img
Syntax	cdomain 36076	Declare the syntax for the domain function.
class Domain
Syntax	crange 36077	Declare the syntax for the range function.
class Range
Syntax	capply 36078	Declare the syntax for the application function.
class Apply
Syntax	ccup 36079	Declare the syntax for the cup function.
class Cup
Syntax	ccap 36080	Declare the syntax for the cap function.
class Cap
Syntax	csuccf 36081	Declare the syntax for the successor function.
class Succ
Syntax	cfunpart 36082	Declare the syntax for the functional part functor.
class Funpart𝐹
Syntax	cfullfn 36083	Declare the syntax for the full function functor.
class FullFun𝐹
Syntax	crestrict 36084	Declare the syntax for the restriction function.
class Restrict
Syntax	cub 36085	Declare the syntax for the upper bound relationship functor.
class UB𝑅
Syntax	clb 36086	Declare the syntax for the lower bound relationship functor.
class LB𝑅
Definition	df-txp 36087	Define the tail cross of two classes. Membership in this class is defined by txpss3v 36111 and brtxp 36113. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ (𝐴 ⊗ 𝐵) = ((◡(1st ↾ (V × V)) ∘ 𝐴) ∩ (◡(2nd ↾ (V × V)) ∘ 𝐵))
Definition	df-pprod 36088	Define the parallel product of two classes. Membership in this class is defined by pprodss4v 36117 and brpprod 36118. (Contributed by Scott Fenton, 11-Apr-2014.)
⊢ pprod(𝐴, 𝐵) = ((𝐴 ∘ (1st ↾ (V × V))) ⊗ (𝐵 ∘ (2nd ↾ (V × V))))
Definition	df-sset 36089	Define the subset class. For the value, see brsset 36122. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ SSet = ((V × V) ∖ ran ( E ⊗ (V ∖ E )))
Definition	df-trans 36090	Define the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012.)
⊢ Trans = (V ∖ ran (( E ∘ E ) ∖ E ))
Definition	df-bigcup 36091	Define the Bigcup function, which, per fvbigcup 36135, 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 36092	Define the class of all fixpoints of a relationship. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Fix 𝐴 = dom (𝐴 ∩ I )
Definition	df-limits 36093	Define the class of all limit ordinals. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ Limits = ((On ∩ Fix Bigcup ) ∖ {∅})
Definition	df-funs 36094	Define the class of all functions. See elfuns 36148 for membership. (Contributed by Scott Fenton, 18-Feb-2013.)
⊢ Funs = (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ ◡ E )))
Definition	df-singleton 36095	Define the singleton function. See brsingle 36150 for its value. (Contributed by Scott Fenton, 4-Apr-2014.)
⊢ Singleton = ((V × V) ∖ ran ((V ⊗ E ) △ ( I ⊗ V)))
Definition	df-singles 36096	Define the class of all singletons. See elsingles 36151 for membership. (Contributed by Scott Fenton, 19-Feb-2013.)
⊢ Singletons = ran Singleton
Definition	df-image 36097	Define the image functor. This function takes a set 𝐴 to a function 𝑥 ↦ (𝐴 “ 𝑥), providing that the latter exists. See imageval 36163 for the derivation. (Contributed by Scott Fenton, 27-Mar-2014.)
⊢ Image𝐴 = ((V × V) ∖ ran ((V ⊗ E ) △ (( E ∘ ◡𝐴) ⊗ V)))
Definition	df-cart 36098	Define the cartesian product function. See brcart 36165 for its value. (Contributed by Scott Fenton, 11-Apr-2014.)
⊢ Cart = (((V × V) × V) ∖ ran ((V ⊗ E ) △ (pprod( E , E ) ⊗ V)))
Definition	df-img 36099	Define the image function. See brimg 36170 for its value. (Contributed by Scott Fenton, 12-Apr-2014.)
⊢ Img = (Image((2nd ∘ 1st ) ↾ (1st ↾ (V × V))) ∘ Cart)
Definition	df-domain 36100	Define the domain function. See brdomain 36166 for its value. (Contributed by Scott Fenton, 11-Apr-2014.)
⊢ Domain = Image(1st ↾ (V × V))