Intuitionistic Logic Explorer Home Intuitionistic Logic Explorer
Most Recent Proofs 		 
Mirrors  >  Home  >  ILE Home  >  Th. List  >  Recent MPE Most Recent             Other  >  MM 100
Most recent proofs    These are the 100 (Unicode, GIF) or 1000 (Unicode, GIF) most recent proofs in the iset.mm database for the Intuitionistic Logic Explorer. The iset.mm database is maintained on GitHub with master (stable) and develop (development) versions. This page was created from the commit given on the MPE Most Recent Proofs page. The database from that commit is also available here: iset.mm.

See the MPE Most Recent Proofs page for news and some useful links.

Color key:   Intuitionistic Logic Explorer  Intuitionistic Logic Explorer   User Mathboxes  User Mathboxes  

Last updated on 25-Apr-2025 at 6:44 AM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem
 
23-Apr-20251dom1el 14883 If a set is dominated by one, then any two of its elements are equal. (Contributed by Jim Kingdon, 23-Apr-2025.)
((𝐴 β‰Ό 1o ∧ 𝐡 ∈ 𝐴 ∧ 𝐢 ∈ 𝐴) β†’ 𝐡 = 𝐢)
 
18-Apr-2025lidlmex 13564 Existence of the set a left ideal is built from (when the ideal is inhabited). (Contributed by Jim Kingdon, 18-Apr-2025.)
𝐼 = (LIdealβ€˜π‘Š)    β‡’   (π‘ˆ ∈ 𝐼 β†’ π‘Š ∈ V)
 
18-Apr-2025lsslsp 13521 Spans in submodules correspond to spans in the containing module. (Contributed by Stefan O'Rear, 12-Dec-2014.) Terms in the equation were swapped as proposed by NM on 15-Mar-2015. (Revised by AV, 18-Apr-2025.)
𝑋 = (π‘Š β†Ύs π‘ˆ)    &   π‘€ = (LSpanβ€˜π‘Š)    &   π‘ = (LSpanβ€˜π‘‹)    &   πΏ = (LSubSpβ€˜π‘Š)    β‡’   ((π‘Š ∈ LMod ∧ π‘ˆ ∈ 𝐿 ∧ 𝐺 βŠ† π‘ˆ) β†’ (π‘β€˜πΊ) = (π‘€β€˜πΊ))
 
16-Apr-2025sraex 13538 Existence of a subring algebra. (Contributed by Jim Kingdon, 16-Apr-2025.)
(πœ‘ β†’ 𝐴 = ((subringAlg β€˜π‘Š)β€˜π‘†))    &   (πœ‘ β†’ 𝑆 βŠ† (Baseβ€˜π‘Š))    &   (πœ‘ β†’ π‘Š ∈ 𝑋)    β‡’   (πœ‘ β†’ 𝐴 ∈ V)
 
10-Apr-2025cndcap 14948 Real number trichotomy is equivalent to decidability of complex number apartness. (Contributed by Jim Kingdon, 10-Apr-2025.)
(βˆ€π‘₯ ∈ ℝ βˆ€π‘¦ ∈ ℝ (π‘₯ < 𝑦 ∨ π‘₯ = 𝑦 ∨ 𝑦 < π‘₯) ↔ βˆ€π‘§ ∈ β„‚ βˆ€π‘€ ∈ β„‚ DECID 𝑧 # 𝑀)
 
20-Mar-2025ccoslid 12693 Slot property of comp. (Contributed by Jim Kingdon, 20-Mar-2025.)
(comp = Slot (compβ€˜ndx) ∧ (compβ€˜ndx) ∈ β„•)
 
20-Mar-2025homslid 12691 Slot property of Hom. (Contributed by Jim Kingdon, 20-Mar-2025.)
(Hom = Slot (Hom β€˜ndx) ∧ (Hom β€˜ndx) ∈ β„•)
 
19-Mar-2025ptex 12719 Existence of the product topology. (Contributed by Jim Kingdon, 19-Mar-2025.)
(𝐹 ∈ 𝑉 β†’ (∏tβ€˜πΉ) ∈ V)
 
18-Mar-2025prdsex 12724 Existence of the structure product. (Contributed by Jim Kingdon, 18-Mar-2025.)
((𝑆 ∈ 𝑉 ∧ 𝑅 ∈ π‘Š) β†’ (𝑆Xs𝑅) ∈ V)
 
13-Mar-2025imasex 12732 Existence of the image structure. (Contributed by Jim Kingdon, 13-Mar-2025.)
((𝐹 ∈ 𝑉 ∧ 𝑅 ∈ π‘Š) β†’ (𝐹 β€œs 𝑅) ∈ V)
 
11-Mar-2025imasival 12733 Value of an image structure. The is a lemma for the theorems imasbas 12734, imasplusg 12735, and imasmulr 12736 and should not be needed once they are proved. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Jim Kingdon, 11-Mar-2025.) (New usage is discouraged.)
(πœ‘ β†’ π‘ˆ = (𝐹 β€œs 𝑅))    &   (πœ‘ β†’ 𝑉 = (Baseβ€˜π‘…))    &    + = (+gβ€˜π‘…)    &    Γ— = (.rβ€˜π‘…)    &    Β· = ( ·𝑠 β€˜π‘…)    &   (πœ‘ β†’ ✚ = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩})    &   (πœ‘ β†’ βˆ™ = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩})    &   (πœ‘ β†’ 𝐹:𝑉–onto→𝐡)    &   (πœ‘ β†’ 𝑅 ∈ 𝑍)    β‡’   (πœ‘ β†’ π‘ˆ = {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(+gβ€˜ndx), ✚ ⟩, ⟨(.rβ€˜ndx), βˆ™ ⟩})
 
