Metamath Proof Explorer Home Metamath Proof Explorer
Most Recent Proofs
 
Mirrors  >  Home  >  MPE Home  >  Th. List  >  Recent ILE Most Recent             Other  >  MM 100

Most recent proofs    These are the 100 (Unicode, GIF) or 1000 (Unicode, GIF) most recent proofs in the set.mm database for the Metamath Proof Explorer (and the Hilbert Space Explorer). The set.mm database is maintained on GitHub with master (stable) and develop (development) versions. This page was created from develop commit 212ee7d9, also available here: set.mm (43MB) or set.mm.bz2 (compressed, 13MB).

The original proofs of theorems with recently shortened proofs can often be found by appending "OLD" to the theorem name, for example 19.43OLD for 19.43. The "OLD" versions are usually deleted after a year.

Other links    Email: Norm Megill.    Mailing list: Metamath Google Group Updated 7-Dec-2021 .    Contributing: How can I contribute to Metamath?    Syndication: RSS feed (courtesy of Dan Getz)    Related wikis: Ghilbert site; Ghilbert Google Group.

Recent news items    (7-Aug-2021) Version 0.198 of the metamath program fixes a bug in "write source ... /rewrap" that prevented end-of-sentence punctuation from appearing in column 79, causing some rewrapped lines to be shorter than necessary. Because this affects about 2000 lines in set.mm, you should use version 0.198 or later for rewrapping before submitting to GitHub.

(7-May-2021) Mario Carneiro has written a Metamath verifier in Lean.

(5-May-2021) Marnix Klooster has written a Metamath verifier in Zig.

(24-Mar-2021) Metamath was mentioned in a couple of articles about OpenAI: Researchers find that large language models struggle with math and What Is GPT-F?.

(26-Dec-2020) Version 0.194 of the metamath program adds the keyword "htmlexturl" to the $t comment to specify external versions of theorem pages. This keyward has been added to set.mm, and you must update your local copy of set.mm for "verify markup" to pass with the new program version.

(19-Dec-2020) Aleksandr A. Adamov has translated the Wikipedia Metamath page into Russian.

(19-Nov-2020) Eric Schmidt's checkmm.cpp was used as a test case for C'est, "a non-standard version of the C++20 standard library, with enhanced support for compile-time evaluation." See C++20 Compile-time Metamath Proof Verification using C'est.

(10-Nov-2020) Filip Cernatescu has updated the XPuzzle (Android app) to version 1.2. XPuzzle is a puzzle with math formulas derived from the Metamath system. At the bottom of the web page is a link to the Google Play Store, where the app can be found.

(7-Nov-2020) Richard Penner created a cross-reference guide between Frege's logic notation and the notation used by set.mm.

(4-Sep-2020) Version 0.192 of the metamath program adds the qualifier '/extract' to 'write source'. See 'help write source' and also this Google Group post.

(23-Aug-2020) Version 0.188 of the metamath program adds keywords Conclusion, Fact, Introduction, Paragraph, Scolia, Scolion, Subsection, and Table to bibliographic references. See 'help write bibliography' for the complete current list.

   Older news...

Color key:   Metamath Proof Explorer  Metamath Proof Explorer   Hilbert Space Explorer  Hilbert Space Explorer   User Mathboxes  User Mathboxes  

Last updated on 21-Jan-2025 at 5:21 AM ET.
Recent Additions to the Metamath Proof Explorer   Notes (last updated 7-Dec-2020 )
DateLabelDescription
Theorem
 
19-Jan-2025bj-adjfrombun 35330 Adjunction from singleton and binary union. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.)
(𝑥 ∪ {𝑦}) ∈ V
 
19-Jan-2025bj-prfromadj 35329 Unordered pair from adjunction. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.)
{𝑥, 𝑦} ∈ V
 
19-Jan-2025bj-snfromadj 35328 Singleton from adjunction and empty set. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.)
{𝑥} ∈ V
 
19-Jan-2025bj-adjg1 35327 Existence of the result of the adjunction (generalized only in the first term is this suffices for current applications). (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.)
(𝐴𝑉 → (𝐴 ∪ {𝑥}) ∈ V)
 
19-Jan-2025ax-bj-adj 35326 Axiom of adjunction. (Contributed by BJ, 19-Jan-2025.)
𝑥𝑦𝑧𝑡(𝑡𝑧 ↔ (𝑡𝑥𝑡 = 𝑦))
 
18-Jan-2025bj-clex 35315 Two ways of stating that a class is a set. (Contributed by BJ, 18-Jan-2025.) (Proof modification is discouraged.)
(𝑥𝐴𝜑)       (𝐴 ∈ V ↔ ∃𝑦𝑥(𝑥𝑦𝜑))
 
18-Jan-2025bj-abex 35314 Two ways of stating that the extension of a formula is a set. (Contributed by BJ, 18-Jan-2025.) (Proof modification is discouraged.)
({𝑥𝜑} ∈ V ↔ ∃𝑦𝑥(𝑥𝑦𝜑))
 
17-Jan-2025prjspnn0 40729 A projective point is nonempty. (Contributed by SN, 17-Jan-2025.)
𝑃 = (𝑁ℙ𝕣𝕠𝕛n𝐾)    &   𝑊 = (𝐾 freeLMod (0...𝑁))    &   𝐵 = ((Base‘𝑊) ∖ {(0g𝑊)})    &   (𝜑𝑁 ∈ ℕ0)    &   (𝜑𝐾 ∈ DivRing)    &   (𝜑𝐴𝑃)       (𝜑𝐴 ≠ ∅)
 
17-Jan-2025prjspnssbas 40728 A projective point spans a subset of the (nonzero) affine points. (Contributed by SN, 17-Jan-2025.)
𝑃 = (𝑁ℙ𝕣𝕠𝕛n𝐾)    &   𝑊 = (𝐾 freeLMod (0...𝑁))    &   𝐵 = ((Base‘𝑊) ∖ {(0g𝑊)})    &   (𝜑𝑁 ∈ ℕ0)    &   (𝜑𝐾 ∈ DivRing)       (𝜑𝑃 ⊆ 𝒫 𝐵)
 
17-Jan-2025flddrngd 40523 A field is a division ring. (Contributed by SN, 17-Jan-2025.)
(𝜑𝑅 ∈ Field)       (𝜑𝑅 ∈ DivRing)
 
17-Jan-2025rictr 40513 Ring isomorphism is transitive. (Contributed by SN, 17-Jan-2025.)
((𝑅𝑟 𝑆𝑆𝑟 𝑇) → 𝑅𝑟 𝑇)
 
17-Jan-2025rimco 40510 The composition of ring isomorphisms is a ring isomorphism. (Contributed by SN, 17-Jan-2025.)
((𝐹 ∈ (𝑆 RingIso 𝑇) ∧ 𝐺 ∈ (𝑅 RingIso 𝑆)) → (𝐹𝐺) ∈ (𝑅 RingIso 𝑇))
 
17-Jan-2025bj-elpwgALT 35338 Alternate proof of elpwg 4550. See comment for bj-velpwALT 35337. (Contributed by BJ, 17-Jan-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
(𝐴𝑉 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
 
17-Jan-2025bj-velpwALT 35337 This theorem bj-velpwALT 35337 and the next theorem bj-elpwgALT 35338 are alternate proofs of velpw 4552 and elpwg 4550 respectively, where one proves first the setvar case and then generalizes using vtoclbg 3516 instead of proving first the general case using elab2g 3621 and then specifying. Here, this results in needing an extra DV condition, a longer combined proof and use of ax-12 2170. In other cases, that order is better (e.g., vsnex 5374 proved before snexg 5375). (Contributed by BJ, 17-Jan-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
(𝑥 ∈ 𝒫 𝐴𝑥𝐴)
 
17-Jan-2025intidg 5402 The intersection of all sets to which a set belongs is the singleton of that set. (Contributed by NM, 5-Jun-2009.) Put in closed form and avoid ax-nul 5250. (Revised by BJ, 17-Jan-2025.)
(𝐴𝑉 {𝑥𝐴𝑥} = {𝐴})
 
17-Jan-2025snelpwg 5387 A singleton of a set is a member of the powerclass of a class if and only if that set is a member of that class. (Contributed by NM, 1-Apr-1998.) Put in closed form and avoid ax-nul 5250. (Revised by BJ, 17-Jan-2025.)
(𝐴𝑉 → (𝐴𝐵 ↔ {𝐴} ∈ 𝒫 𝐵))
 
15-Jan-20251fldgenq 31793 The field of rational numbers is generated by 1 in fld, that is, is the prime field of fld. (Contributed by Thierry Arnoux, 15-Jan-2025.)
(ℂfldfldGen{1}) = ℚ
 
15-Jan-2025fldgenidfld 31789 The subfield generated by a subfield is the subfield itself. (Contributed by Thierry Arnoux, 15-Jan-2025.)
𝐵 = (Base‘𝐹)    &   (𝜑𝐹 ∈ DivRing)    &   (𝜑𝑆 ∈ (SubDRing‘𝐹))       (𝜑 → (𝐹fldGen𝑆) = 𝑆)
 
15-Jan-2025fldgenss 31788 Generated subfields preserve subset ordering. ( see lspss 20352 and spanss 29998) (Contributed by Thierry Arnoux, 15-Jan-2025.)
𝐵 = (Base‘𝐹)    &   (𝜑𝐹 ∈ DivRing)    &   (𝜑𝑆𝐵)    &   (𝜑𝑇𝑆)       (𝜑 → (𝐹fldGen𝑇) ⊆ (𝐹fldGen𝑆))
 
15-Jan-2025fldgenssid 31786 The field generated by a set of elements contains those elements. See lspssid 20353. (Contributed by Thierry Arnoux, 15-Jan-2025.)
𝐵 = (Base‘𝐹)    &   (𝜑𝐹 ∈ DivRing)    &   (𝜑𝑆𝐵)       (𝜑𝑆 ⊆ (𝐹fldGen𝑆))
 
15-Jan-2025sdrginvcl 31781 A sub-division-ring is closed under the ring inverse operation. (Contributed by Thierry Arnoux, 15-Jan-2025.)
𝐼 = (invr𝑅)    &    0 = (0g𝑅)       ((𝐴 ∈ (SubDRing‘𝑅) ∧ 𝑋𝐴𝑋0 ) → (𝐼𝑋) ∈ 𝐴)
 
15-Jan-2025sdrgdvcl 31780 A sub-division-ring is closed under the ring division operation. (Contributed by Thierry Arnoux, 15-Jan-2025.)
/ = (/r𝑅)    &    0 = (0g𝑅)    &   (𝜑𝐴 ∈ (SubDRing‘𝑅))    &   (𝜑𝑋𝐴)    &   (𝜑𝑌𝐴)    &   (𝜑𝑌0 )       (𝜑 → (𝑋 / 𝑌) ∈ 𝐴)
 
15-Jan-2025cshwsexa 14635 The class of (different!) words resulting by cyclically shifting something (not necessarily a word) is a set. (Contributed by AV, 8-Jun-2018.) (Revised by Mario Carneiro/AV, 25-Oct-2018.) (Proof shortened by SN, 15-Jan-2025.)
{𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(♯‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤} ∈ V
 
15-Jan-2025sels 5383 If a class is a set, then it is a member of a set. (Contributed by NM, 4-Jan-2002.) Generalize from the proof of elALT 5385. (Revised by BJ, 3-Apr-2019.) Avoid ax-sep 5243, ax-nul 5250, ax-pow 5308. (Revised by BTernaryTau, 15-Jan-2025.)
(𝐴𝑉 → ∃𝑥 𝐴𝑥)
 
15-Jan-2025snexg 5375 A singleton built on a set is a set. Special case of snex 5376 which does not require ax-nul 5250 and is intuitionistically valid. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.) Extract from snex 5376. (Revised by BJ, 15-Jan-2025.)
(𝐴𝑉 → {𝐴} ∈ V)
 
15-Jan-2025vsnex 5374 A singleton built on a setvar is a set. (Contributed by BJ, 15-Jan-2025.)
{𝑥} ∈ V
 
15-Jan-2025iunid 5007 An indexed union of singletons recovers the index set. (Contributed by NM, 6-Sep-2005.) (Proof shortened by SN, 15-Jan-2025.)
𝑥𝐴 {𝑥} = 𝐴
 
15-Jan-2025rabeqc 3415 A restricted class abstraction equals the restricting class if its condition follows from the membership of the free setvar variable in the restricting class. (Contributed by AV, 20-Apr-2022.) (Proof shortened by SN, 15-Jan-2025.)
(𝑥𝐴𝜑)       {𝑥𝐴𝜑} = 𝐴
 
14-Jan-2025resisoeq45d 41357 Equality deduction for equally restricted isometries. (Contributed by RP, 14-Jan-2025.)
(𝜑𝐴 = 𝐶)    &   (𝜑𝐵 = 𝐷)       (𝜑 → ((𝐹𝐴) Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐹𝐶) Isom 𝑅, 𝑆 (𝐶, 𝐷)))
 
14-Jan-2025isoeq145d 41356 Equality deduction for isometries. (Contributed by RP, 14-Jan-2025.)
(𝜑𝐹 = 𝐺)    &   (𝜑𝐴 = 𝐶)    &   (𝜑𝐵 = 𝐷)       (𝜑 → (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐺 Isom 𝑅, 𝑆 (𝐶, 𝐷)))
 
14-Jan-2025sdomne0 41350 A class that strictly dominates any set is not empty. (Suggested by SN, 14-Jan-2025.) (Contributed by RP, 14-Jan-2025.)
(𝐵𝐴𝐴 ≠ ∅)
 
14-Jan-2025omcl3g 41327 Closure law for ordinal multiplication. (Contributed by RP, 14-Jan-2025.)
(((𝐴𝐶𝐵𝐶) ∧ (𝐶 ∈ 3o ∨ (𝐶 = (ω ↑o (ω ↑o 𝐷)) ∧ 𝐷 ∈ On))) → (𝐴 ·o 𝐵) ∈ 𝐶)
 
13-Jan-2025mbfmbfm 32525 A measurable function to a Borel Set is measurable. (Contributed by Thierry Arnoux, 24-Jan-2017.) Remove hypotheses. (Revised by SN, 13-Jan-2025.)
(𝜑𝐹 ∈ (dom 𝑀MblFnM(sigaGen‘𝐽)))       (𝜑𝐹 ran MblFnM)
 
13-Jan-2025isanmbfm 32523 The predicate to be a measurable function. (Contributed by Thierry Arnoux, 30-Jan-2017.) Remove hypotheses. (Revised by SN, 13-Jan-2025.)
(𝜑𝐹 ∈ (𝑆MblFnM𝑇))       (𝜑𝐹 ran MblFnM)
 
13-Jan-2025fvssunirn 6858 The result of a function value is always a subset of the union of the range, even if it is invalid and thus empty. (Contributed by Stefan O'Rear, 2-Nov-2014.) (Revised by Mario Carneiro, 31-Aug-2015.) (Proof shortened by SN, 13-Jan-2025.)
(𝐹𝑋) ⊆ ran 𝐹
 
13-Jan-2025fvn0fvelrn 6856 If the value of a function is not null, the value is an element of the range of the function. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Proof shortened by SN, 13-Jan-2025.)
((𝐹𝑋) ≠ ∅ → (𝐹𝑋) ∈ ran 𝐹)
 
12-Jan-2025dfno2 41365 A surreal number, in the functional sign expansion representation, is a function which maps from an ordinal into a set of two possible signs. (Contributed by RP, 12-Jan-2025.)
No = {𝑓 ∈ 𝒫 (On × {1o, 2o}) ∣ (Fun 𝑓 ∧ dom 𝑓 ∈ On)}
 
12-Jan-2025omcl2 41326 Closure law for ordinal multiplication. (Contributed by RP, 12-Jan-2025.)
(((𝐴𝐶𝐵𝐶) ∧ (𝐶 = ∅ ∨ (𝐶 = (ω ↑o (ω ↑o 𝐷)) ∧ 𝐷 ∈ On))) → (𝐴 ·o 𝐵) ∈ 𝐶)
 
12-Jan-2025omabs2 41325 Ordinal multiplication by a larger ordinal is absorbed when the larger ordinal is either 2 or ω raised to some power of ω. (Contributed by RP, 12-Jan-2025.)
(((𝐴𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = ∅ ∨ 𝐵 = 2o ∨ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On))) → (𝐴 ·o 𝐵) = 𝐵)
 
12-Jan-2025bj-axadj 35325 Two ways of stating the axiom of adjunction (which is the universal closure of either side). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
((𝑥 ∪ {𝑦}) ∈ V ↔ ∃𝑧𝑡(𝑡𝑧 ↔ (𝑡𝑥𝑡 = 𝑦)))
 
12-Jan-2025bj-prex 35324 Existence of unordered pairs proved from ax-bj-sn 35317 and ax-bj-bun 35321. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
{𝐴, 𝐵} ∈ V
 
12-Jan-2025bj-prexg 35323 Existence of unordered pairs formed on sets, proved from ax-bj-sn 35317 and ax-bj-bun 35321. Contrary to bj-prex 35324, this proof is intuitionistically valid and does not require ax-nul 5250. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
((𝐴𝑉𝐵𝑊) → {𝐴, 𝐵} ∈ V)
 
12-Jan-2025bj-unexg 35322 Existence of binary unions of sets, proved from ax-bj-bun 35321. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
((𝐴𝑉𝐵𝑊) → (𝐴𝐵) ∈ V)
 
12-Jan-2025ax-bj-bun 35321 Axiom of binary union. (Contributed by BJ, 12-Jan-2025.)
𝑥𝑦𝑧𝑡(𝑡𝑧 ↔ (𝑡𝑥𝑡𝑦))
 
12-Jan-2025bj-axbun 35320 Two ways of stating the axiom of binary union (which is the universal closure of either side, see ax-bj-bun 35321). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
((𝑥𝑦) ∈ V ↔ ∃𝑧𝑡(𝑡𝑧 ↔ (𝑡𝑥𝑡𝑦)))
 
12-Jan-2025bj-snex 35319 A singleton is a set. See also snex 5376, snexALT 5326. (Contributed by NM, 7-Aug-1994.) Prove it from ax-bj-sn 35317. (Revised by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
{𝐴} ∈ V
 
12-Jan-2025bj-snexg 35318 A singleton built on a set is a set. Contrary to bj-snex 35319, this proof is intuitionistically valid and does not require ax-nul 5250. (Contributed by NM, 7-Aug-1994.) Extract it from snex 5376 and prove it from ax-bj-sn 35317. (Revised by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
(𝐴𝑉 → {𝐴} ∈ V)
 
12-Jan-2025ax-bj-sn 35317 Axiom of singleton. (Contributed by BJ, 12-Jan-2025.)
𝑥𝑦𝑧(𝑧𝑦𝑧 = 𝑥)
 
12-Jan-2025bj-axsn 35316 Two ways of stating the axiom of singleton (which is the universal closure of either side, see ax-bj-sn 35317). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.)
({𝑥} ∈ V ↔ ∃𝑦𝑧(𝑧𝑦𝑧 = 𝑥))
 
12-Jan-2025isrim 20073 An isomorphism of rings is a bijective homomorphism. (Contributed by AV, 22-Oct-2019.) Remove sethood antecedent. (Revised by SN, 12-Jan-2025.)
𝐵 = (Base‘𝑅)    &   𝐶 = (Base‘𝑆)       (𝐹 ∈ (𝑅 RingIso 𝑆) ↔ (𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹:𝐵1-1-onto𝐶))
 
12-Jan-2025rabbiia 3407 Equivalent formulas yield equal restricted class abstractions (inference form). (Contributed by NM, 22-May-1999.) (Proof shortened by Wolf Lammen, 12-Jan-2025.)
(𝑥𝐴 → (𝜑𝜓))       {𝑥𝐴𝜑} = {𝑥𝐴𝜓}
 
12-Jan-2025reuanid 3360 Cancellation law for restricted unique existential quantification. (Contributed by Peter Mazsa, 12-Feb-2018.) (Proof shortened by Wolf Lammen, 12-Jan-2025.)
(∃!𝑥𝐴 (𝑥𝐴𝜑) ↔ ∃!𝑥𝐴 𝜑)
 
12-Jan-2025rmoanid 3359 Cancellation law for restricted at-most-one quantification. (Contributed by Peter Mazsa, 24-May-2018.) (Proof shortened by Wolf Lammen, 12-Jan-2025.)
(∃*𝑥𝐴 (𝑥𝐴𝜑) ↔ ∃*𝑥𝐴 𝜑)
 
11-Jan-2025primefldgen1 31792 The prime field of a division ring is the subfield generated by the multiplicative identity element. In general, we should write "prime division ring", but since most later usages are in the case where the ambient ring is commutative, we keep the term "prime field". (Contributed by Thierry Arnoux, 11-Jan-2025.)
𝐵 = (Base‘𝑅)    &    1 = (1r𝑅)    &   (𝜑𝑅 ∈ DivRing)       (𝜑 (SubDRing‘𝑅) = (𝑅fldGen{ 1 }))
 
11-Jan-2025fldgenfld 31791 A generated subfield is a field. (Contributed by Thierry Arnoux, 11-Jan-2025.)
𝐵 = (Base‘𝐹)    &   (𝜑𝐹 ∈ Field)    &   (𝜑𝑆𝐵)       (𝜑 → (𝐹s (𝐹fldGen𝑆)) ∈ Field)
 
11-Jan-2025fldgenid 31790 The subfield of a field 𝐹 generated by the whole base set of 𝐹 is 𝐹 itself. (Contributed by Thierry Arnoux, 11-Jan-2025.)
𝐵 = (Base‘𝐹)    &   (𝜑𝐹 ∈ DivRing)       (𝜑 → (𝐹fldGen𝐵) = 𝐵)
 
11-Jan-2025fldgensdrg 31787 A generated subfield is a sub-division-ring. (Contributed by Thierry Arnoux, 11-Jan-2025.)
𝐵 = (Base‘𝐹)    &   (𝜑𝐹 ∈ DivRing)    &   (𝜑𝑆𝐵)       (𝜑 → (𝐹fldGen𝑆) ∈ (SubDRing‘𝐹))
 
11-Jan-2025fldgenval 31785 Value of the field generating function: (𝐹fldGen𝑆) is the smallest sub-division-ring of 𝐹 containing 𝑆. (Contributed by Thierry Arnoux, 11-Jan-2025.)
𝐵 = (Base‘𝐹)    &   (𝜑𝐹 ∈ DivRing)    &   (𝜑𝑆𝐵)       (𝜑 → (𝐹fldGen𝑆) = {𝑎 ∈ (SubDRing‘𝐹) ∣ 𝑆𝑎})
 
11-Jan-2025resrng 20932 The real numbers form a star ring. (Contributed by Thierry Arnoux, 19-Apr-2019.) (Proof shortened by Thierry Arnoux, 11-Jan-2025.)
fld ∈ *-Ring
 
11-Jan-2025fldsdrgfld 20172 A sub-division-ring of a field is itself a field, so it is a subfield. We can therefore use SubDRing to express subfields. (Contributed by Thierry Arnoux, 11-Jan-2025.)
((𝐹 ∈ Field ∧ 𝐴 ∈ (SubDRing‘𝐹)) → (𝐹s 𝐴) ∈ Field)
 
11-Jan-2025sucdom 9100 Strict dominance of a set over a natural number is the same as dominance over its successor. (Contributed by Mario Carneiro, 12-Jan-2013.) Avoid ax-pow 5308. (Revised by BTernaryTau, 4-Dec-2024.) (Proof shortened by BJ, 11-Jan-2025.)
(𝐴 ∈ ω → (𝐴𝐵 ↔ suc 𝐴𝐵))
 
11-Jan-2025onuniorsuc 7750 An ordinal number is either its own union (if zero or a limit ordinal) or the successor of its union. (Contributed by NM, 13-Jun-1994.) Put in closed form. (Revised by BJ, 11-Jan-2025.)
(𝐴 ∈ On → (𝐴 = 𝐴𝐴 = suc 𝐴))
 
11-Jan-2025sucexeloni 7722 If the successor of an ordinal number exists, it is an ordinal number. This variation of suceloni 7724 does not require ax-un 7650. (Contributed by BTernaryTau, 30-Nov-2024.) (Proof shortened by BJ, 11-Jan-2025.)
((𝐴 ∈ On ∧ suc 𝐴𝑉) → suc 𝐴 ∈ On)
 
11-Jan-2025ordsuci 7721 The successor of an ordinal class is an ordinal class. (Contributed by NM, 6-Jun-1994.) Extract and adapt from a subproof of suceloni 7724. (Revised by BTernaryTau, 6-Jan-2025.) (Proof shortened by BJ, 11-Jan-2025.)
(Ord 𝐴 → Ord suc 𝐴)
 
10-Jan-2025riccrng 40515 A ring is commutative if and only if an isomorphic ring is commutative. (Contributed by SN, 10-Jan-2025.)
(𝑅𝑟 𝑆 → (𝑅 ∈ CRing ↔ 𝑆 ∈ CRing))
 
10-Jan-2025riccrng1 40514 Ring isomorphism preserves (multiplicative) commutativity. (Contributed by SN, 10-Jan-2025.)
((𝑅𝑟 𝑆𝑅 ∈ CRing) → 𝑆 ∈ CRing)
 
10-Jan-2025ricsym 40512 Ring isomorphism is symmetric. (Contributed by SN, 10-Jan-2025.)
(𝑅𝑟 𝑆𝑆𝑟 𝑅)
 
10-Jan-2025brrici 40511 Prove isomorphic by an explicit isomorphism. (Contributed by SN, 10-Jan-2025.)
(𝐹 ∈ (𝑅 RingIso 𝑆) → 𝑅𝑟 𝑆)
 
10-Jan-2025rimcnv 40509 The converse of a ring isomorphism is a ring isomorphism. (Contributed by SN, 10-Jan-2025.)
(𝐹 ∈ (𝑅 RingIso 𝑆) → 𝐹 ∈ (𝑆 RingIso 𝑅))
 
10-Jan-2025rncrhmcl 40508 The range of a commutative ring homomorphism is a commutative ring. (Contributed by SN, 10-Jan-2025.)
𝐶 = (𝑁s ran 𝐹)    &   (𝜑𝐹 ∈ (𝑀 RingHom 𝑁))    &   (𝜑𝑀 ∈ CRing)       (𝜑𝐶 ∈ CRing)
 
10-Jan-2025ressbasss2 40481 The base set of a restriction to 𝐴 is a subset of 𝐴. (Contributed by SN, 10-Jan-2025.)
𝑅 = (𝑊s 𝐴)       (Base‘𝑅) ⊆ 𝐴
 
10-Jan-2025ressbasssg 40480 The base set of a restriction to 𝐴 is a subset of 𝐴 and the base set 𝐵 of the original structure. (Contributed by SN, 10-Jan-2025.)
𝑅 = (𝑊s 𝐴)    &   𝐵 = (Base‘𝑊)       (Base‘𝑅) ⊆ (𝐴𝐵)
 
10-Jan-2025rimrhm 20077 A ring isomorphism is a homomorphism. Compare gimghm 18976. (Contributed by AV, 22-Oct-2019.) Remove hypotheses. (Revised by SN, 10-Jan-2025.)
(𝐹 ∈ (𝑅 RingIso 𝑆) → 𝐹 ∈ (𝑅 RingHom 𝑆))
 
10-Jan-2025isrim0 20064 A ring isomorphism is a homomorphism whose converse is also a homomorphism. Compare isgim2 18977. (Contributed by AV, 22-Oct-2019.) Remove sethood antecedent. (Revised by SN, 10-Jan-2025.)
(𝐹 ∈ (𝑅 RingIso 𝑆) ↔ (𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐹 ∈ (𝑆 RingHom 𝑅)))
 
10-Jan-2025xpfi 9182 The Cartesian product of two finite sets is finite. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Mar-2015.) Avoid ax-pow 5308. (Revised by BTernaryTau, 10-Jan-2025.)
((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 × 𝐵) ∈ Fin)
 
10-Jan-2025elfvunirn 6857 A function value is a subset of the union of the range. (An artifact of our function value definition, compare elfvdm 6862). (Contributed by Thierry Arnoux, 13-Nov-2016.) Remove functionhood antecedent. (Revised by SN, 10-Jan-2025.)
(𝐵 ∈ (𝐹𝐴) → 𝐵 ran 𝐹)
 
9-Jan-2025ply1fermltlchr 31967 Fermat's little theorem for polynomials in a commutative ring 𝐹 of characteristic 𝑃 prime: we have the polynomial equation (𝑋 + 𝐴)↑𝑃 = ((𝑋𝑃) + 𝐴). (Contributed by Thierry Arnoux, 9-Jan-2025.)
𝑊 = (Poly1𝐹)    &   𝑋 = (var1𝐹)    &    + = (+g𝑊)    &   𝑁 = (mulGrp‘𝑊)    &    = (.g𝑁)    &   𝐶 = (algSc‘𝑊)    &   𝐴 = (𝐶‘((ℤRHom‘𝐹)‘𝐸))    &   𝑃 = (chr‘𝐹)    &   (𝜑𝐹 ∈ CRing)    &   (𝜑𝑃 ∈ ℙ)    &   (𝜑𝐸 ∈ ℤ)       (𝜑 → (𝑃 (𝑋 + 𝐴)) = ((𝑃 𝑋) + 𝐴))
 
9-Jan-2025df-fldgen 31784 Define a function generating the smallest sub-division-ring of a given ring containing a given set. If the base structure is a division ring, then this is also a division ring (see fldgensdrg 31787). If the base structure is a field, this is a subfield (see fldgenfld 31791 and fldsdrgfld 20172). In general this will be used in the context of fields, hence the name fldGen. (Contributed by Saveliy Skresanov and Thierry Arnoux, 9-Jan-2025.)
fldGen = (𝑓 ∈ V, 𝑠 ∈ V ↦ {𝑎 ∈ (SubDRing‘𝑓) ∣ 𝑠𝑎})
 
8-Jan-2025dflim5 41323 A limit ordinal is either the proper class of ordinals or some non-zero product with omega. (Contributed by RP, 8-Jan-2025.)
(Lim 𝐴 ↔ (𝐴 = On ∨ ∃𝑥 ∈ (On ∖ 1o)𝐴 = (ω ·o 𝑥)))
 
8-Jan-2025succlg 41322 Closure law for ordinal successor. (Contributed by RP, 8-Jan-2025.)
((𝐴𝐵 ∧ (𝐵 = ∅ ∨ (𝐵 = (ω ·o 𝐶) ∧ 𝐶 ∈ (On ∖ 1o)))) → suc 𝐴𝐵)
 
8-Jan-2025omlimcl2 41319 The product of a limit ordinal with any nonzero ordinal is a limit ordinal. (Contributed by RP, 8-Jan-2025.)
(((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → Lim (𝐵 ·o 𝐴))
 
8-Jan-2025infn0 9172 An infinite set is not empty. For a shorter proof using ax-un 7650, see infn0ALT 9173. (Contributed by NM, 23-Oct-2004.) Avoid ax-un 7650. (Revised by BTernaryTau, 8-Jan-2025.)
(ω ≼ 𝐴𝐴 ≠ ∅)
 
8-Jan-2025cbvrexdva2 3320 Rule used to change the bound variable in a restricted existential quantifier with implicit substitution which also changes the quantifier domain. Deduction form. (Contributed by David Moews, 1-May-2017.) (Proof shortened by Wolf Lammen, 8-Jan-2025.)
((𝜑𝑥 = 𝑦) → (𝜓𝜒))    &   ((𝜑𝑥 = 𝑦) → 𝐴 = 𝐵)       (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑦𝐵 𝜒))
 
7-Jan-2025nnawordexg 41321 If an ordinal, 𝐵, is in a half-open interval between some 𝐴 and the next limit ordinal, 𝐵 is the sum of the 𝐴 and some natural number. This weakens the antecedent of nnawordex 8539. (Contributed by RP, 7-Jan-2025.)
((𝐴 ∈ On ∧ 𝐴𝐵𝐵 ∈ (𝐴 +o ω)) → ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵)
 
7-Jan-2025oawordex2 41320 If 𝐶 is between 𝐴 (inclusive) and (𝐴 +o 𝐵) (exclusive), there is an ordinal which equals 𝐶 when summed to 𝐴. This is a slightly different statement than oawordex 8459 or oawordeu 8457. (Contributed by RP, 7-Jan-2025.)
(((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴𝐶𝐶 ∈ (𝐴 +o 𝐵))) → ∃𝑥𝐵 (𝐴 +o 𝑥) = 𝐶)
 
7-Jan-2025aks6d1c2p2 40362 Injective condition for countability argument assuming that 𝑁 is not a prime power. (Contributed by metakunt, 7-Jan-2025.)
(𝜑𝑁 ∈ ℕ)    &   (𝜑𝑃 ∈ ℙ)    &   (𝜑𝑃𝑁)    &   𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃𝑘) · ((𝑁 / 𝑃)↑𝑙)))    &   (𝜑𝑄 ∈ ℙ)    &   (𝜑𝑄𝑁)    &   (𝜑𝑃𝑄)       (𝜑𝐸:(ℕ0 × ℕ0)–1-1→ℕ)
 
