P. 441 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 44001-44100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pren2d 44001	A pair of two distinct sets is equinumerous to ordinal two. (Contributed by RP, 21-Oct-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ≈ 2o)
Theorem	aleph1min 44002	(ℵ‘1o) is the least uncountable ordinal. (Contributed by RP, 18-Nov-2023.)
⊢ (ℵ‘1o) = ∩ {𝑥 ∈ On ∣ ω ≺ 𝑥}
Theorem	alephiso2 44003	ℵ 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 44004	ℵ 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 ∖ ω))
21.36.4.5  Infinite Sets
Theorem	pwelg 44005*	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 44006*	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 44007	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 44008	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 44009	The powerclass of an infinite set is an infinite set, and vice-versa. (Contributed by RP, 21-Mar-2020.)
⊢ (𝐴 ∈ (V ∖ Fin) ↔ 𝒫 𝐴 ∈ (V ∖ Fin))
21.36.4.6  Finite intersection property While there is not yet a definition, the finite intersection property of a class is introduced by fiint 9230 where two textbook definitions are shown to be equivalent. This property is seen often with ordinal numbers (onin 6348, ordelinel 6420), chains of sets ordered by the proper subset relation (sorpssin 7678), various sets in the field of topology (inopn 22874, incld 23018, innei 23100, ... ) and "universal" classes like weak universes (wunin 10627, tskin 10673) and the class of all sets (inex1g 5256).
Theorem	fipjust 44010*	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 44011*	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 44012*	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 44013*	The class of all supersets of a class is closed under binary union. (Contributed by RP, 3-Jan-2020.)
⊢ 𝐴 = {𝑧 ∣ 𝐵 ⊆ 𝑧}    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴
Theorem	ssficl 44014*	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 44015*	The class of all subsets of a class is closed under binary union. (Contributed by RP, 3-Jan-2020.)
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵}    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴
Theorem	ssdifcl 44016*	The class of all subsets of a class is closed under class difference. (Contributed by RP, 3-Jan-2020.)
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵}    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∖ 𝑦) ∈ 𝐴
Theorem	sssymdifcl 44017*	The class of all subsets of a class is closed under symmetric difference. (Contributed by RP, 3-Jan-2020.)
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵}    ⇒   ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∖ 𝑦) ∪ (𝑦 ∖ 𝑥)) ∈ 𝐴
Theorem	fiinfi 44018*	If two classes have the finite intersection property, then so does their intersection. (Contributed by RP, 1-Jan-2020.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ∈ 𝐵)    &   ⊢ (𝜑 → 𝐶 = (𝐴 ∩ 𝐵))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥 ∩ 𝑦) ∈ 𝐶)
21.36.4.7  RP ADDTO: Subclasses and subsets
Theorem	rababg 44019	Condition when restricted class is equal to unrestricted class. (Contributed by RP, 13-Aug-2020.)
⊢ (∀𝑥(𝜑 → 𝑥 ∈ 𝐴) ↔ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ 𝜑})
21.36.4.8  RP ADDTO: The intersection of a class
Theorem	elinintab 44020*	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 44021*	Two ways to say a set is an element of the intersection of a class of images. (Contributed by RP, 16-Aug-2020.)
⊢ 𝐶 ∈ V    &   ⊢ 𝐶 ⊆ 𝐵    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑤 ∈ 𝒫 𝐵 ∣ ∃𝑥(𝑤 = 𝐶 ∧ 𝜑)} ↔ ((∃𝑥𝜑 → 𝐴 ∈ 𝐵) ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝐶))))
21.36.4.9  RP ADDTO: Theorems requiring subset and intersection existence
Theorem	elinintrab 44022*	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 44023*	Upper bound on intersection of class and the intersection of a class. (Contributed by RP, 13-Aug-2020.)
⊢ (𝐴 ∩ ∩ {𝑥 ∣ 𝜑}) ⊆ ∩ {𝑤 ∈ 𝒫 𝐴 ∣ ∃𝑥(𝑤 = (𝐴 ∩ 𝑥) ∧ 𝜑)}
Theorem	inintabd 44024*	Value of the intersection of class with the intersection of a nonempty class. (Contributed by RP, 13-Aug-2020.)
⊢ (𝜑 → ∃𝑥𝜓)    ⇒   ⊢ (𝜑 → (𝐴 ∩ ∩ {𝑥 ∣ 𝜓}) = ∩ {𝑤 ∈ 𝒫 𝐴 ∣ ∃𝑥(𝑤 = (𝐴 ∩ 𝑥) ∧ 𝜓)})
21.36.4.10  RP ADDTO: Relations
Theorem	xpinintabd 44025*	Value of the intersection of Cartesian product with the intersection of a nonempty class. (Contributed by RP, 12-Aug-2020.)
⊢ (𝜑 → ∃𝑥𝜓)    ⇒   ⊢ (𝜑 → ((𝐴 × 𝐵) ∩ ∩ {𝑥 ∣ 𝜓}) = ∩ {𝑤 ∈ 𝒫 (𝐴 × 𝐵) ∣ ∃𝑥(𝑤 = ((𝐴 × 𝐵) ∩ 𝑥) ∧ 𝜓)})
Theorem	relintabex 44026	If the intersection of a class is a relation, then the class is nonempty. (Contributed by RP, 12-Aug-2020.)
⊢ (Rel ∩ {𝑥 ∣ 𝜑} → ∃𝑥𝜑)
Theorem	elcnvcnvintab 44027*	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 44028*	Value of the intersection of a class when it is a relation. (Contributed by RP, 12-Aug-2020.)
⊢ (Rel ∩ {𝑥 ∣ 𝜑} → ∩ {𝑥 ∣ 𝜑} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜑)})
Theorem	nonrel 44029	A non-relation is equal to the base class with all ordered pairs removed. (Contributed by RP, 25-Oct-2020.)
⊢ (𝐴 ∖ ◡◡𝐴) = (𝐴 ∖ (V × V))
Theorem	elnonrel 44030	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 44031	Subclass theorem for converse. (Contributed by RP, 22-Oct-2020.)
⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ◡𝐴 ⊆ ◡𝐵))
Theorem	relnonrel 44032	The non-relation part of a relation is empty. (Contributed by RP, 22-Oct-2020.)
⊢ (Rel 𝐴 ↔ (𝐴 ∖ ◡◡𝐴) = ∅)
Theorem	cnvnonrel 44033	The converse of the non-relation part of a class is empty. (Contributed by RP, 18-Oct-2020.)
⊢ ◡(𝐴 ∖ ◡◡𝐴) = ∅
Theorem	brnonrel 44034	A non-relation cannot relate any two classes. (Contributed by RP, 23-Oct-2020.)
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) → ¬ 𝑋(𝐴 ∖ ◡◡𝐴)𝑌)
Theorem	dmnonrel 44035	The domain of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
⊢ dom (𝐴 ∖ ◡◡𝐴) = ∅
Theorem	rnnonrel 44036	The range of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
⊢ ran (𝐴 ∖ ◡◡𝐴) = ∅
Theorem	resnonrel 44037	A restriction of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
⊢ ((𝐴 ∖ ◡◡𝐴) ↾ 𝐵) = ∅
Theorem	imanonrel 44038	An image under the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
⊢ ((𝐴 ∖ ◡◡𝐴) “ 𝐵) = ∅
Theorem	cononrel1 44039	Composition with the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
⊢ ((𝐴 ∖ ◡◡𝐴) ∘ 𝐵) = ∅
Theorem	cononrel2 44040	Composition with the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.)
⊢ (𝐴 ∘ (𝐵 ∖ ◡◡𝐵)) = ∅
21.36.4.11  RP ADDTO: Functions See also idssxp 6008 by Thierry Arnoux.
Theorem	elmapintab 44041*	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 44042	The function value of any class under a non-relation is empty. (Contributed by RP, 23-Oct-2020.)
⊢ ((𝐴 ∖ ◡◡𝐴)‘𝑋) = ∅
Theorem	elinlem 44043	Two ways to say a set is a member of an intersection. (Contributed by RP, 19-Aug-2020.)
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ( I ‘𝐴) ∈ 𝐶))
Theorem	elcnvcnvlem 44044	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 ‘𝐴) ∈ 𝐵))
21.36.4.12  RP ADDTO: Finite induction (for finite ordinals) Original probably needs new subsection for Relation-related existence theorems.
Theorem	cnvcnvintabd 44045*	Value of the relationship content of the intersection of a class. (Contributed by RP, 20-Aug-2020.)
⊢ (𝜑 → ∃𝑥𝜓)    ⇒   ⊢ (𝜑 → ◡◡∩ {𝑥 ∣ 𝜓} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜓)})
21.36.4.13  RP ADDTO: First and second members of an ordered pair
Theorem	elcnvlem 44046	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 44047*	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 44048*	Value of the converse of the intersection of a nonempty class. (Contributed by RP, 20-Aug-2020.)
⊢ (𝜑 → ∃𝑥𝜓)    ⇒   ⊢ (𝜑 → ◡∩ {𝑥 ∣ 𝜓} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡𝑥 ∧ 𝜓)})
21.36.4.14  RP ADDTO: The reflexive and transitive properties of relations
Theorem	undmrnresiss 44049*	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 44050. (Contributed by RP, 26-Sep-2020.)
⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐵 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → (𝑥𝐵𝑥 ∧ 𝑦𝐵𝑦)))
Theorem	reflexg 44050*	Two ways of saying a relation is reflexive over its domain and range. (Contributed by RP, 4-Aug-2020.)
⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐴 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → (𝑥𝐴𝑥 ∧ 𝑦𝐴𝑦)))
Theorem	cnvssco 44051*	A condition weaker than reflexivity. (Contributed by RP, 3-Aug-2020.)
⊢ (◡𝐴 ⊆ ◡(𝐵 ∘ 𝐶) ↔ ∀𝑥∀𝑦∃𝑧(𝑥𝐴𝑦 → (𝑥𝐶𝑧 ∧ 𝑧𝐵𝑦)))
Theorem	refimssco 44052	Reflexive relations are subsets of their self-composition. (Contributed by RP, 4-Aug-2020.)
⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐴 → ◡𝐴 ⊆ ◡(𝐴 ∘ 𝐴))
21.36.4.15  RP ADDTO: Basic properties of closures
Theorem	cleq2lem 44053	Equality implies bijection. (Contributed by RP, 24-Jul-2020.)
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 = 𝐵 → ((𝑅 ⊆ 𝐴 ∧ 𝜑) ↔ (𝑅 ⊆ 𝐵 ∧ 𝜓)))
Theorem	cbvcllem 44054*	Change of bound variable in class of supersets of a with a property. (Contributed by RP, 24-Jul-2020.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜑)} = {𝑦 ∣ (𝑋 ⊆ 𝑦 ∧ 𝜓)}
Theorem	clublem 44055*	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 44056*	The closure of a property is a superset of the closure of a less restrictive property. (Contributed by RP, 24-Jul-2020.)
⊢ (𝜑 → (𝜒 → 𝜓))    ⇒   ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} ⊆ ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜒)})
Theorem	dfid7 44057*	Definition of identity relation as the trivial closure. (Contributed by RP, 26-Jul-2020.)
⊢ I = (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ ⊤)})
Theorem	mptrcllem 44058*	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 44059	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 44060*	The reflexive closure of a set exists. (Contributed by RP, 27-Oct-2020.)
⊢ 𝐴 ∈ 𝑉    ⇒   ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)} ∈ V
Theorem	rtrclexlem 44061	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 44062*	The reflexive-transitive closure of a set exists. (Contributed by RP, 1-Nov-2020.)
⊢ (𝐴 ∈ V ↔ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V)
Theorem	trclubgNEW 44063*	If a relation exists then the transitive closure has an upper bound. (Contributed by RP, 24-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    ⇒   ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅)))
Theorem	trclubNEW 44064*	If a relation exists then the transitive closure has an upper bound. (Contributed by RP, 24-Jul-2020.)
⊢ (𝜑 → 𝑅 ∈ V)    &   ⊢ (𝜑 → Rel 𝑅)    ⇒   ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ⊆ (dom 𝑅 × ran 𝑅))
Theorem	trclexi 44065*	The transitive closure of a set exists. (Contributed by RP, 27-Oct-2020.)
⊢ 𝐴 ∈ 𝑉    ⇒   ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ∈ V
Theorem	rtrclexi 44066*	The reflexive-transitive closure of a set exists. (Contributed by RP, 27-Oct-2020.)
⊢ 𝐴 ∈ 𝑉    ⇒   ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V
Theorem	clrellem 44067*	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 44068*	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 44069*	The converse of the trivial closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.)
⊢ (𝑋 ∈ 𝑉 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ ⊤)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ ⊤)})
Theorem	cnvrcl0 44070*	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 44071*	The converse of the transitive closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.)
⊢ (𝑋 ∈ 𝑉 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦)})
Theorem	dmtrcl 44072*	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 44073*	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 44074*	Definition of reflexive-transitive closure as a standard closure. (Contributed by RP, 1-Nov-2020.)
⊢ t* = (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ (( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦))})
21.36.4.16  RP REPLACE: Definitions and basic properties of transitive closures
Theorem	trcleq2lemRP 44075	Equality implies bijection. (Contributed by RP, 5-May-2020.) (Proof modification is discouraged.)
⊢ (𝐴 = 𝐵 → ((𝑅 ⊆ 𝐴 ∧ (𝐴 ∘ 𝐴) ⊆ 𝐴) ↔ (𝑅 ⊆ 𝐵 ∧ (𝐵 ∘ 𝐵) ⊆ 𝐵)))
21.36.4.17  Additions for square root; absolute value This is based on the observation that the real and imaginary parts of a complex number can be calculated from the number's absolute and real part and the sign of its imaginary part. Formalization of the formula in sqrtcval 44086 was motivated by a short Michael Penn video.
Theorem	sqrtcvallem1 44076	Two ways of saying a complex number does not lie on the positive real axis. Lemma for sqrtcval 44086. (Contributed by RP, 17-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (((ℑ‘𝐴) = 0 → (ℜ‘𝐴) ≤ 0) ↔ ¬ 𝐴 ∈ ℝ+))
Theorem	reabsifneg 44077	Alternate expression for the absolute value of a real number. Lemma for sqrtcval 44086. (Contributed by RP, 11-May-2024.)
⊢ (𝐴 ∈ ℝ → (abs‘𝐴) = if(𝐴 < 0, -𝐴, 𝐴))
Theorem	reabsifnpos 44078	Alternate expression for the absolute value of a real number. (Contributed by RP, 11-May-2024.)
⊢ (𝐴 ∈ ℝ → (abs‘𝐴) = if(𝐴 ≤ 0, -𝐴, 𝐴))
Theorem	reabsifpos 44079	Alternate expression for the absolute value of a real number. (Contributed by RP, 11-May-2024.)
⊢ (𝐴 ∈ ℝ → (abs‘𝐴) = if(0 < 𝐴, 𝐴, -𝐴))
Theorem	reabsifnneg 44080	Alternate expression for the absolute value of a real number. (Contributed by RP, 11-May-2024.)
⊢ (𝐴 ∈ ℝ → (abs‘𝐴) = if(0 ≤ 𝐴, 𝐴, -𝐴))
Theorem	reabssgn 44081	Alternate expression for the absolute value of a real number. (Contributed by RP, 22-May-2024.)
⊢ (𝐴 ∈ ℝ → (abs‘𝐴) = ((sgn‘𝐴) · 𝐴))
Theorem	sqrtcvallem2 44082	Equivalent to saying that the square of the imaginary component of the square root of a complex number is a nonnegative real number. Lemma for sqrtcval 44086. See imsqrtval 44089. (Contributed by RP, 11-May-2024.)
⊢ (𝐴 ∈ ℂ → 0 ≤ (((abs‘𝐴) − (ℜ‘𝐴)) / 2))
Theorem	sqrtcvallem3 44083	Equivalent to saying that the absolute value of the imaginary component of the square root of a complex number is a real number. Lemma for sqrtcval 44086, sqrtcval2 44087, resqrtval 44088, and imsqrtval 44089. (Contributed by RP, 11-May-2024.)
⊢ (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) ∈ ℝ)
Theorem	sqrtcvallem4 44084	Equivalent to saying that the square of the real component of the square root of a complex number is a nonnegative real number. Lemma for sqrtcval 44086. See resqrtval 44088. (Contributed by RP, 11-May-2024.)
⊢ (𝐴 ∈ ℂ → 0 ≤ (((abs‘𝐴) + (ℜ‘𝐴)) / 2))
Theorem	sqrtcvallem5 44085	Equivalent to saying that the real component of the square root of a complex number is a real number. Lemma for resqrtval 44088 and imsqrtval 44089. (Contributed by RP, 11-May-2024.)
⊢ (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) ∈ ℝ)
Theorem	sqrtcval 44086	Explicit formula for the complex square root in terms of the square root of nonnegative reals. The right-hand side is decomposed into real and imaginary parts in the format expected by crrei 15145 and crimi 15146. This formula can be found in section 3.7.27 of Handbook of Mathematical Functions, ed. M. Abramowitz and I. A. Stegun (1965, Dover Press). (Contributed by RP, 18-May-2024.)
⊢ (𝐴 ∈ ℂ → (√‘𝐴) = ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))
Theorem	sqrtcval2 44087	Explicit formula for the complex square root in terms of the square root of nonnegative reals. The right side is slightly more compact than sqrtcval 44086. (Contributed by RP, 18-May-2024.)
⊢ (𝐴 ∈ ℂ → (√‘𝐴) = ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (if((ℑ‘𝐴) < 0, -i, i) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))
Theorem	resqrtval 44088	Real part of the complex square root. (Contributed by RP, 18-May-2024.)
⊢ (𝐴 ∈ ℂ → (ℜ‘(√‘𝐴)) = (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)))
Theorem	imsqrtval 44089	Imaginary part of the complex square root. (Contributed by RP, 18-May-2024.)
⊢ (𝐴 ∈ ℂ → (ℑ‘(√‘𝐴)) = (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))
Theorem	resqrtvalex 44090	Example for resqrtval 44088. (Contributed by RP, 21-May-2024.)
⊢ (ℜ‘(√‘(;15 + (i · 8)))) = 4
Theorem	imsqrtvalex 44091	Example for imsqrtval 44089. (Contributed by RP, 21-May-2024.)
⊢ (ℑ‘(√‘(;15 + (i · 8)))) = 1
21.36.5  Additional statements on relations and subclasses
Theorem	al3im 44092	Version of ax-4 1811 for a nested implication. (Contributed by RP, 13-Apr-2020.)
⊢ (∀𝑥(𝜑 → (𝜓 → (𝜒 → 𝜃))) → (∀𝑥𝜑 → (∀𝑥𝜓 → (∀𝑥𝜒 → ∀𝑥𝜃))))
Theorem	intima0 44093*	Two ways of expressing the intersection of images of a class. (Contributed by RP, 13-Apr-2020.)
⊢ ∩ 𝑎 ∈ 𝐴 (𝑎 “ 𝐵) = ∩ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵)}
Theorem	elimaint 44094*	Element of image of intersection. (Contributed by RP, 13-Apr-2020.)
⊢ (𝑦 ∈ (∩ 𝐴 “ 𝐵) ↔ ∃𝑏 ∈ 𝐵 ∀𝑎 ∈ 𝐴 ⟨𝑏, 𝑦⟩ ∈ 𝑎)
Theorem	cnviun 44095*	Converse of indexed union. (Contributed by RP, 20-Jun-2020.)
⊢ ◡∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 ◡𝐵
Theorem	imaiun1 44096*	The image of an indexed union is the indexed union of the images. (Contributed by RP, 29-Jun-2020.)
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 “ 𝐶) = ∪ 𝑥 ∈ 𝐴 (𝐵 “ 𝐶)
Theorem	coiun1 44097*	Composition with an indexed union. Proof analogous to that of coiun 6215. (Contributed by RP, 20-Jun-2020.)
⊢ (∪ 𝑥 ∈ 𝐶 𝐴 ∘ 𝐵) = ∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵)
Theorem	elintima 44098*	Element of intersection of images. (Contributed by RP, 13-Apr-2020.)
⊢ (𝑦 ∈ ∩ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵)} ↔ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ⟨𝑏, 𝑦⟩ ∈ 𝑎)
Theorem	intimass 44099*	The image under the intersection of relations is a subset of the intersection of the images. (Contributed by RP, 13-Apr-2020.)
⊢ (∩ 𝐴 “ 𝐵) ⊆ ∩ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵)}
Theorem	intimass2 44100*	The image under the intersection of relations is a subset of the intersection of the images. (Contributed by RP, 13-Apr-2020.)
⊢ (∩ 𝐴 “ 𝐵) ⊆ ∩ 𝑥 ∈ 𝐴 (𝑥 “ 𝐵)