8-Mar-2025subgex 13042 The class of subgroups of a group is a set. (Contributed by Jim Kingdon, 8-Mar-2025.)
(𝐺 ∈ Grp β†’ (SubGrpβ€˜πΊ) ∈ V)
 
28-Feb-2025ringressid 13244 A ring restricted to its base set is a ring. It will usually be the original ring exactly, of course, but to show that needs additional conditions such as those in strressid 12533. (Contributed by Jim Kingdon, 28-Feb-2025.)
𝐡 = (Baseβ€˜πΊ)    β‡’   (𝐺 ∈ Ring β†’ (𝐺 β†Ύs 𝐡) ∈ Ring)
 
28-Feb-2025grpressid 12937 A group restricted to its base set is a group. It will usually be the original group exactly, of course, but to show that needs additional conditions such as those in strressid 12533. (Contributed by Jim Kingdon, 28-Feb-2025.)
𝐡 = (Baseβ€˜πΊ)    β‡’   (𝐺 ∈ Grp β†’ (𝐺 β†Ύs 𝐡) ∈ Grp)
 
26-Feb-2025strext 12567 Extending the upper range of a structure. This works because when we say that a structure has components in 𝐴...𝐢 we are not saying that every slot in that range is present, just that all the slots that are present are within that range. (Contributed by Jim Kingdon, 26-Feb-2025.)
(πœ‘ β†’ 𝐹 Struct ⟨𝐴, 𝐡⟩)    &   (πœ‘ β†’ 𝐢 ∈ (β„€β‰₯β€˜π΅))    β‡’   (πœ‘ β†’ 𝐹 Struct ⟨𝐴, 𝐢⟩)
 