7-Jan-2025aks6d1c2p1 40361 In the AKS-theorem the subset defined by 𝐸 takes values in the positive integers. (Contributed by metakunt, 7-Jan-2025.)
(𝜑𝑁 ∈ ℕ)    &   (𝜑𝑃 ∈ ℙ)    &   (𝜑𝑃𝑁)    &   𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0 ↦ ((𝑃𝑘) · ((𝑁 / 𝑃)↑𝑙)))       (𝜑𝐸:(ℕ0 × ℕ0)⟶ℕ)
 
7-Jan-2025fldhmf1 40360 A field homomorphism is injective. This follows immediately from the definition of the ring homomorphism that sends the multiplicative identity to the multiplicative identity. (Contributed by metakunt, 7-Jan-2025.)
(𝜑𝐾 ∈ Field)    &   (𝜑𝐿 ∈ Field)    &   (𝜑𝐹 ∈ (𝐾 RingHom 𝐿))    &   𝐴 = (Base‘𝐾)    &   𝐵 = (Base‘𝐿)       (𝜑𝐹:𝐴1-1𝐵)
 
7-Jan-2025infsdomnn 9170 An infinite set strictly dominates a natural number. (Contributed by NM, 22-Nov-2004.) (Revised by Mario Carneiro, 27-Apr-2015.) Avoid ax-pow 5308. (Revised by BTernaryTau, 7-Jan-2025.)
((ω ≼ 𝐴𝐵 ∈ ω) → 𝐵𝐴)
 
7-Jan-2025nnsdomg 9167 Omega strictly dominates a natural number. Example 3 of [Enderton] p. 146. In order to avoid the Axiom of Infinity, we include it as part of the antecedent. See nnsdom 9511 for the version without this sethood requirement. (Contributed by NM, 15-Jun-1998.) Avoid ax-pow 5308. (Revised by BTernaryTau, 7-Jan-2025.)
((ω ∈ V ∧ 𝐴 ∈ ω) → 𝐴 ≺ ω)
 
7-Jan-2025findcard3 9150 Schema for strong induction on the cardinality of a finite set. The inductive hypothesis is that the result is true on any proper subset. The result is then proven to be true for all finite sets. (Contributed by Mario Carneiro, 13-Dec-2013.) Avoid ax-pow 5308. (Revised by BTernaryTau, 7-Jan-2025.)
(𝑥 = 𝑦 → (𝜑𝜒))    &   (𝑥 = 𝐴 → (𝜑𝜏))    &   (𝑦 ∈ Fin → (∀𝑥(𝑥𝑦𝜑) → 𝜒))       (𝐴 ∈ Fin → 𝜏)
 
6-Jan-2025enp1i 9144 Proof induction for en2 9146 and related theorems. (Contributed by Mario Carneiro, 5-Jan-2016.) Generalize to all ordinals and avoid ax-pow 5308, ax-un 7650. (Revised by BTernaryTau, 6-Jan-2025.)
Ord 𝑀    &   𝑁 = suc 𝑀    &   ((𝐴 ∖ {𝑥}) ≈ 𝑀𝜑)    &   (𝑥𝐴 → (𝜑𝜓))       (𝐴𝑁 → ∃𝑥𝜓)
 
6-Jan-2025dif1ennn 9026 If a set 𝐴 is equinumerous to the successor of a natural number 𝑀, then 𝐴 with an element removed is equinumerous to 𝑀. See also dif1ennnALT 9142. (Contributed by BTernaryTau, 6-Jan-2025.)
((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀)
 
6-Jan-2025dif1en 9025 If a set 𝐴 is equinumerous to the successor of an ordinal 𝑀, then 𝐴 with an element removed is equinumerous to 𝑀. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, 16-Aug-2015.) Avoid ax-pow 5308. (Revised by BTernaryTau, 26-Aug-2024.) Generalize to all ordinals. (Revised by BTernaryTau, 6-Jan-2025.)
((𝑀 ∈ On ∧ 𝐴 ≈ suc 𝑀𝑋𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀)
 
6-Jan-2025ord3 8384 Ordinal 3 is an ordinal class. (Contributed by BTernaryTau, 6-Jan-2025.)
Ord 3o
 
6-Jan-2025ordsuc 7726 A class is ordinal if and only if its successor is ordinal. (Contributed by NM, 3-Apr-1995.) Avoid ax-un 7650. (Revised by BTernaryTau, 6-Jan-2025.)
(Ord 𝐴 ↔ Ord suc 𝐴)
 
5-Jan-2025smfdivdmmbl2 44724 If a functions and a sigma-measurable function have domains in the sigma-algebra, the domain of the division of the two functions is in the sigma-algebra. This is the third statement of Proposition 121H of [Fremlin1] p. 39 . Note: While the theorem in the book assumes both functions are sigma-measurable, this assumption is unnecessary for the part concerning their division, for the function at the numerator. It is required only for the function at the denominator. (Contributed by Glauco Siliprandi, 5-Jan-2025.)
𝑥𝜑    &   𝑥𝐹    &   𝑥𝐺    &   (𝜑𝑆 ∈ SAlg)    &   (𝜑𝐹:𝐴𝑉)    &   (𝜑𝐺 ∈ (SMblFn‘𝑆))    &   (𝜑𝐴𝑆)    &   (𝜑 → dom 𝐺𝑆)    &   𝐷 = {𝑥 ∈ dom 𝐺 ∣ (𝐺𝑥) ≠ 0}    &   𝐻 = (𝑥 ∈ (dom 𝐹𝐷) ↦ ((𝐹𝑥) / (𝐺𝑥)))       (𝜑 → dom 𝐻𝑆)
 
5-Jan-2025smfpimne2 44723 Given a function measurable w.r.t. to a sigma-algebra, the preimage of reals that are different from a value is in the subspace sigma-algebra induced by its domain. Notice that 𝐴 is not assumed to be an extended real. (Contributed by Glauco Siliprandi, 5-Jan-2025.)
𝑥𝜑    &   𝑥𝐹    &   (𝜑𝑆 ∈ SAlg)    &   (𝜑𝐹 ∈ (SMblFn‘𝑆))    &   𝐷 = dom 𝐹       (𝜑 → {𝑥𝐷 ∣ (𝐹𝑥) ≠ 𝐴} ∈ (𝑆t 𝐷))
 
5-Jan-2025smfpimne 44722 Given a function measurable w.r.t. to a sigma-algebra, the preimage of reals that are different from a value in the extended reals is in the subspace of sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 5-Jan-2025.)
𝑥𝜑    &   𝑥𝐹    &   (𝜑𝑆 ∈ SAlg)    &   (𝜑𝐹 ∈ (SMblFn‘𝑆))    &   𝐷 = dom 𝐹    &   (𝜑𝐴 ∈ ℝ*)       (𝜑 → {𝑥𝐷 ∣ (𝐹𝑥) ≠ 𝐴} ∈ (𝑆t 𝐷))
 
5-Jan-2025smfdivdmmbl 44721 If a functions and a sigma-measurable function have domains in the sigma-algebra, the domain of the division of the two functions is in the sigma-algebra. This is the third statement of Proposition 121H of [Fremlin1] p. 39 . Note: While the theorem in the book assumes both functions are sigma-measurable, this assumption is unnecessary for the part concerning their division, for the function at the numerator (it is needed only for the function at the denominator). (Contributed by Glauco Siliprandi, 5-Jan-2025.)
𝑥𝜑    &   𝑥𝐵    &   (𝜑𝑆 ∈ SAlg)    &   (𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)    &   ((𝜑𝑥𝐵) → 𝐷𝑊)    &   (𝜑 → (𝑥𝐵𝐷) ∈ (SMblFn‘𝑆))    &   𝐸 = {𝑥𝐵𝐷 ≠ 0}       (𝜑 → (𝐴𝐸) ∈ 𝑆)
 
5-Jan-2025smfdmmblpimne 44720 If a measurable function w.r.t. to a sigma-algebra has domain in the sigma-algebra, the set of elements that are not mapped to a given real, is in the sigma-algebra (Contributed by Glauco Siliprandi, 5-Jan-2025.)
𝑥𝜑    &   𝑥𝐴    &   (𝜑𝑆 ∈ SAlg)    &   (𝜑𝐴𝑆)    &   ((𝜑𝑥𝐴) → 𝐵 ∈ ℝ)    &   (𝜑 → (𝑥𝐴𝐵) ∈ (SMblFn‘𝑆))    &   (𝜑𝐶 ∈ ℝ)    &   𝐷 = {𝑥𝐴𝐵𝐶}       (𝜑𝐷𝑆)
 
5-Jan-2025smffmptf 44687 A function measurable w.r.t. to a sigma-algebra, is actually a function. (Contributed by Glauco Siliprandi, 5-Jan-2025.)
𝑥𝜑    &   𝑥𝐴    &   (𝜑𝑆 ∈ SAlg)    &   ((𝜑𝑥𝐴) → 𝐵𝑉)    &   (𝜑 → (𝑥𝐴𝐵) ∈ (SMblFn‘𝑆))       (𝜑 → (𝑥𝐴𝐵):𝐴⟶ℝ)
 
5-Jan-2025fmptdff 43155 A version of fmptd 7044 using bound-variable hypothesis instead of a distinct variable condition for 𝜑. (Contributed by Glauco Siliprandi, 5-Jan-2025.)
𝑥𝜑    &   𝑥𝐴    &   𝑥𝐶    &   ((𝜑𝑥𝐴) → 𝐵𝐶)    &   𝐹 = (𝑥𝐴𝐵)       (𝜑𝐹:𝐴𝐶)
 
5-Jan-2025fvmptelcdmf 43154 The value of a function at a point of its domain belongs to its codomain. (Contributed by Glauco Siliprandi, 5-Jan-2025.)
𝑥𝐴    &   𝑥𝐶    &   (𝜑 → (𝑥𝐴𝐵):𝐴𝐶)       ((𝜑𝑥𝐴) → 𝐵𝐶)
 
5-Jan-2025fmptff 43153 Functionality of the mapping operation. (Contributed by Glauco Siliprandi, 5-Jan-2025.)
𝑥𝐴    &   𝑥𝐵    &   𝐹 = (𝑥𝐴𝐶)       (∀𝑥𝐴 𝐶𝐵𝐹:𝐴𝐵)
 
5-Jan-2025dmmpt1 43152 The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 5-Jan-2025.)
𝑥𝜑    &   𝑥𝐵    &   ((𝜑𝑥𝐵) → 𝐶𝑉)       (𝜑 → dom (𝑥𝐵𝐶) = 𝐵)
 
5-Jan-2025ssrabdf 42993 Subclass of a restricted class abstraction (deduction form). (Contributed by Glauco Siliprandi, 5-Jan-2025.)
𝑥𝐴    &   𝑥𝐵    &   𝑥𝜑    &   (𝜑𝐵𝐴)    &   ((𝜑𝑥𝐵) → 𝜓)       (𝜑𝐵 ⊆ {𝑥𝐴𝜓})
 
5-Jan-2025ofoacom 41335 Component-wise addition of natural numnber-yielding functions commutes. (Contributed by RP, 5-Jan-2025.)
((𝐴𝑉 ∧ (𝐹 ∈ (ω ↑m 𝐴) ∧ 𝐺 ∈ (ω ↑m 𝐴))) → (𝐹f +o 𝐺) = (𝐺f +o 𝐹))
 
5-Jan-2025ofoaass 41334 Component-wise addition of ordinal-yielding functions is associative. (Contributed by RP, 5-Jan-2025.)
(((𝐴𝑉𝐵 ∈ On) ∧ (𝐹 ∈ (𝐵m 𝐴) ∧ 𝐺 ∈ (𝐵m 𝐴) ∧ 𝐻 ∈ (𝐵m 𝐴))) → ((𝐹f +o 𝐺) ∘f +o 𝐻) = (𝐹f +o (𝐺f +o 𝐻)))
 
5-Jan-2025ofoaid2 41333 Identity law for component wise addition of ordinal-yielding functions. (Contributed by RP, 5-Jan-2025.)
(((𝐴𝑉𝐵 ∈ On) ∧ 𝐹 ∈ (𝐵m 𝐴)) → ((𝐴 × {∅}) ∘f +o 𝐹) = 𝐹)
 
5-Jan-2025ofoaid1 41332 Identity law for component wise addition of ordinal-yielding functions. (Contributed by RP, 5-Jan-2025.)
(((𝐴𝑉𝐵 ∈ On) ∧ 𝐹 ∈ (𝐵m 𝐴)) → (𝐹f +o (𝐴 × {∅})) = 𝐹)
 
5-Jan-2025ofoacl 41331 Closure law for component wise addition of ordinal-yielding functions. (Contributed by RP, 5-Jan-2025.)
(((𝐴𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ (𝐹 ∈ (𝐶m 𝐴) ∧ 𝐺 ∈ (𝐶m 𝐴))) → (𝐹f +o 𝐺) ∈ (𝐶m 𝐴))
 
5-Jan-2025ofoafo 41330 Addition operator for functions from a set into a power of omega is an onto binary operator. (Contributed by RP, 5-Jan-2025.)
((𝐴𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) → ( ∘f +o ↾ ((𝐶m 𝐴) × (𝐶m 𝐴))):((𝐶m 𝐴) × (𝐶m 𝐴))–onto→(𝐶m 𝐴))
 
5-Jan-2025ofoaf 41329 Addition operator for functions from sets into power of omega results in a function from the intersection of sets to that power of omega. (Contributed by RP, 5-Jan-2025.)
(((𝐴𝑉𝐵𝑊𝐶 = (𝐴𝐵)) ∧ (𝐷 ∈ On ∧ 𝐸 = (ω ↑o 𝐷))) → ( ∘f +o ↾ ((𝐸m 𝐴) × (𝐸m 𝐵))):((𝐸m 𝐴) × (𝐸m 𝐵))⟶(𝐸m 𝐶))
 
5-Jan-2025ofoafg 41328 Addition operator for functions from sets into ordinals results in a function from the intersection of sets into an ordinal. (Contributed by RP, 5-Jan-2025.)
(((𝐴𝑉𝐵𝑊𝐶 = (𝐴𝐵)) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = 𝑑𝐷 (𝑑 +o 𝐸))) → ( ∘f +o ↾ ((𝐷m 𝐴) × (𝐸m 𝐵))):((𝐷m 𝐴) × (𝐸m 𝐵))⟶(𝐹m 𝐶))
 
5-Jan-2025oacl2g 41324 Closure law for ordinal addition. Here we show that ordinal addition is closed within the empty set or any ordinal power of omega. (Contributed by RP, 5-Jan-2025.)
(((𝐴𝐶𝐵𝐶) ∧ (𝐶 = ∅ ∨ (𝐶 = (ω ↑o 𝐷) ∧ 𝐷 ∈ On))) → (𝐴 +o 𝐵) ∈ 𝐶)
 
5-Jan-2025rexdif1en 9023 If a set is equinumerous to a nonzero ordinal, then there exists an element in that set such that removing it leaves the set equinumerous to the predecessor of that ordinal. (Contributed by BTernaryTau, 26-Aug-2024.) Generalize to all ordinals and avoid ax-un 7650. (Revised by BTernaryTau, 5-Jan-2025.)
((𝑀 ∈ On ∧ 𝐴 ≈ suc 𝑀) → ∃𝑥𝐴 (𝐴 ∖ {𝑥}) ≈ 𝑀)
 
5-Jan-2025dif1enlem 9021 Lemma for rexdif1en 9023 and dif1en 9025. (Contributed by BTernaryTau, 18-Aug-2024.) Generalize to all ordinals and add a sethood requirement to avoid ax-un 7650. (Revised by BTernaryTau, 5-Jan-2025.)
(((𝐹𝑉𝐴𝑊𝑀 ∈ On) ∧ 𝐹:𝐴1-1-onto→suc 𝑀) → (𝐴 ∖ {(𝐹𝑀)}) ≈ 𝑀)
 
5-Jan-2025imbibi 392 The antecedent of one side of a biconditional can be moved out of the biconditional to become the antecedent of the remaining biconditional. (Contributed by BJ, 1-Jan-2025.) (Proof shortened by Wolf Lammen, 5-Jan-2025.)
(((𝜑𝜓) ↔ 𝜒) → (𝜑 → (𝜓𝜒)))
 
4-Jan-2025en1eqsn 9139 A set with one element is a singleton. (Contributed by FL, 18-Aug-2008.) Avoid ax-pow 5308, ax-un 7650. (Revised by BTernaryTau, 4-Jan-2025.)
((𝐴𝐵𝐵 ≈ 1o) → 𝐵 = {𝐴})
 
4-Jan-2025f1finf1o 9136 Any injection from one finite set to another of equal size must be a bijection. (Contributed by Jeff Madsen, 5-Jun-2010.) (Revised by Mario Carneiro, 27-Feb-2014.) Avoid ax-pow 5308. (Revised by BTernaryTau, 4-Jan-2025.)
((𝐴𝐵𝐵 ∈ Fin) → (𝐹:𝐴1-1𝐵𝐹:𝐴1-1-onto𝐵))
 
3-Jan-2025naddcnfass 41343 Component-wise addition of Cantor normal forms is associative. (Contributed by RP, 3-Jan-2025.)
(((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ (𝐹𝑆𝐺𝑆𝐻𝑆)) → ((𝐹f +o 𝐺) ∘f +o 𝐻) = (𝐹f +o (𝐺f +o 𝐻)))
 
3-Jan-2025naddcnfid2 41342 Identity law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 3-Jan-2025.)
(((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ 𝐹𝑆) → ((𝑋 × {∅}) ∘f +o 𝐹) = 𝐹)
 
3-Jan-2025naddcnfid1 41341 Identity law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 3-Jan-2025.)
(((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ 𝐹𝑆) → (𝐹f +o (𝑋 × {∅})) = 𝐹)
 
3-Jan-2025glbconN 37652 De Morgan's law for GLB and LUB. This holds in any complete ortholattice, although we assume HL for convenience. (Contributed by NM, 17-Jan-2012.) New df-riota 7293. (Revised by SN, 3-Jan-2025.) (New usage is discouraged.)
𝐵 = (Base‘𝐾)    &   𝑈 = (lub‘𝐾)    &   𝐺 = (glb‘𝐾)    &    = (oc‘𝐾)       ((𝐾 ∈ HL ∧ 𝑆𝐵) → (𝐺𝑆) = ( ‘(𝑈‘{𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆})))
 
3-Jan-2025nfra2w 3278 Similar to Lemma 24 of [Monk2] p. 114, except that quantification is restricted. Once derived from hbra2VD 42809. Version of nfra2 3345 with a disjoint variable condition not requiring ax-13 2370. (Contributed by Alan Sare, 31-Dec-2011.) Reduce axiom usage. (Revised by Gino Giotto, 24-Sep-2024.) (Proof shortened by Wolf Lammen, 3-Jan-2025.)
𝑦𝑥𝐴𝑦𝐵 𝜑
 
2-Jan-2025naddcnfcom 41340 Component-wise ordinal addition of Cantor normal forms commutes. (Contributed by RP, 2-Jan-2025.)
(((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ (𝐹𝑆𝐺𝑆)) → (𝐹f +o 𝐺) = (𝐺f +o 𝐹))
 
2-Jan-2025naddcnfcl 41339 Closure law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 2-Jan-2025.)
(((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ (𝐹𝑆𝐺𝑆)) → (𝐹f +o 𝐺) ∈ 𝑆)
 
2-Jan-2025naddcnffo 41338 Addition of Cantor normal forms is a function onto Cantor normal forms. (Contributed by RP, 2-Jan-2025.)
((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) → ( ∘f +o ↾ (𝑆 × 𝑆)):(𝑆 × 𝑆)–onto𝑆)
 
2-Jan-2025naddcnffn 41337 Addition operator for Cantor normal forms is a function. (Contributed by RP, 2-Jan-2025.)
((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) → ( ∘f +o ↾ (𝑆 × 𝑆)) Fn (𝑆 × 𝑆))
 
2-Jan-2025naddcnff 41336 Addition operator for Cantor normal forms is a function into Cantor normal forms. (Contributed by RP, 2-Jan-2025.)
((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) → ( ∘f +o ↾ (𝑆 × 𝑆)):(𝑆 × 𝑆)⟶𝑆)
 
2-Jan-2025isinf 9125 Any set that is not finite is literally infinite, in the sense that it contains subsets of arbitrarily large finite cardinality. (It cannot be proven that the set has countably infinite subsets unless AC is invoked.) The proof does not require the Axiom of Infinity. (Contributed by Mario Carneiro, 15-Jan-2013.) Avoid ax-pow 5308. (Revised by BTernaryTau, 2-Jan-2025.)
𝐴 ∈ Fin → ∀𝑛 ∈ ω ∃𝑥(𝑥𝐴𝑥𝑛))
 
2-Jan-2025ominf 9123 The set of natural numbers is infinite. Corollary 6D(b) of [Enderton] p. 136. (Contributed by NM, 2-Jun-1998.) Avoid ax-pow 5308. (Revised by BTernaryTau, 2-Jan-2025.)
¬ ω ∈ Fin
 
2-Jan-2025dtru 5381 Given any set (the "𝑦 " in the statement), not all sets are equal to it. The same statement without disjoint variable condition is false since it contradicts stdpc6 2030. The same comments and revision history concerning axiom usage as in exneq 5380 apply. (Contributed by NM, 7-Nov-2006.) Extract exneq 5380 as an intermediate result. (Revised by BJ, 2-Jan-2025.)
¬ ∀𝑥 𝑥 = 𝑦
 
2-Jan-2025exneq 5380 Given any set (the "𝑦 " in the statement), there exists a set not equal to it.

The same statement without disjoint variable condition is false, since we do not have 𝑥¬ 𝑥 = 𝑥. This theorem is proved directly from set theory axioms (no class definitions) and does not depend on ax-ext 2707, ax-sep 5243, or ax-pow 5308 nor auxiliary logical axiom schemes ax-10 2136 to ax-13 2370. See dtruALT 5331 for a shorter proof using more axioms, and dtruALT2 5313 for a proof using ax-pow 5308 instead of ax-pr 5372. (Contributed by NM, 7-Nov-2006.) Avoid ax-13 2370. (Revised by BJ, 31-May-2019.) Avoid ax-8 2107. (Revised by SN, 21-Sep-2023.) Avoid ax-12 2170. (Revised by Rohan Ridenour, 9-Oct-2024.) Use ax-pr 5372 instead of ax-pow 5308. (Revised by BTernaryTau, 3-Dec-2024.) Extract this result from the proof of dtru 5381. (Revised by BJ, 2-Jan-2025.)

𝑥 ¬ 𝑥 = 𝑦
 
2-Jan-2025exexneq 5379 There exist two different sets. (Contributed by NM, 7-Nov-2006.) Avoid ax-13 2370. (Revised by BJ, 31-May-2019.) Avoid ax-8 2107. (Revised by SN, 21-Sep-2023.) Avoid ax-12 2170. (Revised by Rohan Ridenour, 9-Oct-2024.) Use ax-pr 5372 instead of ax-pow 5308. (Revised by BTernaryTau, 3-Dec-2024.) Extract this result from the proof of dtru 5381. (Revised by BJ, 2-Jan-2025.)
𝑥𝑦 ¬ 𝑥 = 𝑦
 
2-Jan-2025ralcom13 3273 Swap first and third restricted universal quantifiers. (Contributed by AV, 3-Dec-2021.) (Proof shortened by Wolf Lammen, 2-Jan-2025.)
(∀𝑥𝐴𝑦𝐵𝑧𝐶 𝜑 ↔ ∀𝑧𝐶𝑦𝐵𝑥𝐴 𝜑)
 
1-Jan-2025snssg 4731 The singleton formed on a set is included in a class if and only if the set is an element of that class. Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 22-Jul-2001.) (Proof shortened by BJ, 1-Jan-2025.)
(𝐴𝑉 → (𝐴𝐵 ↔ {𝐴} ⊆ 𝐵))
 
1-Jan-2025snssb 4730 Characterization of the inclusion of a singleton in a class. (Contributed by BJ, 1-Jan-2025.)
({𝐴} ⊆ 𝐵 ↔ (𝐴 ∈ V → 𝐴𝐵))
 
31-Dec-2024mpets 37117 Member Partition-Equivalence Theorem in its shortest possible form: it shows that member partitions and comember equivalence relations are literally the same. Cf. pet 37126, the Partition-Equivalence Theorem, with general 𝑅. (Contributed by Peter Mazsa, 31-Dec-2024.)
MembParts = CoMembErs
 
31-Dec-2024cpet 37113 The conventional form of Member Partition-Equivalence Theorem. In the conventional case there is no (general) disjoint and no (general) partition concept: mathematicians have been calling disjoint or partition what we call element disjoint or member partition, see also cpet2 37112. Cf. mpet 37114, mpet2 37115 and mpet3 37111 for unconventional forms of Member Partition-Equivalence Theorem. Cf. pet 37126 and pet2 37125 for Partition-Equivalence Theorem with general 𝑅. (Contributed by Peter Mazsa, 31-Dec-2024.)
( MembPart 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ ( 𝐴 /𝐴) = 𝐴))
 
31-Dec-2024eqvrelcossid 37069 The cosets by the identity class are in equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2024.)
EqvRel ≀ I
 
31-Dec-2024eqvrelcoss0 37063 The cosets by the null class are in equivalence relation. (Contributed by Peter Mazsa, 31-Dec-2024.)
EqvRel ≀ ∅
 
31-Dec-2024eldisjn0elb 37020 Two forms of disjoint elements when the empty set is not an element of the class. (Contributed by Peter Mazsa, 31-Dec-2024.)
(( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴) ↔ ( Disj ( E ↾ 𝐴) ∧ (dom ( E ↾ 𝐴) / ( E ↾ 𝐴)) = 𝐴))
 
31-Dec-2024suceqsneq 36507 One-to-one relationship between the successor operation and the singleton. (Contributed by Peter Mazsa, 31-Dec-2024.)
(𝐴𝑉 → (suc 𝐴 = suc 𝐵 ↔ {𝐴} = {𝐵}))
 
30-Dec-2024muldmmbl2 44719 If two functions have domains in the sigma-algebra, the domain of their multiplication also belongs to the sigma-algebra. This is the second statement of Proposition 121H of [Fremlin1], p. 39. Note: While the theorem in the book assumes the functions are sigma-measurable, this assumption is unnecessary for the part concerning their multiplication. (Contributed by Glauco Siliprandi, 30-Dec-2024.)
𝑥𝐹    &   𝑥𝐺    &   (𝜑𝑆 ∈ SAlg)    &   (𝜑 → dom 𝐹𝑆)    &   (𝜑 → dom 𝐺𝑆)    &   𝐻 = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥) · (𝐺𝑥)))       (𝜑 → dom 𝐻𝑆)
 
30-Dec-2024muldmmbl 44718 If two functions have domains in the sigma-algebra, the domain of their multiplication also belongs to the sigma-algebra. This is the second statement of Proposition 121H of [Fremlin1], p. 39. Note: While the theorem in the book assumes the functions are sigma-measurable, this assumption is unnecessary for the part concerning their multiplication. (Contributed by Glauco Siliprandi, 30-Dec-2024.)
𝑥𝜑    &   𝑥𝐴    &   𝑥𝐵    &   (𝜑𝑆 ∈ SAlg)    &   (𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)       (𝜑 → dom (𝑥 ∈ (𝐴𝐵) ↦ (𝐶 · 𝐷)) ∈ 𝑆)
 
30-Dec-2024adddmmbl2 44717 If two functions have domains in the sigma-algebra, the domain of their addition also belongs to the sigma-algebra. This is the first statement of Proposition 121H of [Fremlin1], p. 39. Note: While the theorem in the book assumes the functions are sigma-measurable, this assumption is unnecessary for the part concerning their addition. (Contributed by Glauco Siliprandi, 30-Dec-2024.)
𝑥𝐹    &   𝑥𝐺    &   (𝜑𝑆 ∈ SAlg)    &   (𝜑 → dom 𝐹𝑆)    &   (𝜑 → dom 𝐺𝑆)    &   𝐻 = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥) + (𝐺𝑥)))       (𝜑 → dom 𝐻𝑆)
 
30-Dec-2024adddmmbl 44716 If two functions have domains in the sigma-algebra, the domain of their addition also belongs to the sigma-algebra. This is the first statement of Proposition 121H of [Fremlin1], p. 39. Note: While the theorem in the book assumes the functions are sigma-measurable, this assumption is unnecessary for the part concerning their addition. (Contributed by Glauco Siliprandi, 30-Dec-2024.)
𝑥𝜑    &   𝑥𝐴    &   𝑥𝐵    &   (𝜑𝑆 ∈ SAlg)    &   (𝜑𝐴𝑆)    &   (𝜑𝐵𝑆)       (𝜑 → dom (𝑥 ∈ (𝐴𝐵) ↦ (𝐶 + 𝐷)) ∈ 𝑆)
 
30-Dec-2024cpet2 37112 The conventional form of the Member Partition-Equivalence Theorem. In the conventional case there is no (general) disjoint and no (general) partition concept: mathematicians have called disjoint or partition what we call element disjoint or member partition, see also cpet 37113. Together with cpet 37113, mpet 37114 mpet2 37115, this is what we used to think of as the partition equivalence theorem (but cf. pet2 37125 with general 𝑅). (Contributed by Peter Mazsa, 30-Dec-2024.)
(( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴) ↔ ( EqvRel ∼ 𝐴 ∧ ( 𝐴 /𝐴) = 𝐴))
 
30-Dec-2024fences3 37105 Implication of eqvrelqseqdisj2 37104 and n0eldmqseq 36924, see comment of fences 37119. (Contributed by Peter Mazsa, 30-Dec-2024.)
(( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) → ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴))
 
30-Dec-2024eldisjim2 37060 Alternate form of eldisjim 37059. (Contributed by Peter Mazsa, 30-Dec-2024.)
( ElDisj 𝐴 → EqvRel ∼ 𝐴)
 
30-Dec-2024eqvreldmqs2 36951 Two ways to express comember equivalence relation on its domain quotient. (Contributed by Peter Mazsa, 30-Dec-2024.)
(( EqvRel ≀ ( E ↾ 𝐴) ∧ (dom ≀ ( E ↾ 𝐴) / ≀ ( E ↾ 𝐴)) = 𝐴) ↔ ( EqvRel ∼ 𝐴 ∧ ( 𝐴 /𝐴) = 𝐴))
 
30-Dec-2024n0elim 36925 Implication of that the empty set is not an element of a class. (Contributed by Peter Mazsa, 30-Dec-2024.)
(¬ ∅ ∈ 𝐴 → (dom ( E ↾ 𝐴) / ( E ↾ 𝐴)) = 𝐴)
 
30-Dec-2024pr2ne 9861 If an unordered pair has two elements, then they are different. (Contributed by FL, 14-Feb-2010.) Avoid ax-pow 5308, ax-un 7650. (Revised by BTernaryTau, 30-Dec-2024.)
((𝐴𝐶𝐵𝐷) → ({𝐴, 𝐵} ≈ 2o𝐴𝐵))
 
30-Dec-2024enpr2 9859 An unordered pair with distinct elements is equinumerous to ordinal two. This is a closed-form version of enpr2d 8914. (Contributed by FL, 17-Aug-2008.) Avoid ax-pow 5308, ax-un 7650. (Revised by BTernaryTau, 30-Dec-2024.)
((𝐴𝐶𝐵𝐷𝐴𝐵) → {𝐴, 𝐵} ≈ 2o)
 
30-Dec-20241sdom 9113 A set that strictly dominates ordinal 1 has at least 2 different members. (Closely related to 2dom 8895.) (Contributed by Mario Carneiro, 12-Jan-2013.) Avoid ax-un 7650. (Revised by BTernaryTau, 30-Dec-2024.)
(𝐴𝑉 → (1o𝐴 ↔ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 = 𝑦))
 
30-Dec-2024rex2dom 9111 A set that has at least 2 different members dominates ordinal 2. (Contributed by BTernaryTau, 30-Dec-2024.)
((𝐴𝑉 ∧ ∃𝑥𝐴𝑦𝐴 𝑥𝑦) → 2o𝐴)
 
29-Dec-2024dffun2 6489 Alternate definition of a function. (Contributed by NM, 29-Dec-1996.) Avoid ax-10 2136, ax-12 2170. (Revised by SN, 19-Dec-2024.) Avoid ax-11 2153. (Revised by BTernaryTau, 29-Dec-2024.)
(Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥𝑦𝑧((𝑥𝐴𝑦𝑥𝐴𝑧) → 𝑦 = 𝑧)))
 
29-Dec-2024cnvsym 6052 Two ways of saying a relation is symmetric. Similar to definition of symmetry in [Schechter] p. 51. (Contributed by NM, 28-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof shortened by SN, 23-Dec-2024.) Avoid ax-11 2153. (Revised by BTernaryTau, 29-Dec-2024.)
(𝑅𝑅 ↔ ∀𝑥𝑦(𝑥𝑅𝑦𝑦𝑅𝑥))
 
29-Dec-2024cotrg 6047 Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr 6050 for the main application. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Generalized from its special instance cotr 6050. (Revised by Richard Penner, 24-Dec-2019.) (Proof shortened by SN, 19-Dec-2024.) Avoid ax-11 2153. (Revised by BTernaryTau, 29-Dec-2024.)
((𝐴𝐵) ⊆ 𝐶 ↔ ∀𝑥𝑦𝑧((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))
 
28-Dec-2024onunisuc 6410 An ordinal number is equal to the union of its successor. (Contributed by NM, 12-Jun-1994.) Generalize from onunisuci 6420. (Revised by BJ, 28-Dec-2024.)
(𝐴 ∈ On → suc 𝐴 = 𝐴)
 
28-Dec-2024unisucg 6379 A transitive class is equal to the union of its successor, closed form. Combines Theorem 4E of [Enderton] p. 72 and Exercise 6 of [Enderton] p. 73. (Contributed by NM, 30-Aug-1993.) Generalize from unisuc 6380. (Revised by BJ, 28-Dec-2024.)
(𝐴𝑉 → (Tr 𝐴 suc 𝐴 = 𝐴))
 
28-Dec-2024unisucs 6378 The union of the successor of a set is equal to the binary union of that set with its union. (Contributed by NM, 30-Aug-1993.) Extract from unisuc 6380. (Revised by BJ, 28-Dec-2024.)
(𝐴𝑉 suc 𝐴 = ( 𝐴𝐴))
 
28-Dec-2024dftr5 5213 An alternate way of defining a transitive class. (Contributed by NM, 20-Mar-2004.) Avoid ax-11 2153. (Revised by BTernaryTau, 28-Dec-2024.)
(Tr 𝐴 ↔ ∀𝑥𝐴𝑦𝑥 𝑦𝐴)
 
28-Dec-2024dftr2c 5212 Variant of dftr2 5211 with commuted quantifiers, useful for shortening proofs and avoiding ax-11 2153. (Contributed by BTernaryTau, 28-Dec-2024.)
(Tr 𝐴 ↔ ∀𝑦𝑥((𝑥𝑦𝑦𝐴) → 𝑥𝐴))
 
28-Dec-2024unissb 4887 Relationship involving membership, subset, and union. Exercise 5 of [Enderton] p. 26 and its converse. (Contributed by NM, 20-Sep-2003.) Avoid ax-11 2153. (Revised by BTernaryTau, 28-Dec-2024.)
( 𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
 
28-Dec-2024alcomw 2046 Weak version of alcom 2155 and biconditional form of alcomiw 2045. Uses only Tarski's FOL axiom schemes. (Contributed by BTernaryTau, 28-Dec-2024.)
(𝑥 = 𝑤 → (𝜑𝜓))    &   (𝑦 = 𝑧 → (𝜑𝜒))       (∀𝑥𝑦𝜑 ↔ ∀𝑦𝑥𝜑)
 
25-Dec-2024partimeq 37084 Partition implies that the class of coelements on the natural domain is equal to the class of cosets of the relation, cf. erimeq 36954. (Contributed by Peter Mazsa, 25-Dec-2024.)
(𝑅𝑉 → (𝑅 Part 𝐴 → ∼ 𝐴 = ≀ 𝑅))
 
23-Dec-2024rmxyelqirr 41002 The solutions used to construct the X and Y sequences are quadratic irrationals. (Contributed by Stefan O'Rear, 21-Sep-2014.) (Proof shortened by SN, 23-Dec-2024.)
((𝐴 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁) ∈ {𝑎 ∣ ∃𝑐 ∈ ℕ0𝑑 ∈ ℤ 𝑎 = (𝑐 + ((√‘((𝐴↑2) − 1)) · 𝑑))})
 
23-Dec-20241sdom2dom 9112 Strict dominance over 1 is the same as dominance over 2. (Contributed by BTernaryTau, 23-Dec-2024.)
(1o𝐴 ↔ 2o𝐴)
 
23-Dec-2024enpr2d 8914 A pair with distinct elements is equinumerous to ordinal two. (Contributed by Rohan Ridenour, 3-Aug-2023.) Avoid ax-un 7650. (Revised by BTernaryTau, 23-Dec-2024.)
(𝜑𝐴𝐶)    &   (𝜑𝐵𝐷)    &   (𝜑 → ¬ 𝐴 = 𝐵)       (𝜑 → {𝐴, 𝐵} ≈ 2o)
 
23-Dec-2024en2prd 8913 Two unordered pairs are equinumerous. (Contributed by BTernaryTau, 23-Dec-2024.)
(𝜑𝐴𝑉)    &   (𝜑𝐵𝑊)    &   (𝜑𝐶𝑋)    &   (𝜑𝐷𝑌)    &   (𝜑𝐴𝐵)    &   (𝜑𝐶𝐷)       (𝜑 → {𝐴, 𝐵} ≈ {𝐶, 𝐷})
 
23-Dec-2024tz6.12-1 6848 Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27. (Contributed by NM, 30-Apr-2004.) (Proof shortened by SN, 23-Dec-2024.)
((𝐴𝐹𝑦 ∧ ∃!𝑦 𝐴𝐹𝑦) → (𝐹𝐴) = 𝑦)
 
23-Dec-2024tz6.12c 6847 Corollary of Theorem 6.12(1) of [TakeutiZaring] p. 27. (Contributed by NM, 30-Apr-2004.) (Proof shortened by SN, 23-Dec-2024.)
(∃!𝑦 𝐴𝐹𝑦 → ((𝐹𝐴) = 𝑦𝐴𝐹𝑦))
 
23-Dec-2024relssdmrn 6206 A relation is included in the Cartesian product of its domain and range. Exercise 4.12(t) of [Mendelson] p. 235. (Contributed by NM, 3-Aug-1994.) (Proof shortened by SN, 23-Dec-2024.)
(Rel 𝐴𝐴 ⊆ (dom 𝐴 × ran 𝐴))
 
23-Dec-2024cnvsymOLD 6053 Obsolete proof of cnvsym 6052 as of 29-Dec-2024. (Contributed by NM, 28-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof shortened by SN, 23-Dec-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
(𝑅𝑅 ↔ ∀𝑥𝑦(𝑥𝑅𝑦𝑦𝑅𝑥))
 
23-Dec-2024exel 5378 There exist two sets, one a member of the other.

This theorem looks similar to el 5382, but its meaning is different. It only depends on the axioms ax-mp 5 to ax-4 1810, ax-6 1970, and ax-pr 5372. This theorem does not exclude that these two sets could actually be one single set containing itself. That two different sets exist is proved by exexneq 5379. (Contributed by SN, 23-Dec-2024.)

𝑦𝑥 𝑥𝑦
 
23-Dec-2024rexlimivw 3144 Weaker version of rexlimiv 3141. (Contributed by FL, 19-Sep-2011.) (Proof shortened by Wolf Lammen, 23-Dec-2024.)
(𝜑𝜓)       (∃𝑥𝐴 𝜑𝜓)
 
23-Dec-2024rexlimiva 3140 Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Dec-2006.) Shorten dependent theorems. (Revised by Wolf lammen, 23-Dec-2024.)
((𝑥𝐴𝜑) → 𝜓)       (∃𝑥𝐴 𝜑𝜓)
 
22-Dec-2024ssabdv 40454 Deduction of abstraction subclass from implication. (Contributed by SN, 22-Dec-2024.)
(𝜑 → (𝑥𝐴𝜓))       (𝜑𝐴 ⊆ {𝑥𝜓})
 
22-Dec-2024ss2ab1 40453 Class abstractions in a subclass relationship, closed form. One direction of ss2ab 4004 using fewer axioms. (Contributed by SN, 22-Dec-2024.)
(∀𝑥(𝜑𝜓) → {𝑥𝜑} ⊆ {𝑥𝜓})
 
22-Dec-2024mainpart 37118 Partition with general 𝑅 also imply member partition. (Contributed by Peter Mazsa, 23-Sep-2021.) (Revised by Peter Mazsa, 22-Dec-2024.)
(𝑅 Part 𝐴 → MembPart 𝐴)
 
22-Dec-2024partimcomember 37110 Partition with general 𝑅 (in addition to the member partition cf. mpet 37114 and mpet2 37115) implies equivalent comembers. (Contributed by Peter Mazsa, 23-Sep-2021.) (Revised by Peter Mazsa, 22-Dec-2024.)
(𝑅 Part 𝐴 → CoMembEr 𝐴)
 
22-Dec-2024abssdv 4013 Deduction of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.) (Proof shortened by SN, 22-Dec-2024.)
(𝜑 → (𝜓𝑥𝐴))       (𝜑 → {𝑥𝜓} ⊆ 𝐴)
 
22-Dec-2024r19.29 3113 Restricted quantifier version of 19.29 1875. See also r19.29r 3115. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 22-Dec-2024.)
((∀𝑥𝐴 𝜑 ∧ ∃𝑥𝐴 𝜓) → ∃𝑥𝐴 (𝜑𝜓))
 
22-Dec-2024r19.35 3107 Restricted quantifier version of 19.35 1879. (Contributed by NM, 20-Sep-2003.) (Proof shortened by Wolf Lammen, 22-Dec-2024.)
(∃𝑥𝐴 (𝜑𝜓) ↔ (∀𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓))
 
22-Dec-2024ralcom3 3096 A commutation law for restricted universal quantifiers that swaps the domains of the restriction. (Contributed by NM, 22-Feb-2004.) (Proof shortened by Wolf Lammen, 22-Dec-2024.)
(∀𝑥𝐴 (𝑥𝐵𝜑) ↔ ∀𝑥𝐵 (𝑥𝐴𝜑))
 
21-Dec-2024salrestss 44244 A sigma-algebra restricted to one of its elements is a subset of the original sigma-algebra. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
(𝜑𝑆 ∈ SAlg)    &   (𝜑𝐸𝑆)       (𝜑 → (𝑆t 𝐸) ⊆ 𝑆)
 
21-Dec-2024pimxrneun 43372 The preimage of a set of extended reals that does not contain a value 𝐶 is the union of the preimage of the elements smaller than 𝐶 and the preimage of the subset of elements larger than 𝐶. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
𝑥𝜑    &   ((𝜑𝑥𝐴) → 𝐵 ∈ ℝ*)    &   ((𝜑𝑥𝐴) → 𝐶 ∈ ℝ*)       (𝜑 → {𝑥𝐴𝐵𝐶} = ({𝑥𝐴𝐵 < 𝐶} ∪ {𝑥𝐴𝐶 < 𝐵}))
 
21-Dec-2024mpteq2dfa 43151 Slightly more general equality inference for the maps-to notation. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
𝑥𝜑    &   ((𝜑𝑥𝐴) → 𝐵 = 𝐶)       (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
 
21-Dec-2024dmmptif 43150 Domain of the mapping operation. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
𝑥𝐴    &   𝐵 ∈ V    &   𝐹 = (𝑥𝐴𝐵)       dom 𝐹 = 𝐴
 
21-Dec-2024fnmptif 43149 Functionality and domain of an ordered-pair class abstraction. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
𝑥𝐴    &   𝐵 ∈ V    &   𝐹 = (𝑥𝐴𝐵)       𝐹 Fn 𝐴
 
21-Dec-2024dmmptdff 43098 The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
𝑥𝜑    &   𝑥𝐵    &   𝐴 = (𝑥𝐵𝐶)    &   ((𝜑𝑥𝐵) → 𝐶𝑉)       (𝜑 → dom 𝐴 = 𝐵)
 
21-Dec-2024toprestsubel 43037 A subset is open in the topology it generates via restriction. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
(𝜑𝐽 ∈ Top)    &   (𝜑𝐴 𝐽)       (𝜑𝐴 ∈ (𝐽t 𝐴))
 
21-Dec-2024restsubel 43036 A subset belongs in the space it generates via restriction. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
(𝜑𝐽𝑉)    &   (𝜑 𝐽𝐽)    &   (𝜑𝐴 𝐽)       (𝜑𝐴 ∈ (𝐽t 𝐴))
 
21-Dec-2024restopnssd 43035 A topology restricted to an open set is a subset of the original topology. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
(𝜑𝐽 ∈ Top)    &   (𝜑𝐴𝐽)       (𝜑 → (𝐽t 𝐴) ⊆ 𝐽)
 
21-Dec-2024restopn3 43034 If 𝐴 is open, then 𝐴 is open in the restriction to itself. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
((𝐽 ∈ Top ∧ 𝐴𝐽) → 𝐴 ∈ (𝐽t 𝐴))
 
21-Dec-2024ss2rabdf 43033 Deduction of restricted abstraction subclass from implication. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
𝑥𝜑    &   ((𝜑𝑥𝐴) → (𝜓𝜒))       (𝜑 → {𝑥𝐴𝜓} ⊆ {𝑥𝐴𝜒})
 
21-Dec-2024inopnd 43032 The intersection of two open sets of a topology is an open set. (Contributed by Glauco Siliprandi, 21-Dec-2024.)
(𝜑𝐽 ∈ Top)    &   (𝜑𝐴𝐽)    &   (𝜑𝐵𝐽)       (𝜑 → (𝐴𝐵) ∈ 𝐽)
 
20-Dec-2024smfpimgtxrmpt 44668 Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded above is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) (Revised by Glauco Siliprandi, 20-Dec-2024.)
𝑥𝜑    &   (𝜑𝑆 ∈ SAlg)    &   ((𝜑𝑥𝐴) → 𝐵𝑉)    &   (𝜑 → (𝑥𝐴𝐵) ∈ (SMblFn‘𝑆))    &   (𝜑𝐿 ∈ ℝ*)       (𝜑 → {𝑥𝐴𝐿 < 𝐵} ∈ (𝑆t 𝐴))
 
20-Dec-2024smfpimgtxrmptf 44667 Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded above is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 20-Dec-2024.)
𝑥𝜑    &   𝑥𝐴    &   (𝜑𝑆 ∈ SAlg)    &   ((𝜑𝑥𝐴) → 𝐵𝑉)    &   (𝜑 → (𝑥𝐴𝐵) ∈ (SMblFn‘𝑆))    &   (𝜑𝐿 ∈ ℝ*)       (𝜑 → {𝑥𝐴𝐿 < 𝐵} ∈ (𝑆t 𝐴))
 
20-Dec-2024smfpimltxrmpt 44642 Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded below is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) (Revised by Glauco Siliprandi, 20-Dec-2024.)
𝑥𝜑    &   (𝜑𝑆 ∈ SAlg)    &   ((𝜑𝑥𝐴) → 𝐵𝑉)    &   (𝜑 → (𝑥𝐴𝐵) ∈ (SMblFn‘𝑆))    &   (𝜑𝑅 ∈ ℝ*)       (𝜑 → {𝑥𝐴𝐵 < 𝑅} ∈ (𝑆t 𝐴))
 
20-Dec-2024smfpimltxrmptf 44641 Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded below is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 20-Dec-2024.)
𝑥𝜑    &   𝑥𝐴    &   (𝜑𝑆 ∈ SAlg)    &   ((𝜑𝑥𝐴) → 𝐵𝑉)    &   (𝜑 → (𝑥𝐴𝐵) ∈ (SMblFn‘𝑆))    &   (𝜑𝑅 ∈ ℝ*)       (𝜑 → {𝑥𝐴𝐵 < 𝑅} ∈ (𝑆t 𝐴))
 
20-Dec-2024pimgtmnf 44606 Given a real-valued function, the preimage of an open interval, unbounded above, with lower bound -∞, is the whole domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) (Revised by Glauco Siliprandi, 20-Dec-2024.)
𝑥𝜑    &   ((𝜑𝑥𝐴) → 𝐵 ∈ ℝ)       (𝜑 → {𝑥𝐴 ∣ -∞ < 𝐵} = 𝐴)
 
20-Dec-2024pimgtmnff 44605 Given a real-valued function, the preimage of an open interval, unbounded above, with lower bound -∞, is the whole domain. (Contributed by Glauco Siliprandi, 20-Dec-2024.)
𝑥𝜑    &   𝑥𝐴    &   ((𝜑𝑥𝐴) → 𝐵 ∈ ℝ)       (𝜑 → {𝑥𝐴 ∣ -∞ < 𝐵} = 𝐴)
 
20-Dec-2024pimltpnf 44587 Given a real-valued function, the preimage of an open interval, unbounded below, with upper bound +∞, is the whole domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) (Revised by Glauco Siliprandi, 20-Dec-2024.)
𝑥𝜑    &   ((𝜑𝑥𝐴) → 𝐵 ∈ ℝ)       (𝜑 → {𝑥𝐴𝐵 < +∞} = 𝐴)
 
20-Dec-2024pimltpnff 44586 Given a real-valued function, the preimage of an open interval, unbounded below, with upper bound +∞, is the whole domain. (Contributed by Glauco Siliprandi, 20-Dec-2024.)
𝑥𝜑    &   𝑥𝐴    &   ((𝜑𝑥𝐴) → 𝐵 ∈ ℝ)       (𝜑 → {𝑥𝐴𝐵 < +∞} = 𝐴)
 
19-Dec-2024isarep1 6573 Part of a study of the Axiom of Replacement used by the Isabelle prover. The object PrimReplace is apparently the image of the function encoded by 𝜑(𝑥, 𝑦) i.e. the class ({⟨𝑥, 𝑦⟩ ∣ 𝜑} “ 𝐴). If so, we can prove Isabelle's "Axiom of Replacement" conclusion without using the Axiom of Replacement, for which I (N. Megill) currently have no explanation. (Contributed by NM, 26-Oct-2006.) (Proof shortened by Mario Carneiro, 4-Dec-2016.) (Proof shortened by SN, 19-Dec-2024.)
(𝑏 ∈ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} “ 𝐴) ↔ ∃𝑥𝐴 [𝑏 / 𝑦]𝜑)
 
19-Dec-2024funimaexg 6570 Axiom of Replacement using abbreviations. Axiom 39(vi) of [Quine] p. 284. Compare Exercise 9 of [TakeutiZaring] p. 29. (Contributed by NM, 10-Sep-2006.) Shorten proof and avoid ax-10 2136, ax-12 2170. (Revised by SN, 19-Dec-2024.)
((Fun 𝐴𝐵𝐶) → (𝐴𝐵) ∈ V)
 
19-Dec-2024funmo 6499 A function has at most one value for each argument. (Contributed by NM, 24-May-1998.) (Proof shortened by SN, 19-Dec-2024.)
(Fun 𝐹 → ∃*𝑦 𝐴𝐹𝑦)
 
19-Dec-2024dffun3 6493 Alternate definition of function. (Contributed by NM, 29-Dec-1996.) (Proof shortened by SN, 19-Dec-2024.)
(Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥𝑧𝑦(𝑥𝐴𝑦𝑦 = 𝑧)))
 
19-Dec-2024dffun6 6492 Alternate definition of a function using "at most one" notation. (Contributed by NM, 9-Mar-1995.) Avoid ax-10 2136, ax-12 2170. (Revised by SN, 19-Dec-2024.)
(Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∃*𝑦 𝑥𝐹𝑦))
 
19-Dec-2024dffun2OLD 6490 Obsolete version of dffun2 6489 as of 29-Dec-2024. (Contributed by NM, 29-Dec-1996.) Avoid ax-10 2136, ax-12 2170. (Revised by SN, 19-Dec-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
(Fun 𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥𝑦𝑧((𝑥𝐴𝑦𝑥𝐴𝑧) → 𝑦 = 𝑧)))
 
19-Dec-2024cotrgOLD 6048 Obsolete version of cotrg 6047 as of 29-Dec-2024. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Generalized from its special instance cotr 6050. (Revised by Richard Penner, 24-Dec-2019.) (Proof shortened by SN, 19-Dec-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
((𝐴𝐵) ⊆ 𝐶 ↔ ∀𝑥𝑦𝑧((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))
 
19-Dec-2024difopab 5772 Difference of two ordered-pair class abstractions. (Contributed by Stefan O'Rear, 17-Jan-2015.) (Proof shortened by SN, 19-Dec-2024.)
({⟨𝑥, 𝑦⟩ ∣ 𝜑} ∖ {⟨𝑥, 𝑦⟩ ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ ¬ 𝜓)}
 
15-Dec-2024smfpimgtxr 44663 Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded above is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) (Revised by Glauco Siliprandi, 15-Dec-2024.)
𝑥𝐹    &   (𝜑𝑆 ∈ SAlg)    &   (𝜑𝐹 ∈ (SMblFn‘𝑆))    &   𝐷 = dom 𝐹    &   (𝜑𝐴 ∈ ℝ*)       (𝜑 → {𝑥𝐷𝐴 < (𝐹𝑥)} ∈ (𝑆t 𝐷))
 
15-Dec-2024smfpimltxr 44630 Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded below is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) (Revised by Glauco Siliprandi, 15-Dec-2024.)
𝑥𝐹    &   (𝜑𝑆 ∈ SAlg)    &   (𝜑𝐹 ∈ (SMblFn‘𝑆))    &   𝐷 = dom 𝐹    &   (𝜑𝐴 ∈ ℝ*)       (𝜑 → {𝑥𝐷 ∣ (𝐹𝑥) < 𝐴} ∈ (𝑆t 𝐷))
 
15-Dec-2024pimltpnf2 44596 Given a real-valued function, the preimage of an open interval, unbounded below, with upper bound +∞, is the whole domain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) (Revised by Glauco Siliprandi, 15-Dec-2024.)
𝑥𝐹    &   (𝜑𝐹:𝐴⟶ℝ)       (𝜑 → {𝑥𝐴 ∣ (𝐹𝑥) < +∞} = 𝐴)
 
15-Dec-2024pimltpnf2f 44595 Given a real-valued function, the preimage of an open interval, unbounded below, with upper bound +∞, is the whole domain. (Contributed by Glauco Siliprandi, 15-Dec-2024.)
𝑥𝐹    &   𝑥𝐴    &   (𝜑𝐹:𝐴⟶ℝ)       (𝜑 → {𝑥𝐴 ∣ (𝐹𝑥) < +∞} = 𝐴)
 
15-Dec-2024pimgtpnf2 44589 Given a real-valued function, the preimage of an open interval, unbounded above, with lower bound +∞, is the empty set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) (Revised by Glauco Siliprandi, 15-Dec-2024.)
𝑥𝐹    &   (𝜑𝐹:𝐴⟶ℝ)       (𝜑 → {𝑥𝐴 ∣ +∞ < (𝐹𝑥)} = ∅)
 
15-Dec-2024pimltmnf2 44581 Given a real-valued function, the preimage of an open interval, unbounded below, with upper bound -∞, is the empty set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) (Revised by Glauco Siliprandi, 15-Dec-2024.)
𝑥𝐹    &   (𝜑𝐹:𝐴⟶ℝ)       (𝜑 → {𝑥𝐴 ∣ (𝐹𝑥) < -∞} = ∅)
 
15-Dec-2024pimltmnf2f 44580 Given a real-valued function, the preimage of an open interval, unbounded below, with upper bound -∞, is the empty set. (Contributed by Glauco Siliprandi, 15-Dec-2024.)
𝑥𝐹    &   𝑥𝐴    &   (𝜑𝐹:𝐴⟶ℝ)       (𝜑 → {𝑥𝐴 ∣ (𝐹𝑥) < -∞} = ∅)
 
14-Dec-2024fzuntgd 41395 Union of two adjacent or overlapping finite sets of sequential integers. (Contributed by RP, 14-Dec-2024.)
(𝜑𝐾 ∈ ℤ)    &   (𝜑𝐿 ∈ ℤ)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝑁 ∈ ℤ)    &   (𝜑𝐾𝑀)    &   (𝜑𝑀 ≤ (𝐿 + 1))    &   (𝜑𝐿𝑁)       (𝜑 → ((𝐾...𝐿) ∪ (𝑀...𝑁)) = (𝐾...𝑁))
 
14-Dec-2024fzunt1d 41394 Union of two overlapping finite sets of sequential integers. (Contributed by RP, 14-Dec-2024.)
(𝜑𝐾 ∈ ℤ)    &   (𝜑𝐿 ∈ ℤ)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝑁 ∈ ℤ)    &   (𝜑𝐾𝑀)    &   (𝜑𝑀𝐿)    &   (𝜑𝐿𝑁)       (𝜑 → ((𝐾...𝐿) ∪ (𝑀...𝑁)) = (𝐾...𝑁))
 
14-Dec-2024fzuntd 41393 Union of two adjacent finite sets of sequential integers that share a common endpoint. (Contributed by RP, 14-Dec-2024.)
(𝜑𝐾 ∈ ℤ)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝑁 ∈ ℤ)    &   (𝜑𝐾𝑀)    &   (𝜑𝑀𝑁)       (𝜑 → ((𝐾...𝑀) ∪ (𝑀...𝑁)) = (𝐾...𝑁))
 
14-Dec-2024fzunt 41392 Union of two adjacent finite sets of sequential integers that share a common endpoint. (Suggested by NM, 21-Jul-2005.) (Contributed by RP, 14-Dec-2024.)
(((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾𝑀𝑀𝑁)) → ((𝐾...𝑀) ∪ (𝑀...𝑁)) = (𝐾...𝑁))
 
13-Dec-2024nlim4 41382 4 is not a limit ordinal. (Contributed by RP, 13-Dec-2024.)
¬ Lim 4o
 
13-Dec-2024nlim3 41381 3 is not a limit ordinal. (Contributed by RP, 13-Dec-2024.)
¬ Lim 3o
 
