P. 395 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39401-39500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ensucne0 39401	A class equinumerous to a successor is never empty. (Contributed by RP, 11-Nov-2023.) (Proof shortened by SN, 16-Nov-2023.)
⊢ (𝐴 ≈ suc 𝐵 → 𝐴 ≠ ∅)
Theorem	ensucne0OLD 39402	A class equinumerous to a successor is never empty. (Contributed by RP, 11-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ≈ suc 𝐵 → 𝐴 ≠ ∅)
Theorem	nndomog 39403	Cardinal ordering agrees with ordinal number ordering when the smaller number is a natural number. Compare with nndomo 8565 when both are natural numbers. (Originally by NM, 17-Jun-1998.) (Contributed by RP, 5-Nov-2023.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ On) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	dfom6 39404	Let ω be defined to be the union of the set of all finite ordinals. (Contributed by RP, 27-Sep-2023.)
⊢ ω = ∪ (On ∩ Fin)
Theorem	infordmin 39405	ω is the smallest infinite ordinal. (Contributed by RP, 27-Sep-2023.)
⊢ ∀𝑥 ∈ (On ∖ Fin)ω ⊆ 𝑥
Theorem	iscard4 39406	Two ways to express the property of being a cardinal number. (Contributed by RP, 8-Nov-2023.)
⊢ ((card‘𝐴) = 𝐴 ↔ 𝐴 ∈ ran card)
Theorem	iscard5 39407*	Two ways to express the property of being a cardinal number. (Contributed by RP, 8-Nov-2023.)
⊢ ((card‘𝐴) = 𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ≈ 𝐴))
Theorem	elrncard 39408*	Let us define a cardinal number to be an element 𝐴 ∈ On such that 𝐴 is not equipotent with any 𝑥 ∈ 𝐴. (Contributed by RP, 1-Oct-2023.)
⊢ (𝐴 ∈ ran card ↔ (𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ≈ 𝐴))
Theorem	harsucnn 39409	The next cardinal after a finite ordinal is the successor ordinal. (Contributed by RP, 5-Nov-2023.)
⊢ (𝐴 ∈ ω → (har‘𝐴) = suc 𝐴)
Theorem	harval3 39410*	(har‘𝐴) is the least cardinal that is greater than 𝐴. (Contributed by RP, 4-Nov-2023.)
⊢ (𝐴 ∈ dom card → (har‘𝐴) = ∩ {𝑥 ∈ ran card ∣ 𝐴 ≺ 𝑥})
Theorem	harval3on 39411*	For any ordinal number 𝐴 let (har‘𝐴) denote the least cardinal that is greater than 𝐴; (Contributed by RP, 4-Nov-2023.)
⊢ (𝐴 ∈ On → (har‘𝐴) = ∩ {𝑥 ∈ ran card ∣ 𝐴 ≺ 𝑥})
Theorem	en2pr 39412*	A class is equinumerous to ordinal two iff it is a pair of distinct sets. (Contributed by RP, 11-Oct-2023.)
⊢ (𝐴 ≈ 2o ↔ ∃𝑥∃𝑦(𝐴 = {𝑥, 𝑦} ∧ 𝑥 ≠ 𝑦))
Theorem	pr2cv 39413	If an unordered pair is equinumerous to ordinal two, then both parts are sets. (Contributed by RP, 8-Oct-2023.)
⊢ ({𝐴, 𝐵} ≈ 2o → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	pr2el1 39414	If an unordered pair is equinumerous to ordinal two, then a part is a member. (Contributed by RP, 21-Oct-2023.)
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐴 ∈ {𝐴, 𝐵})
Theorem	pr2cv1 39415	If an unordered pair is equinumerous to ordinal two, then a part is a set. (Contributed by RP, 21-Oct-2023.)
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐴 ∈ V)
Theorem	pr2el2 39416	If an unordered pair is equinumerous to ordinal two, then a part is a member. (Contributed by RP, 21-Oct-2023.)
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐵 ∈ {𝐴, 𝐵})
Theorem	pr2cv2 39417	If an unordered pair is equinumerous to ordinal two, then a part is a set. (Contributed by RP, 21-Oct-2023.)
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐵 ∈ V)
Theorem	pren2 39418	An unordered pair is equinumerous to ordinal two iff both parts are sets not equal to each other. (Contributed by RP, 8-Oct-2023.)
⊢ ({𝐴, 𝐵} ≈ 2o ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵))
Theorem	pr2eldif1 39419	If an unordered pair is equinumerous to ordinal two, then a part is an element of the difference of the pair and the singleton of the other part. (Contributed by RP, 21-Oct-2023.)
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐴 ∈ ({𝐴, 𝐵} ∖ {𝐵}))
Theorem	pr2eldif2 39420	If an unordered pair is equinumerous to ordinal two, then a part is an element of the difference of the pair and the singleton of the other part. (Contributed by RP, 21-Oct-2023.)
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐵 ∈ ({𝐴, 𝐵} ∖ {𝐴}))
Theorem	pren2d 39421	A pair of two distinct sets is equinumerous to ordinal two. (Contributed by RP, 21-Oct-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ≈ 2o)
Theorem	aleph1min 39422	(ℵ‘1o) is the least uncountable ordinal. (Contributed by RP, 18-Nov-2023.)
⊢ (ℵ‘1o) = ∩ {𝑥 ∈ On ∣ ω ≺ 𝑥}
Theorem	alephiso2 39423	ℵ is a strictly order-preserving mapping of On onto the class of all infinite cardinal numbers. (Contributed by RP, 18-Nov-2023.)
⊢ ℵ Isom E , ≺ (On, {𝑥 ∈ ran card ∣ ω ⊆ 𝑥})
Theorem	alephiso3 39424	ℵ is a strictly order-preserving mapping of On onto the class of all infinite cardinal numbers. (Contributed by RP, 18-Nov-2023.)
⊢ ℵ Isom E , ≺ (On, (ran card ∖ ω))
20.29.1.5  Infinite Sets
Theorem	pwelg 39425*	The powerclass is an element of a class closed under union and powerclass operations iff the element is a member of that class. (Contributed by RP, 21-Mar-2020.)
⊢ (∀𝑥 ∈ 𝐵 (∪ 𝑥 ∈ 𝐵 ∧ 𝒫 𝑥 ∈ 𝐵) → (𝐴 ∈ 𝐵 ↔ 𝒫 𝐴 ∈ 𝐵))
Theorem	pwinfig 39426*	The powerclass of an infinite set is an infinite set, and vice-versa. Here 𝐵 is a class which is closed under both the union and the powerclass operations and which may have infinite sets as members. (Contributed by RP, 21-Mar-2020.)
⊢ (∀𝑥 ∈ 𝐵 (∪ 𝑥 ∈ 𝐵 ∧ 𝒫 𝑥 ∈ 𝐵) → (𝐴 ∈ (𝐵 ∖ Fin) ↔ 𝒫 𝐴 ∈ (𝐵 ∖ Fin)))
Theorem	pwinfi2 39427	The powerclass of an infinite set is an infinite set, and vice-versa. Here 𝑈 is a weak universe. (Contributed by RP, 21-Mar-2020.)
⊢ (𝑈 ∈ WUni → (𝐴 ∈ (𝑈 ∖ Fin) ↔ 𝒫 𝐴 ∈ (𝑈 ∖ Fin)))
Theorem	pwinfi3 39428	The powerclass of an infinite set is an infinite set, and vice-versa. Here 𝑇 is a transitive Tarski universe. (Contributed by RP, 21-Mar-2020.)
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇) → (𝐴 ∈ (𝑇 ∖ Fin) ↔ 𝒫 𝐴 ∈ (𝑇 ∖ Fin)))
Theorem	pwinfi 39429	The powerclass of an infinite set is an infinite set, and vice-versa. (Contributed by RP, 21-Mar-2020.)
⊢ (𝐴 ∈ (V ∖ Fin) ↔ 𝒫 𝐴 ∈ (V ∖ Fin))
20.29.1.6  Finite intersection property While there is not yet a definition, the finite intersection property of a class is introduced by fiint 8648 where two textbook definitions are shown to be equivalent. This property is seen often with ordinal numbers (onin 6104, ordelinel 6171), chains of sets ordered by the proper subset relation (sorpssin 7322), various sets in the field of topology (inopn 21195, incld 21339, innei 21421, ... ) and "universal" classes like weak universes (wunin 9988, tskin 10034) and the class of all sets (inex1g 5121).
Theorem	fipjust 39430*	A definition of the finite intersection property of a class based on closure under pairwise intersection of its elements is independent of the dummy variables. (Contributed by RP, 1-Jan-2020.)
⊢ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 ∩ 𝑣) ∈ 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴)
Theorem	cllem0 39431*	The class of all sets with property 𝜑(𝑧) is closed under the binary operation on sets defined in 𝑅(𝑥, 𝑦). (Contributed by RP, 3-Jan-2020.)
⊢ 𝑉 = {𝑧 ∣ 𝜑}    &   ⊢ 𝑅 ∈ 𝑈    &   ⊢ (𝑧 = 𝑅 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑧 = 𝑥 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜃))    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜓)    ⇒   ⊢ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 𝑅 ∈ 𝑉
Theorem	superficl 39432*	The class of all supersets of a class has the finite intersection property. (Contributed by RP, 1-Jan-2020.) (Proof shortened by RP, 3-Jan-2020.)
⊢ 𝐴 = {𝑧 ∣ 𝐵 ⊆ 𝑧}    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴
Theorem	superuncl 39433*	The class of all supersets of a class is closed under binary union. (Contributed by RP, 3-Jan-2020.)
⊢ 𝐴 = {𝑧 ∣ 𝐵 ⊆ 𝑧}    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴
Theorem	ssficl 39434*	The class of all subsets of a class has the finite intersection property. (Contributed by RP, 1-Jan-2020.) (Proof shortened by RP, 3-Jan-2020.)
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵}    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴
Theorem	ssuncl 39435*	The class of all subsets of a class is closed under binary union. (Contributed by RP, 3-Jan-2020.)
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵}    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴
Theorem	ssdifcl 39436*	The class of all subsets of a class is closed under class difference. (Contributed by RP, 3-Jan-2020.)
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵}    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∖ 𝑦) ∈ 𝐴
Theorem	sssymdifcl 39437*	The class of all subsets of a class is closed under symmetric difference. (Contributed by RP, 3-Jan-2020.)
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵}    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∖ 𝑦) ∪ (𝑦 ∖ 𝑥)) ∈ 𝐴
Theorem	fiinfi 39438*	If two classes have the finite intersection property, then so does their intersection. (Contributed by RP, 1-Jan-2020.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 = (𝐴 ∩ 𝐵))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥 ∩ 𝑦) ∈ 𝐶)
20.29.1.7  RP ADDTO: Subclasses and subsets
Theorem	rababg 39439	Condition when restricted class is equal to unrestricted class. (Contributed by RP, 13-Aug-2020.)
⊢ (∀𝑥(𝜑 → 𝑥 ∈ 𝐴) ↔ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ 𝜑})
20.29.1.8  RP ADDTO: The intersection of a class
Theorem	elintabg 39440*	Two ways of saying a set is an element of the intersection of a class. (Contributed by RP, 13-Aug-2020.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥)))
Theorem	elinintab 39441*	Two ways of saying a set is an element of the intersection of a class with the intersection of a class. (Contributed by RP, 13-Aug-2020.)
⊢ (𝐴 ∈ (𝐵 ∩ ∩ {𝑥 ∣ 𝜑}) ↔ (𝐴 ∈ 𝐵 ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥)))
Theorem	elmapintrab 39442*	Two ways to say a set is an element of the intersection of a class of images. (Contributed by RP, 16-Aug-2020.)
⊢ 𝐶 ∈ V    &   ⊢ 𝐶 ⊆ 𝐵    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑤 ∈ 𝒫 𝐵 ∣ ∃𝑥(𝑤 = 𝐶 ∧ 𝜑)} ↔ ((∃𝑥𝜑 → 𝐴 ∈ 𝐵) ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝐶))))
20.29.1.9  RP ADDTO: Theorems requiring subset and intersection existence
Theorem	elinintrab 39443*	Two ways of saying a set is an element of the intersection of a class with the intersection of a class. (Contributed by RP, 14-Aug-2020.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑤 ∈ 𝒫 𝐵 ∣ ∃𝑥(𝑤 = (𝐵 ∩ 𝑥) ∧ 𝜑)} ↔ ((∃𝑥𝜑 → 𝐴 ∈ 𝐵) ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))))
Theorem	inintabss 39444*	Upper bound on intersection of class and the intersection of a class. (Contributed by RP, 13-Aug-2020.)
⊢ (𝐴 ∩ ∩ {𝑥 ∣ 𝜑}) ⊆ ∩ {𝑤 ∈ 𝒫 𝐴 ∣ ∃𝑥(𝑤 = (𝐴 ∩ 𝑥) ∧ 𝜑)}
Theorem	inintabd 39445*	Value of the intersection of class with the intersection of a nonempty class. (Contributed by RP, 13-Aug-2020.)
⊢ (𝜑 → ∃𝑥𝜓)    ⇒   ⊢ (𝜑 → (𝐴 ∩ ∩ {𝑥 ∣ 𝜓}) = ∩ {𝑤 ∈ 𝒫 𝐴 ∣ ∃𝑥(𝑤 = (𝐴 ∩ 𝑥) ∧ 𝜓)})
20.29.1.10  RP ADDTO: Relations
Theorem	xpinintabd 39446*	Value of the intersection of cross-product with the intersection of a nonempty class. (Contributed by RP, 12-Aug-2020.)
⊢ (𝜑 → ∃𝑥𝜓)    ⇒   ⊢ (𝜑 → ((𝐴 × 𝐵) ∩ ∩ {𝑥 ∣ 𝜓}) = ∩ {𝑤 ∈ 𝒫 (𝐴 × 𝐵) ∣ ∃𝑥(𝑤 = ((𝐴 × 𝐵) ∩ 𝑥) ∧ 𝜓)})
Theorem	relintabex 39447	If the intersection of a class is a relation, then the class is nonempty. (Contributed by RP, 12-Aug-2020.)
⊢ (Rel ∩ {𝑥 ∣ 𝜑} → ∃𝑥𝜑)
Theorem	elcnvcnvintab 39448*	Two ways of saying a set is an element of the converse of the converse of the intersection of a class. (Contributed by RP, 20-Aug-2020.)
⊢ (𝐴 ∈ ◡◡∩ {𝑥 ∣ 𝜑} ↔ (𝐴 ∈ (V × V) ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥)))
Theorem	relintab 39449*	Value of the intersection of a class when it is a relation. (Contributed by RP, 12-Aug-2020.)
⊢ (Rel ∩ {𝑥 ∣ 𝜑} → ∩ {𝑥 ∣ 𝜑} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜑)})
Theorem	nonrel 39450	A non-relation is equal to the base class with all ordered pairs removed. (Contributed by RP, 25-Oct-2020.)
⊢ (𝐴 ∖ ◡◡𝐴) = (𝐴 ∖ (V × V))
Theorem	elnonrel 39451	Only an ordered pair where not both entries are sets could be an element of the non-relation part of class. (Contributed by RP, 25-Oct-2020.)
⊢ (⟨𝑋, 𝑌⟩ ∈ (𝐴 ∖ ◡◡𝐴) ↔ (∅ ∈ 𝐴 ∧ ¬ (𝑋 ∈ V ∧ 𝑌 ∈ V)))
Theorem	cnvssb 39452	Subclass theorem for converse. (Contributed by RP, 22-Oct-2020.)
⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ◡𝐴 ⊆ ◡𝐵))
Theorem	relnonrel 39453	The non-relation part of a relation is empty. (Contributed by RP, 22-Oct-2020.)
⊢ (Rel 𝐴 ↔ (𝐴 ∖ ◡◡𝐴) = ∅)
Theorem	cnvnonrel 39454	The converse of the non-relation part of a class is empty. (Contributed by RP, 18-Oct-2020.)
⊢ ◡(𝐴 ∖ ◡◡𝐴) = ∅
Theorem	brnonrel 39455	A non-relation cannot relate any two classes. (Contributed by RP, 23-Oct-2020.)
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) → ¬ 𝑋(𝐴 ∖ ◡◡𝐴)𝑌)
Theorem	dmnonrel 39456	The domain of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
⊢ dom (𝐴 ∖ ◡◡𝐴) = ∅
Theorem	rnnonrel 39457	The range of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
⊢ ran (𝐴 ∖ ◡◡𝐴) = ∅
Theorem	resnonrel 39458	A restriction of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
⊢ ((𝐴 ∖ ◡◡𝐴) ↾ 𝐵) = ∅
Theorem	imanonrel 39459	An image under the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
⊢ ((𝐴 ∖ ◡◡𝐴) “ 𝐵) = ∅
Theorem	cononrel1 39460	Composition with the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
⊢ ((𝐴 ∖ ◡◡𝐴) ∘ 𝐵) = ∅
Theorem	cononrel2 39461	Composition with the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
⊢ (𝐴 ∘ (𝐵 ∖ ◡◡𝐵)) = ∅
20.29.1.11  RP ADDTO: Functions See also idssxp 5803 by Thierry Arnoux.
Theorem	elmapintab 39462*	Two ways to say a set is an element of mapped intersection of a class. Here 𝐹 maps elements of 𝐶 to elements of ∩ {𝑥 ∣ 𝜑} or 𝑥. (Contributed by RP, 19-Aug-2020.)
⊢ (𝐴 ∈ 𝐵 ↔ (𝐴 ∈ 𝐶 ∧ (𝐹‘𝐴) ∈ ∩ {𝑥 ∣ 𝜑}))    &   ⊢ (𝐴 ∈ 𝐸 ↔ (𝐴 ∈ 𝐶 ∧ (𝐹‘𝐴) ∈ 𝑥))    ⇒   ⊢ (𝐴 ∈ 𝐵 ↔ (𝐴 ∈ 𝐶 ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝐸)))
Theorem	fvnonrel 39463	The function value of any class under a non-relation is empty. (Contributed by RP, 23-Oct-2020.)
⊢ ((𝐴 ∖ ◡◡𝐴)‘𝑋) = ∅
Theorem	elinlem 39464	Two ways to say a set is a member of an intersection. (Contributed by RP, 19-Aug-2020.)
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ( I ‘𝐴) ∈ 𝐶))
Theorem	elcnvcnvlem 39465	Two ways to say a set is a member of the converse of the converse of a class. (Contributed by RP, 20-Aug-2020.)
⊢ (𝐴 ∈ ◡◡𝐵 ↔ (𝐴 ∈ (V × V) ∧ ( I ‘𝐴) ∈ 𝐵))
20.29.1.12  RP ADDTO: Finite induction (for finite ordinals) Original probably needs new subsection for Relation-related existence theorems.
Theorem	cnvcnvintabd 39466*	Value of the relationship content of the intersection of a class. (Contributed by RP, 20-Aug-2020.)
⊢ (𝜑 → ∃𝑥𝜓)    ⇒   ⊢ (𝜑 → ◡◡∩ {𝑥 ∣ 𝜓} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜓)})
20.29.1.13  RP ADDTO: First and second members of an ordered pair
Theorem	elcnvlem 39467	Two ways to say a set is a member of the converse of a class. (Contributed by RP, 19-Aug-2020.)
⊢ 𝐹 = (𝑥 ∈ (V × V) ↦ ⟨(2nd ‘𝑥), (1st ‘𝑥)⟩)    ⇒   ⊢ (𝐴 ∈ ◡𝐵 ↔ (𝐴 ∈ (V × V) ∧ (𝐹‘𝐴) ∈ 𝐵))
Theorem	elcnvintab 39468*	Two ways of saying a set is an element of the converse of the intersection of a class. (Contributed by RP, 19-Aug-2020.)
⊢ (𝐴 ∈ ◡∩ {𝑥 ∣ 𝜑} ↔ (𝐴 ∈ (V × V) ∧ ∀𝑥(𝜑 → 𝐴 ∈ ◡𝑥)))
Theorem	cnvintabd 39469*	Value of the converse of the intersection of a nonempty class. (Contributed by RP, 20-Aug-2020.)
⊢ (𝜑 → ∃𝑥𝜓)    ⇒   ⊢ (𝜑 → ◡∩ {𝑥 ∣ 𝜓} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡𝑥 ∧ 𝜓)})
20.29.1.14  RP ADDTO: The reflexive and transitive properties of relations
Theorem	undmrnresiss 39470*	Two ways of saying the identity relation restricted to the union of the domain and range of a relation is a subset of a relation. Generalization of reflexg 39471. (Contributed by RP, 26-Sep-2020.)
⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐵 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → (𝑥𝐵𝑥 ∧ 𝑦𝐵𝑦)))
Theorem	reflexg 39471*	Two ways of saying a relation is reflexive over its domain and range. (Contributed by RP, 4-Aug-2020.)
⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐴 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → (𝑥𝐴𝑥 ∧ 𝑦𝐴𝑦)))
Theorem	cnvssco 39472*	A condition weaker than reflexivity. (Contributed by RP, 3-Aug-2020.)
⊢ (◡𝐴 ⊆ ◡(𝐵 ∘ 𝐶) ↔ ∀𝑥∀𝑦∃𝑧(𝑥𝐴𝑦 → (𝑥𝐶𝑧 ∧ 𝑧𝐵𝑦)))
Theorem	refimssco 39473	Reflexive relations are subsets of their self-composition. (Contributed by RP, 4-Aug-2020.)
⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐴 → ◡𝐴 ⊆ ◡(𝐴 ∘ 𝐴))
20.29.1.15  RP ADDTO: Basic properties of closures
Theorem	cleq2lem 39474	Equality implies bijection. (Contributed by RP, 24-Jul-2020.)
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 = 𝐵 → ((𝑅 ⊆ 𝐴 ∧ 𝜑) ↔ (𝑅 ⊆ 𝐵 ∧ 𝜓)))
Theorem	cbvcllem 39475*	Change of bound variable in class of supersets of a with a property. (Contributed by RP, 24-Jul-2020.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜑)} = {𝑦 ∣ (𝑋 ⊆ 𝑦 ∧ 𝜓)}
Theorem	clublem 39476*	If a superset 𝑌 of 𝑋 possesses the property parameterized in 𝑥 in 𝜓, then 𝑌 is a superset of the closure of that property for the set 𝑋. (Contributed by RP, 23-Jul-2020.)
⊢ (𝜑 → 𝑌 ∈ V)    &   ⊢ (𝑥 = 𝑌 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑌)    &   ⊢ (𝜑 → 𝜒)    ⇒   ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} ⊆ 𝑌)
Theorem	clss2lem 39477*	The closure of a property is a superset of the closure of a less restrictive property. (Contributed by RP, 24-Jul-2020.)
⊢ (𝜑 → (𝜒 → 𝜓))    ⇒   ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} ⊆ ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜒)})
Theorem	dfid7 39478*	Definition of identity relation as the trivial closure. (Contributed by RP, 26-Jul-2020.)
⊢ I = (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ ⊤)})
Theorem	mptrcllem 39479*	Show two versions of a closure with reflexive properties are equal. (Contributed by RP, 19-Oct-2020.)
⊢ (𝑥 ∈ 𝑉 → ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ (𝜑 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))} ∈ V)    &   ⊢ (𝑥 ∈ 𝑉 → ∩ {𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ 𝜓)} ∈ V)    &   ⊢ (𝑥 ∈ 𝑉 → 𝜒)    &   ⊢ (𝑥 ∈ 𝑉 → 𝜃)    &   ⊢ (𝑥 ∈ 𝑉 → 𝜏)    &   ⊢ (𝑦 = ∩ {𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ 𝜓)} → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = ∩ {𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ 𝜓)} → (( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦 ↔ 𝜃))    &   ⊢ (𝑧 = ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ (𝜑 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))} → (𝜓 ↔ 𝜏))    ⇒   ⊢ (𝑥 ∈ 𝑉 ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ (𝜑 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))}) = (𝑥 ∈ 𝑉 ↦ ∩ {𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ 𝜓)})
Theorem	cotrintab 39480	The intersection of a class is a transitive relation if membership in the class implies the member is a transitive relation. (Contributed by RP, 28-Oct-2020.)
⊢ (𝜑 → (𝑥 ∘ 𝑥) ⊆ 𝑥)    ⇒   ⊢ (∩ {𝑥 ∣ 𝜑} ∘ ∩ {𝑥 ∣ 𝜑}) ⊆ ∩ {𝑥 ∣ 𝜑}
Theorem	rclexi 39481*	The reflexive closure of a set exists. (Contributed by RP, 27-Oct-2020.)
⊢ 𝐴 ∈ 𝑉    ⇒   ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)} ∈ V
Theorem	rtrclexlem 39482	Existence of relation implies existence of union with Cartesian product of domain and range. (Contributed by RP, 1-Nov-2020.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∪ ((dom 𝑅 ∪ ran 𝑅) × (dom 𝑅 ∪ ran 𝑅))) ∈ V)
Theorem	rtrclex 39483*	The reflexive-transitive closure of a set exists. (Contributed by RP, 1-Nov-2020.)
⊢ (𝐴 ∈ V ↔ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V)
Theorem	trclubgNEW 39484*	If a relation exists then the transitive closure has an upper bound. (Contributed by RP, 24-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))
Theorem	trclubNEW 39485*	If a relation exists then the transitive closure has an upper bound. (Contributed by RP, 24-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → Rel 𝑅)    ⇒   ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ⊆ (dom 𝑅 × ran 𝑅))
Theorem	trclexi 39486*	The transitive closure of a set exists. (Contributed by RP, 27-Oct-2020.)
⊢ 𝐴 ∈ 𝑉    ⇒   ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ∈ V
Theorem	rtrclexi 39487*	The reflexive-transitive closure of a set exists. (Contributed by RP, 27-Oct-2020.)
⊢ 𝐴 ∈ 𝑉    ⇒   ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V
Theorem	clrellem 39488*	When the property 𝜓 holds for a relation substituted for 𝑥, then the closure on that property is a relation if the base set is a relation. (Contributed by RP, 30-Jul-2020.)
⊢ (𝜑 → 𝑌 ∈ V)    &   ⊢ (𝜑 → Rel 𝑋)    &   ⊢ (𝑥 = ◡◡𝑌 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝑌)    &   ⊢ (𝜑 → 𝜒)    ⇒   ⊢ (𝜑 → Rel ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)})
Theorem	clcnvlem 39489*	When 𝐴, an upper bound of the closure, exists and certain substitutions hold the converse of the closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.)
⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → (𝜒 → 𝜓))    &   ⊢ ((𝜑 ∧ 𝑦 = ◡𝑥) → (𝜓 → 𝜒))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝜃)    ⇒   ⊢ (𝜑 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)})
Theorem	cnvtrucl0 39490*	The converse of the trivial closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.)
⊢ (𝑋 ∈ 𝑉 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ ⊤)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ ⊤)})
Theorem	cnvrcl0 39491*	The converse of the reflexive closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.)
⊢ (𝑋 ∈ 𝑉 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦)})
Theorem	cnvtrcl0 39492*	The converse of the transitive closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.)
⊢ (𝑋 ∈ 𝑉 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦)})
Theorem	dmtrcl 39493*	The domain of the transitive closure is equal to the domain of its base relation. (Contributed by RP, 1-Nov-2020.)
⊢ (𝑋 ∈ 𝑉 → dom ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} = dom 𝑋)
Theorem	rntrcl 39494*	The range of the transitive closure is equal to the range of its base relation. (Contributed by RP, 1-Nov-2020.)
⊢ (𝑋 ∈ 𝑉 → ran ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} = ran 𝑋)
Theorem	dfrtrcl5 39495*	Definition of reflexive-transitive closure as a standard closure. (Contributed by RP, 1-Nov-2020.)
⊢ t* = (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ (( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦))})
20.29.1.16  RP REPLACE: Definitions and basic properties of transitive closures
Theorem	trcleq2lemRP 39496	Equality implies bijection. (Contributed by RP, 5-May-2020.) (Proof modification is discouraged.)
⊢ (𝐴 = 𝐵 → ((𝑅 ⊆ 𝐴 ∧ (𝐴 ∘ 𝐴) ⊆ 𝐴) ↔ (𝑅 ⊆ 𝐵 ∧ (𝐵 ∘ 𝐵) ⊆ 𝐵)))
20.29.2  Additional statements on relations and subclasses
Theorem	al3im 39497	Version of ax-4 1795 for a nested implication. (Contributed by RP, 13-Apr-2020.)
⊢ (∀𝑥(𝜑 → (𝜓 → (𝜒 → 𝜃))) → (∀𝑥𝜑 → (∀𝑥𝜓 → (∀𝑥𝜒 → ∀𝑥𝜃))))
Theorem	intima0 39498*	Two ways of expressing the intersection of images of a class. (Contributed by RP, 13-Apr-2020.)
⊢ ∩ 𝑎 ∈ 𝐴 (𝑎 “ 𝐵) = ∩ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵)}
Theorem	elimaint 39499*	Element of image of intersection. (Contributed by RP, 13-Apr-2020.)
⊢ (𝑦 ∈ (∩ 𝐴 “ 𝐵) ↔ ∃𝑏 ∈ 𝐵 ∀𝑎 ∈ 𝐴 ⟨𝑏, 𝑦⟩ ∈ 𝑎)
Theorem	csbcog 39500	Distribute proper substitution through a composition of relations. (Contributed by RP, 28-Jun-2020.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵 ∘ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∘ ⦋𝐴 / 𝑥⦌𝐶))