23-Feb-2025ltlenmkv 14959 If < can be expressed as holding exactly when ≀ holds and the values are not equal, then the analytic Markov's Principle applies. (To get the regular Markov's Principle, combine with neapmkv 14957). (Contributed by Jim Kingdon, 23-Feb-2025.)
(βˆ€π‘₯ ∈ ℝ βˆ€π‘¦ ∈ ℝ (π‘₯ < 𝑦 ↔ (π‘₯ ≀ 𝑦 ∧ 𝑦 β‰  π‘₯)) β†’ βˆ€π‘₯ ∈ ℝ βˆ€π‘¦ ∈ ℝ (π‘₯ β‰  𝑦 β†’ π‘₯ # 𝑦))
 
23-Feb-2025neap0mkv 14958 The analytic Markov principle can be expressed either with two arbitrary real numbers, or one arbitrary number and zero. (Contributed by Jim Kingdon, 23-Feb-2025.)
(βˆ€π‘₯ ∈ ℝ βˆ€π‘¦ ∈ ℝ (π‘₯ β‰  𝑦 β†’ π‘₯ # 𝑦) ↔ βˆ€π‘₯ ∈ ℝ (π‘₯ β‰  0 β†’ π‘₯ # 0))
 
23-Feb-2025lringuplu 13343 If the sum of two elements of a local ring is invertible, then at least one of the summands must be invertible. (Contributed by Jim Kingdon, 18-Feb-2025.) (Revised by SN, 23-Feb-2025.)
(πœ‘ β†’ 𝐡 = (Baseβ€˜π‘…))    &   (πœ‘ β†’ π‘ˆ = (Unitβ€˜π‘…))    &   (πœ‘ β†’ + = (+gβ€˜π‘…))    &   (πœ‘ β†’ 𝑅 ∈ LRing)    &   (πœ‘ β†’ (𝑋 + π‘Œ) ∈ π‘ˆ)    &   (πœ‘ β†’ 𝑋 ∈ 𝐡)    &   (πœ‘ β†’ π‘Œ ∈ 𝐡)    β‡’   (πœ‘ β†’ (𝑋 ∈ π‘ˆ ∨ π‘Œ ∈ π‘ˆ))
 
23-Feb-2025lringnz 13342 A local ring is a nonzero ring. (Contributed by Jim Kingdon, 20-Feb-2025.) (Revised by SN, 23-Feb-2025.)
1 = (1rβ€˜π‘…)    &    0 = (0gβ€˜π‘…)    β‡’   (𝑅 ∈ LRing β†’ 1 β‰  0 )
 
23-Feb-2025lringring 13341 A local ring is a ring. (Contributed by Jim Kingdon, 20-Feb-2025.) (Revised by SN, 23-Feb-2025.)
(𝑅 ∈ LRing β†’ 𝑅 ∈ Ring)
 
23-Feb-2025lringnzr 13340 A local ring is a nonzero ring. (Contributed by SN, 23-Feb-2025.)
(𝑅 ∈ LRing β†’ 𝑅 ∈ NzRing)
 
23-Feb-2025islring 13339 The predicate "is a local ring". (Contributed by SN, 23-Feb-2025.)
𝐡 = (Baseβ€˜π‘…)    &    + = (+gβ€˜π‘…)    &    1 = (1rβ€˜π‘…)    &   π‘ˆ = (Unitβ€˜π‘…)    β‡’   (𝑅 ∈ LRing ↔ (𝑅 ∈ NzRing ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 ((π‘₯ + 𝑦) = 1 β†’ (π‘₯ ∈ π‘ˆ ∨ 𝑦 ∈ π‘ˆ))))
 
23-Feb-2025df-lring 13338 A local ring is a nonzero ring where for any two elements summing to one, at least one is invertible. Any field is a local ring; the ring of integers is an example of a ring which is not a local ring. (Contributed by Jim Kingdon, 18-Feb-2025.) (Revised by SN, 23-Feb-2025.)
LRing = {π‘Ÿ ∈ NzRing ∣ βˆ€π‘₯ ∈ (Baseβ€˜π‘Ÿ)βˆ€π‘¦ ∈ (Baseβ€˜π‘Ÿ)((π‘₯(+gβ€˜π‘Ÿ)𝑦) = (1rβ€˜π‘Ÿ) β†’ (π‘₯ ∈ (Unitβ€˜π‘Ÿ) ∨ 𝑦 ∈ (Unitβ€˜π‘Ÿ)))}
 
23-Feb-202501eq0ring 13336 If the zero and the identity element of a ring are the same, the ring is the zero ring. (Contributed by AV, 16-Apr-2019.) (Proof shortened by SN, 23-Feb-2025.)
𝐡 = (Baseβ€˜π‘…)    &    0 = (0gβ€˜π‘…)    &    1 = (1rβ€˜π‘…)    β‡’   ((𝑅 ∈ Ring ∧ 0 = 1 ) β†’ 𝐡 = { 0 })
 
23-Feb-2025nzrring 13333 A nonzero ring is a ring. (Contributed by Stefan O'Rear, 24-Feb-2015.) (Proof shortened by SN, 23-Feb-2025.)
(𝑅 ∈ NzRing β†’ 𝑅 ∈ Ring)
 
21-Feb-2025dftap2 7253 Tight apartness with the apartness properties from df-pap 7250 expanded. (Contributed by Jim Kingdon, 21-Feb-2025.)
(𝑅 TAp 𝐴 ↔ (𝑅 βŠ† (𝐴 Γ— 𝐴) ∧ (βˆ€π‘₯ ∈ 𝐴 Β¬ π‘₯𝑅π‘₯ ∧ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯𝑅𝑦 β†’ 𝑦𝑅π‘₯)) ∧ (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘§ ∈ 𝐴 (π‘₯𝑅𝑦 β†’ (π‘₯𝑅𝑧 ∨ 𝑦𝑅𝑧)) ∧ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (Β¬ π‘₯𝑅𝑦 β†’ π‘₯ = 𝑦))))
 
20-Feb-2025aprap 13382 The relation given by df-apr 13377 for a local ring is an apartness relation. (Contributed by Jim Kingdon, 20-Feb-2025.)
(𝑅 ∈ LRing β†’ (#rβ€˜π‘…) Ap (Baseβ€˜π‘…))
 
20-Feb-2025setscomd 12506 Different components can be set in any order. (Contributed by Jim Kingdon, 20-Feb-2025.)
(πœ‘ β†’ 𝐴 ∈ π‘Œ)    &   (πœ‘ β†’ 𝐡 ∈ 𝑍)    &   (πœ‘ β†’ 𝑆 ∈ 𝑉)    &   (πœ‘ β†’ 𝐴 β‰  𝐡)    &   (πœ‘ β†’ 𝐢 ∈ π‘Š)    &   (πœ‘ β†’ 𝐷 ∈ 𝑋)    β‡’   (πœ‘ β†’ ((𝑆 sSet ⟨𝐴, 𝐢⟩) sSet ⟨𝐡, 𝐷⟩) = ((𝑆 sSet ⟨𝐡, 𝐷⟩) sSet ⟨𝐴, 𝐢⟩))
 
17-Feb-2025aprcotr 13381 The apartness relation given by df-apr 13377 for a local ring is cotransitive. (Contributed by Jim Kingdon, 17-Feb-2025.)
(πœ‘ β†’ 𝐡 = (Baseβ€˜π‘…))    &   (πœ‘ β†’ # = (#rβ€˜π‘…))    &   (πœ‘ β†’ 𝑅 ∈ LRing)    &   (πœ‘ β†’ 𝑋 ∈ 𝐡)    &   (πœ‘ β†’ π‘Œ ∈ 𝐡)    &   (πœ‘ β†’ 𝑍 ∈ 𝐡)    β‡’   (πœ‘ β†’ (𝑋 # π‘Œ β†’ (𝑋 # 𝑍 ∨ π‘Œ # 𝑍)))
 
17-Feb-2025aprsym 13380 The apartness relation given by df-apr 13377 for a ring is symmetric. (Contributed by Jim Kingdon, 17-Feb-2025.)
(πœ‘ β†’ 𝐡 = (Baseβ€˜π‘…))    &   (πœ‘ β†’ # = (#rβ€˜π‘…))    &   (πœ‘ β†’ 𝑅 ∈ Ring)    &   (πœ‘ β†’ 𝑋 ∈ 𝐡)    &   (πœ‘ β†’ π‘Œ ∈ 𝐡)    β‡’   (πœ‘ β†’ (𝑋 # π‘Œ β†’ π‘Œ # 𝑋))
 
17-Feb-2025aprval 13378 Expand Definition df-apr 13377. (Contributed by Jim Kingdon, 17-Feb-2025.)
(πœ‘ β†’ 𝐡 = (Baseβ€˜π‘…))    &   (πœ‘ β†’ # = (#rβ€˜π‘…))    &   (πœ‘ β†’ βˆ’ = (-gβ€˜π‘…))    &   (πœ‘ β†’ π‘ˆ = (Unitβ€˜π‘…))    &   (πœ‘ β†’ 𝑅 ∈ Ring)    &   (πœ‘ β†’ 𝑋 ∈ 𝐡)    &   (πœ‘ β†’ π‘Œ ∈ 𝐡)    β‡’   (πœ‘ β†’ (𝑋 # π‘Œ ↔ (𝑋 βˆ’ π‘Œ) ∈ π‘ˆ))
 
16-Feb-2025aprirr 13379 The apartness relation given by df-apr 13377 for a nonzero ring is irreflexive. (Contributed by Jim Kingdon, 16-Feb-2025.)
(πœ‘ β†’ 𝐡 = (Baseβ€˜π‘…))    &   (πœ‘ β†’ # = (#rβ€˜π‘…))    &   (πœ‘ β†’ 𝑅 ∈ Ring)    &   (πœ‘ β†’ 𝑋 ∈ 𝐡)    &   (πœ‘ β†’ (1rβ€˜π‘…) β‰  (0gβ€˜π‘…))    β‡’   (πœ‘ β†’ Β¬ 𝑋 # 𝑋)
 
16-Feb-2025aptap 8610 Complex apartness (as defined at df-ap 8542) is a tight apartness (as defined at df-tap 7252). (Contributed by Jim Kingdon, 16-Feb-2025.)
# TAp β„‚
 
15-Feb-2025tapeq2 7255 Equality theorem for tight apartness predicate. (Contributed by Jim Kingdon, 15-Feb-2025.)
(𝐴 = 𝐡 β†’ (𝑅 TAp 𝐴 ↔ 𝑅 TAp 𝐡))
 
14-Feb-2025exmidmotap 7263 The proposition that every class has at most one tight apartness is equivalent to excluded middle. (Contributed by Jim Kingdon, 14-Feb-2025.)
(EXMID ↔ βˆ€π‘₯βˆƒ*π‘Ÿ π‘Ÿ TAp π‘₯)
 
14-Feb-2025exmidapne 7262 Excluded middle implies there is only one tight apartness on any class, namely negated equality. (Contributed by Jim Kingdon, 14-Feb-2025.)
(EXMID β†’ (𝑅 TAp 𝐴 ↔ 𝑅 = {βŸ¨π‘’, π‘£βŸ© ∣ ((𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑒 β‰  𝑣)}))
 
14-Feb-2025df-pap 7250 Apartness predicate. A relation 𝑅 is an apartness if it is irreflexive, symmetric, and cotransitive. (Contributed by Jim Kingdon, 14-Feb-2025.)
(𝑅 Ap 𝐴 ↔ ((𝑅 βŠ† (𝐴 Γ— 𝐴) ∧ βˆ€π‘₯ ∈ 𝐴 Β¬ π‘₯𝑅π‘₯) ∧ (βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (π‘₯𝑅𝑦 β†’ 𝑦𝑅π‘₯) ∧ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 βˆ€π‘§ ∈ 𝐴 (π‘₯𝑅𝑦 β†’ (π‘₯𝑅𝑧 ∨ 𝑦𝑅𝑧)))))
 
13-Feb-2025df-apr 13377 The relation between elements whose difference is invertible, which for a local ring is an apartness relation by aprap 13382. (Contributed by Jim Kingdon, 13-Feb-2025.)
#r = (𝑀 ∈ V ↦ {⟨π‘₯, π‘¦βŸ© ∣ ((π‘₯ ∈ (Baseβ€˜π‘€) ∧ 𝑦 ∈ (Baseβ€˜π‘€)) ∧ (π‘₯(-gβ€˜π‘€)𝑦) ∈ (Unitβ€˜π‘€))})
 
8-Feb-20252oneel 7258 βˆ… and 1o are two unequal elements of 2o. (Contributed by Jim Kingdon, 8-Feb-2025.)
βŸ¨βˆ…, 1o⟩ ∈ {βŸ¨π‘’, π‘£βŸ© ∣ ((𝑒 ∈ 2o ∧ 𝑣 ∈ 2o) ∧ 𝑒 β‰  𝑣)}
 
8-Feb-2025tapeq1 7254 Equality theorem for tight apartness predicate. (Contributed by Jim Kingdon, 8-Feb-2025.)
(𝑅 = 𝑆 β†’ (𝑅 TAp 𝐴 ↔ 𝑆 TAp 𝐴))
 
6-Feb-20252omotap 7261 If there is at most one tight apartness on 2o, excluded middle follows. Based on online discussions by Tom de Jong, Andrew W Swan, and Martin Escardo. (Contributed by Jim Kingdon, 6-Feb-2025.)
(βˆƒ*π‘Ÿ π‘Ÿ TAp 2o β†’ EXMID)
 
6-Feb-20252omotaplemst 7260 Lemma for 2omotap 7261. (Contributed by Jim Kingdon, 6-Feb-2025.)
((βˆƒ*π‘Ÿ π‘Ÿ TAp 2o ∧ Β¬ Β¬ πœ‘) β†’ πœ‘)
 
6-Feb-20252omotaplemap 7259 Lemma for 2omotap 7261. (Contributed by Jim Kingdon, 6-Feb-2025.)
(Β¬ Β¬ πœ‘ β†’ {βŸ¨π‘’, π‘£βŸ© ∣ ((𝑒 ∈ 2o ∧ 𝑣 ∈ 2o) ∧ (πœ‘ ∧ 𝑒 β‰  𝑣))} TAp 2o)
 
6-Feb-20252onetap 7257 Negated equality is a tight apartness on 2o. (Contributed by Jim Kingdon, 6-Feb-2025.)
{βŸ¨π‘’, π‘£βŸ© ∣ ((𝑒 ∈ 2o ∧ 𝑣 ∈ 2o) ∧ 𝑒 β‰  𝑣)} TAp 2o
 
5-Feb-2025netap 7256 Negated equality on a set with decidable equality is a tight apartness. (Contributed by Jim Kingdon, 5-Feb-2025.)
(βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 DECID π‘₯ = 𝑦 β†’ {βŸ¨π‘’, π‘£βŸ© ∣ ((𝑒 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑒 β‰  𝑣)} TAp 𝐴)
 
5-Feb-2025df-tap 7252 Tight apartness predicate. A relation 𝑅 is a tight apartness if it is irreflexive, symmetric, cotransitive, and tight. (Contributed by Jim Kingdon, 5-Feb-2025.)
(𝑅 TAp 𝐴 ↔ (𝑅 Ap 𝐴 ∧ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 (Β¬ π‘₯𝑅𝑦 β†’ π‘₯ = 𝑦)))
 
1-Feb-2025mulgnn0cld 13010 Closure of the group multiple (exponentiation) operation for a nonnegative multiplier in a monoid. Deduction associated with mulgnn0cl 13005. (Contributed by SN, 1-Feb-2025.)
𝐡 = (Baseβ€˜πΊ)    &    Β· = (.gβ€˜πΊ)    &   (πœ‘ β†’ 𝐺 ∈ Mnd)    &   (πœ‘ β†’ 𝑁 ∈ β„•0)    &   (πœ‘ β†’ 𝑋 ∈ 𝐡)    β‡’   (πœ‘ β†’ (𝑁 Β· 𝑋) ∈ 𝐡)
 
31-Jan-20250subg 13065 The zero subgroup of an arbitrary group. (Contributed by Stefan O'Rear, 10-Dec-2014.) (Proof shortened by SN, 31-Jan-2025.)
0 = (0gβ€˜πΊ)    β‡’   (𝐺 ∈ Grp β†’ { 0 } ∈ (SubGrpβ€˜πΊ))
 
28-Jan-2025dvdsrex 13273 Existence of the divisibility relation. (Contributed by Jim Kingdon, 28-Jan-2025.)
(𝑅 ∈ SRing β†’ (βˆ₯rβ€˜π‘…) ∈ V)
 
24-Jan-2025reldvdsrsrg 13267 The divides relation is a relation. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2025.)
(𝑅 ∈ SRing β†’ Rel (βˆ₯rβ€˜π‘…))
 
18-Jan-2025rerecapb 8803 A real number has a multiplicative inverse if and only if it is apart from zero. Theorem 11.2.4 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 18-Jan-2025.)
(𝐴 ∈ ℝ β†’ (𝐴 # 0 ↔ βˆƒπ‘₯ ∈ ℝ (𝐴 Β· π‘₯) = 1))
 
18-Jan-2025recapb 8631 A complex number has a multiplicative inverse if and only if it is apart from zero. Theorem 11.2.4 of [HoTT], p. (varies), generalized from real to complex numbers. (Contributed by Jim Kingdon, 18-Jan-2025.)
(𝐴 ∈ β„‚ β†’ (𝐴 # 0 ↔ βˆƒπ‘₯ ∈ β„‚ (𝐴 Β· π‘₯) = 1))
 
17-Jan-2025ressval3d 12534 Value of structure restriction, deduction version. (Contributed by AV, 14-Mar-2020.) (Revised by Jim Kingdon, 17-Jan-2025.)
𝑅 = (𝑆 β†Ύs 𝐴)    &   π΅ = (Baseβ€˜π‘†)    &   πΈ = (Baseβ€˜ndx)    &   (πœ‘ β†’ 𝑆 ∈ 𝑉)    &   (πœ‘ β†’ Fun 𝑆)    &   (πœ‘ β†’ 𝐸 ∈ dom 𝑆)    &   (πœ‘ β†’ 𝐴 βŠ† 𝐡)    β‡’   (πœ‘ β†’ 𝑅 = (𝑆 sSet ⟨𝐸, 𝐴⟩))
 
17-Jan-2025strressid 12533 Behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Revised by Jim Kingdon, 17-Jan-2025.)
(πœ‘ β†’ 𝐡 = (Baseβ€˜π‘Š))    &   (πœ‘ β†’ π‘Š Struct βŸ¨π‘€, π‘βŸ©)    &   (πœ‘ β†’ Fun π‘Š)    &   (πœ‘ β†’ (Baseβ€˜ndx) ∈ dom π‘Š)    β‡’   (πœ‘ β†’ (π‘Š β†Ύs 𝐡) = π‘Š)
 
16-Jan-2025ressex 12528 Existence of structure restriction. (Contributed by Jim Kingdon, 16-Jan-2025.)
((π‘Š ∈ 𝑋 ∧ 𝐴 ∈ π‘Œ) β†’ (π‘Š β†Ύs 𝐴) ∈ V)
 
16-Jan-2025ressvalsets 12527 Value of structure restriction. (Contributed by Jim Kingdon, 16-Jan-2025.)
((π‘Š ∈ 𝑋 ∧ 𝐴 ∈ π‘Œ) β†’ (π‘Š β†Ύs 𝐴) = (π‘Š sSet ⟨(Baseβ€˜ndx), (𝐴 ∩ (Baseβ€˜π‘Š))⟩))
 
10-Jan-2025opprex 13251 Existence of the opposite ring. If you know that 𝑅 is a ring, see opprring 13255. (Contributed by Jim Kingdon, 10-Jan-2025.)
𝑂 = (opprβ€˜π‘…)    β‡’   (𝑅 ∈ 𝑉 β†’ 𝑂 ∈ V)
 
10-Jan-2025mgpex 13141 Existence of the multiplication group. If 𝑅 is known to be a semiring, see srgmgp 13157. (Contributed by Jim Kingdon, 10-Jan-2025.)
𝑀 = (mulGrpβ€˜π‘…)    β‡’   (𝑅 ∈ 𝑉 β†’ 𝑀 ∈ V)
 
5-Jan-2025imbibi 252 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.)
(((πœ‘ β†’ πœ“) ↔ πœ’) β†’ (πœ‘ β†’ (πœ“ ↔ πœ’)))
 
1-Jan-2025snss 3729 The singleton of an element of a class is a subset of the class (inference form of snssg 3728). Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 21-Jun-1993.) (Proof shortened by BJ, 1-Jan-2025.)
𝐴 ∈ V    β‡’   (𝐴 ∈ 𝐡 ↔ {𝐴} βŠ† 𝐡)
 
1-Jan-2025snssg 3728 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 3727 Characterization of the inclusion of a singleton in a class. (Contributed by BJ, 1-Jan-2025.)
({𝐴} βŠ† 𝐡 ↔ (𝐴 ∈ V β†’ 𝐴 ∈ 𝐡))
 
9-Dec-2024nninfwlpoim 7179 Decidable equality for β„•βˆž implies the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 9-Dec-2024.)
(βˆ€π‘₯ ∈ β„•βˆž βˆ€π‘¦ ∈ β„•βˆž DECID π‘₯ = 𝑦 β†’ Ο‰ ∈ WOmni)
 
8-Dec-2024nninfwlpoimlemdc 7178 Lemma for nninfwlpoim 7179. (Contributed by Jim Kingdon, 8-Dec-2024.)
(πœ‘ β†’ 𝐹:Ο‰βŸΆ2o)    &   πΊ = (𝑖 ∈ Ο‰ ↦ if(βˆƒπ‘₯ ∈ suc 𝑖(πΉβ€˜π‘₯) = βˆ…, βˆ…, 1o))    &   (πœ‘ β†’ βˆ€π‘₯ ∈ β„•βˆž βˆ€π‘¦ ∈ β„•βˆž DECID π‘₯ = 𝑦)    β‡’   (πœ‘ β†’ DECID βˆ€π‘› ∈ Ο‰ (πΉβ€˜π‘›) = 1o)
 
8-Dec-2024nninfwlpoimlemginf 7177 Lemma for nninfwlpoim 7179. (Contributed by Jim Kingdon, 8-Dec-2024.)
(πœ‘ β†’ 𝐹:Ο‰βŸΆ2o)    &   πΊ = (𝑖 ∈ Ο‰ ↦ if(βˆƒπ‘₯ ∈ suc 𝑖(πΉβ€˜π‘₯) = βˆ…, βˆ…, 1o))    β‡’   (πœ‘ β†’ (𝐺 = (𝑖 ∈ Ο‰ ↦ 1o) ↔ βˆ€π‘› ∈ Ο‰ (πΉβ€˜π‘›) = 1o))
 
8-Dec-2024nninfwlpoimlemg 7176 Lemma for nninfwlpoim 7179. (Contributed by Jim Kingdon, 8-Dec-2024.)
(πœ‘ β†’ 𝐹:Ο‰βŸΆ2o)    &   πΊ = (𝑖 ∈ Ο‰ ↦ if(βˆƒπ‘₯ ∈ suc 𝑖(πΉβ€˜π‘₯) = βˆ…, βˆ…, 1o))    β‡’   (πœ‘ β†’ 𝐺 ∈ β„•βˆž)
 
7-Dec-2024nninfwlpor 7175 The Weak Limited Principle of Omniscience (WLPO) implies that equality for β„•βˆž is decidable. (Contributed by Jim Kingdon, 7-Dec-2024.)
(Ο‰ ∈ WOmni β†’ βˆ€π‘₯ ∈ β„•βˆž βˆ€π‘¦ ∈ β„•βˆž DECID π‘₯ = 𝑦)
 
7-Dec-2024nninfwlporlem 7174 Lemma for nninfwlpor 7175. The result. (Contributed by Jim Kingdon, 7-Dec-2024.)
(πœ‘ β†’ 𝑋:Ο‰βŸΆ2o)    &   (πœ‘ β†’ π‘Œ:Ο‰βŸΆ2o)    &   π· = (𝑖 ∈ Ο‰ ↦ if((π‘‹β€˜π‘–) = (π‘Œβ€˜π‘–), 1o, βˆ…))    &   (πœ‘ β†’ Ο‰ ∈ WOmni)    β‡’   (πœ‘ β†’ DECID 𝑋 = π‘Œ)
 
6-Dec-2024nninfwlporlemd 7173 Given two countably infinite sequences of zeroes and ones, they are equal if and only if a sequence formed by pointwise comparing them is all ones. (Contributed by Jim Kingdon, 6-Dec-2024.)
(πœ‘ β†’ 𝑋:Ο‰βŸΆ2o)    &   (πœ‘ β†’ π‘Œ:Ο‰βŸΆ2o)    &   π· = (𝑖 ∈ Ο‰ ↦ if((π‘‹β€˜π‘–) = (π‘Œβ€˜π‘–), 1o, βˆ…))    β‡’   (πœ‘ β†’ (𝑋 = π‘Œ ↔ 𝐷 = (𝑖 ∈ Ο‰ ↦ 1o)))
 
3-Dec-2024nninfwlpo 7180 Decidability of equality for β„•βˆž is equivalent to the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 3-Dec-2024.)
(βˆ€π‘₯ ∈ β„•βˆž βˆ€π‘¦ ∈ β„•βˆž DECID π‘₯ = 𝑦 ↔ Ο‰ ∈ WOmni)
 
3-Dec-2024nninfdcinf 7172 The Weak Limited Principle of Omniscience (WLPO) implies that it is decidable whether an element of β„•βˆž equals the point at infinity. (Contributed by Jim Kingdon, 3-Dec-2024.)
(πœ‘ β†’ Ο‰ ∈ WOmni)    &   (πœ‘ β†’ 𝑁 ∈ β„•βˆž)    β‡’   (πœ‘ β†’ DECID 𝑁 = (𝑖 ∈ Ο‰ ↦ 1o))
 
28-Nov-2024basmexd 12525 A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 28-Nov-2024.)
(πœ‘ β†’ 𝐡 = (Baseβ€˜πΊ))    &   (πœ‘ β†’ 𝐴 ∈ 𝐡)    β‡’   (πœ‘ β†’ 𝐺 ∈ V)
 
22-Nov-2024eliotaeu 5207 An inhabited iota expression has a unique value. (Contributed by Jim Kingdon, 22-Nov-2024.)
(𝐴 ∈ (β„©π‘₯πœ‘) β†’ βˆƒ!π‘₯πœ‘)
 
22-Nov-2024eliota 5206 An element of an iota expression. (Contributed by Jim Kingdon, 22-Nov-2024.)
(𝐴 ∈ (β„©π‘₯πœ‘) ↔ βˆƒπ‘¦(𝐴 ∈ 𝑦 ∧ βˆ€π‘₯(πœ‘ ↔ π‘₯ = 𝑦)))
 
18-Nov-2024basmex 12524 A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 18-Nov-2024.)
𝐡 = (Baseβ€˜πΊ)    β‡’   (𝐴 ∈ 𝐡 β†’ 𝐺 ∈ V)
 
12-Nov-2024sravscag 13535 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-2024srascag 13534 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-2024slotsdifipndx 12636 The slot for the scalar is not the index of other slots. (Contributed by AV, 12-Nov-2024.)
(( ·𝑠 β€˜ndx) β‰  (Β·π‘–β€˜ndx) ∧ (Scalarβ€˜ndx) β‰  (Β·π‘–β€˜ndx))
 
11-Nov-2024bj-con1st 14643 Contraposition when the antecedent is a negated stable proposition. See con1dc 856. (Contributed by BJ, 11-Nov-2024.)
(STAB πœ‘ β†’ ((Β¬ πœ‘ β†’ πœ“) β†’ (Β¬ πœ“ β†’ πœ‘)))
 
11-Nov-2024slotsdifdsndx 12682 The index of the slot for the distance is not the index of other slots. (Contributed by AV, 11-Nov-2024.)
((*π‘Ÿβ€˜ndx) β‰  (distβ€˜ndx) ∧ (leβ€˜ndx) β‰  (distβ€˜ndx))
 
11-Nov-2024slotsdifplendx 12671 The index of the slot for the distance is not the index of other slots. (Contributed by AV, 11-Nov-2024.)
((*π‘Ÿβ€˜ndx) β‰  (leβ€˜ndx) ∧ (TopSetβ€˜ndx) β‰  (leβ€˜ndx))
 
11-Nov-2024tsetndxnstarvndx 12655 The slot for the topology is not the slot for the involution in an extensible structure. (Contributed by AV, 11-Nov-2024.)
(TopSetβ€˜ndx) β‰  (*π‘Ÿβ€˜ndx)
 
11-Nov-2024const 852 Contraposition when the antecedent is a negated stable proposition. See comment of condc 853. (Contributed by BJ, 18-Nov-2023.) (Proof shortened by BJ, 11-Nov-2024.)
(STAB πœ‘ β†’ ((Β¬ πœ‘ β†’ Β¬ πœ“) β†’ (πœ“ β†’ πœ‘)))
 
10-Nov-2024slotsdifunifndx 12689 The index of the slot for the uniform set is not the index of other slots. (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)))
 
7-Nov-2024ressbasd 12530 Base set of a structure restriction. (Contributed by Stefan O'Rear, 26-Nov-2014.) (Proof shortened by AV, 7-Nov-2024.)
(πœ‘ β†’ 𝑅 = (π‘Š β†Ύs 𝐴))    &   (πœ‘ β†’ 𝐡 = (Baseβ€˜π‘Š))    &   (πœ‘ β†’ π‘Š ∈ 𝑋)    &   (πœ‘ β†’ 𝐴 ∈ 𝑉)    β‡’   (πœ‘ β†’ (𝐴 ∩ 𝐡) = (Baseβ€˜π‘…))
 
6-Nov-2024oppraddg 13254 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-2024opprbasg 13253 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-2024opprsllem 13252 Lemma for opprbasg 13253 and oppraddg 13254. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by AV, 6-Nov-2024.)
𝑂 = (opprβ€˜π‘…)    &   (𝐸 = Slot (πΈβ€˜ndx) ∧ (πΈβ€˜ndx) ∈ β„•)    &   (πΈβ€˜ndx) β‰  (.rβ€˜ndx)    β‡’   (𝑅 ∈ 𝑉 β†’ (πΈβ€˜π‘…) = (πΈβ€˜π‘‚))
 
4-Nov-2024lgsfvalg 14546 Value of the function 𝐹 which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.) (Revised by Jim Kingdon, 4-Nov-2024.)
𝐹 = (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, (if(𝑛 = 2, if(2 βˆ₯ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑛 βˆ’ 1) / 2)) + 1) mod 𝑛) βˆ’ 1))↑(𝑛 pCnt 𝑁)), 1))    β‡’   ((𝐴 ∈ β„€ ∧ 𝑁 ∈ β„• ∧ 𝑀 ∈ β„•) β†’ (πΉβ€˜π‘€) = if(𝑀 ∈ β„™, (if(𝑀 = 2, if(2 βˆ₯ 𝐴, 0, if((𝐴 mod 8) ∈ {1, 7}, 1, -1)), ((((𝐴↑((𝑀 βˆ’ 1) / 2)) + 1) mod 𝑀) βˆ’ 1))↑(𝑀 pCnt 𝑁)), 1))
 