13-Dec-2024nlim2NEW 41380 2 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024.) (Proof shortened by RP, 13-Dec-2024.)
¬ Lim 2o
 
13-Dec-2024nlim1NEW 41379 1 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024.) (Proof shortened by RP, 13-Dec-2024.)
¬ Lim 1o
 
13-Dec-2024nlimsuc 41378 A successor is not a limit ordinal. (Contributed by RP, 13-Dec-2024.)
(𝐴 ∈ On → ¬ Lim suc 𝐴)
 
13-Dec-2024wksonproplem 28360 Lemma for theorems for properties of walks between two vertices, e.g., trlsonprop 28364. (Contributed by AV, 16-Jan-2021.) Remove is-walk hypothesis. (Revised by SN, 13-Dec-2024.)
𝑉 = (Vtx‘𝐺)    &   (((𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝐴(𝑊𝐺)𝐵)𝑃 ↔ (𝐹(𝐴(𝑂𝐺)𝐵)𝑃𝐹(𝑄𝐺)𝑃)))    &   𝑊 = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑎(𝑂𝑔)𝑏)𝑝𝑓(𝑄𝑔)𝑝)}))       (𝐹(𝐴(𝑊𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴𝑉𝐵𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(𝑂𝐺)𝐵)𝑃𝐹(𝑄𝐺)𝑃)))
 
13-Dec-2024mptmpoopabovd 7990 The operation value of a function value of a collection of ordered pairs of related elements. (Contributed by Alexander van der Vekens, 8-Nov-2017.) (Revised by AV, 15-Jan-2021.) Add disjoint variable condition on 𝐷, 𝑓, to remove hypotheses. (Revised by SN, 13-Dec-2024.)
(𝜑𝐺𝑊)    &   (𝜑𝑋 ∈ (𝐴𝐺))    &   (𝜑𝑌 ∈ (𝐵𝐺))    &   𝑀 = (𝑔 ∈ V ↦ (𝑎 ∈ (𝐴𝑔), 𝑏 ∈ (𝐵𝑔) ↦ {⟨𝑓, ⟩ ∣ (𝑓(𝑎(𝐶𝑔)𝑏)𝑓(𝐷𝑔))}))       (𝜑 → (𝑋(𝑀𝐺)𝑌) = {⟨𝑓, ⟩ ∣ (𝑓(𝑋(𝐶𝐺)𝑌)𝑓(𝐷𝐺))})
 
13-Dec-2024mptmpoopabbrd 7989 The operation value of a function value of a collection of ordered pairs of elements related in two ways. (Contributed by Alexander van Vekens, 8-Nov-2017.) (Revised by AV, 15-Jan-2021.) Add disjoint variable condition on 𝐷, 𝑓, to remove hypotheses. (Revised by SN, 13-Dec-2024.)
(𝜑𝐺𝑊)    &   (𝜑𝑋 ∈ (𝐴𝐺))    &   (𝜑𝑌 ∈ (𝐵𝐺))    &   ((𝑎 = 𝑋𝑏 = 𝑌) → (𝜏𝜃))    &   (𝑔 = 𝐺 → (𝜒𝜏))    &   𝑀 = (𝑔 ∈ V ↦ (𝑎 ∈ (𝐴𝑔), 𝑏 ∈ (𝐵𝑔) ↦ {⟨𝑓, ⟩ ∣ (𝜒𝑓(𝐷𝑔))}))       (𝜑 → (𝑋(𝑀𝐺)𝑌) = {⟨𝑓, ⟩ ∣ (𝜃𝑓(𝐷𝐺))})
 
13-Dec-2024fvmptopab 7391 The function value of a mapping 𝑀 to a restricted binary relation expressed as an ordered-pair class abstraction: The restricted binary relation is a binary relation given as value of a function 𝐹 restricted by the condition 𝜓. (Contributed by AV, 31-Jan-2021.) (Revised by AV, 29-Oct-2021.) Add disjoint variable condition on 𝐹, 𝑥, 𝑦 to remove a sethood hypothesis. (Revised by SN, 13-Dec-2024.)
(𝑧 = 𝑍 → (𝜑𝜓))    &   𝑀 = (𝑧 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥(𝐹𝑧)𝑦𝜑)})       (𝑀𝑍) = {⟨𝑥, 𝑦⟩ ∣ (𝑥(𝐹𝑍)𝑦𝜓)}
 
13-Dec-2024opabresex2 7389 Restrictions of a collection of ordered pairs of related elements are sets. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 15-Jan-2021.) Add disjoint variable conditions betweem 𝑊, 𝐺 and 𝑥, 𝑦 to remove hypotheses. (Revised by SN, 13-Dec-2024.)
{⟨𝑥, 𝑦⟩ ∣ (𝑥(𝑊𝐺)𝑦𝜃)} ∈ V
 
13-Dec-2024nfralw 3290 Bound-variable hypothesis builder for restricted quantification. Version of nfral 3343 with a disjoint variable condition, which does not require ax-13 2370. (Contributed by NM, 1-Sep-1999.) Avoid ax-13 2370. (Revised by Gino Giotto, 10-Jan-2024.) (Proof shortened by Wolf Lammen, 13-Dec-2024.)
𝑥𝐴    &   𝑥𝜑       𝑥𝑦𝐴 𝜑
 
12-Dec-2024sdom1 9107 A set has less than one member iff it is empty. (Contributed by Stefan O'Rear, 28-Oct-2014.) Avoid ax-pow 5308, ax-un 7650. (Revised by BTernaryTau, 12-Dec-2024.)
(𝐴 ≺ 1o𝐴 = ∅)
 
11-Dec-2024wksv 28275 The class of walks is a set. (Contributed by AV, 15-Jan-2021.) (Proof shortened by SN, 11-Dec-2024.)
{⟨𝑓, 𝑝⟩ ∣ 𝑓(Walks‘𝐺)𝑝} ∈ V
 
11-Dec-2024abrexexg 7871 Existence of a class abstraction of existentially restricted sets. The class 𝐵 can be thought of as an expression in 𝑥 (which is typically a free variable in the class expression substituted for 𝐵) and the class abstraction appearing in the statement as the class of values 𝐵 as 𝑥 varies through 𝐴. If the "domain" 𝐴 is a set, then the abstraction is also a set. Therefore, this statement is a kind of Replacement. This can be seen by tracing back through the path axrep6g 5237, axrep6 5236, ax-rep 5229. See also abrexex2g 7875. There are partial converses under additional conditions, see for instance abnexg 7668. (Contributed by NM, 3-Nov-2003.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) Avoid ax-10 2136, ax-11 2153, ax-12 2170, ax-pr 5372, ax-un 7650 and shorten proof. (Revised by SN, 11-Dec-2024.)
(𝐴𝑉 → {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ∈ V)
 
11-Dec-2024ssrel 5724 A subclass relationship depends only on a relation's ordered pairs. Theorem 3.2(i) of [Monk1] p. 33. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Remove dependency on ax-sep 5243, ax-nul 5250, ax-pr 5372. (Revised by KP, 25-Oct-2021.) Remove dependency on ax-12 2170. (Revised by SN, 11-Dec-2024.)
(Rel 𝐴 → (𝐴𝐵 ↔ ∀𝑥𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)))
 
11-Dec-2024elopaelxp 5707 Membership in an ordered-pair class abstraction implies membership in a Cartesian product. (Contributed by Alexander van der Vekens, 23-Jun-2018.) Avoid ax-sep 5243, ax-nul 5250, ax-pr 5372. (Revised by SN, 11-Dec-2024.)
(𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜓} → 𝐴 ∈ (V × V))
 
11-Dec-2024elopabr 5505 Membership in an ordered-pair class abstraction defined by a binary relation. (Contributed by AV, 16-Feb-2021.) (Proof shortened by SN, 11-Dec-2024.)
(𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑅𝑦} → 𝐴𝑅)
 
11-Dec-2024elopabw 5470 Membership in a class abstraction of ordered pairs. Weaker version of elopab 5471 with a sethood antecedent, avoiding ax-sep 5243, ax-nul 5250, and ax-pr 5372. Originally a subproof of elopab 5471. (Contributed by SN, 11-Dec-2024.)
(𝐴𝑉 → (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
 
11-Dec-2024axrep6g 5237 axrep6 5236 in class notation. It is equivalent to both ax-rep 5229 and abrexexg 7871, providing a direct link between the two. (Contributed by SN, 11-Dec-2024.)
((𝐴𝑉 ∧ ∀𝑥∃*𝑦𝜓) → {𝑦 ∣ ∃𝑥𝐴 𝜓} ∈ V)
 
11-Dec-2024dfiun2g 4977 Alternate definition of indexed union when 𝐵 is a set. Definition 15(a) of [Suppes] p. 44. (Contributed by NM, 23-Mar-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (Proof shortened by Rohan Ridenour, 11-Aug-2023.) Avoid ax-10 2136, ax-12 2170. (Revised by SN, 11-Dec-2024.)
(∀𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵})
 
11-Dec-2024r19.21v 3172 Restricted quantifier version of 19.21v 1941. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 2-Jan-2020.) (Proof shortened by Wolf Lammen, 11-Dec-2024.)
(∀𝑥𝐴 (𝜑𝜓) ↔ (𝜑 → ∀𝑥𝐴 𝜓))
 
10-Dec-2024sltn0 34181 If 𝑋 is less than 𝑌, then either ( L ‘𝑌) or ( R ‘𝑋) is non-empty. (Contributed by Scott Fenton, 10-Dec-2024.)
((𝑋 No 𝑌 No 𝑋 <s 𝑌) → (( L ‘𝑌) ≠ ∅ ∨ ( R ‘𝑋) ≠ ∅))
 
10-Dec-2024cbvreuw 3379 Change the bound variable of a restricted unique existential quantifier using implicit substitution. Version of cbvreu 3395 with a disjoint variable condition, which does not require ax-13 2370. (Contributed by Mario Carneiro, 15-Oct-2016.) Avoid ax-13 2370. (Revised by Gino Giotto, 10-Jan-2024.) Avoid ax-10 2136. (Revised by Wolf Lammen, 10-Dec-2024.)
𝑦𝜑    &   𝑥𝜓    &   (𝑥 = 𝑦 → (𝜑𝜓))       (∃!𝑥𝐴 𝜑 ↔ ∃!𝑦𝐴 𝜓)
 
8-Dec-20241sdom2 9105 Ordinal 1 is strictly dominated by ordinal 2. For a shorter proof requiring ax-un 7650, see 1sdom2ALT 9106. (Contributed by NM, 4-Apr-2007.) Avoid ax-un 7650. (Revised by BTernaryTau, 8-Dec-2024.)
1o ≺ 2o
 
8-Dec-2024rexcom 3269 Commutation of restricted existential quantifiers. (Contributed by NM, 19-Nov-1995.) (Revised by Mario Carneiro, 14-Oct-2016.) (Proof shortened by BJ, 26-Aug-2023.) (Proof shortened by Wolf Lammen, 8-Dec-2024.)
(∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑦𝐵𝑥𝐴 𝜑)
 
7-Dec-20240sdom1dom 9103 Strict dominance over 0 is the same as dominance over 1. For a shorter proof requiring ax-un 7650, see 0sdom1domALT . (Contributed by NM, 28-Sep-2004.) Avoid ax-un 7650. (Revised by BTernaryTau, 7-Dec-2024.)
(∅ ≺ 𝐴 ↔ 1o𝐴)
 
7-Dec-2024ssct 8916 Any subset of a countable set is countable. (Contributed by Thierry Arnoux, 31-Jan-2017.) Avoid ax-pow 5308, ax-un 7650. (Revised by BTernaryTau, 7-Dec-2024.)
((𝐴𝐵𝐵 ≼ ω) → 𝐴 ≼ ω)
 
7-Dec-2024domssr 8860 If 𝐶 is a superset of 𝐵 and 𝐵 dominates 𝐴, then 𝐶 also dominates 𝐴. (Contributed by BTernaryTau, 7-Dec-2024.)
((𝐶𝑉𝐵𝐶𝐴𝐵) → 𝐴𝐶)
 
7-Dec-2024domssl 8859 If 𝐴 is a subset of 𝐵 and 𝐶 dominates 𝐵, then 𝐶 also dominates 𝐴. (Contributed by BTernaryTau, 7-Dec-2024.)
((𝐴𝐵𝐵𝐶) → 𝐴𝐶)
 
7-Dec-2024f1dom4g 8826 The domain of a one-to-one set function is dominated by its codomain when the latter is a set. This variation of f1domg 8833 does not require the Axiom of Replacement nor the Axiom of Power Sets nor the Axiom of Union. (Contributed by BTernaryTau, 7-Dec-2024.)
(((𝐹𝑉𝐴𝑊𝐵𝑋) ∧ 𝐹:𝐴1-1𝐵) → 𝐴𝐵)
 
7-Dec-2024f1oen4g 8825 The domain and range of a one-to-one, onto set function are equinumerous. This variation of f1oeng 8832 does not require the Axiom of Replacement nor the Axiom of Power Sets nor the Axiom of Union. (Contributed by BTernaryTau, 7-Dec-2024.)
(((𝐹𝑉𝐴𝑊𝐵𝑋) ∧ 𝐹:𝐴1-1-onto𝐵) → 𝐴𝐵)
 
5-Dec-2024sb8f 2349 Substitution of variable in universal quantifier. Version of sb8 2519 with a disjoint variable condition, not requiring ax-10 2136 or ax-13 2370. (Contributed by NM, 16-May-1993.) (Revised by Wolf Lammen, 19-Jan-2023.) Avoid ax-10 2136. (Revised by SN, 5-Dec-2024.)
𝑦𝜑       (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑)
 
5-Dec-2024sb8v 2348 Substitution of variable in universal quantifier. Version of sb8f 2349 with a disjoint variable condition replacing the nonfree hypothesis 𝑦𝜑, not requiring ax-12 2170. (Contributed by SN, 5-Dec-2024.)
(∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑)
 
4-Dec-2024sucdom2 9071 Strict dominance of a set over another set implies dominance over its successor. (Contributed by Mario Carneiro, 12-Jan-2013.) (Proof shortened by Mario Carneiro, 27-Apr-2015.) Avoid ax-pow 5308. (Revised by BTernaryTau, 4-Dec-2024.)
(𝐴𝐵 → suc 𝐴𝐵)
 
4-Dec-2024undom 8924 Dominance law for union. Proposition 4.24(a) of [Mendelson] p. 257. (Contributed by NM, 3-Sep-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) Avoid ax-pow 5308. (Revised by BTernaryTau, 4-Dec-2024.)
(((𝐴𝐵𝐶𝐷) ∧ (𝐵𝐷) = ∅) → (𝐴𝐶) ≼ (𝐵𝐷))
 
3-Dec-2024eqvreldisj1 37099 The elements of the quotient set of an equivalence relation are disjoint (cf. eqvreldisj2 37100, eqvreldisj3 37101). (Contributed by Mario Carneiro, 10-Dec-2016.) (Revised by Peter Mazsa, 3-Dec-2024.)
( EqvRel 𝑅 → ∀𝑥 ∈ (𝐴 / 𝑅)∀𝑦 ∈ (𝐴 / 𝑅)(𝑥 = 𝑦 ∨ (𝑥𝑦) = ∅))
 
3-Dec-2024fvprc 6817 A function's value at a proper class is the empty set. See fvprcALT 6818 for a proof that uses ax-pow 5308 instead of ax-pr 5372. (Contributed by NM, 20-May-1998.) Avoid ax-pow 5308. (Revised by BTernaryTau, 3-Aug-2024.) (Proof shortened by BTernaryTau, 3-Dec-2024.)
𝐴 ∈ V → (𝐹𝐴) = ∅)
 
3-Dec-2024f1un 6787 The union of two one-to-one functions with disjoint domains and codomains. (Contributed by BTernaryTau, 3-Dec-2024.)
(((𝐹:𝐴1-1𝐵𝐺:𝐶1-1𝐷) ∧ ((𝐴𝐶) = ∅ ∧ (𝐵𝐷) = ∅)) → (𝐹𝐺):(𝐴𝐶)–1-1→(𝐵𝐷))
 
3-Dec-2024dtruOLD 5386 Obsolete proof of dtru 5381 as of 01-Jan-2025. (Contributed by NM, 7-Nov-2006.) Avoid ax-13 2370. (Revised by BJ, 31-May-2019.) Avoid ax-12 2170. (Revised by Rohan Ridenour, 9-Oct-2024.) Use ax-pr 5372 instead of ax-pow 5308. (Revised by BTernaryTau, 3-Dec-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
¬ ∀𝑥 𝑥 = 𝑦
 
2-Dec-2024onomeneq 9093 An ordinal number equinumerous to a natural number is equal to it. Proposition 10.22 of [TakeutiZaring] p. 90 and its converse. (Contributed by NM, 26-Jul-2004.) Avoid ax-pow 5308. (Revised by BTernaryTau, 2-Dec-2024.)
((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴𝐵𝐴 = 𝐵))
 
2-Dec-2024el 5382 Any set is an element of some other set. See elALT 5385 for a shorter proof using more axioms, and see elALT2 5312 for a proof that uses ax-9 2115 and ax-pow 5308 instead of ax-pr 5372. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) Use ax-pr 5372 instead of ax-9 2115 and ax-pow 5308. (Revised by BTernaryTau, 2-Dec-2024.)
𝑦 𝑥𝑦
 
1-Dec-2024frrlem16 9615 Lemma for general well-founded recursion. Establish a subset relationship. (Contributed by Scott Fenton, 11-Sep-2023.) Revised notion of transitive closure. (Revised by Scott Fenton, 1-Dec-2024.)
(((𝑅 Fr 𝐴𝑅 Se 𝐴) ∧ 𝑧𝐴) → ∀𝑤 ∈ Pred (t++(𝑅𝐴), 𝐴, 𝑧)Pred(𝑅, 𝐴, 𝑤) ⊆ Pred(t++(𝑅𝐴), 𝐴, 𝑧))
 
1-Dec-2024snnen2o 9102 A singleton {𝐴} is never equinumerous with the ordinal number 2. This holds for proper singletons (𝐴 ∈ V) as well as for singletons being the empty set (𝐴 ∉ V). (Contributed by AV, 6-Aug-2019.) Avoid ax-pow 5308, ax-un 7650. (Revised by BTernaryTau, 1-Dec-2024.)
¬ {𝐴} ≈ 2o
 
1-Dec-20242onn 8543 The ordinal 2 is a natural number. For a shorter proof using Peano's postulates that depends on ax-un 7650, see 2onnALT 8544. (Contributed by NM, 28-Sep-2004.) Avoid ax-un 7650. (Revised by BTernaryTau, 1-Dec-2024.)
2o ∈ ω
 
1-Dec-20241onn 8541 The ordinal 1 is a natural number. For a shorter proof using Peano's postulates that depends on ax-un 7650, see 1onnALT 8542. (Contributed by NM, 29-Oct-1995.) Avoid ax-un 7650. (Revised by BTernaryTau, 1-Dec-2024.)
1o ∈ ω
 
1-Dec-20242ellim 8400 A limit ordinal contains 2. (Contributed by BTernaryTau, 1-Dec-2024.)
(Lim 𝐴 → 2o𝐴)
 
1-Dec-20241ellim 8399 A limit ordinal contains 1. (Contributed by BTernaryTau, 1-Dec-2024.)
(Lim 𝐴 → 1o𝐴)
 
1-Dec-2024ord2eln012 8398 An ordinal that is not 0, 1, or 2 contains 2. (Contributed by BTernaryTau, 1-Dec-2024.)
(Ord 𝐴 → (2o𝐴 ↔ (𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o𝐴 ≠ 2o)))
 
1-Dec-2024ord1eln01 8397 An ordinal that is not 0 or 1 contains 1. (Contributed by BTernaryTau, 1-Dec-2024.)
(Ord 𝐴 → (1o𝐴 ↔ (𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o)))
 
1-Dec-2024nlim2 8391 2 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024.)
¬ Lim 2o
 
1-Dec-2024nlim1 8390 1 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024.)
¬ Lim 1o
 
1-Dec-2024f1cdmsn 7210 If a one-to-one function with a nonempty domain has a singleton as its codomain, its domain must also be a singleton. (Contributed by BTernaryTau, 1-Dec-2024.)
((𝐹:𝐴1-1→{𝐵} ∧ 𝐴 ≠ ∅) → ∃𝑥 𝐴 = {𝑥})
 
30-Nov-20242on 8381 Ordinal 2 is an ordinal number. (Contributed by NM, 18-Feb-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) Avoid ax-un 7650. (Revised by BTernaryTau, 30-Nov-2024.)
2o ∈ On
 
30-Nov-20241on 8379 Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995.) Avoid ax-un 7650. (Revised by BTernaryTau, 30-Nov-2024.)
1o ∈ On
 
30-Nov-2024suceloni 7724 The successor of an ordinal number is an ordinal number. Proposition 7.24 of [TakeutiZaring] p. 41. (Contributed by NM, 6-Jun-1994.) (Proof shortened by BTernaryTau, 30-Nov-2024.)
(𝐴 ∈ On → suc 𝐴 ∈ On)
 
30-Nov-2024sucexeloniOLD 7723 Obsolete version of sucexeloni 7722 as of 6-Jan-2025. (Contributed by BTernaryTau, 30-Nov-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
((𝐴 ∈ On ∧ suc 𝐴𝑉) → suc 𝐴 ∈ On)
 
30-Nov-2024epweon 7687 The membership relation well-orders the class of ordinal numbers. This proof does not require the axiom of regularity. Proposition 4.8(g) of [Mendelson] p. 244. For a shorter proof requiring ax-un 7650, see epweonALT 7688. (Contributed by NM, 1-Nov-2003.) Avoid ax-un 7650. (Revised by BTernaryTau, 30-Nov-2024.)
E We On
 
30-Nov-2024elex2 2816 If a class contains another class, then it contains some set. (Contributed by Alan Sare, 25-Sep-2011.) Avoid ax-9 2115, ax-ext 2707, df-clab 2714. (Revised by Wolf Lammen, 30-Nov-2024.)
(𝐴𝐵 → ∃𝑥 𝑥𝐵)
 
29-Nov-2024nndomog 9081 Cardinal ordering agrees with ordinal number ordering when the smaller number is a natural number. Compare with nndomo 9098 when both are natural numbers. (Contributed by NM, 17-Jun-1998.) Generalize from nndomo 9098. (Revised by RP, 5-Nov-2023.) Avoid ax-pow 5308. (Revised by BTernaryTau, 29-Nov-2024.)
((𝐴 ∈ ω ∧ 𝐵 ∈ On) → (𝐴𝐵𝐴𝐵))
 
29-Nov-2024sdom0 8973 The empty set does not strictly dominate any set. (Contributed by NM, 26-Oct-2003.) Avoid ax-pow 5308, ax-un 7650. (Revised by BTernaryTau, 29-Nov-2024.)
¬ 𝐴 ≺ ∅
 
29-Nov-20240sdomg 8969 A set strictly dominates the empty set iff it is not empty. (Contributed by NM, 23-Mar-2006.) Avoid ax-pow 5308, ax-un 7650. (Revised by BTernaryTau, 29-Nov-2024.)
(𝐴𝑉 → (∅ ≺ 𝐴𝐴 ≠ ∅))
 
29-Nov-2024dom0 8967 A set dominated by the empty set is empty. (Contributed by NM, 22-Nov-2004.) Avoid ax-pow 5308, ax-un 7650. (Revised by BTernaryTau, 29-Nov-2024.)
(𝐴 ≼ ∅ ↔ 𝐴 = ∅)
 
29-Nov-20240domg 8965 Any set dominates the empty set. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) Avoid ax-pow 5308, ax-un 7650. (Revised by BTernaryTau, 29-Nov-2024.)
(𝐴𝑉 → ∅ ≼ 𝐴)
 
29-Nov-2024en0r 8881 The empty set is equinumerous only to itself. (Contributed by BTernaryTau, 29-Nov-2024.)
(∅ ≈ 𝐴𝐴 = ∅)
 
29-Nov-2024brdomi 8819 Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015.) Avoid ax-un 7650. (Revised by BTernaryTau, 29-Nov-2024.)
(𝐴𝐵 → ∃𝑓 𝑓:𝐴1-1𝐵)
 
29-Nov-2024brdomg 8817 Dominance relation. (Contributed by NM, 15-Jun-1998.) Extract brdom2g 8816 as an intermediate result. (Revised by BTernaryTau, 29-Nov-2024.)
(𝐵𝐶 → (𝐴𝐵 ↔ ∃𝑓 𝑓:𝐴1-1𝐵))
 
29-Nov-2024brdom2g 8816 Dominance relation. This variation of brdomg 8817 does not require the Axiom of Union. (Contributed by NM, 15-Jun-1998.) Extract from a subproof of brdomg 8817. (Revised by BTernaryTau, 29-Nov-2024.)
((𝐴𝑉𝐵𝑊) → (𝐴𝐵 ↔ ∃𝑓 𝑓:𝐴1-1𝐵))
 
29-Nov-2024peano1 7803 Zero is a natural number. One of Peano's five postulates for arithmetic. Proposition 7.30(1) of [TakeutiZaring] p. 42. Note: Unlike most textbooks, our proofs of peano1 7803 through peano5 7808 do not use the Axiom of Infinity. Unlike Takeuti and Zaring, they also do not use the Axiom of Regularity. (Contributed by NM, 15-May-1994.) Avoid ax-un 7650. (Revised by BTernaryTau, 29-Nov-2024.)
∅ ∈ ω
 
28-Nov-2024phpeqd 9080 Corollary of the Pigeonhole Principle using equality. Strengthening of php 9075 expressed without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.) Avoid ax-pow. (Revised by BTernaryTau, 28-Nov-2024.)
(𝜑𝐴 ∈ Fin)    &   (𝜑𝐵𝐴)    &   (𝜑𝐴𝐵)       (𝜑𝐴 = 𝐵)
 
27-Nov-2024frmin 9606 Every (possibly proper) subclass of a class 𝐴 with a well-founded set-like relation 𝑅 has a minimal element. This is a very strong generalization of tz6.26 6286 and tz7.5 6323. (Contributed by Scott Fenton, 4-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) (Revised by Scott Fenton, 27-Nov-2024.)
(((𝑅 Fr 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → ∃𝑦𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)
 
26-Nov-2024php3 9077 Corollary of Pigeonhole Principle. If 𝐴 is finite and 𝐵 is a proper subset of 𝐴, the 𝐵 is strictly less numerous than 𝐴. Stronger version of Corollary 6C of [Enderton] p. 135. (Contributed by NM, 22-Aug-2008.) Avoid ax-pow 5308. (Revised by BTernaryTau, 26-Nov-2024.)
((𝐴 ∈ Fin ∧ 𝐵𝐴) → 𝐵𝐴)
 
25-Nov-2024domsdomtrfi 9070 Transitivity of dominance and strict dominance when 𝐴 is finite, proved without using the Axiom of Power Sets (unlike domsdomtr 8977). (Contributed by BTernaryTau, 25-Nov-2024.)
((𝐴 ∈ Fin ∧ 𝐴𝐵𝐵𝐶) → 𝐴𝐶)
 
25-Nov-2024sdomdomtrfi 9069 Transitivity of strict dominance and dominance when 𝐴 is finite, proved without using the Axiom of Power Sets (unlike sdomdomtr 8975). (Contributed by BTernaryTau, 25-Nov-2024.)
((𝐴 ∈ Fin ∧ 𝐴𝐵𝐵𝐶) → 𝐴𝐶)
 
25-Nov-2024predres 6278 Predecessor class is unaffected by restriction to the base class. (Contributed by Scott Fenton, 25-Nov-2024.)
Pred(𝑅, 𝐴, 𝑋) = Pred((𝑅𝐴), 𝐴, 𝑋)
 
25-Nov-2024predprc 6277 The predecessor of a proper class is empty. (Contributed by Scott Fenton, 25-Nov-2024.)
𝑋 ∈ V → Pred(𝑅, 𝐴, 𝑋) = ∅)
 
25-Nov-2024predrelss 6276 Subset carries from relation to predecessor class. (Contributed by Scott Fenton, 25-Nov-2024.)
(𝑅𝑆 → Pred(𝑅, 𝐴, 𝑋) ⊆ Pred(𝑆, 𝐴, 𝑋))
 
24-Nov-2024ssdomfi2 9065 A set dominates its finite subsets, proved without using the Axiom of Power Sets (unlike ssdomg 8861). (Contributed by BTernaryTau, 24-Nov-2024.)
((𝐴 ∈ Fin ∧ 𝐵𝑉𝐴𝐵) → 𝐴𝐵)
 
24-Nov-2024domtrfir 9062 Transitivity of dominance relation for finite sets, proved without using the Axiom of Power Sets (unlike domtr 8868). (Contributed by BTernaryTau, 24-Nov-2024.)
((𝐶 ∈ Fin ∧ 𝐴𝐵𝐵𝐶) → 𝐴𝐶)
 
24-Nov-2024domtrfi 9061 Transitivity of dominance relation when 𝐵 is finite, proved without using the Axiom of Power Sets (unlike domtr 8868). (Contributed by BTernaryTau, 24-Nov-2024.)
((𝐵 ∈ Fin ∧ 𝐴𝐵𝐵𝐶) → 𝐴𝐶)
 
24-Nov-2024domtrfil 9060 Transitivity of dominance relation when 𝐴 is finite, proved without using the Axiom of Power Sets (unlike domtr 8868). (Contributed by BTernaryTau, 24-Nov-2024.)
((𝐴 ∈ Fin ∧ 𝐴𝐵𝐵𝐶) → 𝐴𝐶)
 
24-Nov-2024f1domfi2 9050 If the domain of a one-to-one function is finite, then the function's domain is dominated by its codomain when the latter is a set. This theorem is proved without using the Axiom of Power Sets (unlike f1dom2g 8830). (Contributed by BTernaryTau, 24-Nov-2024.)
((𝐴 ∈ Fin ∧ 𝐵𝑉𝐹:𝐴1-1𝐵) → 𝐴𝐵)
 
24-Nov-2024rabid2 3432 An "identity" law for restricted class abstraction. (Contributed by NM, 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2024.)
(𝐴 = {𝑥𝐴𝜑} ↔ ∀𝑥𝐴 𝜑)
 
24-Nov-2024clelsb2 2865 Substitution for the second argument of the membership predicate in an atomic formula (class version of elsb2 2122). (Contributed by Jim Kingdon, 22-Nov-2018.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 24-Nov-2024.)
([𝑦 / 𝑥]𝐴𝑥𝐴𝑦)
 
23-Nov-2024natglobalincr 46871 Local monotonicity on half-open integer range implies global monotonicity. (Contributed by Ender Ting, 23-Nov-2024.)
𝑘 ∈ (0..^𝑇)(𝐵𝑘) < (𝐵‘(𝑘 + 1))    &   𝑇 ∈ ℤ       𝑘 ∈ (0..^𝑇)∀𝑡 ∈ ((𝑘 + 1)...𝑇)(𝐵𝑘) < (𝐵𝑡)
 
23-Nov-2024prjcrv0 40740 The "curve" (zero set) corresponding to the zero polynomial contains all coordinates. (Contributed by SN, 23-Nov-2024.)
𝑌 = ((0...𝑁) mPoly 𝐾)    &    0 = (0g𝑌)    &   𝑃 = (𝑁ℙ𝕣𝕠𝕛n𝐾)    &   (𝜑𝑁 ∈ ℕ0)    &   (𝜑𝐾 ∈ Field)       (𝜑 → ((𝑁ℙ𝕣𝕠𝕛Crv𝐾)‘ 0 ) = 𝑃)
 
23-Nov-2024prjcrvval 40739 Value of the projective curve function. (Contributed by SN, 23-Nov-2024.)
𝐻 = ((0...𝑁) mHomP 𝐾)    &   𝐸 = ((0...𝑁) eval 𝐾)    &   𝑃 = (𝑁ℙ𝕣𝕠𝕛n𝐾)    &    0 = (0g𝐾)    &   (𝜑𝑁 ∈ ℕ0)    &   (𝜑𝐾 ∈ Field)    &   (𝜑𝐹 ran 𝐻)       (𝜑 → ((𝑁ℙ𝕣𝕠𝕛Crv𝐾)‘𝐹) = {𝑝𝑃 ∣ ((𝐸𝐹) “ 𝑝) = { 0 }})
 
23-Nov-2024prjcrvfval 40738 Value of the projective curve function. (Contributed by SN, 23-Nov-2024.)
𝐻 = ((0...𝑁) mHomP 𝐾)    &   𝐸 = ((0...𝑁) eval 𝐾)    &   𝑃 = (𝑁ℙ𝕣𝕠𝕛n𝐾)    &    0 = (0g𝐾)    &   (𝜑𝑁 ∈ ℕ0)    &   (𝜑𝐾 ∈ Field)       (𝜑 → (𝑁ℙ𝕣𝕠𝕛Crv𝐾) = (𝑓 ran 𝐻 ↦ {𝑝𝑃 ∣ ((𝐸𝑓) “ 𝑝) = { 0 }}))
 
23-Nov-2024df-prjcrv 40737 Define the projective curve function. This takes a homogeneous polynomial and outputs the homogeneous coordinates where the polynomial evaluates to zero (the "zero set"). (In other words, scalar multiples are collapsed into the same projective point. See mhphf4 40556 and prjspvs 40717). (Contributed by SN, 23-Nov-2024.)
ℙ𝕣𝕠𝕛Crv = (𝑛 ∈ ℕ0, 𝑘 ∈ Field ↦ (𝑓 ran ((0...𝑛) mHomP 𝑘) ↦ {𝑝 ∈ (𝑛ℙ𝕣𝕠𝕛n𝑘) ∣ ((((0...𝑛) eval 𝑘)‘𝑓) “ 𝑝) = {(0g𝑘)}}))
 
23-Nov-2024mhphf4 40556 A homogeneous polynomial defines a homogeneous function; this is mhphf3 40555 with evalSub collapsed to eval. (Contributed by SN, 23-Nov-2024.)
𝑄 = (𝐼 eval 𝑆)    &   𝐻 = (𝐼 mHomP 𝑆)    &   𝐾 = (Base‘𝑆)    &   𝐹 = (𝑆 freeLMod 𝐼)    &   𝑀 = (Base‘𝐹)    &    = ( ·𝑠𝐹)    &    · = (.r𝑆)    &    = (.g‘(mulGrp‘𝑆))    &   (𝜑𝐼𝑉)    &   (𝜑𝑆 ∈ CRing)    &   (𝜑𝐿𝐾)    &   (𝜑𝑁 ∈ ℕ0)    &   (𝜑𝑋 ∈ (𝐻𝑁))    &   (𝜑𝐴𝑀)       (𝜑 → ((𝑄𝑋)‘(𝐿 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑋)‘𝐴)))
 
