P. 337 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33601-33700   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	chlim 33601	Direct limit structure.
class HomLim
Syntax	cpfl 33602	Polynomial extension field.
class polyFld
Syntax	csf1 33603	Splitting field for a single polynomial (auxiliary).
class splitFld1
Syntax	csf 33604	Splitting field for a finite set of polynomials.
class splitFld
Syntax	cpsl 33605	Splitting field for a sequence of polynomials.
class polySplitLim
Definition	df-irng 33606*	Define the subring of elements of 𝑟 integral over 𝑠 in a ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ IntgRing = (𝑟 ∈ V, 𝑠 ∈ V ↦ ∪ 𝑓 ∈ (Monic1p‘(𝑟 ↾s 𝑠))(◡𝑓 “ {(0g‘𝑟)}))
Definition	df-cplmet 33607*	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 33608*	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 33609*	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 33610*	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.)
⊢ polyFld = (𝑟 ∈ V, 𝑝 ∈ V ↦ ⦋(Poly1‘𝑟) / 𝑠⦌⦋((RSpan‘𝑠)‘{𝑝}) / 𝑖⦌⦋(𝑧 ∈ (Base‘𝑟) ↦ [(𝑧( ·𝑠 ‘𝑠)(1r‘𝑠))](𝑠 ~QG 𝑖)) / 𝑓⦌⟨⦋(𝑠 /s (𝑠 ~QG 𝑖)) / 𝑡⦌((𝑡 toNrmGrp (℩𝑛 ∈ (AbsVal‘𝑡)(𝑛 ∘ 𝑓) = (norm‘𝑟))) sSet ⟨(le‘ndx), ⦋(𝑧 ∈ (Base‘𝑡) ↦ (℩𝑞 ∈ 𝑧 (𝑟 deg1 𝑞) < (𝑟 deg1 𝑝))) / 𝑔⦌(◡𝑔 ∘ ((le‘𝑠) ∘ 𝑔))⟩), 𝑓⟩)
Definition	df-sfl1 33611*	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 ↦ ⦋( mPoly ‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠 deg1 𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)), 𝑗)‘(card‘(1...(𝑟 deg1 𝑝))))))
Definition	df-sfl 33612*	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 33613*	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 ∘ 𝑓)))
20.6.17  p-adic number fields
Syntax	czr 33614	Integral elements of a ring.
class ZRing
Syntax	cgf 33615	Galois finite field.
class GF
Syntax	cgfo 33616	Galois limit field.
class GF∞
Syntax	ceqp 33617	Equivalence relation for df-qp 33628.
class ~Qp
Syntax	crqp 33618	Equivalence relation representatives for df-qp 33628.
class /Qp
Syntax	cqp 33619	The set of 𝑝-adic rational numbers.
class Qp
Syntax	czp 33620	The set of 𝑝-adic integers. (Not to be confused with czn 20713.)
class Zp
Syntax	cqpa 33621	Algebraic completion of the 𝑝-adic rational numbers.
class _Qp
Syntax	ccp 33622	Metric completion of _Qp.
class Cp
Definition	df-zrng 33623	Define the subring of integral elements in a ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ ZRing = (𝑟 ∈ V ↦ (𝑟 IntgRing ran (ℤRHom‘𝑟)))
Definition	df-gf 33624*	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 33625*	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 33626*	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 33627*	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 33628*	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 33629	Define the 𝑝-adic integers, as a subset of the 𝑝-adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ Zp = (ZRing ∘ Qp)
Definition	df-qpa 33630*	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 33631	Define the metric completion of the algebraic completion of the 𝑝 -adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ Cp = ( cplMetSp ∘ _Qp)
20.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 33632	Practice problem 1. Clues: 5p4e9 12140 3p2e5 12133 eqtri 2767 oveq1i 7294. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.)
⊢ ((3 + 2) + 4) = 9
Theorem	problem2 33633	Practice problem 2. Clues: oveq12i 7296 adddiri 10997 add4i 11208 mulcli 10991 recni 10998 2re 12056 3eqtri 2771 10re 12465 5re 12069 1re 10984 4re 12066 eqcomi 2748 5p4e9 12140 oveq1i 7294 df-3 12046. (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 33634	Practice problem 3. Clues: eqcomi 2748 eqtri 2767 subaddrii 11319 recni 10998 4re 12066 3re 12062 1re 10984 df-4 12047 addcomi 11175. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ ℂ    &   ⊢ (𝐴 + 3) = 4    ⇒   ⊢ 𝐴 = 1
Theorem	problem4 33635	Practice problem 4. Clues: pm3.2i 471 eqcomi 2748 eqtri 2767 subaddrii 11319 recni 10998 7re 12075 6re 12072 ax-1cn 10938 df-7 12050 ax-mp 5 oveq1i 7294 3cn 12063 2cn 12057 df-3 12046 mulid2i 10989 subdiri 11434 mp3an 1460 mulcli 10991 subadd23 11242 oveq2i 7295 oveq12i 7296 3t2e6 12148 mulcomi 10992 subcli 11306 biimpri 227 subadd2i 11318. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ (𝐴 + 𝐵) = 3    &   ⊢ ((3 · 𝐴) + (2 · 𝐵)) = 7    ⇒   ⊢ (𝐴 = 1 ∧ 𝐵 = 2)
Theorem	problem5 33636	Practice problem 5. Clues: 3brtr3i 5104 mpbi 229 breqtri 5100 ltaddsubi 11545 remulcli 11000 2re 12056 3re 12062 9re 12081 eqcomi 2748 mvlladdi 11248 3cn 6cn 12073 eqtr3i 2769 6p3e9 12142 addcomi 11175 ltdiv1ii 11913 6re 12072 nngt0i 12021 2nn 12055 divcan3i 11730 recni 10998 2cn 12057 2ne0 12086 mpbir 230 eqtri 2767 mulcomi 10992 3t2e6 12148 divmuli 11738. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ ℝ    &   ⊢ ((2 · 𝐴) + 3) < 9    ⇒   ⊢ 𝐴 < 3
Theorem	quad3 33637	Variant of quadratic equation with discriminant expanded. (Contributed by Filip Cernatescu, 19-Oct-2019.)
⊢ 𝑋 ∈ ℂ    &   ⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 ≠ 0    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0    ⇒   ⊢ (𝑋 = ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)))
20.8  Mathbox for Paul Chapman
20.8.1  Real and complex numbers (cont.)
Theorem	climuzcnv 33638*	Utility lemma to convert between 𝑚 ≤ 𝑘 and 𝑘 ∈ (ℤ≥‘𝑚) in limit theorems. (Contributed by Paul Chapman, 10-Nov-2012.)
⊢ (𝑚 ∈ ℕ → ((𝑘 ∈ (ℤ≥‘𝑚) → 𝜑) ↔ (𝑘 ∈ ℕ → (𝑚 ≤ 𝑘 → 𝜑))))
Theorem	sinccvglem 33639*	((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 33640*	((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 33641*	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 · π) · 𝑅)
20.8.2  Miscellaneous theorems
Theorem	elfzm12 33642	Membership in a curtailed finite sequence of integers. (Contributed by Paul Chapman, 17-Nov-2012.)
⊢ (𝑁 ∈ ℕ → (𝑀 ∈ (1...(𝑁 − 1)) → 𝑀 ∈ (1...𝑁)))
Theorem	nn0seqcvg 33643*	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 33644	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 33645	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 33646	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 33647	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 33648	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 33649	Difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((abs‘𝐴) − (abs‘𝐵)) ≤ (abs‘(𝐴 − 𝐵))
Theorem	abs2difabsi 33650	Absolute value of difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (abs‘((abs‘𝐴) − (abs‘𝐵))) ≤ (abs‘(𝐴 − 𝐵))
20.9  Mathbox for Scott Fenton
20.9.1  ZFC Axioms in primitive form
Theorem	axextprim 33651	ax-ext 2710 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
⊢ ¬ ∀𝑥 ¬ ((𝑥 ∈ 𝑦 → 𝑥 ∈ 𝑧) → ((𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦) → 𝑦 = 𝑧))
Theorem	axrepprim 33652	ax-rep 5210 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
⊢ ¬ ∀𝑥 ¬ (¬ ∀𝑦 ¬ ∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧 ¬ ((∀𝑦 𝑧 ∈ 𝑥 → ¬ ∀𝑥(∀𝑧 𝑥 ∈ 𝑦 → ¬ ∀𝑦𝜑)) → ¬ (¬ ∀𝑥(∀𝑧 𝑥 ∈ 𝑦 → ¬ ∀𝑦𝜑) → ∀𝑦 𝑧 ∈ 𝑥)))
Theorem	axunprim 33653	ax-un 7597 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
⊢ ¬ ∀𝑥 ¬ ∀𝑦(¬ ∀𝑥(𝑦 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)
Theorem	axpowprim 33654	ax-pow 5289 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
⊢ (∀𝑥 ¬ ∀𝑦(∀𝑥(¬ ∀𝑧 ¬ 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) → 𝑥 = 𝑦)
Theorem	axregprim 33655	ax-reg 9360 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
⊢ (𝑥 ∈ 𝑦 → ¬ ∀𝑥(𝑥 ∈ 𝑦 → ¬ ∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦)))
Theorem	axinfprim 33656	ax-inf 9405 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 13-Oct-2010.)
⊢ ¬ ∀𝑥 ¬ (𝑦 ∈ 𝑧 → ¬ (𝑦 ∈ 𝑥 → ¬ ∀𝑦(𝑦 ∈ 𝑥 → ¬ ∀𝑧(𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑥))))
Theorem	axacprim 33657	ax-ac 10224 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 26-Oct-2010.)
⊢ ¬ ∀𝑥 ¬ ∀𝑦∀𝑧(∀𝑥 ¬ (𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑤) → ¬ ∀𝑤 ¬ ∀𝑦 ¬ ((¬ ∀𝑤(𝑦 ∈ 𝑧 → (𝑧 ∈ 𝑤 → (𝑦 ∈ 𝑤 → ¬ 𝑤 ∈ 𝑥))) → 𝑦 = 𝑤) → ¬ (𝑦 = 𝑤 → ¬ ∀𝑤(𝑦 ∈ 𝑧 → (𝑧 ∈ 𝑤 → (𝑦 ∈ 𝑤 → ¬ 𝑤 ∈ 𝑥))))))
20.9.2  Untangled classes
Theorem	untelirr 33658*	We call a class "untanged" if all its members are not members of themselves. The term originates from Isbell (see citation in dfon2 33777). 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 33659*	The union of a class is untangled iff all its members are untangled. (Contributed by Scott Fenton, 28-Feb-2011.)
⊢ (∀𝑥 ∈ ∪ 𝐴 ¬ 𝑥 ∈ 𝑥 ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝑦 ¬ 𝑥 ∈ 𝑥)
Theorem	untsucf 33660*	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 33661	The null set is untangled. (Contributed by Scott Fenton, 10-Mar-2011.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ∀𝑥 ∈ ∅ ¬ 𝑥 ∈ 𝑥
Theorem	untint 33662*	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 33663*	If 𝐴 is well-founded by E, then it is untangled. (Contributed by Scott Fenton, 1-Mar-2011.)
⊢ ( E Fr 𝐴 → ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥)
Theorem	untangtr 33664*	A transitive class is untangled iff its elements are. (Contributed by Scott Fenton, 7-Mar-2011.)
⊢ (Tr 𝐴 → (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑦))
20.9.3  Extra propositional calculus theorems
Theorem	3pm3.2ni 33665	Triple negated disjunction introduction. (Contributed by Scott Fenton, 20-Apr-2011.)
⊢ ¬ 𝜑    &   ⊢ ¬ 𝜓    &   ⊢ ¬ 𝜒    ⇒   ⊢ ¬ (𝜑 ∨ 𝜓 ∨ 𝜒)
Theorem	3jaodd 33666	Double deduction form of 3jaoi 1426. (Contributed by Scott Fenton, 20-Apr-2011.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))    &   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜂)))    &   ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜃 ∨ 𝜏) → 𝜂)))
Theorem	3orit 33667	Closed form of 3ori 1423. (Contributed by Scott Fenton, 20-Apr-2011.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜒))
Theorem	biimpexp 33668	A biconditional in the antecedent is the same as two implications. (Contributed by Scott Fenton, 12-Dec-2010.)
⊢ (((𝜑 ↔ 𝜓) → 𝜒) ↔ ((𝜑 → 𝜓) → ((𝜓 → 𝜑) → 𝜒)))
Theorem	3orel13 33669	Elimination of two disjuncts in a triple disjunction. (Contributed by Scott Fenton, 9-Jun-2011.)
⊢ ((¬ 𝜑 ∧ ¬ 𝜒) → ((𝜑 ∨ 𝜓 ∨ 𝜒) → 𝜓))
Theorem	onelssex 33670*	Ordinal less than is equivalent to having an ordinal between them. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐶 ↔ ∃𝑏 ∈ 𝐶 𝐴 ⊆ 𝑏))
20.9.4  Misc. Useful Theorems
Theorem	nepss 33671	Two classes are unequal iff their intersection is a proper subset of one of them. (Contributed by Scott Fenton, 23-Feb-2011.)
⊢ (𝐴 ≠ 𝐵 ↔ ((𝐴 ∩ 𝐵) ⊊ 𝐴 ∨ (𝐴 ∩ 𝐵) ⊊ 𝐵))
Theorem	3ccased 33672	Triple disjunction form of ccased 1036. (Contributed by Scott Fenton, 27-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (𝜑 → ((𝜒 ∧ 𝜂) → 𝜓))    &   ⊢ (𝜑 → ((𝜒 ∧ 𝜁) → 𝜓))    &   ⊢ (𝜑 → ((𝜒 ∧ 𝜎) → 𝜓))    &   ⊢ (𝜑 → ((𝜃 ∧ 𝜂) → 𝜓))    &   ⊢ (𝜑 → ((𝜃 ∧ 𝜁) → 𝜓))    &   ⊢ (𝜑 → ((𝜃 ∧ 𝜎) → 𝜓))    &   ⊢ (𝜑 → ((𝜏 ∧ 𝜂) → 𝜓))    &   ⊢ (𝜑 → ((𝜏 ∧ 𝜁) → 𝜓))    &   ⊢ (𝜑 → ((𝜏 ∧ 𝜎) → 𝜓))    ⇒   ⊢ (𝜑 → (((𝜒 ∨ 𝜃 ∨ 𝜏) ∧ (𝜂 ∨ 𝜁 ∨ 𝜎)) → 𝜓))
Theorem	dfso3 33673*	Expansion of the definition of a strict order. (Contributed by Scott Fenton, 6-Jun-2016.)
⊢ (𝑅 Or 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
Theorem	brtpid1 33674	A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.)
⊢ 𝐴{⟨𝐴, 𝐵⟩, 𝐶, 𝐷}𝐵
Theorem	brtpid2 33675	A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.)
⊢ 𝐴{𝐶, ⟨𝐴, 𝐵⟩, 𝐷}𝐵
Theorem	brtpid3 33676	A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.)
⊢ 𝐴{𝐶, 𝐷, ⟨𝐴, 𝐵⟩}𝐵
Theorem	ceqsrexv2 33677*	Alternate elimitation of a restricted existential quantifier, using implicit substitution. (Contributed by Scott Fenton, 5-Sep-2017.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))
Theorem	iota5f 33678*	A method for computing iota. (Contributed by Scott Fenton, 13-Dec-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (𝜓 ↔ 𝑥 = 𝐴))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (℩𝑥𝜓) = 𝐴)
Theorem	ceqsralv2 33679*	Alternate elimination of a restricted universal quantifier, using implicit substitution. (Contributed by Scott Fenton, 7-Dec-2020.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐵 (𝑥 = 𝐴 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓))
Theorem	dford5 33680	A class is ordinal iff it is a subclass of On and transitive. (Contributed by Scott Fenton, 21-Nov-2021.)
⊢ (Ord 𝐴 ↔ (𝐴 ⊆ On ∧ Tr 𝐴))
Theorem	jath 33681	Closed form of ja 186. Proved using the completeness script. (Proof modification is discouraged.) (Contributed by Scott Fenton, 13-Dec-2021.)
⊢ ((¬ 𝜑 → 𝜒) → ((𝜓 → 𝜒) → ((𝜑 → 𝜓) → 𝜒)))
Theorem	riotarab 33682*	Restricted iota of a restricted abstraction. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜓}𝜒) = (℩𝑥 ∈ 𝐴 (𝜑 ∧ 𝜒))
Theorem	reurab 33683*	Restricted existential uniqueness of a restricted abstraction. (Contributed by Scott Fenton, 8-Aug-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜓}𝜒 ↔ ∃!𝑥 ∈ 𝐴 (𝜑 ∧ 𝜒))
Theorem	snres0 33684	Condition for restriction of a singleton to be empty. (Contributed by Scott Fenton, 9-Aug-2024.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (({⟨𝐴, 𝐵⟩} ↾ 𝐶) = ∅ ↔ ¬ 𝐴 ∈ 𝐶)
Theorem	fnssintima 33685*	Condition for subset of an intersection of an image. (Contributed by Scott Fenton, 16-Aug-2024.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ⊆ ∩ (𝐹 “ 𝐵) ↔ ∀𝑥 ∈ 𝐵 𝐶 ⊆ (𝐹‘𝑥)))
Theorem	xpab 33686*	Cross product of two class abstractions. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ ({𝑥 ∣ 𝜑} × {𝑦 ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ 𝜓)}
Theorem	ralxpes 33687*	A version of ralxp 5753 with explicit substitution. (Contributed by Scott Fenton, 21-Aug-2024.)
⊢ (∀𝑥 ∈ (𝐴 × 𝐵)[(1st ‘𝑥) / 𝑦][(2nd ‘𝑥) / 𝑧]𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 𝜑)
Theorem	ot2elxp 33688	Ordered triple membership in a triple cross product. (Contributed by Scott Fenton, 21-Aug-2024.)
⊢ (⟨⟨𝐴, 𝐵⟩, 𝐶⟩ ∈ ((𝐷 × 𝐸) × 𝐹) ↔ (𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐸 ∧ 𝐶 ∈ 𝐹))
Theorem	ot21std 33689	Extract the first member of an ordered triple. Deduction version. (Contributed by Scott Fenton, 21-Aug-2024.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝑋 = ⟨⟨𝐴, 𝐵⟩, 𝐶⟩ → (1st ‘(1st ‘𝑋)) = 𝐴)
Theorem	ot22ndd 33690	Extract the second member of an ordered triple. Deduction version. (Contributed by Scott Fenton, 21-Aug-2024.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (𝑋 = ⟨⟨𝐴, 𝐵⟩, 𝐶⟩ → (2nd ‘(1st ‘𝑋)) = 𝐵)
Theorem	otthne 33691	Contrapositive of the ordered triple theorem. (Contributed by Scott Fenton, 21-Aug-2024.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    ⇒   ⊢ (⟨⟨𝐴, 𝐵⟩, 𝐶⟩ ≠ ⟨⟨𝐷, 𝐸⟩, 𝐹⟩ ↔ (𝐴 ≠ 𝐷 ∨ 𝐵 ≠ 𝐸 ∨ 𝐶 ≠ 𝐹))
Theorem	elxpxp 33692*	Membership in a triple cross product. (Contributed by Scott Fenton, 21-Aug-2024.)
⊢ (𝐴 ∈ ((𝐵 × 𝐶) × 𝐷) ↔ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 ∃𝑧 ∈ 𝐷 𝐴 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
Theorem	elxpxpss 33693*	Version of elrel 5710 for triple cross products. (Contributed by Scott Fenton, 21-Aug-2024.)
⊢ ((𝑅 ⊆ ((𝐵 × 𝐶) × 𝐷) ∧ 𝐴 ∈ 𝑅) → ∃𝑥∃𝑦∃𝑧 𝐴 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
Theorem	ralxp3f 33694*	Restricted for all over a triple cross product. (Contributed by Scott Fenton, 22-Aug-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = ⟨⟨𝑦, 𝑧⟩, 𝑤⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ ((𝐴 × 𝐵) × 𝐶)𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐶 𝜓)
Theorem	ralxp3 33695*	Restricted for-all over a triple cross product. (Contributed by Scott Fenton, 21-Aug-2024.)
⊢ (𝑝 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑝 ∈ ((𝐴 × 𝐵) × 𝐶)𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓)
Theorem	sbcoteq1a 33696	Equality theorem for substitution of a class for an ordered triple. (Contributed by Scott Fenton, 22-Aug-2024.)
⊢ (𝐴 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → ([(1st ‘(1st ‘𝐴)) / 𝑥][(2nd ‘(1st ‘𝐴)) / 𝑦][(2nd ‘𝐴) / 𝑧]𝜑 ↔ 𝜑))
Theorem	ralxp3es 33697*	Restricted for-all over a triple cross product with explicit substitution. (Contributed by Scott Fenton, 22-Aug-2024.)
⊢ (∀𝑥 ∈ ((𝐴 × 𝐵) × 𝐶)[(1st ‘(1st ‘𝑥)) / 𝑦][(2nd ‘(1st ‘𝑥)) / 𝑧][(2nd ‘𝑥) / 𝑤]𝜑 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐶 𝜑)
Theorem	onunel 33698	The union of two ordinals is in a third iff both of the first two are. (Contributed by Scott Fenton, 10-Sep-2024.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ∪ 𝐵) ∈ 𝐶 ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)))
Theorem	imaeqsexv 33699*	Substitute a function value into an existential quantifier over an image. (Contributed by Scott Fenton, 27-Sep-2024.)
⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∃𝑥 ∈ (𝐹 “ 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓))
Theorem	imaeqsalv 33700*	Substitute a function value into a universal quantifier over an image. (Contributed by Scott Fenton, 27-Sep-2024.)
⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∀𝑥 ∈ (𝐹 “ 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓))