P. 362 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36101-36200   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	chlb 36101	Embeddings for a direct limit.
class HomLimB
Syntax	chlim 36102	Direct limit structure.
class HomLim
Syntax	cpfl 36103	Polynomial extension field.
class polyFld
Syntax	csf1 36104	Splitting field for a single polynomial (auxiliary).
class splitFld1
Syntax	csf 36105	Splitting field for a finite set of polynomials.
class splitFld
Syntax	cpsl 36106	Splitting field for a sequence of polynomials.
class polySplitLim
Definition	df-cplmet 36107*	A function which completes the given metric space. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ cplMetSp = (𝑤 ∈ V ↦ ⦋((𝑤 ↑s ℕ) ↾s (Cau‘(dist‘𝑤))) / 𝑟⦌⦋(Base‘𝑟) / 𝑣⦌⦋{⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥))} / 𝑒⦌((𝑟 /s 𝑒) sSet {⟨(dist‘ndx), {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘f (dist‘𝑟)𝑞) ⇝ 𝑧)}⟩}))
Definition	df-homlimb 36108*	The input to this function is a sequence (on ℕ) of homomorphisms 𝐹(𝑛):𝑅(𝑛)⟶𝑅(𝑛 + 1). The resulting structure is the direct limit of the direct system so defined. This function returns the pair ⟨𝑆, 𝐺⟩ where 𝑆 is the terminal object and 𝐺 is a sequence of functions such that 𝐺(𝑛):𝑅(𝑛)⟶𝑆 and 𝐺(𝑛) = 𝐹(𝑛) ∘ 𝐺(𝑛 + 1). (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ HomLimB = (𝑓 ∈ V ↦ ⦋∪ 𝑛 ∈ ℕ ({𝑛} × dom (𝑓‘𝑛)) / 𝑣⦌⦋∩ {𝑠 ∣ (𝑠 Er 𝑣 ∧ (𝑥 ∈ 𝑣 ↦ ⟨((1st ‘𝑥) + 1), ((𝑓‘(1st ‘𝑥))‘(2nd ‘𝑥))⟩) ⊆ 𝑠)} / 𝑒⦌⟨(𝑣 / 𝑒), (𝑛 ∈ ℕ ↦ (𝑥 ∈ dom (𝑓‘𝑛) ↦ [⟨𝑛, 𝑥⟩]𝑒))⟩)
Definition	df-homlim 36109*	The input to this function is a sequence (on ℕ) of structures 𝑅(𝑛) and homomorphisms 𝐹(𝑛):𝑅(𝑛)⟶𝑅(𝑛 + 1). The resulting structure is the direct limit of the direct system so defined, and maintains any structures that were present in the original objects. TODO: generalize to directed sets? (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ HomLim = (𝑟 ∈ V, 𝑓 ∈ V ↦ ⦋( HomLimB ‘𝑓) / 𝑒⦌⦋(1st ‘𝑒) / 𝑣⦌⦋(2nd ‘𝑒) / 𝑔⦌({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), ∪ 𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔‘𝑛), 𝑦 ∈ dom (𝑔‘𝑛) ↦ ⟨⟨((𝑔‘𝑛)‘𝑥), ((𝑔‘𝑛)‘𝑦)⟩, ((𝑔‘𝑛)‘(𝑥(+g‘(𝑟‘𝑛))𝑦))⟩)⟩, ⟨(.r‘ndx), ∪ 𝑛 ∈ ℕ ran (𝑥 ∈ dom (𝑔‘𝑛), 𝑦 ∈ dom (𝑔‘𝑛) ↦ ⟨⟨((𝑔‘𝑛)‘𝑥), ((𝑔‘𝑛)‘𝑦)⟩, ((𝑔‘𝑛)‘(𝑥(.r‘(𝑟‘𝑛))𝑦))⟩)⟩} ∪ {⟨(TopOpen‘ndx), {𝑠 ∈ 𝒫 𝑣 ∣ ∀𝑛 ∈ ℕ (◡(𝑔‘𝑛) “ 𝑠) ∈ (TopOpen‘(𝑟‘𝑛))}⟩, ⟨(dist‘ndx), ∪ 𝑛 ∈ ℕ ran (𝑥 ∈ dom ((𝑔‘𝑛)‘𝑛), 𝑦 ∈ dom ((𝑔‘𝑛)‘𝑛) ↦ ⟨⟨((𝑔‘𝑛)‘𝑥), ((𝑔‘𝑛)‘𝑦)⟩, (𝑥(dist‘(𝑟‘𝑛))𝑦)⟩)⟩, ⟨(le‘ndx), ∪ 𝑛 ∈ ℕ (◡(𝑔‘𝑛) ∘ ((le‘(𝑟‘𝑛)) ∘ (𝑔‘𝑛)))⟩}))
Definition	df-plfl 36110*	Define the field extension that augments a field with the root of the given irreducible polynomial, and extends the norm if one exists and the extension is unique. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Thierry Arnoux and Steven Nguyen, 21-Jun-2025.)
⊢ polyFld = (𝑟 ∈ V, 𝑝 ∈ V ↦ ⦋(Poly1‘𝑟) / 𝑠⦌⦋((RSpan‘𝑠)‘{𝑝}) / 𝑖⦌⦋(𝑐 ∈ (Base‘𝑟) ↦ [(𝑐( ·𝑠 ‘𝑠)(1r‘𝑠))](𝑠 ~QG 𝑖)) / 𝑓⦌⟨⦋(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡⦌((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), ⦋(𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑞(rem1p‘𝑟)𝑝) = 𝑞)) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩), 𝑓⟩)
Theorem	rexxfr3d 36111*	Transfer existential quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by SN, 20-Jun-2025.)
⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ ∃𝑦 ∈ 𝐵 𝑥 = 𝑋))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒))
Theorem	rexxfr3dALT 36112*	Longer proof of rexxfr3d 36111 using ax-11 2192 instead of ax-12 2213, without the disjoint variable condition 𝐴𝑥𝑦. (Contributed by SN, 19-Jun-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ ∃𝑦 ∈ 𝐵 𝑥 = 𝑋))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒))
Theorem	rspssbasd 36113	The span of a set of ring elements is a set of ring elements. (Contributed by SN, 19-Jun-2025.)
⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐺 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐾‘𝐺) ⊆ 𝐵)
Theorem	ellcsrspsn 36114*	Membership in a left coset in a quotient of a ring by the span of a singleton (that is, by the ideal generated by an element). This characterization comes from eqglact 19248 and elrspsn 21352. (Contributed by SN, 19-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑈 = (𝑅 /s ∼ )    &   ⊢ 𝐼 = ((RSpan‘𝑅)‘{𝑀})    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝑈))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 (𝑋 = [𝑥] ∼ ∧ 𝑋 = {𝑧 ∣ ∃𝑦 ∈ 𝐵 𝑧 = (𝑥 + (𝑦 · 𝑀))}))
Theorem	ply1divalg3 36115*	Uniqueness of polynomial remainder: convert the subtraction in ply1divalg2 26277 to addition. (Contributed by SN, 20-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ + = (+g‘𝑃)    &   ⊢ ∙ = (.r‘𝑃)    &   ⊢ 𝐶 = (Unic1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐶)    ⇒   ⊢ (𝜑 → ∃!𝑞 ∈ 𝐵 (𝐷‘(𝐹 + (𝑞 ∙ 𝐺))) < (𝐷‘𝐺))
Theorem	r1peuqusdeg1 36116*	Uniqueness of polynomial remainder in terms of a quotient structure in the sense of the right hand side of r1pid2 26300. (Contributed by SN, 21-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐼 = ((RSpan‘𝑃)‘{𝐹})    &   ⊢ 𝑇 = (𝑃 /s (𝑃 ~QG 𝐼))    &   ⊢ 𝑄 = (Base‘𝑇)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑁)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑄)    ⇒   ⊢ (𝜑 → ∃!𝑞 ∈ 𝑍 (𝐷‘𝑞) < (𝐷‘𝐹))
Definition	df-sfl1 36117*	Temporary construction for the splitting field of a polynomial. The inputs are a field 𝑟 and a polynomial 𝑝 that we want to split, along with a tuple 𝑗 in the same format as the output. The output is a tuple ⟨𝑆, 𝐹⟩ where 𝑆 is the splitting field and 𝐹 is an injective homomorphism from the original field 𝑟. The function works by repeatedly finding the smallest monic irreducible factor, and extending the field by that factor using the polyFld construction. We keep track of a total order in each of the splitting fields so that we can pick an element definably without needing global choice. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ splitFld1 = (𝑟 ∈ V, 𝑗 ∈ V ↦ (𝑝 ∈ (Poly1‘𝑟) ↦ (rec((𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋(Poly1‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)), 𝑗)‘(card‘(1...(𝑟deg1𝑝))))))
Definition	df-sfl 36118*	Define the splitting field of a finite collection of polynomials, given a total ordered base field. The output is a tuple ⟨𝑆, 𝐹⟩ where 𝑆 is the totally ordered splitting field and 𝐹 is an injective homomorphism from the original field 𝑟. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ splitFld = (𝑟 ∈ V, 𝑝 ∈ V ↦ (℩𝑥∃𝑓(𝑓 Isom < , (lt‘𝑟)((1...(♯‘𝑝)), 𝑝) ∧ 𝑥 = (seq0((𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔)), (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}))‘(♯‘𝑝)))))
Definition	df-psl 36119*	Define the direct limit of an increasing sequence of fields produced by pasting together the splitting fields for each sequence of polynomials. That is, given a ring 𝑟, a strict order on 𝑟, and a sequence 𝑝:ℕ⟶(𝒫 𝑟 ∩ Fin) of finite sets of polynomials to split, we construct the direct limit system of field extensions by splitting one set at a time and passing the resulting construction to HomLim. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ polySplitLim = (𝑟 ∈ V, 𝑝 ∈ ((𝒫 (Base‘𝑟) ∩ Fin) ↑m ℕ) ↦ ⦋(1st ∘ seq0((𝑔 ∈ V, 𝑞 ∈ V ↦ ⦋(1st ‘𝑔) / 𝑒⦌⦋(1st ‘𝑒) / 𝑠⦌⦋(𝑠 splitFld ran (𝑥 ∈ 𝑞 ↦ (𝑥 ∘ (2nd ‘𝑔)))) / 𝑓⦌⟨𝑓, ((2nd ‘𝑔) ∘ (2nd ‘𝑓))⟩), (𝑝 ∪ {⟨0, ⟨⟨𝑟, ∅⟩, ( I ↾ (Base‘𝑟))⟩⟩}))) / 𝑓⦌((1st ∘ (𝑓 shift 1)) HomLim (2nd ∘ 𝑓)))
21.6.17  p-adic number fields
Syntax	czr 36120	Integral elements of a ring.
class ZRing
Syntax	cgf 36121	Galois finite field.
class GF
Syntax	cgfo 36122	Galois limit field.
class GF∞
Syntax	ceqp 36123	Equivalence relation for df-qp 36134.
class ~Qp
Syntax	crqp 36124	Equivalence relation representatives for df-qp 36134.
class /Qp
Syntax	cqp 36125	The set of 𝑝-adic rational numbers.
class Qp
Syntax	czp 36126	The set of 𝑝-adic integers. (Not to be confused with czn 21633.)
class Zp
Syntax	cqpa 36127	Algebraic completion of the 𝑝-adic rational numbers.
class _Qp
Syntax	ccp 36128	Metric completion of _Qp.
class Cp
Definition	df-zrng 36129	Define the subring of integral elements in a ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ ZRing = (𝑟 ∈ V ↦ (𝑟 IntgRing ran (ℤRHom‘𝑟)))
Definition	df-gf 36130*	Define the Galois finite field of order 𝑝↑𝑛. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ GF = (𝑝 ∈ ℙ, 𝑛 ∈ ℕ ↦ ⦋(ℤ/nℤ‘𝑝) / 𝑟⦌(1st ‘(𝑟 splitFld {⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)})))
Definition	df-gfoo 36131*	Define the Galois field of order 𝑝↑+∞, as a direct limit of the Galois finite fields. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ GF∞ = (𝑝 ∈ ℙ ↦ ⦋(ℤ/nℤ‘𝑝) / 𝑟⦌(𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)})))
Definition	df-eqp 36132*	Define an equivalence relation on ℤ-indexed sequences of integers such that two sequences are equivalent iff the difference is equivalent to zero, and a sequence is equivalent to zero iff the sum Σ𝑘 ≤ 𝑛𝑓(𝑘)(𝑝↑𝑘) is a multiple of 𝑝↑(𝑛 + 1) for every 𝑛. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ ~Qp = (𝑝 ∈ ℙ ↦ {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ (ℤ ↑m ℤ) ∧ ∀𝑛 ∈ ℤ Σ𝑘 ∈ (ℤ≥‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ)})
Definition	df-rqp 36133*	There is a unique element of (ℤ ↑m (0...(𝑝 − 1))) ~Qp -equivalent to any element of (ℤ ↑m ℤ), if the sequences are zero for sufficiently large negative values; this function selects that element. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ /Qp = (𝑝 ∈ ℙ ↦ (~Qp ∩ ⦋{𝑓 ∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ≥(◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦⦌(𝑦 × (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1)))))))
Definition	df-qp 36134*	Define the 𝑝-adic completion of the rational numbers, as a normed field structure with a total order (that is not compatible with the operations). (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by AV, 10-Oct-2021.)
⊢ Qp = (𝑝 ∈ ℙ ↦ ⦋{ℎ ∈ (ℤ ↑m (0...(𝑝 − 1))) ∣ ∃𝑥 ∈ ran ℤ≥(◡ℎ “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑏⦌(({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))⟩} ∪ {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩}) toNrmGrp (𝑓 ∈ 𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-inf((◡𝑓 “ (ℤ ∖ {0})), ℝ, < ))))))
Definition	df-zp 36135	Define the 𝑝-adic integers, as a subset of the 𝑝-adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ Zp = (ZRing ∘ Qp)
Definition	df-qpa 36136*	Define the completion of the 𝑝-adic rationals. Here we simply define it as the splitting field of a dense sequence of polynomials (using as the 𝑛-th set the collection of polynomials with degree less than 𝑛 and with coefficients < (𝑝↑𝑛)). Krasner's lemma will then show that all monic polynomials have splitting fields isomorphic to a sufficiently close Eisenstein polynomial from the list, and unramified extensions are generated by the polynomial 𝑥↑(𝑝↑𝑛) − 𝑥, which is in the list. Thus, every finite extension of Qp is a subfield of this field extension, so it is algebraically closed. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ _Qp = (𝑝 ∈ ℙ ↦ ⦋(Qp‘𝑝) / 𝑟⦌(𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {𝑓 ∈ (Poly1‘𝑟) ∣ ((𝑟deg1𝑓) ≤ 𝑛 ∧ ∀𝑑 ∈ ran (coe1‘𝑓)(◡𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛))})))
Definition	df-cp 36137	Define the metric completion of the algebraic completion of the 𝑝 -adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ Cp = ( cplMetSp ∘ _Qp)
21.7  Mathbox for Filip Cernatescu I hope someone will enjoy solving (proving) the simple equations, inequalities, and calculations from this mathbox. I have proved these problems (theorems) using the Milpgame proof assistant. (It can be downloaded from https://us.metamath.org/other/milpgame/milpgame.html.)
Theorem	problem1 36138	Practice problem 1. Clues: 5p4e9 12399 3p2e5 12392 eqtri 2786 oveq1i 7422. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.)
⊢ ((3 + 2) + 4) = 9
Theorem	problem2 36139	Practice problem 2. Clues: oveq12i 7424 adddiri 11223 add4i 11436 mulcli 11217 recni 11224 2re 12316 3eqtri 2790 10re 12735 5re 12329 1re 11209 4re 12326 eqcomi 2772 5p4e9 12399 oveq1i 7422 df-3 12305. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Revised by AV, 9-Sep-2021.) (Proof modification is discouraged.)
⊢ (((2 · ;10) + 5) + ((1 · ;10) + 4)) = ((3 · ;10) + 9)
Theorem	problem3 36140	Practice problem 3. Clues: eqcomi 2772 eqtri 2786 subaddrii 11548 recni 11224 4re 12326 3re 12322 1re 11209 df-4 12306 addcomi 11402. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ ℂ    &   ⊢ (𝐴 + 3) = 4    ⇒   ⊢ 𝐴 = 1
Theorem	problem4 36141	Practice problem 4. Clues: pm3.2i 475 eqcomi 2772 eqtri 2786 subaddrii 11548 recni 11224 7re 12335 6re 12332 ax-1cn 11159 df-7 12309 ax-mp 5 oveq1i 7422 3cn 12323 2cn 12317 df-3 12305 mullidi 11215 subdiri 11665 mp3an 1490 mulcli 11217 subadd23 11470 oveq2i 7423 oveq12i 7424 3t2e6 12407 mulcomi 11218 subcli 11535 biimpri 231 subadd2i 11547. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ (𝐴 + 𝐵) = 3    &   ⊢ ((3 · 𝐴) + (2 · 𝐵)) = 7    ⇒   ⊢ (𝐴 = 1 ∧ 𝐵 = 2)
Theorem	problem5 36142	Practice problem 5. Clues: 3brtr3i 5141 mpbi 233 breqtri 5137 ltaddsubi 11776 remulcli 11226 2re 12316 3re 12322 9re 12341 eqcomi 2772 mvlladdi 11477 3cn 6cn 12333 eqtr3i 2788 6p3e9 12401 addcomi 11402 ltdiv1ii 12145 6re 12332 nngt0i 12276 2nn 12315 divcan3i 11962 recni 11224 2cn 12317 2ne0 12348 mpbir 234 eqtri 2786 mulcomi 11218 3t2e6 12407 divmuli 11970. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ ℝ    &   ⊢ ((2 · 𝐴) + 3) < 9    ⇒   ⊢ 𝐴 < 3
Theorem	quad3 36143	Variant of quadratic equation with discriminant expanded. (Contributed by Filip Cernatescu, 19-Oct-2019.)
⊢ 𝑋 ∈ ℂ    &   ⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 ≠ 0    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0    ⇒   ⊢ (𝑋 = ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)))
21.8  Mathbox for Paul Chapman
21.8.1  Real and complex numbers (cont.)
Theorem	climuzcnv 36144*	Utility lemma to convert between 𝑚 ≤ 𝑘 and 𝑘 ∈ (ℤ≥‘𝑚) in limit theorems. (Contributed by Paul Chapman, 10-Nov-2012.)
⊢ (𝑚 ∈ ℕ → ((𝑘 ∈ (ℤ≥‘𝑚) → 𝜑) ↔ (𝑘 ∈ ℕ → (𝑚 ≤ 𝑘 → 𝜑))))
Theorem	sinccvglem 36145*	((sin‘𝑥) / 𝑥) ⇝ 1 as (real) 𝑥 ⇝ 0. (Contributed by Paul Chapman, 10-Nov-2012.) (Revised by Mario Carneiro, 21-May-2014.)
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ ∖ {0}))    &   ⊢ (𝜑 → 𝐹 ⇝ 0)    &   ⊢ 𝐺 = (𝑥 ∈ (ℝ ∖ {0}) ↦ ((sin‘𝑥) / 𝑥))    &   ⊢ 𝐻 = (𝑥 ∈ ℂ ↦ (1 − ((𝑥↑2) / 3)))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (abs‘(𝐹‘𝑘)) < 1)    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) ⇝ 1)
Theorem	sinccvg 36146*	((sin‘𝑥) / 𝑥) ⇝ 1 as (real) 𝑥 ⇝ 0. (Contributed by Paul Chapman, 10-Nov-2012.) (Proof shortened by Mario Carneiro, 21-May-2014.)
⊢ ((𝐹:ℕ⟶(ℝ ∖ {0}) ∧ 𝐹 ⇝ 0) → ((𝑥 ∈ (ℝ ∖ {0}) ↦ ((sin‘𝑥) / 𝑥)) ∘ 𝐹) ⇝ 1)
Theorem	circum 36147*	The circumference of a circle of radius 𝑅, defined as the limit as 𝑛 ⇝ +∞ of the perimeter of an inscribed n-sided isogons, is ((2 · π) · 𝑅). (Contributed by Paul Chapman, 10-Nov-2012.) (Proof shortened by Mario Carneiro, 21-May-2014.)
⊢ 𝐴 = ((2 · π) / 𝑛)    &   ⊢ 𝑃 = (𝑛 ∈ ℕ ↦ ((2 · 𝑛) · (𝑅 · (sin‘(𝐴 / 2)))))    &   ⊢ 𝑅 ∈ ℝ    ⇒   ⊢ 𝑃 ⇝ ((2 · π) · 𝑅)
21.8.2  Miscellaneous theorems
Theorem	elfzm12 36148	Membership in a curtailed finite sequence of integers. (Contributed by Paul Chapman, 17-Nov-2012.)
⊢ (𝑁 ∈ ℕ → (𝑀 ∈ (1...(𝑁 − 1)) → 𝑀 ∈ (1...𝑁)))
Theorem	nn0seqcvg 36149*	A strictly-decreasing nonnegative integer sequence with initial term 𝑁 reaches zero by the 𝑁 th term. Inference version. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ 𝐹:ℕ0⟶ℕ0    &   ⊢ 𝑁 = (𝐹‘0)    &   ⊢ (𝑘 ∈ ℕ0 → ((𝐹‘(𝑘 + 1)) ≠ 0 → (𝐹‘(𝑘 + 1)) < (𝐹‘𝑘)))    ⇒   ⊢ (𝐹‘𝑁) = 0
Theorem	lediv2aALT 36150	Division of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) → (𝐴 ≤ 𝐵 → (𝐶 / 𝐵) ≤ (𝐶 / 𝐴)))
Theorem	abs2sqlei 36151	The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((abs‘𝐴) ≤ (abs‘𝐵) ↔ ((abs‘𝐴)↑2) ≤ ((abs‘𝐵)↑2))
Theorem	abs2sqlti 36152	The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((abs‘𝐴) < (abs‘𝐵) ↔ ((abs‘𝐴)↑2) < ((abs‘𝐵)↑2))
Theorem	abs2sqle 36153	The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘𝐴) ≤ (abs‘𝐵) ↔ ((abs‘𝐴)↑2) ≤ ((abs‘𝐵)↑2)))
Theorem	abs2sqlt 36154	The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘𝐴) < (abs‘𝐵) ↔ ((abs‘𝐴)↑2) < ((abs‘𝐵)↑2)))
Theorem	abs2difi 36155	Difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((abs‘𝐴) − (abs‘𝐵)) ≤ (abs‘(𝐴 − 𝐵))
Theorem	abs2difabsi 36156	Absolute value of difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (abs‘((abs‘𝐴) − (abs‘𝐵))) ≤ (abs‘(𝐴 − 𝐵))
21.9  Mathbox for Hongxiu Chen
Theorem	2thALT 36157	Alternate proof of 2th 267. (Contributed by Hongxiu Chen, 29-Jun-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ (𝜑 ↔ 𝜓)
Theorem	orbi2iALT 36158	Alternate proof of orbi2i 925. (Contributed by Hongxiu Chen, 29-Jun-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))
Theorem	pm3.48ALT 36159	Alternate proof of pm3.48 978. (Contributed by Hongxiu Chen, 29-Jun-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜃)) → ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃)))
Theorem	3jcadALT 36160	Alternate proof of 3jcad 1147. (Contributed by Hongxiu Chen, 29-Jun-2025.) (Proof modification is discouraged.) Use 3jcad instead. (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ (𝜑 → (𝜓 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃 ∧ 𝜏)))
21.10  Mathbox for Adrian Ducourtial
21.10.1  Propositional calculus
Theorem	currybi 36161	Biconditional version of Curry's paradox. If some proposition 𝜑 amounts to the self-referential statement "This very statement is equivalent to 𝜓", then 𝜓 is true. See bj-currypara 37133 in BJ's mathbox for the classical version. (Contributed by Adrian Ducourtial, 18-Mar-2025.)
⊢ ((𝜑 ↔ (𝜑 ↔ 𝜓)) → 𝜓)
Theorem	antnest 36162	Suppose 𝜑, 𝜓 are distinct atomic propositional formulas, and let Γ be the smallest class of formulas for which ⊤ ∈ Γ and (𝜒 → 𝜑), (𝜒 → 𝜓) ∈ Γ for 𝜒 ∈ Γ. The present theorem is then an element of Γ, and the implications occurring in the theorem are in one-to-one correspondence with the formulas in Γ up to logical equivalence. In particular, the theorem itself is equivalent to ⊤ ∈ Γ. (Contributed by Adrian Ducourtial, 2-Oct-2025.)
⊢ ((((((⊤ → 𝜑) → 𝜓) → 𝜓) → 𝜑) → 𝜓) → 𝜓)
Theorem	antnestlaw3lem 36163	Lemma for antnestlaw3 36166. (Contributed by Adrian Ducourtial, 5-Dec-2025.)
⊢ (¬ (((𝜑 → 𝜓) → 𝜒) → 𝜒) → ¬ (((𝜑 → 𝜒) → 𝜓) → 𝜓))
Theorem	antnestlaw1 36164	A law of nested antecedents. The converse direction is a subschema of pm2.27 43. (Contributed by Adrian Ducourtial, 5-Dec-2025.)
⊢ ((((𝜑 → 𝜓) → 𝜓) → 𝜓) ↔ (𝜑 → 𝜓))
Theorem	antnestlaw2 36165	A law of nested antecedents. (Contributed by Adrian Ducourtial, 5-Dec-2025.)
⊢ ((((𝜑 → 𝜓) → 𝜓) → 𝜒) ↔ (((𝜑 → 𝜒) → 𝜓) → 𝜒))
Theorem	antnestlaw3 36166	A law of nested antecedents. Compare with looinv 206. (Contributed by Adrian Ducourtial, 5-Dec-2025.)
⊢ ((((𝜑 → 𝜓) → 𝜒) → 𝜒) ↔ (((𝜑 → 𝜒) → 𝜓) → 𝜓))
Theorem	antnestALT 36167	Alternative proof of antnest 36162 from the valid schema ((((⊤ → 𝜑) → 𝜑) → 𝜓) → 𝜓) using laws of nested antecedents. Our proof uses only the laws antnestlaw1 36164 and antnestlaw3 36166. (Contributed by Adrian Ducourtial, 5-Dec-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((((((⊤ → 𝜑) → 𝜓) → 𝜓) → 𝜑) → 𝜓) → 𝜓)
21.10.2  Clone theory
Syntax	ccloneop 36168	Syntax for the function of the class of operations on a set.
class CloneOp
Definition	df-cloneop 36169*	Define the function that sends a set to the class of clone-theoretic operations on the set. For convenience, we take an operation on 𝑎 to be a function on finite sequences of elements of 𝑎 (rather than tuples) with values in 𝑎. Following line 6 of [Szendrei] p. 11, the arity 𝑛 of an operation (here, the length of the sequences at which the operation is defined) is always finite and nonzero, whence 𝑛 is taken to be a nonzero finite ordinal. (Contributed by Adrian Ducourtial, 3-Apr-2025.)
⊢ CloneOp = (𝑎 ∈ V ↦ {𝑥 ∣ ∃𝑛 ∈ (ω ∖ 1o)𝑥 ∈ (𝑎 ↑m (𝑎 ↑m 𝑛))})
Syntax	cprj 36170	Syntax for the function of projections on sets.
class prj
Definition	df-prj 36171*	Define the function that, for a set 𝑎, arity 𝑛, and index 𝑖, returns the 𝑖-th 𝑛-ary projection on 𝑎. This is the 𝑛-ary operation on 𝑎 that, for any sequence of 𝑛 elements of 𝑎, returns the element having index 𝑖. (Contributed by Adrian Ducourtial, 3-Apr-2025.)
⊢ prj = (𝑎 ∈ V ↦ (𝑛 ∈ (ω ∖ 1o), 𝑖 ∈ 𝑛 ↦ (𝑥 ∈ (𝑎 ↑m 𝑛) ↦ (𝑥‘𝑖))))
Syntax	csuppos 36172	Syntax for the function of superpositions.
class suppos
Definition	df-suppos 36173*	Define the function that, when given an 𝑛-ary operation 𝑓 and 𝑛 many 𝑚-ary operations (𝑔‘∅), ..., (𝑔‘∪ 𝑛), returns the superposition of 𝑓 with the (𝑔‘𝑖), itself another 𝑚-ary operation on 𝑎. Given 𝑥 (a sequence of 𝑚 arguments in 𝑎), the superposition effectively applies each of the (𝑔‘𝑖) to 𝑥, then applies 𝑓 to the resulting sequence of 𝑛 function values. This can be seen as a generalized version of function composition; see paragraph 3 of [Szendrei] p. 11. (Contributed by Adrian Ducourtial, 3-Apr-2025.)
⊢ suppos = (𝑎 ∈ V ↦ (𝑛 ∈ (ω ∖ 1o), 𝑚 ∈ (ω ∖ 1o) ↦ (𝑓 ∈ (𝑎 ↑m (𝑎 ↑m 𝑛)), 𝑔 ∈ ((𝑎 ↑m (𝑎 ↑m 𝑚)) ↑m 𝑛) ↦ (𝑥 ∈ (𝑎 ↑m 𝑚) ↦ (𝑓‘(𝑖 ∈ 𝑛 ↦ ((𝑔‘𝑖)‘𝑥)))))))
21.11  Mathbox for Scott Fenton
21.11.1  ZFC Axioms in primitive form
Theorem	axextprim 36174	ax-ext 2735 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
⊢ ¬ ∀𝑥 ¬ ((𝑥 ∈ 𝑦 → 𝑥 ∈ 𝑧) → ((𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦) → 𝑦 = 𝑧))
Theorem	axrepprim 36175	ax-rep 5239 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
⊢ ¬ ∀𝑥 ¬ (¬ ∀𝑦 ¬ ∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧 ¬ ((∀𝑦 𝑧 ∈ 𝑥 → ¬ ∀𝑥(∀𝑧 𝑥 ∈ 𝑦 → ¬ ∀𝑦𝜑)) → ¬ (¬ ∀𝑥(∀𝑧 𝑥 ∈ 𝑦 → ¬ ∀𝑦𝜑) → ∀𝑦 𝑧 ∈ 𝑥)))
Theorem	axunprim 36176	ax-un 7734 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
⊢ ¬ ∀𝑥 ¬ ∀𝑦(¬ ∀𝑥(𝑦 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)
Theorem	axpowprim 36177	ax-pow 5338 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
⊢ (∀𝑥 ¬ ∀𝑦(∀𝑥(¬ ∀𝑧 ¬ 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) → 𝑥 = 𝑦)
Theorem	axregprim 36178	ax-reg 9555 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
⊢ (𝑥 ∈ 𝑦 → ¬ ∀𝑥(𝑥 ∈ 𝑦 → ¬ ∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦)))
Theorem	axinfprim 36179	ax-inf 9608 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 13-Oct-2010.)
⊢ ¬ ∀𝑥 ¬ (𝑦 ∈ 𝑧 → ¬ (𝑦 ∈ 𝑥 → ¬ ∀𝑦(𝑦 ∈ 𝑥 → ¬ ∀𝑧(𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑥))))
Theorem	axacprim 36180	ax-ac 10444 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 26-Oct-2010.)
⊢ ¬ ∀𝑥 ¬ ∀𝑦∀𝑧(∀𝑥 ¬ (𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑤) → ¬ ∀𝑤 ¬ ∀𝑦 ¬ ((¬ ∀𝑤(𝑦 ∈ 𝑧 → (𝑧 ∈ 𝑤 → (𝑦 ∈ 𝑤 → ¬ 𝑤 ∈ 𝑥))) → 𝑦 = 𝑤) → ¬ (𝑦 = 𝑤 → ¬ ∀𝑤(𝑦 ∈ 𝑧 → (𝑧 ∈ 𝑤 → (𝑦 ∈ 𝑤 → ¬ 𝑤 ∈ 𝑥))))))
21.11.2  Untangled classes
Theorem	untelirr 36181*	We call a class "untanged" if all its members are not members of themselves. The term originates from Isbell (see citation in dfon2 36263). Using this concept, we can avoid a lot of the uses of the Axiom of Regularity. Here, we prove a series of properties of untanged classes. First, we prove that an untangled class is not a member of itself. (Contributed by Scott Fenton, 28-Feb-2011.)
⊢ (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 → ¬ 𝐴 ∈ 𝐴)
Theorem	untuni 36182*	The union of a class is untangled iff all its members are untangled. (Contributed by Scott Fenton, 28-Feb-2011.)
⊢ (∀𝑥 ∈ ∪ 𝐴 ¬ 𝑥 ∈ 𝑥 ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝑦 ¬ 𝑥 ∈ 𝑥)
Theorem	untsucf 36183*	If a class is untangled, then so is its successor. (Contributed by Scott Fenton, 28-Feb-2011.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ Ⅎ𝑦𝐴    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 → ∀𝑦 ∈ suc 𝐴 ¬ 𝑦 ∈ 𝑦)
Theorem	unt0 36184	The empty set is untangled. (Contributed by Scott Fenton, 10-Mar-2011.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ∀𝑥 ∈ ∅ ¬ 𝑥 ∈ 𝑥
Theorem	untint 36185*	If there is an untangled element of a class, then the intersection of the class is untangled. (Contributed by Scott Fenton, 1-Mar-2011.)
⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑦 → ∀𝑦 ∈ ∩ 𝐴 ¬ 𝑦 ∈ 𝑦)
Theorem	efrunt 36186*	If 𝐴 is well-founded by E, then it is untangled. (Contributed by Scott Fenton, 1-Mar-2011.)
⊢ ( E Fr 𝐴 → ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥)
Theorem	untangtr 36187*	A transitive class is untangled iff its elements are. (Contributed by Scott Fenton, 7-Mar-2011.)
⊢ (Tr 𝐴 → (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑦))
21.11.3  Extra propositional calculus theorems
Theorem	3jaodd 36188	Double deduction form of 3jaoi 1454. (Contributed by Scott Fenton, 20-Apr-2011.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))    &   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜂)))    &   ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜃 ∨ 𝜏) → 𝜂)))
Theorem	3orit 36189	Closed form of 3ori 1451. (Contributed by Scott Fenton, 20-Apr-2011.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜒))
Theorem	biimpexp 36190	A biconditional in the antecedent is the same as two implications. (Contributed by Scott Fenton, 12-Dec-2010.)
⊢ (((𝜑 ↔ 𝜓) → 𝜒) ↔ ((𝜑 → 𝜓) → ((𝜓 → 𝜑) → 𝜒)))
21.11.4  Misc. Useful Theorems
Theorem	nepss 36191	Two classes are unequal iff their intersection is a proper subset of one of them. (Contributed by Scott Fenton, 23-Feb-2011.)
⊢ (𝐴 ≠ 𝐵 ↔ ((𝐴 ∩ 𝐵) ⊊ 𝐴 ∨ (𝐴 ∩ 𝐵) ⊊ 𝐵))
Theorem	3ccased 36192	Triple disjunction form of ccased 1054. (Contributed by Scott Fenton, 27-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (𝜑 → ((𝜒 ∧ 𝜂) → 𝜓))    &   ⊢ (𝜑 → ((𝜒 ∧ 𝜁) → 𝜓))    &   ⊢ (𝜑 → ((𝜒 ∧ 𝜎) → 𝜓))    &   ⊢ (𝜑 → ((𝜃 ∧ 𝜂) → 𝜓))    &   ⊢ (𝜑 → ((𝜃 ∧ 𝜁) → 𝜓))    &   ⊢ (𝜑 → ((𝜃 ∧ 𝜎) → 𝜓))    &   ⊢ (𝜑 → ((𝜏 ∧ 𝜂) → 𝜓))    &   ⊢ (𝜑 → ((𝜏 ∧ 𝜁) → 𝜓))    &   ⊢ (𝜑 → ((𝜏 ∧ 𝜎) → 𝜓))    ⇒   ⊢ (𝜑 → (((𝜒 ∨ 𝜃 ∨ 𝜏) ∧ (𝜂 ∨ 𝜁 ∨ 𝜎)) → 𝜓))
Theorem	dfso3 36193*	Expansion of the definition of a strict order. (Contributed by Scott Fenton, 6-Jun-2016.)
⊢ (𝑅 Or 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
Theorem	brtpid1 36194	A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.)
⊢ 𝐴{⟨𝐴, 𝐵⟩, 𝐶, 𝐷}𝐵
Theorem	brtpid2 36195	A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.)
⊢ 𝐴{𝐶, ⟨𝐴, 𝐵⟩, 𝐷}𝐵
Theorem	brtpid3 36196	A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.)
⊢ 𝐴{𝐶, 𝐷, ⟨𝐴, 𝐵⟩}𝐵
Theorem	iota5f 36197*	A method for computing iota. (Contributed by Scott Fenton, 13-Dec-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (𝜓 ↔ 𝑥 = 𝐴))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (℩𝑥𝜓) = 𝐴)
Theorem	jath 36198	Closed form of ja 188. Proved using the completeness script. (Proof modification is discouraged.) (Contributed by Scott Fenton, 13-Dec-2021.)
⊢ ((¬ 𝜑 → 𝜒) → ((𝜓 → 𝜒) → ((𝜑 → 𝜓) → 𝜒)))
Theorem	xpab 36199*	Cartesian product of two class abstractions. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ ({𝑥 ∣ 𝜑} × {𝑦 ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ 𝜓)}
Theorem	nnuni 36200	The union of a finite ordinal is a finite ordinal. (Contributed by Scott Fenton, 17-Oct-2024.)
⊢ (𝐴 ∈ ω → ∪ 𝐴 ∈ ω)