23-Nov-2024mhphf3 40555 A homogeneous polynomial defines a homogeneous function; this is mhphf2 40554 with the finite support restriction (frlmpws 21063, frlmbas 21068) on the assignments 𝐴 from variables to values. See comment of mhphf2 40554. (Contributed by SN, 23-Nov-2024.)
𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   𝐻 = (𝐼 mHomP 𝑈)    &   𝑈 = (𝑆s 𝑅)    &   𝐾 = (Base‘𝑆)    &   𝐹 = (𝑆 freeLMod 𝐼)    &   𝑀 = (Base‘𝐹)    &    = ( ·𝑠𝐹)    &    · = (.r𝑆)    &    = (.g‘(mulGrp‘𝑆))    &   (𝜑𝐼𝑉)    &   (𝜑𝑆 ∈ CRing)    &   (𝜑𝑅 ∈ (SubRing‘𝑆))    &   (𝜑𝐿𝑅)    &   (𝜑𝑁 ∈ ℕ0)    &   (𝜑𝑋 ∈ (𝐻𝑁))    &   (𝜑𝐴𝑀)       (𝜑 → ((𝑄𝑋)‘(𝐿 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑋)‘𝐴)))
 
23-Nov-2024evl0 40539 The zero polynomial evaluates to zero. (Contributed by SN, 23-Nov-2024.)
𝑄 = (𝐼 eval 𝑅)    &   𝐵 = (Base‘𝑅)    &   𝑊 = (𝐼 mPoly 𝑅)    &   𝑂 = (0g𝑅)    &    0 = (0g𝑊)    &   (𝜑𝐼𝑉)    &   (𝜑𝑅 ∈ CRing)       (𝜑 → (𝑄0 ) = ((𝐵m 𝐼) × {𝑂}))
 
23-Nov-2024mplascl0 40538 The zero scalar as a polynomial. (Contributed by SN, 23-Nov-2024.)
𝑊 = (𝐼 mPoly 𝑅)    &   𝐴 = (algSc‘𝑊)    &   𝑂 = (0g𝑅)    &    0 = (0g𝑊)    &   (𝜑𝐼𝑉)    &   (𝜑𝑅 ∈ CRing)       (𝜑 → (𝐴𝑂) = 0 )
 
23-Nov-2024abbi1sn 40457 Originally part of uniabio 6446. Convert a theorem about df-iota 6431 to one about dfiota2 6432, without ax-10 2136, ax-11 2153, ax-12 2170. Although, eu6 2572 uses ax-10 2136 and ax-12 2170. (Contributed by SN, 23-Nov-2024.)
(∀𝑥(𝜑𝑥 = 𝑦) → {𝑥𝜑} = {𝑦})
 
23-Nov-2024recvs 24415 The field of the real numbers as left module over itself is a subcomplex vector space. The vector operation is +, and the scalar product is ·. (Contributed by AV, 22-Oct-2021.) (Proof shortened by SN, 23-Nov-2024.)
𝑅 = (ringLMod‘ℝfld)       𝑅 ∈ ℂVec
 
23-Nov-2024fldcrngd 20105 A field is a commutative ring. (Contributed by SN, 23-Nov-2024.)
(𝜑𝑅 ∈ Field)       (𝜑𝑅 ∈ CRing)
 
23-Nov-2024iotaval 6450 Theorem 8.19 in [Quine] p. 57. This theorem is the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011.) Remove dependency on ax-10 2136, ax-11 2153, ax-12 2170. (Revised by SN, 23-Nov-2024.)
(∀𝑥(𝜑𝑥 = 𝑦) → (℩𝑥𝜑) = 𝑦)
 
23-Nov-2024nfrabw 3436 A variable not free in a wff remains so in a restricted class abstraction. Version of nfrab 3439 with a disjoint variable condition, which does not require ax-13 2370. (Contributed by NM, 13-Oct-2003.) Avoid ax-13 2370. (Revised by Gino Giotto, 10-Jan-2024.) (Proof shortened by Wolf Lammen, 23-Nov-2024.)
𝑥𝜑    &   𝑥𝐴       𝑥{𝑦𝐴𝜑}
 
23-Nov-2024moel 3371 "At most one" element in a set. (Contributed by Thierry Arnoux, 26-Jul-2018.) Avoid ax-11 2153. (Revised by Wolf Lammen, 23-Nov-2024.)
(∃*𝑥 𝑥𝐴 ↔ ∀𝑥𝐴𝑦𝐴 𝑥 = 𝑦)
 
23-Nov-2024rmobidva 3364 Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 16-Jun-2017.) Avoid ax-6 1970, ax-7 2010, ax-12 2170. (Revised by Wolf Lammen, 23-Nov-2024.)
((𝜑𝑥𝐴) → (𝜓𝜒))       (𝜑 → (∃*𝑥𝐴 𝜓 ↔ ∃*𝑥𝐴 𝜒))
 
22-Nov-2024tworepnotupword 46880 Word of two matching characters is never an increasing sequence. (Contributed by Ender Ting, 22-Nov-2024.)
𝐴 ∈ V        ¬ (⟨“𝐴”⟩ ++ ⟨“𝐴”⟩) ∈ UpWord𝑆
 
22-Nov-2024singoutnupword 46877 Singleton with character out of range 𝑆 is not an increasing sequence for that range. (Contributed by Ender Ting, 22-Nov-2024.)
𝐴 ∈ V       𝐴𝑆 → ¬ ⟨“𝐴”⟩ ∈ UpWord𝑆)
 
22-Nov-2024natlocalincr 46870 Global monotonicity on half-open range implies local monotonicity. (Contributed by Ender Ting, 22-Nov-2024.)
𝑘 ∈ (0..^𝑇)∀𝑡 ∈ (1..^(𝑇 + 1))(𝑘 < 𝑡 → (𝐵𝑘) < (𝐵𝑡))       𝑘 ∈ (0..^𝑇)(𝐵𝑘) < (𝐵‘(𝑘 + 1))
 
22-Nov-2024et-ltneverrefl 46869 Less-than class is never reflexive. (Contributed by Ender Ting, 22-Nov-2024.) Prefer to specify theorem domain and then apply ltnri 11185. (New usage is discouraged.)
¬ 𝐴 < 𝐴
 
22-Nov-2024domnsymfi 9068 If a set dominates a finite set, it cannot also be strictly dominated by the finite set. This theorem is proved without using the Axiom of Power Sets (unlike domnsym 8964). (Contributed by BTernaryTau, 22-Nov-2024.)
((𝐴 ∈ Fin ∧ 𝐴𝐵) → ¬ 𝐵𝐴)
 
21-Nov-2024upwordsseti 46879 Strictly increasing sequences with a set given for range form a set. (Contributed by Ender Ting, 21-Nov-2024.)
𝑆 ∈ V       UpWord𝑆 ∈ V
 
21-Nov-2024upwordsing 46878 Singleton is an increasing sequence for any compatible range. (Contributed by Ender Ting, 21-Nov-2024.)
𝐴𝑆       ⟨“𝐴”⟩ ∈ UpWord𝑆
 
21-Nov-2024singoutnword 46876 Singleton with character out of range 𝑉 is not a word for that range. (Contributed by Ender Ting, 21-Nov-2024.)
𝐴 ∈ V       𝐴𝑉 → ¬ ⟨“𝐴”⟩ ∈ Word 𝑉)
 
21-Nov-2024nfreuw 3383 Bound-variable hypothesis builder for restricted unique existence. Version of nfreu 3402 with a disjoint variable condition, which does not require ax-13 2370. (Contributed by NM, 30-Oct-2010.) Avoid ax-13 2370. (Revised by Gino Giotto, 10-Jan-2024.) Avoid ax-9 2115, ax-ext 2707. (Revised by Wolf Lammen, 21-Nov-2024.)
𝑥𝐴    &   𝑥𝜑       𝑥∃!𝑦𝐴 𝜑
 
21-Nov-2024nfrmow 3382 Bound-variable hypothesis builder for restricted uniqueness. Version of nfrmo 3401 with a disjoint variable condition, which does not require ax-13 2370. (Contributed by NM, 16-Jun-2017.) Avoid ax-13 2370. (Revised by Gino Giotto, 10-Jan-2024.) Avoid ax-9 2115, ax-ext 2707. (Revised by Wolf Lammen, 21-Nov-2024.)
𝑥𝐴    &   𝑥𝜑       𝑥∃*𝑦𝐴 𝜑
 
21-Nov-2024eeor 2329 Distribute existential quantifiers. (Contributed by NM, 8-Aug-1994.) Avoid ax-10 2136. (Revised by Gino Giotto, 21-Nov-2024.)
𝑦𝜑    &   𝑥𝜓       (∃𝑥𝑦(𝜑𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑦𝜓))
 
21-Nov-2024aaan 2327 Distribute universal quantifiers. (Contributed by NM, 12-Aug-1993.) Avoid ax-10 2136. (Revised by Gino Giotto, 21-Nov-2024.)
𝑦𝜑    &   𝑥𝜓       (∀𝑥𝑦(𝜑𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑦𝜓))
 
20-Nov-2024php2 9076 Corollary of Pigeonhole Principle. (Contributed by NM, 31-May-1998.) Avoid ax-pow 5308. (Revised by BTernaryTau, 20-Nov-2024.)
((𝐴 ∈ ω ∧ 𝐵𝐴) → 𝐵𝐴)
 
20-Nov-20242ralor 3215 Distribute restricted universal quantification over "or". (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof shortened by Wolf Lammen, 20-Nov-2024.)
(∀𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∀𝑥𝐴 𝜑 ∨ ∀𝑦𝐵 𝜓))
 
20-Nov-2024sbrim 2300 Substitution in an implication with a variable not free in the antecedent affects only the consequent. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) Avoid ax-10 2136. (Revised by Gino Giotto, 20-Nov-2024.)
𝑥𝜑       ([𝑦 / 𝑥](𝜑𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))
 
19-Nov-2024upwordisword 46875 Any increasing sequence is a sequence. (Contributed by Ender Ting, 19-Nov-2024.)
(𝐴 ∈ UpWord𝑆𝐴 ∈ Word 𝑆)
 
19-Nov-2024upwordnul 46874 Empty set is an increasing sequence for every range. (Contributed by Ender Ting, 19-Nov-2024.)
∅ ∈ UpWord𝑆
 
19-Nov-2024df-upword 46873 Strictly increasing sequence is a sequence, adjacent elements of which increase. (Contributed by Ender Ting, 19-Nov-2024.)
UpWord𝑆 = {𝑤 ∣ (𝑤 ∈ Word 𝑆 ∧ ∀𝑘 ∈ (0..^((♯‘𝑤) − 1))(𝑤𝑘) < (𝑤‘(𝑘 + 1)))}
 
19-Nov-2024moeu2 36636 Uniqueness is equivalent to non-existence or unique existence. Alternate definition of the at-most-one quantifier, in terms of the existential quantifier and the unique existential quantifier. (Contributed by Peter Mazsa, 19-Nov-2024.)
(∃*𝑥𝜑 ↔ (¬ ∃𝑥𝜑 ∨ ∃!𝑥𝜑))
 
19-Nov-2024fri 5580 A nonempty subset of an 𝑅-well-founded class has an 𝑅-minimal element (inference form). (Contributed by BJ, 16-Nov-2024.) (Proof shortened by BJ, 19-Nov-2024.)
(((𝐵𝐶𝑅 Fr 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
 
18-Nov-2024mopickr 36637 "At most one" picks a variable value, eliminating an existential quantifier. The proof begins with references *2.21 (pm2.21 123) and *14.26 (eupickbi 2636) from [WhiteheadRussell] p. 104 and p. 183. (Contributed by Peter Mazsa, 18-Nov-2024.) (Proof modification is discouraged.)
((∃*𝑥𝜓 ∧ ∃𝑥(𝜑𝜓)) → (𝜓𝜑))
 
18-Nov-2024php 9075 Pigeonhole Principle. A natural number is not equinumerous to a proper subset of itself. Theorem (Pigeonhole Principle) of [Enderton] p. 134. The theorem is so-called because you can't put n + 1 pigeons into n holes (if each hole holds only one pigeon). The proof consists of phplem1 9072, phplem2 9073, nneneq 9074, and this final piece of the proof. (Contributed by NM, 29-May-1998.) Avoid ax-pow 5308. (Revised by BTernaryTau, 18-Nov-2024.)
((𝐴 ∈ ω ∧ 𝐵𝐴) → ¬ 𝐴𝐵)
 
18-Nov-2024wfr3 8238 The principle of Well-Ordered Recursion, part 3 of 3. Finally, we show that 𝐹 is unique. We do this by showing that any function 𝐻 with the same properties we proved of 𝐹 in wfr1 8236 and wfr2 8237 is identical to 𝐹. (Contributed by Scott Fenton, 18-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) (Revised by Scott Fenton, 18-Nov-2024.)
𝐹 = wrecs(𝑅, 𝐴, 𝐺)       (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐻 Fn 𝐴 ∧ ∀𝑧𝐴 (𝐻𝑧) = (𝐺‘(𝐻 ↾ Pred(𝑅, 𝐴, 𝑧))))) → 𝐹 = 𝐻)
 
18-Nov-2024wfr1 8236 The Principle of Well-Ordered Recursion, part 1 of 3. We start with an arbitrary function 𝐺. Then, using a base class 𝐴 and a set-like well-ordering 𝑅 of 𝐴, we define a function 𝐹. This function is said to be defined by "well-ordered recursion". The purpose of these three theorems is to demonstrate the properties of 𝐹. We begin by showing that 𝐹 is a function over 𝐴. (Contributed by Scott Fenton, 22-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) (Revised by Scott Fenton, 18-Nov-2024.)
𝐹 = wrecs(𝑅, 𝐴, 𝐺)       ((𝑅 We 𝐴𝑅 Se 𝐴) → 𝐹 Fn 𝐴)
 
18-Nov-2024wfr2a 8235 A weak version of wfr2 8237 which is useful for proofs that avoid the Axiom of Replacement. (Contributed by Scott Fenton, 30-Jul-2020.) (Proof shortened by Scott Fenton, 18-Nov-2024.)
𝐹 = wrecs(𝑅, 𝐴, 𝐺)       (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ 𝑋 ∈ dom 𝐹) → (𝐹𝑋) = (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑋))))
 
18-Nov-2024wfrresex 8234 Show without using the axiom of replacement that the restriction of the well-ordered recursion generator to a predecessor class is a set. (Contributed by Scott Fenton, 18-Nov-2024.)
𝐹 = wrecs(𝑅, 𝐴, 𝐺)       (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ 𝑋 ∈ dom 𝐹) → (𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)) ∈ V)
 
18-Nov-2024csbwrecsg 8207 Move class substitution in and out of the well-founded recursive function generator. (Contributed by ML, 25-Oct-2020.) (Revised by Scott Fenton, 18-Nov-2024.)
(𝐴𝑉𝐴 / 𝑥wrecs(𝑅, 𝐷, 𝐹) = wrecs(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝐴 / 𝑥𝐹))
 
18-Nov-2024fprresex 8196 The restriction of a function defined by well-founded recursion to the predecessor of an element of its domain is a set. Avoids the axiom of replacement. (Contributed by Scott Fenton, 18-Nov-2024.)
𝐹 = frecs(𝑅, 𝐴, 𝐺)       (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ 𝑋 ∈ dom 𝐹) → (𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)) ∈ V)
 
18-Nov-2024fprfung 8195 A "function" defined by well-founded recursion is indeed a function when the relationship is a partial order. Avoids the axiom of replacement. (Contributed by Scott Fenton, 18-Nov-2024.)
𝐹 = frecs(𝑅, 𝐴, 𝐺)       ((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) → Fun 𝐹)
 
18-Nov-2024frrdmss 8193 Show without using the axiom of replacement that the domain of the well-founded recursion generator is a subclass of 𝐴. (Contributed by Scott Fenton, 18-Nov-2024.)
𝐹 = frecs(𝑅, 𝐴, 𝐺)       dom 𝐹𝐴
 
18-Nov-2024frrrel 8192 Show without using the axiom of replacement that the well-founded recursion generator gives a relation. (Contributed by Scott Fenton, 18-Nov-2024.)
𝐹 = frecs(𝑅, 𝐴, 𝐺)       Rel 𝐹
 
18-Nov-2024fpr2 8190 Law of well-founded recursion over a partial order, part two. Now we establish the value of 𝐹 within 𝐴. (Contributed by Scott Fenton, 11-Sep-2023.) (Proof shortened by Scott Fenton, 18-Nov-2024.)
𝐹 = frecs(𝑅, 𝐴, 𝐺)       (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ 𝑋𝐴) → (𝐹𝑋) = (𝑋𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑋))))
 
18-Nov-2024fpr2a 8188 Weak version of fpr2 8190 which is useful for proofs that avoid the axiom of replacement. (Contributed by Scott Fenton, 18-Nov-2024.)
𝐹 = frecs(𝑅, 𝐴, 𝐺)       (((𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴) ∧ 𝑋 ∈ dom 𝐹) → (𝐹𝑋) = (𝑋𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑋))))
 
18-Nov-2024csbfrecsg 8170 Move class substitution in and out of the well-founded recursive function generator. (Contributed by Scott Fenton, 18-Nov-2024.)
(𝐴𝑉𝐴 / 𝑥frecs(𝑅, 𝐷, 𝐹) = frecs(𝐴 / 𝑥𝑅, 𝐴 / 𝑥𝐷, 𝐴 / 𝑥𝐹))
 
18-Nov-2024drnf1v 2368 Formula-building lemma for use with the Distinctor Reduction Theorem. Version of drnf1 2441 with a disjoint variable condition, which does not require ax-13 2370. (Contributed by Mario Carneiro, 4-Oct-2016.) (Revised by BJ, 17-Jun-2019.) Avoid ax-10 2136. (Revised by Gino Giotto, 18-Nov-2024.)
(∀𝑥 𝑥 = 𝑦 → (𝜑𝜓))       (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑦𝜓))
 
18-Nov-2024dral1v 2365 Formula-building lemma for use with the Distinctor Reduction Theorem. Version of dral1 2437 with a disjoint variable condition, which does not require ax-13 2370. Remark: the corresponding versions for dral2 2436 and drex2 2440 are instances of albidv 1922 and exbidv 1923 respectively. (Contributed by NM, 24-Nov-1994.) (Revised by BJ, 17-Jun-2019.) Base the proof on ax12v 2171. (Revised by Wolf Lammen, 30-Mar-2024.) Avoid ax-10 2136. (Revised by Gino Giotto, 18-Nov-2024.)
(∀𝑥 𝑥 = 𝑦 → (𝜑𝜓))       (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓))
 
18-Nov-2024equsexv 2259 An equivalence related to implicit substitution. Version of equsex 2416 with a disjoint variable condition, which does not require ax-13 2370. See equsexvw 2007 for a version with two disjoint variable conditions requiring fewer axioms. See also the dual form equsalv 2258. (Contributed by NM, 5-Aug-1993.) (Revised by BJ, 31-May-2019.) Avoid ax-10 2136. (Revised by Gino Giotto, 18-Nov-2024.)
𝑥𝜓    &   (𝑥 = 𝑦 → (𝜑𝜓))       (∃𝑥(𝑥 = 𝑦𝜑) ↔ 𝜓)
 
17-Nov-2024bj-rdg0gALT 35355 Alternate proof of rdg0g 8328. More direct since it bypasses tz7.44-1 8307 and rdg0 8322 (and vtoclg 3514, vtoclga 3522). (Contributed by NM, 25-Apr-1995.) More direct proof. (Revised by BJ, 17-Nov-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
(𝐴𝑉 → (rec(𝐹, 𝐴)‘∅) = 𝐴)
 
17-Nov-2024wfrfun 8233 The "function" generated by the well-ordered recursion generator is indeed a function. Avoids the axiom of replacement. (Contributed by Scott Fenton, 21-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) (Revised by Scott Fenton, 17-Nov-2024.)
𝐹 = wrecs(𝑅, 𝐴, 𝐺)       ((𝑅 We 𝐴𝑅 Se 𝐴) → Fun 𝐹)
 
17-Nov-2024wfrdmcl 8232 The predecessor class of an element of the well-ordered recursion generator's domain is a subset of its domain. Avoids the axiom of replacement. (Contributed by Scott Fenton, 21-Apr-2011.) (Proof shortened by Scott Fenton, 17-Nov-2024.)
𝐹 = wrecs(𝑅, 𝐴, 𝐺)       (𝑋 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝐹)
 
17-Nov-2024wfrdmss 8231 The domain of the well-ordered recursion generator is a subclass of 𝐴. Avoids the axiom of replacement. (Contributed by Scott Fenton, 21-Apr-2011.) (Proof shortened by Scott Fenton, 17-Nov-2024.)
𝐹 = wrecs(𝑅, 𝐴, 𝐺)       dom 𝐹𝐴
 
17-Nov-2024wfrrel 8230 The well-ordered recursion generator generates a relation. Avoids the axiom of replacement. (Contributed by Scott Fenton, 8-Jun-2018.) (Proof shortened by Scott Fenton, 17-Nov-2024.)
𝐹 = wrecs(𝑅, 𝐴, 𝐺)       Rel 𝐹
 
17-Nov-2024nfwrecs 8202 Bound-variable hypothesis builder for the well-ordered recursive function generator. (Contributed by Scott Fenton, 9-Jun-2018.) (Proof shortened by Scott Fenton, 17-Nov-2024.)
𝑥𝑅    &   𝑥𝐴    &   𝑥𝐹       𝑥wrecs(𝑅, 𝐴, 𝐹)
 
17-Nov-2024wrecseq123 8200 General equality theorem for the well-ordered recursive function generator. (Contributed by Scott Fenton, 7-Jun-2018.) (Proof shortened by Scott Fenton, 17-Nov-2024.)
((𝑅 = 𝑆𝐴 = 𝐵𝐹 = 𝐺) → wrecs(𝑅, 𝐴, 𝐹) = wrecs(𝑆, 𝐵, 𝐺))
 
17-Nov-2024frrdmcl 8194 Show without using the axiom of replacement that for a "function" defined by well-founded recursion, the predecessor class of an element of its domain is a subclass of its domain. (Contributed by Scott Fenton, 21-Apr-2011.) (Proof shortened by Scott Fenton, 17-Nov-2024.)
𝐹 = frecs(𝑅, 𝐴, 𝐺)       (𝑋 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝐹)
 
17-Nov-2024wfis2fg 6295 Well-Ordered Induction Schema, using implicit substitution. (Contributed by Scott Fenton, 11-Feb-2011.) (Proof shortened by Scott Fenton, 17-Nov-2024.)
𝑦𝜓    &   (𝑦 = 𝑧 → (𝜑𝜓))    &   (𝑦𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓𝜑))       ((𝑅 We 𝐴𝑅 Se 𝐴) → ∀𝑦𝐴 𝜑)
 
17-Nov-2024wfisg 6292 Well-Ordered Induction Schema. If a property passes from all elements less than 𝑦 of a well-ordered class 𝐴 to 𝑦 itself (induction hypothesis), then the property holds for all elements of 𝐴. (Contributed by Scott Fenton, 11-Feb-2011.) (Proof shortened by Scott Fenton, 17-Nov-2024.)
(𝑦𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)[𝑧 / 𝑦]𝜑𝜑))       ((𝑅 We 𝐴𝑅 Se 𝐴) → ∀𝑦𝐴 𝜑)
 
17-Nov-2024wfi 6289 The Principle of Well-Ordered Induction. Theorem 6.27 of [TakeutiZaring] p. 32. This principle states that if 𝐵 is a subclass of a well-ordered class 𝐴 with the property that every element of 𝐵 whose inital segment is included in 𝐴 is itself equal to 𝐴. (Contributed by Scott Fenton, 29-Jan-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) (Proof shortened by Scott Fenton, 17-Nov-2024.)
(((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴 ∧ ∀𝑦𝐴 (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵𝑦𝐵))) → 𝐴 = 𝐵)
 
17-Nov-2024tz6.26 6286 All nonempty subclasses of a class having a well-ordered set-like relation have minimal elements for that relation. Proposition 6.26 of [TakeutiZaring] p. 31. (Contributed by Scott Fenton, 29-Jan-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) (Proof shortened by Scott Fenton, 17-Nov-2024.)
(((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → ∃𝑦𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)
 
17-Nov-2024cbvmptv 5205 Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.) Add disjoint variable condition to avoid auxiliary axioms . See cbvmptvg 5207 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 17-Nov-2024.)
(𝑥 = 𝑦𝐵 = 𝐶)       (𝑥𝐴𝐵) = (𝑦𝐴𝐶)
 
17-Nov-2024cbvopab1v 5171 Rule used to change the first bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 31-Jul-2003.) (Proof shortened by Eric Schmidt, 4-Apr-2007.) Reduce axiom usage. (Revised by Gino Giotto, 17-Nov-2024.)
(𝑥 = 𝑧 → (𝜑𝜓))       {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑦⟩ ∣ 𝜓}
 
16-Nov-2024frd 5579 A nonempty subset of an 𝑅-well-founded class has an 𝑅-minimal element (deduction form). (Contributed by BJ, 16-Nov-2024.)
(𝜑𝑅 Fr 𝐴)    &   (𝜑𝐵𝐴)    &   (𝜑𝐵𝑉)    &   (𝜑𝐵 ≠ ∅)       (𝜑 → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
 
16-Nov-2024dffr6 5578 Alternate definition of df-fr 5575. See dffr5 34010 for a definition without dummy variables (but note that their equivalence uses ax-sep 5243). (Contributed by BJ, 16-Nov-2024.)
(𝑅 Fr 𝐴 ↔ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦)
 
15-Nov-20241strbas 17026 The base set of a constructed one-slot structure. (Contributed by AV, 27-Mar-2020.) (Proof shortened by AV, 15-Nov-2024.)
𝐺 = {⟨(Base‘ndx), 𝐵⟩}       (𝐵𝑉𝐵 = (Base‘𝐺))
 
15-Nov-20241strstr1 17025 A constructed one-slot structure. (Contributed by AV, 15-Nov-2024.)
𝐺 = {⟨(Base‘ndx), 𝐵⟩}       𝐺 Struct ⟨(Base‘ndx), (Base‘ndx)⟩
 
14-Nov-2024aks4d1 40359 Lemma 4.1 from https://www3.nd.edu/%7eandyp/notes/AKS.pdf, existence of a polynomially bounded number by the digit size of 𝑁 that asserts the polynomial subspace that we need to search to guarantee that 𝑁 is prime. Eventually we want to show that the polynomial searching space is bounded by degree 𝐵. (Contributed by metakunt, 14-Nov-2024.)
(𝜑𝑁 ∈ (ℤ‘3))    &   𝐵 = (⌈‘((2 logb 𝑁)↑5))       (𝜑 → ∃𝑟 ∈ (1...𝐵)((𝑁 gcd 𝑟) = 1 ∧ ((2 logb 𝑁)↑2) < ((od𝑟)‘𝑁)))
 
14-Nov-2024aks4d1p9 40358 Show that the order is bound by the squared binary logarithm. (Contributed by metakunt, 14-Nov-2024.)
(𝜑𝑁 ∈ (ℤ‘3))    &   𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))    &   𝐵 = (⌈‘((2 logb 𝑁)↑5))    &   𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < )       (𝜑 → ((2 logb 𝑁)↑2) < ((od𝑅)‘𝑁))
 