1-Nov-2024plendxnvscandx 12670 The slot for the "less than or equal to" ordering is not the slot for the scalar product in an extensible structure. (Contributed by AV, 1-Nov-2024.)
(leβ€˜ndx) β‰  ( ·𝑠 β€˜ndx)
 
1-Nov-2024plendxnscandx 12669 The slot for the "less than or equal to" ordering is not the slot for the scalar in an extensible structure. (Contributed by AV, 1-Nov-2024.)
(leβ€˜ndx) β‰  (Scalarβ€˜ndx)
 
1-Nov-2024plendxnmulrndx 12668 The slot for the "less than or equal to" ordering is not the slot for the ring multiplication operation in an extensible structure. (Contributed by AV, 1-Nov-2024.)
(leβ€˜ndx) β‰  (.rβ€˜ndx)
 
1-Nov-2024qsqeqor 10634 The squares of two rational numbers are equal iff one number equals the other or its negative. (Contributed by Jim Kingdon, 1-Nov-2024.)
((𝐴 ∈ β„š ∧ 𝐡 ∈ β„š) β†’ ((𝐴↑2) = (𝐡↑2) ↔ (𝐴 = 𝐡 ∨ 𝐴 = -𝐡)))
 
31-Oct-2024dsndxnmulrndx 12679 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 12654 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 12652 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 12651 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 12650 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) ∈ β„•
 
30-Oct-2024plendxnbasendx 12666 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 12665 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)
  Copyright terms: Public domain W3C HTML validation [external]