14-Nov-2024aks4d1lem1 40332 Technical lemma to reduce proof size. (Contributed by metakunt, 14-Nov-2024.)
(𝜑𝑁 ∈ (ℤ‘3))    &   𝐵 = (⌈‘((2 logb 𝑁)↑5))       (𝜑 → (𝐵 ∈ ℕ ∧ 9 < 𝐵))
 
13-Nov-2024aks4d1p8d3 40356 The remainder of a division with its maximal prime power is coprime with that prime power. (Contributed by metakunt, 13-Nov-2024.)
(𝜑𝑁 ∈ ℕ)    &   (𝜑𝑃 ∈ ℙ)    &   (𝜑𝑃𝑁)       (𝜑 → ((𝑁 / (𝑃↑(𝑃 pCnt 𝑁))) gcd (𝑃↑(𝑃 pCnt 𝑁))) = 1)
 
13-Nov-2024aks4d1p8d2 40355 Any prime power dividing a positive integer is less than that integer if that integer has another prime factor. (Contributed by metakunt, 13-Nov-2024.)
(𝜑𝑅 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑃 ∈ ℙ)    &   (𝜑𝑄 ∈ ℙ)    &   (𝜑𝑃𝑅)    &   (𝜑𝑄𝑅)    &   (𝜑 → ¬ 𝑃𝑁)    &   (𝜑𝑄𝑁)       (𝜑 → (𝑃↑(𝑃 pCnt 𝑅)) < 𝑅)
 
12-Nov-2024prstcocval 46711 Orthocomplementation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) (Proof shortened by AV, 12-Nov-2024.)
(𝜑𝐶 = (ProsetToCat‘𝐾))    &   (𝜑𝐾 ∈ Proset )    &   (𝜑 = (oc‘𝐾))       (𝜑 = (oc‘𝐶))
 
12-Nov-2024prstcleval 46708 Value of the less-than-or-equal-to relation is unchanged. (Contributed by Zhi Wang, 20-Sep-2024.) (Proof shortened by AV, 12-Nov-2024.)
(𝜑𝐶 = (ProsetToCat‘𝐾))    &   (𝜑𝐾 ∈ Proset )    &   (𝜑 = (le‘𝐾))       (𝜑 = (le‘𝐶))
 
12-Nov-2024zlmtset 32212 Topology in a -module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.) (Proof shortened by AV, 12-Nov-2024.)
𝑊 = (ℤMod‘𝐺)    &   𝐽 = (TopSet‘𝐺)       (𝐺𝑉𝐽 = (TopSet‘𝑊))
 
12-Nov-2024setsmsbas 23734 The base set of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) (Proof shortened by AV, 12-Nov-2024.)
(𝜑𝑋 = (Base‘𝑀))    &   (𝜑𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋)))    &   (𝜑𝐾 = (𝑀 sSet ⟨(TopSet‘ndx), (MetOpen‘𝐷)⟩))       (𝜑𝑋 = (Base‘𝐾))
 
12-Nov-2024matvsca 21670 The matrix ring has the same scalar multiplication as its underlying linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015.) (Proof shortened by AV, 12-Nov-2024.)
𝐴 = (𝑁 Mat 𝑅)    &   𝐺 = (𝑅 freeLMod (𝑁 × 𝑁))       ((𝑁 ∈ Fin ∧ 𝑅𝑉) → ( ·𝑠𝐺) = ( ·𝑠𝐴))
 
12-Nov-2024matsca 21668 The matrix ring has the same scalars as its underlying linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015.) (Proof shortened by AV, 12-Nov-2024.)
𝐴 = (𝑁 Mat 𝑅)    &   𝐺 = (𝑅 freeLMod (𝑁 × 𝑁))       ((𝑁 ∈ Fin ∧ 𝑅𝑉) → (Scalar‘𝐺) = (Scalar‘𝐴))
 
12-Nov-2024sravsca 20555 The scalar product operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Proof shortened by AV, 12-Nov-2024.)
(𝜑𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   (𝜑𝑆 ⊆ (Base‘𝑊))       (𝜑 → (.r𝑊) = ( ·𝑠𝐴))
 
12-Nov-2024srasca 20553 The set of scalars of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Proof shortened by AV, 12-Nov-2024.)
(𝜑𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   (𝜑𝑆 ⊆ (Base‘𝑊))       (𝜑 → (𝑊s 𝑆) = (Scalar‘𝐴))
 
12-Nov-2024odubas 18106 Base set of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015.) (Proof shortened by AV, 12-Nov-2024.)
𝐷 = (ODual‘𝑂)    &   𝐵 = (Base‘𝑂)       𝐵 = (Base‘𝐷)
 
12-Nov-2024slotsdifocndx 17225 The index of the slot for the orthocomplementation is not the index of other slots. Formerly part of proof for prstcocval 46711. (Contributed by AV, 12-Nov-2024.)
((oc‘ndx) ≠ (comp‘ndx) ∧ (oc‘ndx) ≠ (Hom ‘ndx))
 
12-Nov-2024slotsdifplendx2 17224 The index of the slot for the "less than or equal to" ordering is not the index of other slots. Formerly part of proof for prstcleval 46708. (Contributed by AV, 12-Nov-2024.)
((le‘ndx) ≠ (comp‘ndx) ∧ (le‘ndx) ≠ (Hom ‘ndx))
 
12-Nov-2024slotsdifipndx 17142 The slot for the scalar is not the index of other slots. Formerly part of proof for srasca 20553 and sravsca 20555. (Contributed by AV, 12-Nov-2024.)
(( ·𝑠 ‘ndx) ≠ (·𝑖‘ndx) ∧ (Scalar‘ndx) ≠ (·𝑖‘ndx))
 
12-Nov-2024ssdomfi 9064 A finite set dominates its subsets, proved without using the Axiom of Power Sets (unlike ssdomg 8861). (Contributed by BTernaryTau, 12-Nov-2024.)
(𝐵 ∈ Fin → (𝐴𝐵𝐴𝐵))
 
11-Nov-2024mpteq1df 43115 An equality theorem for the maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) (Proof shortened by SN, 11-Nov-2024.)
𝑥𝜑    &   (𝜑𝐴 = 𝐵)       (𝜑 → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
 
11-Nov-2024mhphf2 40554 A homogeneous polynomial defines a homogeneous function; this is mhphf 40553 with simpler notation in the conclusion in exchange for a complex definition of , which is based on frlmvscafval 21079 but without the finite support restriction (frlmpws 21063, frlmbas 21068) on the assignments 𝐴 from variables to values.

TODO?: Polynomials (df-mpl 21220) are defined to have a finite amount of terms (of finite degree). As such, any assignment may be replaced by an assignment with finite support (as only a finite amount of variables matter in a given polynomial, even if the set of variables is infinite). So the finite support restriction can be assumed without loss of generality. (Contributed by SN, 11-Nov-2024.)

𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)    &   𝐻 = (𝐼 mHomP 𝑈)    &   𝑈 = (𝑆s 𝑅)    &   𝐾 = (Base‘𝑆)    &    = ( ·𝑠 ‘((ringLMod‘𝑆) ↑s 𝐼))    &    · = (.r𝑆)    &    = (.g‘(mulGrp‘𝑆))    &   (𝜑𝐼𝑉)    &   (𝜑𝑆 ∈ CRing)    &   (𝜑𝑅 ∈ (SubRing‘𝑆))    &   (𝜑𝐿𝑅)    &   (𝜑𝑁 ∈ ℕ0)    &   (𝜑𝑋 ∈ (𝐻𝑁))    &   (𝜑𝐴 ∈ (𝐾m 𝐼))       (𝜑 → ((𝑄𝑋)‘(𝐿 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑋)‘𝐴)))
 
11-Nov-2024zlmds 32210 Distance in a -module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017.) (Proof shortened by AV, 11-Nov-2024.)
𝑊 = (ℤMod‘𝐺)    &   𝐷 = (dist‘𝐺)       (𝐺𝑉𝐷 = (dist‘𝑊))
 
11-Nov-2024setsmsds 23736 The distance function of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) (Proof shortened by AV, 11-Nov-2024.)
(𝜑𝑋 = (Base‘𝑀))    &   (𝜑𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋)))    &   (𝜑𝐾 = (𝑀 sSet ⟨(TopSet‘ndx), (MetOpen‘𝐷)⟩))       (𝜑 → (dist‘𝑀) = (dist‘𝐾))
 
11-Nov-2024thlle 21009 Ordering on the Hilbert lattice of closed subspaces. (Contributed by Mario Carneiro, 25-Oct-2015.) (Proof shortened by AV, 11-Nov-2024.)
𝐾 = (toHL‘𝑊)    &   𝐶 = (ClSubSp‘𝑊)    &   𝐼 = (toInc‘𝐶)    &    = (le‘𝐼)        = (le‘𝐾)
 
11-Nov-2024thlbas 21007 Base set of the Hilbert lattice of closed subspaces. (Contributed by Mario Carneiro, 25-Oct-2015.) (Proof shortened by AV, 11-Nov-2024.)
𝐾 = (toHL‘𝑊)    &   𝐶 = (ClSubSp‘𝑊)       𝐶 = (Base‘𝐾)
 
11-Nov-2024cnfldfunALT 20716 The field of complex numbers is a function. Alternate proof of cnfldfun 20715 not requiring that the index set of the components is ordered, but using quadratically many inequalities for the indices. (Contributed by AV, 14-Nov-2021.) (Proof shortened by AV, 11-Nov-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
Fun ℂfld
 
11-Nov-2024fldidom 20682 A field is an integral domain. (Contributed by Mario Carneiro, 29-Mar-2015.) (Proof shortened by SN, 11-Nov-2024.)
(𝑅 ∈ Field → 𝑅 ∈ IDomn)
 
11-Nov-2024slotsdifdsndx 17201 The index of the slot for the distance is not the index of other slots. Formerly part of proof for cnfldfunALT 20716. (Contributed by AV, 11-Nov-2024.)
((*𝑟‘ndx) ≠ (dist‘ndx) ∧ (le‘ndx) ≠ (dist‘ndx))
 
11-Nov-2024plendxnocndx 17191 The slot for the orthocomplementation is not the slot for the order in an extensible structure. Formerly part of proof for thlle 21009. (Contributed by AV, 11-Nov-2024.)
(le‘ndx) ≠ (oc‘ndx)
 
11-Nov-2024basendxnocndx 17190 The slot for the orthocomplementation is not the slot for the base set in an extensible structure. Formerly part of proof for thlbas 21007. (Contributed by AV, 11-Nov-2024.)
(Base‘ndx) ≠ (oc‘ndx)
 
11-Nov-2024slotsdifplendx 17182 The index of the slot for the distance is not the index of other slots. Formerly part of proof for cnfldfunALT 20716. (Contributed by AV, 11-Nov-2024.)
((*𝑟‘ndx) ≠ (le‘ndx) ∧ (TopSet‘ndx) ≠ (le‘ndx))
 
11-Nov-2024tsetndxnstarvndx 17166 The slot for the topology is not the slot for the involution in an extensible structure. Formerly part of proof for cnfldfunALT 20716. (Contributed by AV, 11-Nov-2024.)
(TopSet‘ndx) ≠ (*𝑟‘ndx)
 
11-Nov-2024nneneq 9074 Two equinumerous natural numbers are equal. Proposition 10.20 of [TakeutiZaring] p. 90 and its converse. Also compare Corollary 6E of [Enderton] p. 136. (Contributed by NM, 28-May-1998.) Avoid ax-pow 5308. (Revised by BTernaryTau, 11-Nov-2024.)
((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴𝐵𝐴 = 𝐵))
 
11-Nov-2024ofeqd 7597 Equality theorem for function operation, deduction form. (Contributed by SN, 11-Nov-2024.)
(𝜑𝑅 = 𝑆)       (𝜑 → ∘f 𝑅 = ∘f 𝑆)
 
11-Nov-2024iunopab 5503 Move indexed union inside an ordered-pair class abstraction. (Contributed by Stefan O'Rear, 20-Feb-2015.) Avoid ax-sep 5243, ax-nul 5250, ax-pr 5372. (Revised by SN, 11-Nov-2024.)
𝑧𝐴 {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝐴 𝜑}
 
11-Nov-2024mpteq2ia 5195 An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Proof shortened by SN, 11-Nov-2024.)
(𝑥𝐴𝐵 = 𝐶)       (𝑥𝐴𝐵) = (𝑥𝐴𝐶)
 
11-Nov-2024mpteq2dva 5192 Slightly more general equality inference for the maps-to notation. (Contributed by Scott Fenton, 25-Apr-2012.) Remove dependency on ax-10 2136. (Revised by SN, 11-Nov-2024.)
((𝜑𝑥𝐴) → 𝐵 = 𝐶)       (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
 
11-Nov-2024mpteq2da 5190 Slightly more general equality inference for the maps-to notation. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.) (Proof shortened by SN, 11-Nov-2024.)
𝑥𝜑    &   ((𝜑𝑥𝐴) → 𝐵 = 𝐶)       (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
 
11-Nov-2024mpteq1i 5188 An equality theorem for the maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.) Remove all disjoint variable conditions. (Revised by SN, 11-Nov-2024.)
𝐴 = 𝐵       (𝑥𝐴𝐶) = (𝑥𝐵𝐶)
 
11-Nov-2024mpteq1 5185 An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Proof shortened by SN, 11-Nov-2024.)
(𝐴 = 𝐵 → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
 
11-Nov-2024mpteq12dva 5181 An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.) Remove dependency on ax-10 2136, ax-12 2170. (Revised by SN, 11-Nov-2024.)
(𝜑𝐴 = 𝐶)    &   ((𝜑𝑥𝐴) → 𝐵 = 𝐷)       (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
 
11-Nov-2024mpteq12df 5178 An equality inference for the maps-to notation. Compare mpteq12dv 5183. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Mario Carneiro, 11-Dec-2016.) (Proof shortened by SN, 11-Nov-2024.)
𝑥𝜑    &   (𝜑𝐴 = 𝐶)    &   (𝜑𝐵 = 𝐷)       (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
 
11-Nov-2024mpteq12da 5177 An equality inference for the maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) Remove dependency on ax-10 2136. (Revised by SN, 11-Nov-2024.)
𝑥𝜑    &   (𝜑𝐴 = 𝐶)    &   ((𝜑𝑥𝐴) → 𝐵 = 𝐷)       (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
 
10-Nov-2024aks4d1p8 40357 Show that 𝑁 and 𝑅 are coprime for AKS existence theorem, with eliminated hypothesis. (Contributed by metakunt, 10-Nov-2024.) (Proof sketch by Thierry Arnoux.)
(𝜑𝑁 ∈ (ℤ‘3))    &   𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))    &   𝐵 = (⌈‘((2 logb 𝑁)↑5))    &   𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < )       (𝜑 → (𝑁 gcd 𝑅) = 1)
 
10-Nov-2024aks4d1p8d1 40354 If a prime divides one number 𝑀, but not another number 𝑁, then it divides the quotient of 𝑀 and the gcd of 𝑀 and 𝑁. (Contributed by Thierry Arnoux, 10-Nov-2024.)
(𝜑𝑃 ∈ ℙ)    &   (𝜑𝑀 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑃𝑀)    &   (𝜑 → ¬ 𝑃𝑁)       (𝜑𝑃 ∥ (𝑀 / (𝑀 gcd 𝑁)))
 
10-Nov-2024slotsdifunifndx 17208 The index of the slot for the uniform set is not the index of other slots. Formerly part of proof for cnfldfunALT 20716. (Contributed by AV, 10-Nov-2024.)
(((+g‘ndx) ≠ (UnifSet‘ndx) ∧ (.r‘ndx) ≠ (UnifSet‘ndx) ∧ (*𝑟‘ndx) ≠ (UnifSet‘ndx)) ∧ ((le‘ndx) ≠ (UnifSet‘ndx) ∧ (dist‘ndx) ≠ (UnifSet‘ndx)))
 
9-Nov-2024bj-flddrng 35573 Fields are division rings (elemental version). (Contributed by BJ, 9-Nov-2024.)
(𝐹 ∈ Field → 𝐹 ∈ DivRing)
 
9-Nov-2024bj-dfid2ALT 35349 Alternate version of dfid2 5520. (Contributed by BJ, 9-Nov-2024.) (Proof modification is discouraged.) Use df-id 5518 instead to make the semantics of the construction df-opab 5155 clearer. (New usage is discouraged.)
I = {⟨𝑥, 𝑥⟩ ∣ ⊤}
 
9-Nov-2024ttgval 27525 Define a function to augment a subcomplex Hilbert space with betweenness and a line definition. (Contributed by Thierry Arnoux, 25-Mar-2019.) (Proof shortened by AV, 9-Nov-2024.)
𝐺 = (toTG‘𝐻)    &   𝐵 = (Base‘𝐻)    &    = (-g𝐻)    &    · = ( ·𝑠𝐻)    &   𝐼 = (Itv‘𝐺)       (𝐻𝑉 → (𝐺 = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})⟩) ∧ 𝐼 = (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})))
 
9-Nov-2024lngndxnitvndx 27093 The slot for the line is not the slot for the Interval (segment) in an extensible structure. Formerly part of proof for ttgval 27525. (Contributed by AV, 9-Nov-2024.)
(LineG‘ndx) ≠ (Itv‘ndx)
 
9-Nov-2024rescabs 17644 Restriction absorption law. (Contributed by Mario Carneiro, 6-Jan-2017.) (Proof shortened by AV, 9-Nov-2024.)
(𝜑𝐶𝑉)    &   (𝜑𝐻 Fn (𝑆 × 𝑆))    &   (𝜑𝐽 Fn (𝑇 × 𝑇))    &   (𝜑𝑆𝑊)    &   (𝜑𝑇𝑆)       (𝜑 → ((𝐶cat 𝐻) ↾cat 𝐽) = (𝐶cat 𝐽))
 
7-Nov-2024ressbas 17044 Base set of a structure restriction. (Contributed by Stefan O'Rear, 26-Nov-2014.) (Proof shortened by AV, 7-Nov-2024.)
𝑅 = (𝑊s 𝐴)    &   𝐵 = (Base‘𝑊)       (𝐴𝑉 → (𝐴𝐵) = (Base‘𝑅))
 
7-Nov-2024setsnid 17007 Value of the structure replacement function at an untouched index. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) (Proof shortened by AV, 7-Nov-2024.)
𝐸 = Slot (𝐸‘ndx)    &   (𝐸‘ndx) ≠ 𝐷       (𝐸𝑊) = (𝐸‘(𝑊 sSet ⟨𝐷, 𝐶⟩))
 
6-Nov-2024sn-iotalemcor 40456 Corollary of sn-iotalem 40455. Compare sb8iota 6443. (Contributed by SN, 6-Nov-2024.)
(℩𝑥𝜑) = (℩𝑦{𝑥𝜑} = {𝑦})
 
6-Nov-2024sn-iotalem 40455 An unused lemma showing that many equivalences involving df-iota 6431 are potentially provable without ax-10 2136, ax-11 2153, ax-12 2170. (Contributed by SN, 6-Nov-2024.)
{𝑦 ∣ {𝑥𝜑} = {𝑦}} = {𝑧 ∣ {𝑦 ∣ {𝑥𝜑} = {𝑦}} = {𝑧}}
 
6-Nov-2024eqimssd 40448 Equality implies inclusion, deduction version. (Contributed by SN, 6-Nov-2024.)
(𝜑𝐴 = 𝐵)       (𝜑𝐴𝐵)
 
6-Nov-2024hlhilsmul 40220 Scalar multiplication for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) (Revised by AV, 6-Nov-2024.)
𝐻 = (LHyp‘𝐾)    &   𝐸 = ((EDRing‘𝐾)‘𝑊)    &   𝑈 = ((HLHil‘𝐾)‘𝑊)    &   𝑅 = (Scalar‘𝑈)    &   (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))    &    · = (.r𝐸)       (𝜑· = (.r𝑅))
 
6-Nov-2024hlhilsplus 40218 Scalar addition for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) (Revised by AV, 6-Nov-2024.)
𝐻 = (LHyp‘𝐾)    &   𝐸 = ((EDRing‘𝐾)‘𝑊)    &   𝑈 = ((HLHil‘𝐾)‘𝑊)    &   𝑅 = (Scalar‘𝑈)    &   (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))    &    + = (+g𝐸)       (𝜑+ = (+g𝑅))
 
6-Nov-2024hlhilsbase 40216 The scalar base set of the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) (Revised by AV, 6-Nov-2024.)
𝐻 = (LHyp‘𝐾)    &   𝐸 = ((EDRing‘𝐾)‘𝑊)    &   𝑈 = ((HLHil‘𝐾)‘𝑊)    &   𝑅 = (Scalar‘𝑈)    &   (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))    &   𝐶 = (Base‘𝐸)       (𝜑𝐶 = (Base‘𝑅))
 
6-Nov-2024hlhilslem 40214 Lemma for hlhilsbase 40216 etc. (Contributed by Mario Carneiro, 28-Jun-2015.) (Revised by AV, 6-Nov-2024.)
𝐻 = (LHyp‘𝐾)    &   𝐸 = ((EDRing‘𝐾)‘𝑊)    &   𝑈 = ((HLHil‘𝐾)‘𝑊)    &   𝑅 = (Scalar‘𝑈)    &   (𝜑 → (𝐾 ∈ HL ∧ 𝑊𝐻))    &   𝐹 = Slot (𝐹‘ndx)    &   (𝐹‘ndx) ≠ (*𝑟‘ndx)    &   𝐶 = (𝐹𝐸)       (𝜑𝐶 = (𝐹𝑅))
 
6-Nov-2024oppradd 19966 Addition operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.)
𝑂 = (oppr𝑅)    &    + = (+g𝑅)        + = (+g𝑂)
 
6-Nov-2024opprbas 19964 Base set of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.)
𝑂 = (oppr𝑅)    &   𝐵 = (Base‘𝑅)       𝐵 = (Base‘𝑂)
 
6-Nov-2024opprlem 19962 Lemma for opprbas 19964 and oppradd 19966. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by AV, 6-Nov-2024.)
𝑂 = (oppr𝑅)    &   𝐸 = Slot (𝐸‘ndx)    &   (𝐸‘ndx) ≠ (.r‘ndx)       (𝐸𝑅) = (𝐸𝑂)
 
6-Nov-2024symgvalstruct 19100 The value of the symmetric group function at 𝐴 represented as extensible structure with three slots. This corresponds to the former definition of SymGrp. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by Mario Carneiro, 12-Jan-2015.) (Revised by AV, 31-Mar-2024.) (Proof shortened by AV, 6-Nov-2024.)
𝐺 = (SymGrp‘𝐴)    &   𝐵 = {𝑥𝑥:𝐴1-1-onto𝐴}    &   𝑀 = (𝐴m 𝐴)    &    + = (𝑓𝑀, 𝑔𝑀 ↦ (𝑓𝑔))    &   𝐽 = (∏t‘(𝐴 × {𝒫 𝐴}))       (𝐴𝑉𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩})
 
6-Nov-2024frmdplusg 18589 The monoid operation of a free monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.) (Proof shortened by AV, 6-Nov-2024.)
𝑀 = (freeMnd‘𝐼)    &   𝐵 = (Base‘𝑀)    &    + = (+g𝑀)        + = ( ++ ↾ (𝐵 × 𝐵))
 
6-Nov-2024iotaex 6452 Theorem 8.23 in [Quine] p. 58. This theorem proves the existence of the class under our definition. (Contributed by Andrew Salmon, 11-Jul-2011.) Remove dependency on ax-10 2136, ax-11 2153, ax-12 2170. (Revised by SN, 6-Nov-2024.)
(℩𝑥𝜑) ∈ V
 
6-Nov-2024iotassuni 6451 The class is a subset of the union of all elements satisfying 𝜑. (Contributed by Mario Carneiro, 24-Dec-2016.) Remove dependency on ax-10 2136, ax-11 2153, ax-12 2170. (Revised by SN, 6-Nov-2024.)
(℩𝑥𝜑) ⊆ {𝑥𝜑}
 
6-Nov-2024iotanul2 6449 Version of iotanul 6457 using df-iota 6431 instead of dfiota2 6432. (Contributed by SN, 6-Nov-2024.)
(¬ ∃𝑦{𝑥𝜑} = {𝑦} → (℩𝑥𝜑) = ∅)
 
6-Nov-2024iotauni2 6448 Version of iotauni 6454 using df-iota 6431 instead of dfiota2 6432. (Contributed by SN, 6-Nov-2024.)
(∃𝑦{𝑥𝜑} = {𝑦} → (℩𝑥𝜑) = {𝑥𝜑})
 
6-Nov-2024iotaval2 6447 Version of iotaval 6450 using df-iota 6431 instead of dfiota2 6432. (Contributed by SN, 6-Nov-2024.)
({𝑥𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦)
 
5-Nov-2024dfid2 5520 Alternate definition of the identity relation. Instance of dfid3 5521 not requiring auxiliary axioms. (Contributed by NM, 15-Mar-2007.) Reduce axiom usage. (Revised by Gino Giotto, 4-Nov-2024.) (Proof shortened by BJ, 5-Nov-2024.)

Use df-id 5518 instead to make the semantics of the constructor df-opab 5155 clearer. (New usage is discouraged.)

I = {⟨𝑥, 𝑥⟩ ∣ 𝑥 = 𝑥}
 
5-Nov-2024r19.30 3119 Restricted quantifier version of 19.30 1883. (Contributed by Scott Fenton, 25-Feb-2011.) (Proof shortened by Wolf Lammen, 5-Nov-2024.)
(∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 ∨ ∃𝑥𝐴 𝜓))
 
4-Nov-2024phplem2 9073 Lemma for Pigeonhole Principle. Equinumerosity of successors implies equinumerosity of the original natural numbers. (Contributed by NM, 28-May-1998.) (Revised by Mario Carneiro, 24-Jun-2015.) Avoid ax-pow 5308. (Revised by BTernaryTau, 4-Nov-2024.)
𝐴 ∈ V       ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc 𝐴 ≈ suc 𝐵𝐴𝐵))
 
4-Nov-2024sbthfi 9067 Schroeder-Bernstein Theorem for finite sets, proved without using the Axiom of Power Sets (unlike sbth 8958). (Contributed by BTernaryTau, 4-Nov-2024.)
((𝐵 ∈ Fin ∧ 𝐴𝐵𝐵𝐴) → 𝐴𝐵)
 
4-Nov-2024sbthfilem 9066 Lemma for sbthfi 9067. (Contributed by BTernaryTau, 4-Nov-2024.)
𝐴 ∈ V    &   𝐷 = {𝑥 ∣ (𝑥𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓𝑥))) ⊆ (𝐴𝑥))}    &   𝐻 = ((𝑓 𝐷) ∪ (𝑔 ↾ (𝐴 𝐷)))    &   𝐵 ∈ V       ((𝐵 ∈ Fin ∧ 𝐴𝐵𝐵𝐴) → 𝐴𝐵)
 
4-Nov-2024r19.12 3293 Restricted quantifier version of 19.12 2320. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) Avoid ax-13 2370, ax-ext 2707. (Revised by Wolf Lammen, 17-Jun-2023.) (Proof shortened by Wolf Lammen, 4-Nov-2024.)
(∃𝑥𝐴𝑦𝐵 𝜑 → ∀𝑦𝐵𝑥𝐴 𝜑)
 
4-Nov-2024r19.29vva 3203 A commonly used pattern based on r19.29 3113, version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Proof shortened by Wolf Lammen, 4-Nov-2024.)
((((𝜑𝑥𝐴) ∧ 𝑦𝐵) ∧ 𝜓) → 𝜒)    &   (𝜑 → ∃𝑥𝐴𝑦𝐵 𝜓)       (𝜑𝜒)
 
4-Nov-2024reximdvai 3158 Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 14-Nov-2002.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 8-Jan-2020.) (Proof shortened by Wolf Lammen, 4-Nov-2024.)
(𝜑 → (𝑥𝐴 → (𝜓𝜒)))       (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
 
4-Nov-2024r19.29d2r 3133 Theorem 19.29 of [Margaris] p. 90 with two restricted quantifiers, deduction version. (Contributed by Thierry Arnoux, 30-Jan-2017.) (Proof shortened by Wolf Lammen, 4-Nov-2024.)
(𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)    &   (𝜑 → ∃𝑥𝐴𝑦𝐵 𝜒)       (𝜑 → ∃𝑥𝐴𝑦𝐵 (𝜓𝜒))
 
4-Nov-2024ralrexbid 3105 Formula-building rule for restricted existential quantifier, using a restricted universal quantifier to bind the quantified variable in the antecedent. (Contributed by AV, 21-Oct-2023.) Reduce axiom usage. (Revised by SN, 13-Nov-2023.) (Proof shortened by Wolf Lammen, 4-Nov-2024.)
(𝜑 → (𝜓𝜃))       (∀𝑥𝐴 𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜃))
 
4-Nov-2024exexw 2053 Existential quantification over a given variable is idempotent. Weak version of bj-exexbiex 34978, requiring fewer axioms. (Contributed by Gino Giotto, 4-Nov-2024.)
(𝑥 = 𝑦 → (𝜑𝜓))       (∃𝑥𝜑 ↔ ∃𝑥𝑥𝜑)
 
3-Nov-2024znmul 20854 The multiplicative structure of ℤ/n is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 3-Nov-2024.)
𝑆 = (RSpan‘ℤring)    &   𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁})))    &   𝑌 = (ℤ/nℤ‘𝑁)       (𝑁 ∈ ℕ0 → (.r𝑈) = (.r𝑌))
 
3-Nov-2024znadd 20852 The additive structure of ℤ/n is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 3-Nov-2024.)
𝑆 = (RSpan‘ℤring)    &   𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁})))    &   𝑌 = (ℤ/nℤ‘𝑁)       (𝑁 ∈ ℕ0 → (+g𝑈) = (+g𝑌))
 
3-Nov-2024znbas2 20850 The base set of ℤ/n is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 3-Nov-2024.)
𝑆 = (RSpan‘ℤring)    &   𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁})))    &   𝑌 = (ℤ/nℤ‘𝑁)       (𝑁 ∈ ℕ0 → (Base‘𝑈) = (Base‘𝑌))
 
3-Nov-2024znbaslem 20848 Lemma for znbas 20857. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 9-Sep-2021.) (Revised by AV, 3-Nov-2024.)
𝑆 = (RSpan‘ℤring)    &   𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁})))    &   𝑌 = (ℤ/nℤ‘𝑁)    &   𝐸 = Slot (𝐸‘ndx)    &   (𝐸‘ndx) ≠ (le‘ndx)       (𝑁 ∈ ℕ0 → (𝐸𝑈) = (𝐸𝑌))
 
3-Nov-2024zlmmulr 20830 Ring operation of a -module (if present). (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
𝑊 = (ℤMod‘𝐺)    &    · = (.r𝐺)        · = (.r𝑊)
 
3-Nov-2024zlmplusg 20828 Group operation of a -module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
𝑊 = (ℤMod‘𝐺)    &    + = (+g𝐺)        + = (+g𝑊)
 
3-Nov-2024zlmbas 20826 Base set of a -module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
𝑊 = (ℤMod‘𝐺)    &   𝐵 = (Base‘𝐺)       𝐵 = (Base‘𝑊)
 
3-Nov-2024zlmlem 20824 Lemma for zlmbas 20826 and zlmplusg 20828. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
𝑊 = (ℤMod‘𝐺)    &   𝐸 = Slot (𝐸‘ndx)    &   (𝐸‘ndx) ≠ (Scalar‘ndx)    &   (𝐸‘ndx) ≠ ( ·𝑠 ‘ndx)       (𝐸𝐺) = (𝐸𝑊)
 
3-Nov-2024nelb 3218 A definition of ¬ 𝐴𝐵. (Contributed by Thierry Arnoux, 20-Nov-2023.) (Proof shortened by SN, 23-Jan-2024.) (Proof shortened by Wolf Lammen, 3-Nov-2024.)
𝐴𝐵 ↔ ∀𝑥𝐵 𝑥𝐴)
 
3-Nov-2024rexbi 3103 Distribute restricted quantification over a biconditional. (Contributed by Scott Fenton, 7-Aug-2024.) (Proof shortened by Wolf Lammen, 3-Nov-2024.)
(∀𝑥𝐴 (𝜑𝜓) → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 𝜓))
 
2-Nov-2024psrvscafval 21265 The scalar multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.) (Proof shortened by AV, 2-Nov-2024.)
𝑆 = (𝐼 mPwSer 𝑅)    &    = ( ·𝑠𝑆)    &   𝐾 = (Base‘𝑅)    &   𝐵 = (Base‘𝑆)    &    · = (.r𝑅)    &   𝐷 = { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}        = (𝑥𝐾, 𝑓𝐵 ↦ ((𝐷 × {𝑥}) ∘f · 𝑓))
 
2-Nov-2024zlmsca 20832 Scalar ring of a -module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.) (Proof shortened by AV, 2-Nov-2024.)
𝑊 = (ℤMod‘𝐺)       (𝐺𝑉 → ℤring = (Scalar‘𝑊))
 
2-Nov-2024rexab 3641 Existential quantification over a class abstraction. (Contributed by Mario Carneiro, 23-Jan-2014.) (Revised by Mario Carneiro, 3-Sep-2015.) Reduce axiom usage. (Revised by Gino Giotto, 2-Nov-2024.)
(𝑦 = 𝑥 → (𝜑𝜓))       (∃𝑥 ∈ {𝑦𝜑}𝜒 ↔ ∃𝑥(𝜓𝜒))
 
2-Nov-2024ralab 3638 Universal quantification over a class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.) Reduce axiom usage. (Revised by Gino Giotto, 2-Nov-2024.)
(𝑦 = 𝑥 → (𝜑𝜓))       (∀𝑥 ∈ {𝑦𝜑}𝜒 ↔ ∀𝑥(𝜓𝜒))
 
1-Nov-2024mnringvscad 42171 The scalar product of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (Proof shortened by AV, 1-Nov-2024.)
𝐹 = (𝑅 MndRing 𝑀)    &   𝐵 = (Base‘𝑀)    &   𝑉 = (𝑅 freeLMod 𝐵)    &   (𝜑𝑅𝑈)    &   (𝜑𝑀𝑊)       (𝜑 → ( ·𝑠𝑉) = ( ·𝑠𝐹))
 
1-Nov-2024mnringscad 42169 The scalar ring of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (Proof shortened by AV, 1-Nov-2024.)
𝐹 = (𝑅 MndRing 𝑀)    &   (𝜑𝑅𝑈)    &   (𝜑𝑀𝑊)       (𝜑𝑅 = (Scalar‘𝐹))
 
1-Nov-2024mnringaddgd 42164 The additive operation of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (Proof shortened by AV, 1-Nov-2024.)
𝐹 = (𝑅 MndRing 𝑀)    &   𝐴 = (Base‘𝑀)    &   𝑉 = (𝑅 freeLMod 𝐴)    &   (𝜑𝑅𝑈)    &   (𝜑𝑀𝑊)       (𝜑 → (+g𝑉) = (+g𝐹))
 
1-Nov-2024mnringbased 42158 The base set of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (Proof shortened by AV, 1-Nov-2024.)
𝐹 = (𝑅 MndRing 𝑀)    &   𝐴 = (Base‘𝑀)    &   𝑉 = (𝑅 freeLMod 𝐴)    &   𝐵 = (Base‘𝑉)    &   (𝜑𝑅𝑈)    &   (𝜑𝑀𝑊)       (𝜑𝐵 = (Base‘𝐹))
 
1-Nov-2024mnringnmulrd 42156 Components of a monoid ring other than its ring product match its underlying free module. (Contributed by Rohan Ridenour, 14-May-2024.) (Revised by AV, 1-Nov-2024.)
𝐹 = (𝑅 MndRing 𝑀)    &   𝐸 = Slot (𝐸‘ndx)    &   (𝐸‘ndx) ≠ (.r‘ndx)    &   𝐴 = (Base‘𝑀)    &   𝑉 = (𝑅 freeLMod 𝐴)    &   (𝜑𝑅𝑈)    &   (𝜑𝑀𝑊)       (𝜑 → (𝐸𝑉) = (𝐸𝐹))
 
1-Nov-2024opsrsca 21366 The scalar ring of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) (Revised by AV, 1-Nov-2024.)
𝑆 = (𝐼 mPwSer 𝑅)    &   𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   (𝜑𝑇 ⊆ (𝐼 × 𝐼))    &   (𝜑𝐼𝑉)    &   (𝜑𝑅𝑊)       (𝜑𝑅 = (Scalar‘𝑂))
 
1-Nov-2024opsrvsca 21364 The scalar product operation of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) (Revised by AV, 1-Nov-2024.)
𝑆 = (𝐼 mPwSer 𝑅)    &   𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   (𝜑𝑇 ⊆ (𝐼 × 𝐼))       (𝜑 → ( ·𝑠𝑆) = ( ·𝑠𝑂))
 
1-Nov-2024opsrmulr 21362 The multiplication operation of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) (Revised by AV, 1-Nov-2024.)
𝑆 = (𝐼 mPwSer 𝑅)    &   𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   (𝜑𝑇 ⊆ (𝐼 × 𝐼))       (𝜑 → (.r𝑆) = (.r𝑂))
 
1-Nov-2024opsrplusg 21360 The addition operation of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) (Revised by AV, 1-Nov-2024.)
𝑆 = (𝐼 mPwSer 𝑅)    &   𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   (𝜑𝑇 ⊆ (𝐼 × 𝐼))       (𝜑 → (+g𝑆) = (+g𝑂))
 
1-Nov-2024opsrbas 21358 The base set of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 30-Aug-2015.) (Revised by AV, 1-Nov-2024.)
𝑆 = (𝐼 mPwSer 𝑅)    &   𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   (𝜑𝑇 ⊆ (𝐼 × 𝐼))       (𝜑 → (Base‘𝑆) = (Base‘𝑂))
 
1-Nov-2024opsrbaslem 21356 Get a component of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 9-Sep-2021.) (Revised by AV, 1-Nov-2024.)
𝑆 = (𝐼 mPwSer 𝑅)    &   𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)    &   (𝜑𝑇 ⊆ (𝐼 × 𝐼))    &   𝐸 = Slot (𝐸‘ndx)    &   (𝐸‘ndx) ≠ (le‘ndx)       (𝜑 → (𝐸𝑆) = (𝐸𝑂))
 
1-Nov-2024plendxnvscandx 17181 The slot for the "less than or equal to" ordering is not the slot for the scalar product in an extensible structure. Formerly part of proof for opsrvsca 21364. (Contributed by AV, 1-Nov-2024.)
(le‘ndx) ≠ ( ·𝑠 ‘ndx)
 
1-Nov-2024plendxnscandx 17180 The slot for the "less than or equal to" ordering is not the slot for the scalar in an extensible structure. Formerly part of proof for opsrsca 21366. (Contributed by AV, 1-Nov-2024.)
(le‘ndx) ≠ (Scalar‘ndx)
 
1-Nov-2024plendxnmulrndx 17179 The slot for the "less than or equal to" ordering is not the slot for the ring multiplication operation in an extensible structure. Formerly part of proof for opsrmulr 21362. (Contributed by AV, 1-Nov-2024.)
(le‘ndx) ≠ (.r‘ndx)
 
31-Oct-2024fnimafnex 41377 The functional image of a function value exists. (Contributed by RP, 31-Oct-2024.)
𝐹 Fn 𝐵       (𝐹 “ (𝐺𝐴)) ∈ V
 
31-Oct-2024mendvscafval 41286 Scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.)
𝐴 = (MEndo‘𝑀)    &    · = ( ·𝑠𝑀)    &   𝐵 = (Base‘𝐴)    &   𝑆 = (Scalar‘𝑀)    &   𝐾 = (Base‘𝑆)    &   𝐸 = (Base‘𝑀)       ( ·𝑠𝐴) = (𝑥𝐾, 𝑦𝐵 ↦ ((𝐸 × {𝑥}) ∘f · 𝑦))
 
31-Oct-2024mendsca 41285 The module endomorphism algebra has the same scalars as the underlying module. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.)
𝐴 = (MEndo‘𝑀)    &   𝑆 = (Scalar‘𝑀)       𝑆 = (Scalar‘𝐴)
 
31-Oct-2024mendmulrfval 41283 Multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.)
𝐴 = (MEndo‘𝑀)    &   𝐵 = (Base‘𝐴)       (.r𝐴) = (𝑥𝐵, 𝑦𝐵 ↦ (𝑥𝑦))
 
31-Oct-2024mendplusgfval 41281 Addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.)
𝐴 = (MEndo‘𝑀)    &   𝐵 = (Base‘𝐴)    &    + = (+g𝑀)       (+g𝐴) = (𝑥𝐵, 𝑦𝐵 ↦ (𝑥f + 𝑦))
 
31-Oct-2024aks4d1p7 40353 Technical step in AKS lemma 4.1 (Contributed by metakunt, 31-Oct-2024.)
(𝜑𝑁 ∈ (ℤ‘3))    &   𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))    &   𝐵 = (⌈‘((2 logb 𝑁)↑5))    &   𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < )       (𝜑 → ∃𝑝 ∈ ℙ (𝑝𝑅 ∧ ¬ 𝑝𝑁))
 
31-Oct-2024aks4d1p7d1 40352 Technical step in AKS lemma 4.1 (Contributed by metakunt, 31-Oct-2024.)
(𝜑𝑁 ∈ (ℤ‘3))    &   𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))    &   𝐵 = (⌈‘((2 logb 𝑁)↑5))    &   𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < )    &   (𝜑 → ∀𝑝 ∈ ℙ (𝑝𝑅𝑝𝑁))       (𝜑𝑅 ∥ (𝑁↑(⌊‘(2 logb 𝐵))))
 
31-Oct-2024resvmulr 31834 .r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.)
𝐻 = (𝐺v 𝐴)    &    · = (.r𝐺)       (𝐴𝑉· = (.r𝐻))
 
31-Oct-2024resvvsca 31832 ·𝑠 is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Proof shortened by AV, 31-Oct-2024.)
𝐻 = (𝐺v 𝐴)    &    · = ( ·𝑠𝐺)       (𝐴𝑉· = ( ·𝑠𝐻))
 
31-Oct-2024resvplusg 31830 +g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.)
𝐻 = (𝐺v 𝐴)    &    + = (+g𝐺)       (𝐴𝑉+ = (+g𝐻))
 
31-Oct-2024resvbas 31828 Base is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.)
𝐻 = (𝐺v 𝐴)    &   𝐵 = (Base‘𝐺)       (𝐴𝑉𝐵 = (Base‘𝐻))
 
31-Oct-2024resvlem 31826 Other elements of a scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.)
𝑅 = (𝑊v 𝐴)    &   𝐶 = (𝐸𝑊)    &   𝐸 = Slot (𝐸‘ndx)    &   (𝐸‘ndx) ≠ (Scalar‘ndx)       (𝐴𝑉𝐶 = (𝐸𝑅))
 
31-Oct-2024nrgtrg 23960 A normed ring is a topological ring. (Contributed by Mario Carneiro, 4-Oct-2015.) (Proof shortened by AV, 31-Oct-2024.)
(𝑅 ∈ NrmRing → 𝑅 ∈ TopRing)
 
31-Oct-2024tngip 23915 The inner product operation of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.)
𝑇 = (𝐺 toNrmGrp 𝑁)    &    , = (·𝑖𝐺)       (𝑁𝑉, = (·𝑖𝑇))
 
31-Oct-2024tngvsca 23913 The scalar multiplication of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.)
𝑇 = (𝐺 toNrmGrp 𝑁)    &    · = ( ·𝑠𝐺)       (𝑁𝑉· = ( ·𝑠𝑇))
 
31-Oct-2024tngsca 23911 The scalar ring of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.)
𝑇 = (𝐺 toNrmGrp 𝑁)    &   𝐹 = (Scalar‘𝐺)       (𝑁𝑉𝐹 = (Scalar‘𝑇))
 
31-Oct-2024tngmulr 23909 The ring multiplication of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.)
𝑇 = (𝐺 toNrmGrp 𝑁)    &    · = (.r𝐺)       (𝑁𝑉· = (.r𝑇))
 
31-Oct-2024tng0 23908 The group identity of a structure augmented with a norm. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by AV, 31-Oct-2024.)
𝑇 = (𝐺 toNrmGrp 𝑁)    &    0 = (0g𝐺)       (𝑁𝑉0 = (0g𝑇))
 
31-Oct-2024tngplusg 23906 The group addition of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.)
𝑇 = (𝐺 toNrmGrp 𝑁)    &    + = (+g𝐺)       (𝑁𝑉+ = (+g𝑇))
 
31-Oct-2024tngbas 23904 The base set of a structure augmented with a norm. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.)
𝑇 = (𝐺 toNrmGrp 𝑁)    &   𝐵 = (Base‘𝐺)       (𝑁𝑉𝐵 = (Base‘𝑇))
 
31-Oct-2024tnglem 23902 Lemma for tngbas 23904 and similar theorems. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 31-Oct-2024.)
𝑇 = (𝐺 toNrmGrp 𝑁)    &   𝐸 = Slot (𝐸‘ndx)    &   (𝐸‘ndx) ≠ (TopSet‘ndx)    &   (𝐸‘ndx) ≠ (dist‘ndx)       (𝑁𝑉 → (𝐸𝐺) = (𝐸𝑇))
 
31-Oct-2024indistpsALT 22269 The indiscrete topology on a set 𝐴 expressed as a topological space. Here we show how to derive the structural version indistps 22267 from the direct component assignment version indistps2 22268. (Contributed by NM, 24-Oct-2012.) (Revised by AV, 31-Oct-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
𝐴 ∈ V    &   𝐾 = {⟨(Base‘ndx), 𝐴⟩, ⟨(TopSet‘ndx), {∅, 𝐴}⟩}       𝐾 ∈ TopSp
 
31-Oct-2024eltpsg 22198 Properties that determine a topological space from a construction (using no explicit indices). (Contributed by Mario Carneiro, 13-Aug-2015.) (Revised by AV, 31-Oct-2024.)
𝐾 = {⟨(Base‘ndx), 𝐴⟩, ⟨(TopSet‘ndx), 𝐽⟩}       (𝐽 ∈ (TopOn‘𝐴) → 𝐾 ∈ TopSp)
 
31-Oct-2024dsndxnmulrndx 17198 The slot for the distance function is not the slot for the ring multiplication operation in an extensible structure. (Contributed by AV, 31-Oct-2024.)
(dist‘ndx) ≠ (.r‘ndx)
 
31-Oct-2024tsetndxnmulrndx 17165 The slot for the topology is not the slot for the ring multiplication operation in an extensible structure. (Contributed by AV, 31-Oct-2024.)
(TopSet‘ndx) ≠ (.r‘ndx)
 
31-Oct-2024tsetndxnbasendx 17163 The slot for the topology is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) (Proof shortened by AV, 31-Oct-2024.)
(TopSet‘ndx) ≠ (Base‘ndx)
 
31-Oct-2024basendxlttsetndx 17162 The index of the slot for the base set is less then the index of the slot for the topology in an extensible structure. (Contributed by AV, 31-Oct-2024.)
(Base‘ndx) < (TopSet‘ndx)
 
31-Oct-2024tsetndxnn 17161 The index of the slot for the group operation in an extensible structure is a positive integer. (Contributed by AV, 31-Oct-2024.)
(TopSet‘ndx) ∈ ℕ
 
31-Oct-2024oveqprc 16990 Lemma for showing the equality of values for functions like slot extractors 𝐸 at a proper class. Extracted from several former proofs of lemmas like resvlem 31826. (Contributed by AV, 31-Oct-2024.)
(𝐸‘∅) = ∅    &   𝑍 = (𝑋𝑂𝑌)    &   Rel dom 𝑂       𝑋 ∈ V → (𝐸𝑋) = (𝐸𝑍))
 
31-Oct-2024fveqprc 16989 Lemma for showing the equality of values for functions like slot extractors 𝐸 at a proper class. Extracted from several former proofs of lemmas like zlmlem 20824. (Contributed by AV, 31-Oct-2024.)
(𝐸‘∅) = ∅    &   𝑌 = (𝐹𝑋)       𝑋 ∈ V → (𝐸𝑋) = (𝐸𝑌))
 
31-Oct-2024ttrclse 9584 If 𝑅 is set-like over 𝐴, then the transitive closure of the restriction of 𝑅 to 𝐴 is set-like over 𝐴.

This theorem requires the axioms of infinity and replacement for its proof. (Contributed by Scott Fenton, 31-Oct-2024.)

(𝑅 Se 𝐴 → t++(𝑅𝐴) Se 𝐴)
 
31-Oct-2024ttrclselem2 9583 Lemma for ttrclse 9584. Show that a suc 𝑁 element long chain gives membership in the 𝑁-th predecessor class and vice-versa. (Contributed by Scott Fenton, 31-Oct-2024.)
𝐹 = rec((𝑏 ∈ V ↦ 𝑤𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))       ((𝑁 ∈ ω ∧ 𝑅 Se 𝐴𝑋𝐴) → (∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓𝑎)(𝑅𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹𝑁)))
 
31-Oct-2024ttrclselem1 9582 Lemma for ttrclse 9584. Show that all finite ordinal function values of 𝐹 are subsets of 𝐴. (Contributed by Scott Fenton, 31-Oct-2024.)
𝐹 = rec((𝑏 ∈ V ↦ 𝑤𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))       (𝑁 ∈ ω → (𝐹𝑁) ⊆ 𝐴)
 
31-Oct-2024rdg0n 8335 If 𝐴 is a proper class, then the recursive function generator at is the empty set. (Contributed by Scott Fenton, 31-Oct-2024.)
𝐴 ∈ V → (rec(𝐹, 𝐴)‘∅) = ∅)
 
31-Oct-2024ralcom4 3265 Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) Reduce axiom dependencies. (Revised by BJ, 13-Jun-2019.) (Proof shortened by Wolf Lammen, 31-Oct-2024.)
(∀𝑥𝐴𝑦𝜑 ↔ ∀𝑦𝑥𝐴 𝜑)
 
31-Oct-2024ralbida 3249 Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 6-Oct-2003.) (Proof shortened by Wolf Lammen, 31-Oct-2024.)
𝑥𝜑    &   ((𝜑𝑥𝐴) → (𝜓𝜒))       (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
 
31-Oct-2024reximia 3080 Inference quantifying both antecedent and consequent. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Wolf Lammen, 31-Oct-2024.)
(𝑥𝐴 → (𝜑𝜓))       (∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓)
 
30-Oct-2024aks4d1p6 40351 The maximal prime power exponent is smaller than the binary logarithm floor of 𝐵. (Contributed by metakunt, 30-Oct-2024.)
(𝜑𝑁 ∈ (ℤ‘3))    &   𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))    &   𝐵 = (⌈‘((2 logb 𝑁)↑5))    &   𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < )    &   (𝜑𝑃 ∈ ℙ)    &   (𝜑𝑃𝑅)    &   𝐾 = (𝑃 pCnt 𝑅)       (𝜑𝐾 ≤ (⌊‘(2 logb 𝐵)))
 
30-Oct-2024aks4d1p5 40350 Show that 𝑁 and 𝑅 are coprime for AKS existence theorem. Precondition will be eliminated in further theorem. (Contributed by metakunt, 30-Oct-2024.)
(𝜑𝑁 ∈ (ℤ‘3))    &   𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))    &   𝐵 = (⌈‘((2 logb 𝑁)↑5))    &   𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < )    &   (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → ¬ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴)       (𝜑 → (𝑁 gcd 𝑅) = 1)
 
30-Oct-2024basendxltedgfndx 27652 The index value of the Base slot is less than the index value of the .ef slot. (Contributed by AV, 21-Sep-2020.) (Proof shortened by AV, 30-Oct-2024.)
(Base‘ndx) < (.ef‘ndx)
 
30-Oct-2024isposix 18140 Properties that determine a poset (explicit structure version). Note that the numeric indices of the structure components are not mentioned explicitly in either the theorem or its proof. (Contributed by NM, 9-Nov-2012.) (Proof shortened by AV, 30-Oct-2024.)
𝐵 ∈ V    &    ∈ V    &   𝐾 = {⟨(Base‘ndx), 𝐵⟩, ⟨(le‘ndx), ⟩}    &   (𝑥𝐵𝑥 𝑥)    &   ((𝑥𝐵𝑦𝐵) → ((𝑥 𝑦𝑦 𝑥) → 𝑥 = 𝑦))    &   ((𝑥𝐵𝑦𝐵𝑧𝐵) → ((𝑥 𝑦𝑦 𝑧) → 𝑥 𝑧))       𝐾 ∈ Poset
 
30-Oct-2024plendxnbasendx 17177 The slot for the order is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) (Proof shortened by AV, 30-Oct-2024.)
(le‘ndx) ≠ (Base‘ndx)
 
30-Oct-2024basendxltplendx 17176 The index value of the Base slot is less than the index value of the le slot. (Contributed by AV, 30-Oct-2024.)
(Base‘ndx) < (le‘ndx)
 
30-Oct-2024plendxnn 17175 The index value of the order slot is a positive integer. This property should be ensured for every concrete coding because otherwise it could not be used in an extensible structure (slots must be positive integers). (Contributed by AV, 30-Oct-2024.)
(le‘ndx) ∈ ℕ
 
30-Oct-2024pm13.181 3023 Theorem *13.181 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.) (Proof shortened by Wolf Lammen, 30-Oct-2024.)
((𝐴 = 𝐵𝐵𝐶) → 𝐴𝐶)
 
29-Oct-2024cchhllem 27543 Lemma for chlbas and chlvsca . (Contributed by Thierry Arnoux, 15-Apr-2019.) (Revised by AV, 29-Oct-2024.)
𝐶 = (((subringAlg ‘ℂfld)‘ℝ) sSet ⟨(·𝑖‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · (∗‘𝑦)))⟩)    &   𝐸 = Slot (𝐸‘ndx)    &   (Scalar‘ndx) ≠ (𝐸‘ndx)    &   ( ·𝑠 ‘ndx) ≠ (𝐸‘ndx)    &   (·𝑖‘ndx) ≠ (𝐸‘ndx)       (𝐸‘ℂfld) = (𝐸𝐶)
 
29-Oct-2024ttgds 27536 The metric of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) (Revised by AV, 29-Oct-2024.)
𝐺 = (toTG‘𝐻)    &   𝐷 = (dist‘𝐻)       𝐷 = (dist‘𝐺)
 
29-Oct-2024ttgvsca 27534 The scalar product of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) (Revised by AV, 29-Oct-2024.)
𝐺 = (toTG‘𝐻)    &    · = ( ·𝑠𝐻)        · = ( ·𝑠𝐺)
 
29-Oct-2024ttgplusg 27531 The addition operation of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) (Revised by AV, 29-Oct-2024.)
𝐺 = (toTG‘𝐻)    &    + = (+g𝐻)        + = (+g𝐺)
 
29-Oct-2024ttgbas 27529 The base set of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019.) (Revised by AV, 29-Oct-2024.)
𝐺 = (toTG‘𝐻)    &   𝐵 = (Base‘𝐻)       𝐵 = (Base‘𝐺)
 
29-Oct-2024ttglem 27527 Lemma for ttgbas 27529, ttgvsca 27534 etc. (Contributed by Thierry Arnoux, 15-Apr-2019.) (Revised by AV, 29-Oct-2024.)
𝐺 = (toTG‘𝐻)    &   𝐸 = Slot (𝐸‘ndx)    &   (𝐸‘ndx) ≠ (LineG‘ndx)    &   (𝐸‘ndx) ≠ (Itv‘ndx)       (𝐸𝐻) = (𝐸𝐺)
 
29-Oct-2024slotslnbpsd 27092 The slots Base, +g, ·𝑠 and dist are different from the slot LineG. Formerly part of ttglem 27527 and proofs using it. (Contributed by AV, 29-Oct-2024.)
(((LineG‘ndx) ≠ (Base‘ndx) ∧ (LineG‘ndx) ≠ (+g‘ndx)) ∧ ((LineG‘ndx) ≠ ( ·𝑠 ‘ndx) ∧ (LineG‘ndx) ≠ (dist‘ndx)))
 
29-Oct-2024slotsinbpsd 27091 The slots Base, +g, ·𝑠 and dist are different from the slot Itv. Formerly part of ttglem 27527 and proofs using it. (Contributed by AV, 29-Oct-2024.)
(((Itv‘ndx) ≠ (Base‘ndx) ∧ (Itv‘ndx) ≠ (+g‘ndx)) ∧ ((Itv‘ndx) ≠ ( ·𝑠 ‘ndx) ∧ (Itv‘ndx) ≠ (dist‘ndx)))
 
29-Oct-2024tngds 23917 The metric function of a structure augmented with a norm. (Contributed by Mario Carneiro, 3-Oct-2015.) (Proof shortened by AV, 29-Oct-2024.)
𝑇 = (𝐺 toNrmGrp 𝑁)    &    = (-g𝐺)       (𝑁𝑉 → (𝑁 ) = (dist‘𝑇))
 
29-Oct-2024srads 20561 Distance function of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
(𝜑𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   (𝜑𝑆 ⊆ (Base‘𝑊))       (𝜑 → (dist‘𝑊) = (dist‘𝐴))
 
29-Oct-2024sratset 20558 Topology component of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
(𝜑𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   (𝜑𝑆 ⊆ (Base‘𝑊))       (𝜑 → (TopSet‘𝑊) = (TopSet‘𝐴))
 
29-Oct-2024sramulr 20551 Multiplicative operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
(𝜑𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   (𝜑𝑆 ⊆ (Base‘𝑊))       (𝜑 → (.r𝑊) = (.r𝐴))
 
29-Oct-2024sraaddg 20549 Additive operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
(𝜑𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   (𝜑𝑆 ⊆ (Base‘𝑊))       (𝜑 → (+g𝑊) = (+g𝐴))
 
29-Oct-2024srabase 20547 Base set of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
(𝜑𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   (𝜑𝑆 ⊆ (Base‘𝑊))       (𝜑 → (Base‘𝑊) = (Base‘𝐴))
 
29-Oct-2024sralem 20545 Lemma for srabase 20547 and similar theorems. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
(𝜑𝐴 = ((subringAlg ‘𝑊)‘𝑆))    &   (𝜑𝑆 ⊆ (Base‘𝑊))    &   𝐸 = Slot (𝐸‘ndx)    &   (Scalar‘ndx) ≠ (𝐸‘ndx)    &   ( ·𝑠 ‘ndx) ≠ (𝐸‘ndx)    &   (·𝑖‘ndx) ≠ (𝐸‘ndx)       (𝜑 → (𝐸𝑊) = (𝐸𝐴))
 
29-Oct-2024dsndxntsetndx 17200 The slot for the distance function is not the slot for the topology in an extensible structure. Formerly part of proof for tngds 23917. (Contributed by AV, 29-Oct-2024.)
(dist‘ndx) ≠ (TopSet‘ndx)
 
29-Oct-2024slotsdnscsi 17199 The slots Scalar, ·𝑠 and ·𝑖 are different from the slot dist. Formerly part of sralem 20545 and proofs using it. (Contributed by AV, 29-Oct-2024.)
((dist‘ndx) ≠ (Scalar‘ndx) ∧ (dist‘ndx) ≠ ( ·𝑠 ‘ndx) ∧ (dist‘ndx) ≠ (·𝑖‘ndx))
 
29-Oct-2024slotstnscsi 17167 The slots Scalar, ·𝑠 and ·𝑖 are different from the slot TopSet. Formerly part of sralem 20545 and proofs using it. (Contributed by AV, 29-Oct-2024.)
((TopSet‘ndx) ≠ (Scalar‘ndx) ∧ (TopSet‘ndx) ≠ ( ·𝑠 ‘ndx) ∧ (TopSet‘ndx) ≠ (·𝑖‘ndx))
 
29-Oct-2024ipndxnmulrndx 17141 The slot for the inner product is not the slot for the ring (multiplication) operation in an extensible structure. Formerly part of proof for mgpsca 19823. (Contributed by AV, 29-Oct-2024.)
(·𝑖‘ndx) ≠ (.r‘ndx)
 
29-Oct-2024ipndxnplusgndx 17140 The slot for the inner product is not the slot for the group operation in an extensible structure. (Contributed by AV, 29-Oct-2024.)
(·𝑖‘ndx) ≠ (+g‘ndx)
 
29-Oct-2024vscandxnmulrndx 17130 The slot for the scalar product is not the slot for the ring (multiplication) operation in an extensible structure. Formerly part of proof for rmodislmod 20297. (Contributed by AV, 29-Oct-2024.)
( ·𝑠 ‘ndx) ≠ (.r‘ndx)
 
29-Oct-2024scandxnmulrndx 17125 The slot for the scalar field is not the slot for the ring (multiplication) operation in an extensible structure. Formerly part of proof for mgpsca 19823. (Contributed by AV, 29-Oct-2024.)
(Scalar‘ndx) ≠ (.r‘ndx)
 
29-Oct-2024pm13.18 3022 Theorem *13.18 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.) (Proof shortened by Wolf Lammen, 29-Oct-2024.)
((𝐴 = 𝐵𝐴𝐶) → 𝐵𝐶)
 
28-Oct-2024aks4d1p4 40349 There exists a small enough number such that it does not divide 𝐴. (Contributed by metakunt, 28-Oct-2024.)
(𝜑𝑁 ∈ (ℤ‘3))    &   𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))    &   𝐵 = (⌈‘((2 logb 𝑁)↑5))    &   𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < )       (𝜑 → (𝑅 ∈ (1...𝐵) ∧ ¬ 𝑅𝐴))
 
28-Oct-2024edgfndxid 27650 The value of the edge function extractor is the value of the corresponding slot of the structure. (Contributed by AV, 21-Sep-2020.) (Proof shortened by AV, 28-Oct-2024.)
(𝐺𝑉 → (.ef‘𝐺) = (𝐺‘(.ef‘ndx)))
 
28-Oct-2024tuslem 23524 Lemma for tusbas 23526, tusunif 23527, and tustopn 23529. (Contributed by Thierry Arnoux, 5-Dec-2017.) (Proof shortened by AV, 28-Oct-2024.)
𝐾 = (toUnifSp‘𝑈)       (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 = (Base‘𝐾) ∧ 𝑈 = (UnifSet‘𝐾) ∧ (unifTop‘𝑈) = (TopOpen‘𝐾)))
 
28-Oct-2024estrreslem1 17950 Lemma 1 for estrres 17953. (Contributed by AV, 14-Mar-2020.) (Proof shortened by AV, 28-Oct-2024.)
(𝜑𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})    &   (𝜑𝐵𝑉)       (𝜑𝐵 = (Base‘𝐶))
 
28-Oct-2024slotsbhcdif 17222 The slots Base, Hom and comp are different. (Contributed by AV, 5-Mar-2020.) (Proof shortened by AV, 28-Oct-2024.)
((Base‘ndx) ≠ (Hom ‘ndx) ∧ (Base‘ndx) ≠ (comp‘ndx) ∧ (Hom ‘ndx) ≠ (comp‘ndx))
 
28-Oct-2024unifndxntsetndx 17207 The slot for the uniform set is not the slot for the topology in an extensible structure. Formerly part of proof for tuslem 23524. (Contributed by AV, 28-Oct-2024.)
(UnifSet‘ndx) ≠ (TopSet‘ndx)
 
28-Oct-2024basendxltunifndx 17205 The index of the slot for the base set is less then the index of the slot for the uniform set in an extensible structure. Formerly part of proof for tuslem 23524. (Contributed by AV, 28-Oct-2024.)
(Base‘ndx) < (UnifSet‘ndx)
 
28-Oct-2024unifndxnn 17204 The index of the slot for the uniform set in an extensible structure is a positive integer. Formerly part of proof for tuslem 23524. (Contributed by AV, 28-Oct-2024.)
(UnifSet‘ndx) ∈ ℕ
 
28-Oct-2024dsndxnbasendx 17196 The slot for the distance is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) (Proof shortened by AV, 28-Oct-2024.)
(dist‘ndx) ≠ (Base‘ndx)
 
28-Oct-2024basendxltdsndx 17195 The index of the slot for the base set is less then the index of the slot for the distance in an extensible structure. Formerly part of proof for tmslem 23743. (Contributed by AV, 28-Oct-2024.)
(Base‘ndx) < (dist‘ndx)
 
28-Oct-2024dsndxnn 17194 The index of the slot for the distance in an extensible structure is a positive integer. Formerly part of proof for tmslem 23743. (Contributed by AV, 28-Oct-2024.)
(dist‘ndx) ∈ ℕ
 
28-Oct-2024basendxnmulrndx 17102 The slot for the base set is not the slot for the ring (multiplication) operation in an extensible structure. (Contributed by AV, 16-Feb-2020.) (Proof shortened by AV, 28-Oct-2024.)
(Base‘ndx) ≠ (.r‘ndx)
 
28-Oct-2024wunress 17057 Closure of structure restriction in a weak universe. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof shortened by AV, 28-Oct-2024.)
(𝜑𝑈 ∈ WUni)    &   (𝜑 → ω ∈ 𝑈)    &   (𝜑𝑊𝑈)       (𝜑 → (𝑊s 𝐴) ∈ 𝑈)
 
28-Oct-2024predpo 6262 Property of the predecessor class for partial orders. (Contributed by Scott Fenton, 28-Apr-2012.) (Proof shortened by Scott Fenton, 28-Oct-2024.)
((𝑅 Po 𝐴𝑋𝐴) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → Pred(𝑅, 𝐴, 𝑌) ⊆ Pred(𝑅, 𝐴, 𝑋)))
 
28-Oct-2024predtrss 6261 If 𝑅 is transitive over 𝐴 and 𝑌𝑅𝑋, then Pred(𝑅, 𝐴, 𝑌) is a subclass of Pred(𝑅, 𝐴, 𝑋). (Contributed by Scott Fenton, 28-Oct-2024.)
((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋𝐴) → Pred(𝑅, 𝐴, 𝑌) ⊆ Pred(𝑅, 𝐴, 𝑋))
 
28-Oct-2024necon3ai 2965 Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 28-Oct-2024.)
(𝜑𝐴 = 𝐵)       (𝐴𝐵 → ¬ 𝜑)
 
28-Oct-2024sbabel 2938 Theorem to move a substitution in and out of a class abstraction. (Contributed by NM, 27-Sep-2003.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 28-Oct-2024.)
𝑥𝐴       ([𝑦 / 𝑥]{𝑧𝜑} ∈ 𝐴 ↔ {𝑧 ∣ [𝑦 / 𝑥]𝜑} ∈ 𝐴)
 
27-Oct-2024aks4d1p3 40348 There exists a small enough number such that it does not divide 𝐴. (Contributed by metakunt, 27-Oct-2024.)
(𝜑𝑁 ∈ (ℤ‘3))    &   𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))    &   𝐵 = (⌈‘((2 logb 𝑁)↑5))       (𝜑 → ∃𝑟 ∈ (1...𝐵) ¬ 𝑟𝐴)
 
27-Oct-2024aks4d1p2 40347 Technical lemma for existence of non-divisor. (Contributed by metakunt, 27-Oct-2024.)
(𝜑𝑁 ∈ (ℤ‘3))    &   𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))    &   𝐵 = (⌈‘((2 logb 𝑁)↑5))       (𝜑 → (2↑𝐵) ≤ (lcm‘(1...𝐵)))
 
27-Oct-2024grpplusg 17095 The operation of a constructed group. (Contributed by Mario Carneiro, 2-Aug-2013.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by AV, 27-Oct-2024.)
𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩}       ( +𝑉+ = (+g𝐺))
 
27-Oct-2024grpbase 17093 The base set of a constructed group. (Contributed by Mario Carneiro, 2-Aug-2013.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by AV, 27-Oct-2024.)
𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩}       (𝐵𝑉𝐵 = (Base‘𝐺))
 
27-Oct-2024grpstrndx 17092 A constructed group is a structure. Version not depending on the implementation of the indices. (Contributed by AV, 27-Oct-2024.)
𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩}       𝐺 Struct ⟨(Base‘ndx), (+g‘ndx)⟩
 
27-Oct-2024df-wrecs 8198 Define the well-ordered recursive function generator. This function takes the usual expressions from recursion theorems and forms a unified definition. Specifically, given a function 𝐹, a relation 𝑅, and a base set 𝐴, this definition generates a function 𝐺 = wrecs(𝑅, 𝐴, 𝐹) that has property that, at any point 𝑥𝐴, (𝐺𝑥) = (𝐹‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑥))). See wfr1 8236, wfr2 8237, and wfr3 8238. (Contributed by Scott Fenton, 7-Jun-2018.) (Revised by BJ, 27-Oct-2024.)
wrecs(𝑅, 𝐴, 𝐹) = frecs(𝑅, 𝐴, (𝐹 ∘ 2nd ))
 
27-Oct-2024opco2 8032 Value of an operation precomposed with the projection on the second component. (Contributed by BJ, 27-Oct-2024.)
(𝜑𝐴𝑉)    &   (𝜑𝐵𝑊)       (𝜑 → (𝐴(𝐹 ∘ 2nd )𝐵) = (𝐹𝐵))
 
27-Oct-2024opco1 8031 Value of an operation precomposed with the projection on the first component. (Contributed by Mario Carneiro, 28-May-2014.) Generalize to closed form. (Revised by BJ, 27-Oct-2024.)
(𝜑𝐴𝑉)    &   (𝜑𝐵𝑊)       (𝜑 → (𝐴(𝐹 ∘ 1st )𝐵) = (𝐹𝐴))
 
27-Oct-2024predexg 6256 The predecessor class exists when 𝐴 does. (Contributed by Scott Fenton, 8-Feb-2011.) Generalize to closed form. (Revised by BJ, 27-Oct-2024.)
(𝐴𝑉 → Pred(𝑅, 𝐴, 𝑋) ∈ V)
 
26-Oct-2024sticksstones22 40389 Non-exhaustive sticks and stones. (Contributed by metakunt, 26-Oct-2024.)
(𝜑𝑁 ∈ ℕ0)    &   (𝜑𝑆 ∈ Fin)    &   (𝜑𝑆 ≠ ∅)    &   𝐴 = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑁)}       (𝜑 → (♯‘𝐴) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆)))
 
26-Oct-2024dfttrcl2 9581 When 𝑅 is a set and a relationship, then its transitive closure can be defined by an intersection. (Contributed by Scott Fenton, 26-Oct-2024.)
((𝑅𝑉 ∧ Rel 𝑅) → t++𝑅 = {𝑧 ∣ (𝑅𝑧 ∧ (𝑧𝑧) ⊆ 𝑧)})
 
26-Oct-2024ttrclexg 9580 If 𝑅 is a set, then so is t++𝑅. (Contributed by Scott Fenton, 26-Oct-2024.)
(𝑅𝑉 → t++𝑅 ∈ V)
 
26-Oct-2024rnttrcl 9579 The range of a transitive closure is the same as the range of the original class. (Contributed by Scott Fenton, 26-Oct-2024.)
ran t++𝑅 = ran 𝑅
 
26-Oct-2024dmttrcl 9578 The domain of a transitive closure is the same as the domain of the original class. (Contributed by Scott Fenton, 26-Oct-2024.)
dom t++𝑅 = dom 𝑅
 
26-Oct-2024nfttrcld 9567 Bound variable hypothesis builder for transitive closure. Deduction form. (Contributed by Scott Fenton, 26-Oct-2024.)
(𝜑𝑥𝑅)       (𝜑𝑥t++𝑅)
 
26-Oct-2024nfopab 5161 Bound-variable hypothesis builder for class abstraction. (Contributed by NM, 1-Sep-1999.) Remove disjoint variable conditions. (Revised by Andrew Salmon, 11-Jul-2011.) (Revised by Scott Fenton, 26-Oct-2024.)
𝑧𝜑       𝑧{⟨𝑥, 𝑦⟩ ∣ 𝜑}
 
26-Oct-2024nfopabd 5160 Bound-variable hypothesis builder for class abstraction. Deduction form. (Contributed by Scott Fenton, 26-Oct-2024.)
𝑥𝜑    &   𝑦𝜑    &   (𝜑 → Ⅎ𝑧𝜓)       (𝜑𝑧{⟨𝑥, 𝑦⟩ ∣ 𝜓})
 
26-Oct-2024sbceqal 3793 Class version of one implication of equvelv 2033. (Contributed by Andrew Salmon, 28-Jun-2011.) (Proof shortened by SN, 26-Oct-2024.)
(𝐴𝑉 → (∀𝑥(𝑥 = 𝐴𝑥 = 𝐵) → 𝐴 = 𝐵))
 
26-Oct-2024sbcim1 3783 Distribution of class substitution over implication. One direction of sbcimg 3778 that holds for proper classes. (Contributed by NM, 17-Aug-2018.) Avoid ax-10 2136, ax-12 2170. (Revised by SN, 26-Oct-2024.)
([𝐴 / 𝑥](𝜑𝜓) → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓))
 
26-Oct-2024sbievg 2359 Substitution applied to expressions linked by implicit substitution. The proof was part of a former cbvabw 2810 version. (Contributed by GG and WL, 26-Oct-2024.)
𝑦𝜑    &   𝑥𝜓    &   (𝑥 = 𝑦 → (𝜑𝜓))       ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓)
 
25-Oct-2024hbab1 2722 Bound-variable hypothesis builder for a class abstraction. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2024.)
(𝑦 ∈ {𝑥𝜑} → ∀𝑥 𝑦 ∈ {𝑥𝜑})
 
25-Oct-2024nfsbv 2323 If 𝑧 is not free in 𝜑, then it is not free in [𝑦 / 𝑥]𝜑 when 𝑧 is disjoint from both 𝑥 and 𝑦. Version of nfsb 2525 with an additional disjoint variable condition on 𝑥, 𝑧 but not requiring ax-13 2370. (Contributed by Mario Carneiro, 11-Aug-2016.) (Revised by Wolf Lammen, 7-Feb-2023.) Remove disjoint variable condition on 𝑥, 𝑦. (Revised by Steven Nguyen, 13-Aug-2023.) (Proof shortened by Wolf Lammen, 25-Oct-2024.)
𝑧𝜑       𝑧[𝑦 / 𝑥]𝜑
 
24-Oct-2024sticksstones21 40388 Lift sticks and stones to arbitrary finite non-empty sets. (Contributed by metakunt, 24-Oct-2024.)
(𝜑𝑁 ∈ ℕ0)    &   (𝜑𝑆 ∈ Fin)    &   (𝜑𝑆 ≠ ∅)    &   𝐴 = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = 𝑁)}       (𝜑 → (♯‘𝐴) = ((𝑁 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)))
 
24-Oct-2024sticksstones20 40387 Lift sticks and stones to arbitrary finite non-empty sets. (Contributed by metakung, 24-Oct-2024.)
(𝜑𝑁 ∈ ℕ0)    &   (𝜑𝑆 ∈ Fin)    &   (𝜑𝐾 ∈ ℕ)    &   𝐴 = {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧ Σ𝑖 ∈ (1...𝐾)(𝑔𝑖) = 𝑁)}    &   𝐵 = { ∣ (:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑖) = 𝑁)}    &   (𝜑 → (♯‘𝑆) = 𝐾)       (𝜑 → (♯‘𝐵) = ((𝑁 + (𝐾 − 1))C(𝐾 − 1)))
 
24-Oct-2024eldifsucnn 8565 Condition for membership in the difference of ω and a nonzero finite ordinal. (Contributed by Scott Fenton, 24-Oct-2024.)
(𝐴 ∈ ω → (𝐵 ∈ (ω ∖ suc 𝐴) ↔ ∃𝑥 ∈ (ω ∖ 𝐴)𝐵 = suc 𝑥))
 
24-Oct-2024eqtr3 2762 A transitive law for class equality. (Contributed by NM, 20-May-2005.) (Proof shortened by Wolf Lammen, 24-Oct-2024.)
((𝐴 = 𝐶𝐵 = 𝐶) → 𝐴 = 𝐵)
 
24-Oct-2024eqtr2 2760 A transitive law for class equality. (Contributed by NM, 20-May-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 24-Oct-2024.)
((𝐴 = 𝐵𝐴 = 𝐶) → 𝐵 = 𝐶)
 
23-Oct-2024sticksstones19 40386 Extend sticks and stones to finite sets, bijective builder. (Contributed by metakunt, 23-Oct-2024.)
(𝜑𝑁 ∈ ℕ0)    &   (𝜑𝐾 ∈ ℕ0)    &   𝐴 = {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧ Σ𝑖 ∈ (1...𝐾)(𝑔𝑖) = 𝑁)}    &   𝐵 = { ∣ (:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑖) = 𝑁)}    &   (𝜑𝑍:(1...𝐾)–1-1-onto𝑆)    &   𝐹 = (𝑎𝐴 ↦ (𝑥𝑆 ↦ (𝑎‘(𝑍𝑥))))    &   𝐺 = (𝑏𝐵 ↦ (𝑦 ∈ (1...𝐾) ↦ (𝑏‘(𝑍𝑦))))       (𝜑𝐹:𝐴1-1-onto𝐵)
 
23-Oct-2024sticksstones18 40385 Extend sticks and stones to finite sets, bijective builder. (Contributed by metakunt, 23-Oct-2024.)
(𝜑𝑁 ∈ ℕ0)    &   (𝜑𝐾 ∈ ℕ0)    &   𝐴 = {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧ Σ𝑖 ∈ (1...𝐾)(𝑔𝑖) = 𝑁)}    &   𝐵 = { ∣ (:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑖) = 𝑁)}    &   (𝜑𝑍:(1...𝐾)–1-1-onto𝑆)    &   𝐹 = (𝑎𝐴 ↦ (𝑥𝑆 ↦ (𝑎‘(𝑍𝑥))))       (𝜑𝐹:𝐴𝐵)
 
23-Oct-2024sticksstones17 40384 Extend sticks and stones to finite sets, bijective builder. (Contributed by metakunt, 23-Oct-2024.)
(𝜑𝑁 ∈ ℕ0)    &   (𝜑𝐾 ∈ ℕ0)    &   𝐴 = {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧ Σ𝑖 ∈ (1...𝐾)(𝑔𝑖) = 𝑁)}    &   𝐵 = { ∣ (:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑖) = 𝑁)}    &   (𝜑𝑍:(1...𝐾)–1-1-onto𝑆)    &   𝐺 = (𝑏𝐵 ↦ (𝑦 ∈ (1...𝐾) ↦ (𝑏‘(𝑍𝑦))))       (𝜑𝐺:𝐵𝐴)
 
23-Oct-2024eqeq12 2753 Equality relationship among four classes. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Wolf Lammen, 23-Oct-2024.)
((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴 = 𝐶𝐵 = 𝐷))
 
23-Oct-2024eqeq12d 2752 A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Oct-2024.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐷)       (𝜑 → (𝐴 = 𝐶𝐵 = 𝐷))
 
23-Oct-2024eqeqan12d 2750 A useful inference for substituting definitions into an equality. See also eqeqan12dALT 2758. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) Shorten other proofs. (Revised by Wolf Lammen, 23-Oct-2024.)
(𝜑𝐴 = 𝐵)    &   (𝜓𝐶 = 𝐷)       ((𝜑𝜓) → (𝐴 = 𝐶𝐵 = 𝐷))
 
21-Oct-2024unifndxnbasendx 17206 The slot for the uniform set is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.)
(UnifSet‘ndx) ≠ (Base‘ndx)
 
21-Oct-2024ipndxnbasendx 17139 The slot for the inner product is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.)
(·𝑖‘ndx) ≠ (Base‘ndx)
 
21-Oct-2024scandxnbasendx 17123 The slot for the scalar is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.)
(Scalar‘ndx) ≠ (Base‘ndx)
 
20-Oct-2024sticksstones16 40383 Sticks and stones with collapsed definitions for positive integers. (Contributed by metakunt, 20-Oct-2024.)
(𝜑𝑁 ∈ ℕ0)    &   (𝜑𝐾 ∈ ℕ)    &   𝐴 = {𝑔 ∣ (𝑔:(1...𝐾)⟶ℕ0 ∧ Σ𝑖 ∈ (1...𝐾)(𝑔𝑖) = 𝑁)}       (𝜑 → (♯‘𝐴) = ((𝑁 + (𝐾 − 1))C(𝐾 − 1)))
 
20-Oct-2024ttrclss 9577 If 𝑅 is a subclass of 𝑆 and 𝑆 is transitive, then the transitive closure of 𝑅 is a subclass of 𝑆. (Contributed by Scott Fenton, 20-Oct-2024.)
((𝑅𝑆 ∧ (𝑆𝑆) ⊆ 𝑆) → t++𝑅𝑆)
 
20-Oct-2024cottrcl 9576 Composition law for the transitive closure of a relationship. (Contributed by Scott Fenton, 20-Oct-2024.)
(𝑅 ∘ t++𝑅) ⊆ t++𝑅
 
20-Oct-2024ttrclco 9575 Composition law for the transitive closure of a relationship. (Contributed by Scott Fenton, 20-Oct-2024.)
(t++𝑅𝑅) ⊆ t++𝑅
 
20-Oct-2024ttrclresv 9574 The transitive closure of 𝑅 restricted to V is the same as the transitive closure of 𝑅 itself. (Contributed by Scott Fenton, 20-Oct-2024.)
t++(𝑅 ↾ V) = t++𝑅
 
19-Oct-2024resseqnbas 17048 The components of an extensible structure except the base set remain unchanged on a structure restriction. (Contributed by Mario Carneiro, 26-Nov-2014.) (Revised by Mario Carneiro, 2-Dec-2014.) (Revised by AV, 19-Oct-2024.)
𝑅 = (𝑊s 𝐴)    &   𝐶 = (𝐸𝑊)    &   𝐸 = Slot (𝐸‘ndx)    &   (𝐸‘ndx) ≠ (Base‘ndx)       (𝐴𝑉𝐶 = (𝐸𝑅))
 
18-Oct-2024rmodislmod 20297 The right module 𝑅 induces a left module 𝐿 by replacing the scalar multiplication with a reversed multiplication if the scalar ring is commutative. The hypothesis "rmodislmod.r" is a definition of a right module analogous to Definition df-lmod 20231 of a left module, see also islmod 20233. (Contributed by AV, 3-Dec-2021.) (Proof shortened by AV, 18-Oct-2024.)
𝑉 = (Base‘𝑅)    &    + = (+g𝑅)    &    · = ( ·𝑠𝑅)    &   𝐹 = (Scalar‘𝑅)    &   𝐾 = (Base‘𝐹)    &    = (+g𝐹)    &    × = (.r𝐹)    &    1 = (1r𝐹)    &   (𝑅 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞𝐾𝑟𝐾𝑥𝑉𝑤𝑉 (((𝑤 · 𝑟) ∈ 𝑉 ∧ ((𝑤 + 𝑥) · 𝑟) = ((𝑤 · 𝑟) + (𝑥 · 𝑟)) ∧ (𝑤 · (𝑞 𝑟)) = ((𝑤 · 𝑞) + (𝑤 · 𝑟))) ∧ ((𝑤 · (𝑞 × 𝑟)) = ((𝑤 · 𝑞) · 𝑟) ∧ (𝑤 · 1 ) = 𝑤)))    &    = (𝑠𝐾, 𝑣𝑉 ↦ (𝑣 · 𝑠))    &   𝐿 = (𝑅 sSet ⟨( ·𝑠 ‘ndx), ⟩)       (𝐹 ∈ CRing → 𝐿 ∈ LMod)
 
18-Oct-2024mgpress 19830 Subgroup commutes with the multiplication group operator. (Contributed by Mario Carneiro, 10-Jan-2015.) (Proof shortened by AV, 18-Oct-2024.)
𝑆 = (𝑅s 𝐴)    &   𝑀 = (mulGrp‘𝑅)       ((𝑅𝑉𝐴𝑊) → (𝑀s 𝐴) = (mulGrp‘𝑆))
 
18-Oct-2024setsplusg 19050 The other components of an extensible structure remain unchanged if the +g component is set/substituted. (Contributed by Stefan O'Rear, 26-Aug-2015.) Generalisation of the former oppglem and mgplem. (Revised by AV, 18-Oct-2024.)
𝑂 = (𝑅 sSet ⟨(+g‘ndx), 𝑆⟩)    &   𝐸 = Slot (𝐸‘ndx)    &   (𝐸‘ndx) ≠ (+g‘ndx)       (𝐸𝑅) = (𝐸𝑂)
 
18-Oct-2024rescbas 17638 Base set of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by AV, 18-Oct-2024.)
𝐷 = (𝐶cat 𝐻)    &   𝐵 = (Base‘𝐶)    &   (𝜑𝐶𝑉)    &   (𝜑𝐻 Fn (𝑆 × 𝑆))    &   (𝜑𝑆𝐵)       (𝜑𝑆 = (Base‘𝐷))
 
18-Oct-2024oppcbas 17525 Base set of an opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.) (Proof shortened by AV, 18-Oct-2024.)
𝑂 = (oppCat‘𝐶)    &   𝐵 = (Base‘𝐶)       𝐵 = (Base‘𝑂)
 
18-Oct-2024dsndxnplusgndx 17197 The slot for the distance function is not the slot for the group operation in an extensible structure. Formerly part of proof for mgpds 19828. (Contributed by AV, 18-Oct-2024.)
(dist‘ndx) ≠ (+g‘ndx)
 
18-Oct-2024plendxnplusgndx 17178 The slot for the "less than or equal to" ordering is not the slot for the group operation in an extensible structure. Formerly part of proof for oppgle 31525. (Contributed by AV, 18-Oct-2024.)
(le‘ndx) ≠ (+g‘ndx)
 
18-Oct-2024tsetndxnplusgndx 17164 The slot for the topology is not the slot for the group operation in an extensible structure. Formerly part of proof for oppgtset 19054. (Contributed by AV, 18-Oct-2024.)
(TopSet‘ndx) ≠ (+g‘ndx)
 
18-Oct-2024vscandxnscandx 17131 The slot for the scalar product is not the slot for the scalar field in an extensible structure. Formerly part of proof for rmodislmod 20297. (Contributed by AV, 18-Oct-2024.)
( ·𝑠 ‘ndx) ≠ (Scalar‘ndx)
 
18-Oct-2024vscandxnplusgndx 17129 The slot for the scalar product is not the slot for the group operation in an extensible structure. Formerly part of proof for rmodislmod 20297. (Contributed by AV, 18-Oct-2024.)
( ·𝑠 ‘ndx) ≠ (+g‘ndx)
 
18-Oct-2024vscandxnbasendx 17128 The slot for the scalar product is not the slot for the base set in an extensible structure. Formerly part of proof for rmodislmod 20297. (Contributed by AV, 18-Oct-2024.)
( ·𝑠 ‘ndx) ≠ (Base‘ndx)
 
18-Oct-2024scandxnplusgndx 17124 The slot for the scalar field is not the slot for the group operation in an extensible structure. Formerly part of proof for mgpsca 19823. (Contributed by AV, 18-Oct-2024.)
(Scalar‘ndx) ≠ (+g‘ndx)
 
18-Oct-2024starvndxnmulrndx 17113 The slot for the involution function is not the slot for the base set in an extensible structure. Formerly part of proof for ressstarv 17115. (Contributed by AV, 18-Oct-2024.)
(*𝑟‘ndx) ≠ (.r‘ndx)
 
18-Oct-2024starvndxnplusgndx 17112 The slot for the involution function is not the slot for the base set in an extensible structure. Formerly part of proof for ressstarv 17115. (Contributed by AV, 18-Oct-2024.)
(*𝑟‘ndx) ≠ (+g‘ndx)
 
18-Oct-2024starvndxnbasendx 17111 The slot for the involution function is not the slot for the base set in an extensible structure. Formerly part of proof for ressstarv 17115. (Contributed by AV, 18-Oct-2024.)
(*𝑟‘ndx) ≠ (Base‘ndx)
 
17-Oct-2024nnuni 33982 The union of a finite ordinal is a finite ordinal. (Contributed by Scott Fenton, 17-Oct-2024.)
(𝐴 ∈ ω → 𝐴 ∈ ω)
 
17-Oct-2024basendxnplusgndx 17089 The slot for the base set is not the slot for the group operation in an extensible structure. (Contributed by AV, 14-Nov-2021.) (Proof shortened by AV, 17-Oct-2024.)
(Base‘ndx) ≠ (+g‘ndx)
 
17-Oct-2024basendxltplusgndx 17088 The index of the slot for the base set is less then the index of the slot for the group operation in an extensible structure. (Contributed by AV, 17-Oct-2024.)
(Base‘ndx) < (+g‘ndx)
 
17-Oct-2024plusgndxnn 17087 The index of the slot for the group operation in an extensible structure is a positive integer. (Contributed by AV, 17-Oct-2024.)
(+g‘ndx) ∈ ℕ
 
17-Oct-2024ressval3d 17053 Value of structure restriction, deduction version. (Contributed by AV, 14-Mar-2020.) (Revised by AV, 3-Jul-2022.) (Proof shortened by AV, 17-Oct-2024.)
𝑅 = (𝑆s 𝐴)    &   𝐵 = (Base‘𝑆)    &   𝐸 = (Base‘ndx)    &   (𝜑𝑆𝑉)    &   (𝜑 → Fun 𝑆)    &   (𝜑𝐸 ∈ dom 𝑆)    &   (𝜑𝐴𝐵)       (𝜑𝑅 = (𝑆 sSet ⟨𝐸, 𝐴⟩))
 
17-Oct-20242strstr1 17034 A constructed two-slot structure. Version of 2strstr 17031 not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020.) (Proof shortened by AV, 17-Oct-2024.)
𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨𝑁, + ⟩}    &   (Base‘ndx) < 𝑁    &   𝑁 ∈ ℕ       𝐺 Struct ⟨(Base‘ndx), 𝑁
 
17-Oct-20241strwun 17029 A constructed one-slot structure in a weak universe. (Contributed by AV, 27-Mar-2020.) (Proof shortened by AV, 17-Oct-2024.)
𝐺 = {⟨(Base‘ndx), 𝐵⟩}    &   (𝜑𝑈 ∈ WUni)    &   (𝜑 → ω ∈ 𝑈)       ((𝜑𝐵𝑈) → 𝐺𝑈)
 </