Recent Additions to the Intuitionistic Logic
Explorer
Date | Label | Description |
Theorem |
|
28-Jan-2025 | dvdsrex 13079 |
Existence of the divisibility relation. (Contributed by Jim Kingdon,
28-Jan-2025.)
|
⊢ (𝑅 ∈ SRing →
(∥r‘𝑅) ∈ V) |
|
24-Jan-2025 | reldvdsrsrg 13073 |
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-2025 | rerecapb 8776 |
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-2025 | recapb 8604 |
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-2025 | ressval3d 12500 |
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-2025 | strressid 12499 |
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-2025 | ressex 12494 |
Existence of structure restriction. (Contributed by Jim Kingdon,
16-Jan-2025.)
|
⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → (𝑊 ↾s 𝐴) ∈ V) |
|
16-Jan-2025 | ressvalsets 12493 |
Value of structure restriction. (Contributed by Jim Kingdon,
16-Jan-2025.)
|
⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → (𝑊 ↾s 𝐴) = (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑊))〉)) |
|
10-Jan-2025 | opprex 13057 |
Existence of the opposite ring. If you know that 𝑅 is a ring, see
opprring 13061. (Contributed by Jim Kingdon, 10-Jan-2025.)
|
⊢ 𝑂 = (oppr‘𝑅)
⇒ ⊢ (𝑅 ∈ 𝑉 → 𝑂 ∈ V) |
|
10-Jan-2025 | mgpex 12949 |
Existence of the multiplication group. If 𝑅 is known to be a
semiring, see srgmgp 12964. (Contributed by Jim Kingdon,
10-Jan-2025.)
|
⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ (𝑅 ∈ 𝑉 → 𝑀 ∈ V) |
|
5-Jan-2025 | imbibi 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-2025 | snss 3726 |
The singleton of an element of a class is a subset of the class
(inference form of snssg 3725). Theorem 7.4 of [Quine] p. 49.
(Contributed by NM, 21-Jun-1993.) (Proof shortened by BJ,
1-Jan-2025.)
|
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵) |
|
1-Jan-2025 | snssg 3725 |
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-2025 | snssb 3724 |
Characterization of the inclusion of a singleton in a class.
(Contributed by BJ, 1-Jan-2025.)
|
⊢ ({𝐴} ⊆ 𝐵 ↔ (𝐴 ∈ V → 𝐴 ∈ 𝐵)) |
|
9-Dec-2024 | nninfwlpoim 7169 |
Decidable equality for ℕ∞
implies the Weak Limited Principle of
Omniscience (WLPO). (Contributed by Jim Kingdon, 9-Dec-2024.)
|
⊢ (∀𝑥 ∈ ℕ∞
∀𝑦 ∈
ℕ∞ DECID 𝑥 = 𝑦 → ω ∈
WOmni) |
|
8-Dec-2024 | nninfwlpoimlemdc 7168 |
Lemma for nninfwlpoim 7169. (Contributed by Jim Kingdon,
8-Dec-2024.)
|
⊢ (𝜑 → 𝐹:ω⟶2o) & ⊢ 𝐺 = (𝑖 ∈ ω ↦ if(∃𝑥 ∈ suc 𝑖(𝐹‘𝑥) = ∅, ∅,
1o))
& ⊢ (𝜑 → ∀𝑥 ∈ ℕ∞
∀𝑦 ∈
ℕ∞ DECID 𝑥 = 𝑦) ⇒ ⊢ (𝜑 → DECID ∀𝑛 ∈ ω (𝐹‘𝑛) = 1o) |
|
8-Dec-2024 | nninfwlpoimlemginf 7167 |
Lemma for nninfwlpoim 7169. (Contributed by Jim Kingdon,
8-Dec-2024.)
|
⊢ (𝜑 → 𝐹:ω⟶2o) & ⊢ 𝐺 = (𝑖 ∈ ω ↦ if(∃𝑥 ∈ suc 𝑖(𝐹‘𝑥) = ∅, ∅,
1o)) ⇒ ⊢ (𝜑 → (𝐺 = (𝑖 ∈ ω ↦ 1o)
↔ ∀𝑛 ∈
ω (𝐹‘𝑛) =
1o)) |
|
8-Dec-2024 | nninfwlpoimlemg 7166 |
Lemma for nninfwlpoim 7169. (Contributed by Jim Kingdon,
8-Dec-2024.)
|
⊢ (𝜑 → 𝐹:ω⟶2o) & ⊢ 𝐺 = (𝑖 ∈ ω ↦ if(∃𝑥 ∈ suc 𝑖(𝐹‘𝑥) = ∅, ∅,
1o)) ⇒ ⊢ (𝜑 → 𝐺 ∈
ℕ∞) |
|
7-Dec-2024 | nninfwlpor 7165 |
The Weak Limited Principle of Omniscience (WLPO) implies that equality
for ℕ∞ is decidable.
(Contributed by Jim Kingdon,
7-Dec-2024.)
|
⊢ (ω ∈ WOmni → ∀𝑥 ∈
ℕ∞ ∀𝑦 ∈ ℕ∞
DECID 𝑥 =
𝑦) |
|
7-Dec-2024 | nninfwlporlem 7164 |
Lemma for nninfwlpor 7165. The result. (Contributed by Jim Kingdon,
7-Dec-2024.)
|
⊢ (𝜑 → 𝑋:ω⟶2o) & ⊢ (𝜑 → 𝑌:ω⟶2o) & ⊢ 𝐷 = (𝑖 ∈ ω ↦ if((𝑋‘𝑖) = (𝑌‘𝑖), 1o, ∅)) & ⊢ (𝜑 → ω ∈
WOmni) ⇒ ⊢ (𝜑 → DECID 𝑋 = 𝑌) |
|
6-Dec-2024 | nninfwlporlemd 7163 |
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-2024 | nninfwlpo 7170 |
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-2024 | nninfdcinf 7162 |
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-2024 | basmexd 12491 |
A structure whose base is inhabited is a set. (Contributed by Jim
Kingdon, 28-Nov-2024.)
|
⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐺 ∈ V) |
|
22-Nov-2024 | eliotaeu 5200 |
An inhabited iota expression has a unique value. (Contributed by Jim
Kingdon, 22-Nov-2024.)
|
⊢ (𝐴 ∈ (℩𝑥𝜑) → ∃!𝑥𝜑) |
|
22-Nov-2024 | eliota 5199 |
An element of an iota expression. (Contributed by Jim Kingdon,
22-Nov-2024.)
|
⊢ (𝐴 ∈ (℩𝑥𝜑) ↔ ∃𝑦(𝐴 ∈ 𝑦 ∧ ∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) |
|
18-Nov-2024 | basmex 12490 |
A structure whose base is inhabited is a set. (Contributed by Jim
Kingdon, 18-Nov-2024.)
|
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝐵 → 𝐺 ∈ V) |
|
11-Nov-2024 | bj-con1st 14125 |
Contraposition when the antecedent is a negated stable proposition. See
con1dc 856. (Contributed by BJ, 11-Nov-2024.)
|
⊢
(STAB 𝜑 → ((¬ 𝜑 → 𝜓) → (¬ 𝜓 → 𝜑))) |
|
11-Nov-2024 | slotsdifdsndx 12622 |
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-2024 | tsetndxnstarvndx 12603 |
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-2024 | const 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 𝜑 → ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑))) |
|
7-Nov-2024 | ressbasd 12496 |
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-2024 | oppraddg 13060 |
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-2024 | opprbasg 13059 |
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-2024 | opprsllem 13058 |
Lemma for opprbasg 13059 and oppraddg 13060. (Contributed by Mario Carneiro,
1-Dec-2014.) (Revised by AV, 6-Nov-2024.)
|
⊢ 𝑂 = (oppr‘𝑅) & ⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ) & ⊢ (𝐸‘ndx) ≠
(.r‘ndx) ⇒ ⊢ (𝑅 ∈ 𝑉 → (𝐸‘𝑅) = (𝐸‘𝑂)) |
|
4-Nov-2024 | lgsfvalg 14039 |
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-2024 | qsqeqor 10603 |
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-2024 | dsndxnmulrndx 12619 |
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-2024 | tsetndxnmulrndx 12602 |
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-2024 | tsetndxnbasendx 12600 |
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-2024 | basendxlttsetndx 12599 |
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-2024 | tsetndxnn 12598 |
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) ∈
ℕ |
|
29-Oct-2024 | dsndxntsetndx 12621 |
The slot for the distance function is not the slot for the topology in an
extensible structure. (Contributed by AV, 29-Oct-2024.)
|
⊢ (dist‘ndx) ≠
(TopSet‘ndx) |
|
29-Oct-2024 | slotsdnscsi 12620 |
The slots Scalar, ·𝑠 and ·𝑖 are different from the
slot
dist. (Contributed by AV, 29-Oct-2024.)
|
⊢ ((dist‘ndx) ≠ (Scalar‘ndx)
∧ (dist‘ndx) ≠ ( ·𝑠 ‘ndx)
∧ (dist‘ndx) ≠
(·𝑖‘ndx)) |
|
29-Oct-2024 | slotstnscsi 12604 |
The slots Scalar, ·𝑠 and ·𝑖 are different from the
slot
TopSet. (Contributed by AV, 29-Oct-2024.)
|
⊢ ((TopSet‘ndx) ≠ (Scalar‘ndx)
∧ (TopSet‘ndx) ≠ ( ·𝑠
‘ndx) ∧ (TopSet‘ndx) ≠
(·𝑖‘ndx)) |
|
29-Oct-2024 | scandxnmulrndx 12576 |
The slot for the scalar field is not the slot for the ring
(multiplication) operation in an extensible structure. (Contributed by
AV, 29-Oct-2024.)
|
⊢ (Scalar‘ndx) ≠
(.r‘ndx) |
|
29-Oct-2024 | fiubnn 10781 |
A finite set of natural numbers has an upper bound which is a a natural
number. (Contributed by Jim Kingdon, 29-Oct-2024.)
|
⊢ ((𝐴 ⊆ ℕ ∧ 𝐴 ∈ Fin) → ∃𝑥 ∈ ℕ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) |
|
29-Oct-2024 | fiubz 10780 |
A finite set of integers has an upper bound which is an integer.
(Contributed by Jim Kingdon, 29-Oct-2024.)
|
⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ∈ Fin) → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) |
|
29-Oct-2024 | fiubm 10779 |
Lemma for fiubz 10780 and fiubnn 10781. A general form of those theorems.
(Contributed by Jim Kingdon, 29-Oct-2024.)
|
⊢ (𝜑 → 𝐴 ⊆ 𝐵)
& ⊢ (𝜑 → 𝐵 ⊆ ℚ) & ⊢ (𝜑 → 𝐶 ∈ 𝐵)
& ⊢ (𝜑 → 𝐴 ∈ Fin) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) |
|
28-Oct-2024 | dsndxnbasendx 12617 |
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-2024 | basendxltdsndx 12616 |
The index of the slot for the base set is less then the index of the slot
for the distance in an extensible structure. (Contributed by AV,
28-Oct-2024.)
|
⊢ (Base‘ndx) <
(dist‘ndx) |
|
28-Oct-2024 | dsndxnn 12615 |
The index of the slot for the distance in an extensible structure is a
positive integer. (Contributed by AV, 28-Oct-2024.)
|
⊢ (dist‘ndx) ∈
ℕ |
|
27-Oct-2024 | bj-nnst 14117 |
Double negation of stability of a formula. Intuitionistic logic refutes
unstability (but does not prove stability) of any formula. This theorem
can also be proved in classical refutability calculus (see
https://us.metamath.org/mpeuni/bj-peircestab.html) but not in minimal
calculus (see https://us.metamath.org/mpeuni/bj-stabpeirce.html). See
nnnotnotr 14364 for the version not using the definition of
stability.
(Contributed by BJ, 9-Oct-2019.) Prove it in ( → ,
¬ )
-intuitionistic calculus with definitions (uses of ax-ia1 106, ax-ia2 107,
ax-ia3 108 are via sylibr 134, necessary for definition unpackaging), and in
( → , ↔ , ¬ )-intuitionistic
calculus, following a discussion
with Jim Kingdon. (Revised by BJ, 27-Oct-2024.)
|
⊢ ¬ ¬
STAB 𝜑 |
|
27-Oct-2024 | bj-imnimnn 14112 |
If a formula is implied by both a formula and its negation, then it is
not refutable. There is another proof using the inference associated
with bj-nnclavius 14111 as its last step. (Contributed by BJ,
27-Oct-2024.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (¬ 𝜑 → 𝜓) ⇒ ⊢ ¬ ¬ 𝜓 |
|
25-Oct-2024 | nnwosdc 12010 |
Well-ordering principle: any inhabited decidable set of positive
integers has a least element (schema form). (Contributed by NM,
17-Aug-2001.) (Revised by Jim Kingdon, 25-Oct-2024.)
|
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((∃𝑥 ∈ ℕ 𝜑 ∧ ∀𝑥 ∈ ℕ DECID 𝜑) → ∃𝑥 ∈ ℕ (𝜑 ∧ ∀𝑦 ∈ ℕ (𝜓 → 𝑥 ≤ 𝑦))) |
|
23-Oct-2024 | nnwodc 12007 |
Well-ordering principle: any inhabited decidable set of positive
integers has a least element. Theorem I.37 (well-ordering principle) of
[Apostol] p. 34. (Contributed by NM,
17-Aug-2001.) (Revised by Jim
Kingdon, 23-Oct-2024.)
|
⊢ ((𝐴 ⊆ ℕ ∧ ∃𝑤 𝑤 ∈ 𝐴 ∧ ∀𝑗 ∈ ℕ DECID 𝑗 ∈ 𝐴) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) |
|
22-Oct-2024 | uzwodc 12008 |
Well-ordering principle: any inhabited decidable subset of an upper set
of integers has a least element. (Contributed by NM, 8-Oct-2005.)
(Revised by Jim Kingdon, 22-Oct-2024.)
|
⊢ ((𝑆 ⊆
(ℤ≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∃𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘) |
|
21-Oct-2024 | nnnotnotr 14364 |
Double negation of double negation elimination. Suggested by an online
post by Martin Escardo. Although this statement resembles nnexmid 850, it
can be proved with reference only to implication and negation (that is,
without use of disjunction). (Contributed by Jim Kingdon,
21-Oct-2024.)
|
⊢ ¬ ¬
(¬ ¬ 𝜑 → 𝜑) |
|
21-Oct-2024 | scandxnbasendx 12574 |
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-2024 | isprm5lem 12111 |
Lemma for isprm5 12112. The interesting direction (showing that
one only
needs to check prime divisors up to the square root of 𝑃).
(Contributed by Jim Kingdon, 20-Oct-2024.)
|
⊢ (𝜑 → 𝑃 ∈
(ℤ≥‘2))
& ⊢ (𝜑 → ∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃)) & ⊢ (𝜑 → 𝑋 ∈ (2...(𝑃 − 1)))
⇒ ⊢ (𝜑 → ¬ 𝑋 ∥ 𝑃) |
|
19-Oct-2024 | resseqnbasd 12501 |
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) ∈ ℕ) & ⊢ (𝐸‘ndx) ≠
(Base‘ndx)
& ⊢ (𝜑 → 𝑊 ∈ 𝑋)
& ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐶 = (𝐸‘𝑅)) |
|
18-Oct-2024 | dsndxnplusgndx 12618 |
The slot for the distance function is not the slot for the group operation
in an extensible structure. (Contributed by AV, 18-Oct-2024.)
|
⊢ (dist‘ndx) ≠
(+g‘ndx) |
|
18-Oct-2024 | tsetndxnplusgndx 12601 |
The slot for the topology is not the slot for the group operation in an
extensible structure. (Contributed by AV, 18-Oct-2024.)
|
⊢ (TopSet‘ndx) ≠
(+g‘ndx) |
|
18-Oct-2024 | scandxnplusgndx 12575 |
The slot for the scalar field is not the slot for the group operation in
an extensible structure. (Contributed by AV, 18-Oct-2024.)
|
⊢ (Scalar‘ndx) ≠
(+g‘ndx) |
|
17-Oct-2024 | elnndc 9588 |
Membership of an integer in ℕ is decidable.
(Contributed by Jim
Kingdon, 17-Oct-2024.)
|
⊢ (𝑁 ∈ ℤ → DECID
𝑁 ∈
ℕ) |
|
14-Oct-2024 | 2zinfmin 11222 |
Two ways to express the minimum of two integers. Because order of
integers is decidable, we have more flexibility than for real numbers.
(Contributed by Jim Kingdon, 14-Oct-2024.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → inf({𝐴, 𝐵}, ℝ, < ) = if(𝐴 ≤ 𝐵, 𝐴, 𝐵)) |
|
14-Oct-2024 | mingeb 11221 |
Equivalence of ≤ and being equal to the minimum of
two reals.
(Contributed by Jim Kingdon, 14-Oct-2024.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ inf({𝐴, 𝐵}, ℝ, < ) = 𝐴)) |
|
13-Oct-2024 | pcxnn0cl 12280 |
Extended nonnegative integer closure of the general prime count
function. (Contributed by Jim Kingdon, 13-Oct-2024.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (𝑃 pCnt 𝑁) ∈
ℕ0*) |
|
13-Oct-2024 | xnn0letri 9777 |
Dichotomy for extended nonnegative integers. (Contributed by Jim Kingdon,
13-Oct-2024.)
|
⊢ ((𝐴 ∈ ℕ0*
∧ 𝐵 ∈
ℕ0*) → (𝐴 ≤ 𝐵 ∨ 𝐵 ≤ 𝐴)) |
|
13-Oct-2024 | xnn0dcle 9776 |
Decidability of ≤ for extended nonnegative integers.
(Contributed by
Jim Kingdon, 13-Oct-2024.)
|
⊢ ((𝐴 ∈ ℕ0*
∧ 𝐵 ∈
ℕ0*) → DECID 𝐴 ≤ 𝐵) |
|
9-Oct-2024 | nn0leexp2 10662 |
Ordering law for exponentiation. (Contributed by Jim Kingdon,
9-Oct-2024.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ 1 < 𝐴) →
(𝑀 ≤ 𝑁 ↔ (𝐴↑𝑀) ≤ (𝐴↑𝑁))) |
|
8-Oct-2024 | pclemdc 12258 |
Lemma for the prime power pre-function's properties. (Contributed by
Jim Kingdon, 8-Oct-2024.)
|
⊢ 𝐴 = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁} ⇒ ⊢ ((𝑃 ∈ (ℤ≥‘2)
∧ (𝑁 ∈ ℤ
∧ 𝑁 ≠ 0)) →
∀𝑥 ∈ ℤ
DECID 𝑥
∈ 𝐴) |
|
8-Oct-2024 | elnn0dc 9587 |
Membership of an integer in ℕ0 is
decidable. (Contributed by Jim
Kingdon, 8-Oct-2024.)
|
⊢ (𝑁 ∈ ℤ → DECID
𝑁 ∈
ℕ0) |
|
7-Oct-2024 | pclemub 12257 |
Lemma for the prime power pre-function's properties. (Contributed by
Mario Carneiro, 23-Feb-2014.) (Revised by Jim Kingdon,
7-Oct-2024.)
|
⊢ 𝐴 = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁} ⇒ ⊢ ((𝑃 ∈ (ℤ≥‘2)
∧ (𝑁 ∈ ℤ
∧ 𝑁 ≠ 0)) →
∃𝑥 ∈ ℤ
∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) |
|
7-Oct-2024 | pclem0 12256 |
Lemma for the prime power pre-function's properties. (Contributed by
Mario Carneiro, 23-Feb-2014.) (Revised by Jim Kingdon,
7-Oct-2024.)
|
⊢ 𝐴 = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁} ⇒ ⊢ ((𝑃 ∈ (ℤ≥‘2)
∧ (𝑁 ∈ ℤ
∧ 𝑁 ≠ 0)) → 0
∈ 𝐴) |
|
7-Oct-2024 | nn0ltexp2 10661 |
Special case of ltexp2 13993 which we use here because we haven't yet
defined df-rpcxp 13913 which is used in the current proof of ltexp2 13993.
(Contributed by Jim Kingdon, 7-Oct-2024.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ 1 < 𝐴) →
(𝑀 < 𝑁 ↔ (𝐴↑𝑀) < (𝐴↑𝑁))) |
|
6-Oct-2024 | suprzcl2dc 11926 |
The supremum of a bounded-above decidable set of integers is a member of
the set. (This theorem avoids ax-pre-suploc 7910.) (Contributed by Mario
Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 6-Oct-2024.)
|
⊢ (𝜑 → 𝐴 ⊆ ℤ) & ⊢ (𝜑 → ∀𝑥 ∈ ℤ
DECID 𝑥
∈ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)
& ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → sup(𝐴, ℝ, < ) ∈ 𝐴) |
|
5-Oct-2024 | zsupssdc 11925 |
An inhabited decidable bounded subset of integers has a supremum in the
set. (The proof does not use ax-pre-suploc 7910.) (Contributed by Mario
Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.)
|
⊢ (𝜑 → 𝐴 ⊆ ℤ) & ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)
& ⊢ (𝜑 → ∀𝑥 ∈ ℤ DECID 𝑥 ∈ 𝐴)
& ⊢ (𝜑 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) |
|
5-Oct-2024 | suprzubdc 11923 |
The supremum of a bounded-above decidable set of integers is greater
than any member of the set. (Contributed by Mario Carneiro,
21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.)
|
⊢ (𝜑 → 𝐴 ⊆ ℤ) & ⊢ (𝜑 → ∀𝑥 ∈ ℤ
DECID 𝑥
∈ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)
& ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ≤ sup(𝐴, ℝ, < )) |
|
1-Oct-2024 | infex2g 7026 |
Existence of infimum. (Contributed by Jim Kingdon, 1-Oct-2024.)
|
⊢ (𝐴 ∈ 𝐶 → inf(𝐵, 𝐴, 𝑅) ∈ V) |
|
30-Sep-2024 | unbendc 12425 |
An unbounded decidable set of positive integers is infinite.
(Contributed by NM, 5-May-2005.) (Revised by Jim Kingdon,
30-Sep-2024.)
|
⊢ ((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ
DECID 𝑥
∈ 𝐴 ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝐴 𝑚 < 𝑛) → 𝐴 ≈ ℕ) |
|
30-Sep-2024 | prmdc 12100 |
Primality is decidable. (Contributed by Jim Kingdon, 30-Sep-2024.)
|
⊢ (𝑁 ∈ ℕ → DECID
𝑁 ∈
ℙ) |
|
30-Sep-2024 | dcfi 6973 |
Decidability of a family of propositions indexed by a finite set.
(Contributed by Jim Kingdon, 30-Sep-2024.)
|
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 DECID 𝜑) → DECID ∀𝑥 ∈ 𝐴 𝜑) |
|
29-Sep-2024 | ssnnct 12418 |
A decidable subset of ℕ is countable.
(Contributed by Jim Kingdon,
29-Sep-2024.)
|
⊢ ((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ
DECID 𝑥
∈ 𝐴) →
∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o)) |
|
29-Sep-2024 | ssnnctlemct 12417 |
Lemma for ssnnct 12418. The result. (Contributed by Jim Kingdon,
29-Sep-2024.)
|
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 1) ⇒ ⊢ ((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ
DECID 𝑥
∈ 𝐴) →
∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o)) |
|
28-Sep-2024 | nninfdcex 11924 |
A decidable set of natural numbers has an infimum. (Contributed by Jim
Kingdon, 28-Sep-2024.)
|
⊢ (𝜑 → 𝐴 ⊆ ℕ) & ⊢ (𝜑 → ∀𝑥 ∈ ℕ
DECID 𝑥
∈ 𝐴) & ⊢ (𝜑 → ∃𝑦 𝑦 ∈ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
|
27-Sep-2024 | infregelbex 9574 |
Any lower bound of a set of real numbers with an infimum is less than or
equal to the infimum. (Contributed by Jim Kingdon, 27-Sep-2024.)
|
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ)
⇒ ⊢ (𝜑 → (𝐵 ≤ inf(𝐴, ℝ, < ) ↔ ∀𝑧 ∈ 𝐴 𝐵 ≤ 𝑧)) |
|
26-Sep-2024 | nninfdclemp1 12421 |
Lemma for nninfdc 12424. Each element of the sequence 𝐹 is
greater
than the previous element. (Contributed by Jim Kingdon,
26-Sep-2024.)
|
⊢ (𝜑 → 𝐴 ⊆ ℕ) & ⊢ (𝜑 → ∀𝑥 ∈ ℕ
DECID 𝑥
∈ 𝐴) & ⊢ (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛)
& ⊢ (𝜑 → (𝐽 ∈ 𝐴 ∧ 1 < 𝐽)) & ⊢ 𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩
(ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽)) & ⊢ (𝜑 → 𝑈 ∈ ℕ)
⇒ ⊢ (𝜑 → (𝐹‘𝑈) < (𝐹‘(𝑈 + 1))) |
|
26-Sep-2024 | nnminle 12006 |
The infimum of a decidable subset of the natural numbers is less than an
element of the set. The infimum is also a minimum as shown at
nnmindc 12005. (Contributed by Jim Kingdon, 26-Sep-2024.)
|
⊢ ((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ
DECID 𝑥
∈ 𝐴 ∧ 𝐵 ∈ 𝐴) → inf(𝐴, ℝ, < ) ≤ 𝐵) |
|
25-Sep-2024 | nninfdclemcl 12419 |
Lemma for nninfdc 12424. (Contributed by Jim Kingdon, 25-Sep-2024.)
|
⊢ (𝜑 → 𝐴 ⊆ ℕ) & ⊢ (𝜑 → ∀𝑥 ∈ ℕ
DECID 𝑥
∈ 𝐴) & ⊢ (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛)
& ⊢ (𝜑 → 𝑃 ∈ 𝐴)
& ⊢ (𝜑 → 𝑄 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑃(𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩
(ℤ≥‘(𝑦 + 1))), ℝ, < ))𝑄) ∈ 𝐴) |
|
24-Sep-2024 | nninfdclemlt 12422 |
Lemma for nninfdc 12424. The function from nninfdclemf 12420 is strictly
monotonic. (Contributed by Jim Kingdon, 24-Sep-2024.)
|
⊢ (𝜑 → 𝐴 ⊆ ℕ) & ⊢ (𝜑 → ∀𝑥 ∈ ℕ
DECID 𝑥
∈ 𝐴) & ⊢ (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛)
& ⊢ (𝜑 → (𝐽 ∈ 𝐴 ∧ 1 < 𝐽)) & ⊢ 𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩
(ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽)) & ⊢ (𝜑 → 𝑈 ∈ ℕ) & ⊢ (𝜑 → 𝑉 ∈ ℕ) & ⊢ (𝜑 → 𝑈 < 𝑉) ⇒ ⊢ (𝜑 → (𝐹‘𝑈) < (𝐹‘𝑉)) |
|
23-Sep-2024 | nninfdc 12424 |
An unbounded decidable set of positive integers is infinite.
(Contributed by Jim Kingdon, 23-Sep-2024.)
|
⊢ ((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ
DECID 𝑥
∈ 𝐴 ∧
∀𝑚 ∈ ℕ
∃𝑛 ∈ 𝐴 𝑚 < 𝑛) → ω ≼ 𝐴) |
|
23-Sep-2024 | nninfdclemf1 12423 |
Lemma for nninfdc 12424. The function from nninfdclemf 12420 is one-to-one.
(Contributed by Jim Kingdon, 23-Sep-2024.)
|
⊢ (𝜑 → 𝐴 ⊆ ℕ) & ⊢ (𝜑 → ∀𝑥 ∈ ℕ
DECID 𝑥
∈ 𝐴) & ⊢ (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛)
& ⊢ (𝜑 → (𝐽 ∈ 𝐴 ∧ 1 < 𝐽)) & ⊢ 𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩
(ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))
⇒ ⊢ (𝜑 → 𝐹:ℕ–1-1→𝐴) |
|
23-Sep-2024 | nninfdclemf 12420 |
Lemma for nninfdc 12424. A function from the natural numbers into
𝐴. (Contributed by Jim Kingdon,
23-Sep-2024.)
|
⊢ (𝜑 → 𝐴 ⊆ ℕ) & ⊢ (𝜑 → ∀𝑥 ∈ ℕ
DECID 𝑥
∈ 𝐴) & ⊢ (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛)
& ⊢ (𝜑 → (𝐽 ∈ 𝐴 ∧ 1 < 𝐽)) & ⊢ 𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩
(ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))
⇒ ⊢ (𝜑 → 𝐹:ℕ⟶𝐴) |
|
23-Sep-2024 | nnmindc 12005 |
An inhabited decidable subset of the natural numbers has a minimum.
(Contributed by Jim Kingdon, 23-Sep-2024.)
|
⊢ ((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ
DECID 𝑥
∈ 𝐴 ∧
∃𝑦 𝑦 ∈ 𝐴) → inf(𝐴, ℝ, < ) ∈ 𝐴) |
|
19-Sep-2024 | ssomct 12416 |
A decidable subset of ω is countable.
(Contributed by Jim
Kingdon, 19-Sep-2024.)
|
⊢ ((𝐴 ⊆ ω ∧ ∀𝑥 ∈ ω
DECID 𝑥
∈ 𝐴) →
∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o)) |
|
14-Sep-2024 | nnpredlt 4619 |
The predecessor (see nnpredcl 4618) of a nonzero natural number is less
than (see df-iord 4362) that number. (Contributed by Jim Kingdon,
14-Sep-2024.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐴 ≠ ∅) → ∪ 𝐴
∈ 𝐴) |
|
13-Sep-2024 | nninfisollemeq 7123 |
Lemma for nninfisol 7124. The case where 𝑁 is a successor and 𝑁
and 𝑋 are equal. (Contributed by Jim
Kingdon, 13-Sep-2024.)
|
⊢ (𝜑 → 𝑋 ∈
ℕ∞)
& ⊢ (𝜑 → (𝑋‘𝑁) = ∅) & ⊢ (𝜑 → 𝑁 ∈ ω) & ⊢ (𝜑 → 𝑁 ≠ ∅) & ⊢ (𝜑 → (𝑋‘∪ 𝑁) =
1o) ⇒ ⊢ (𝜑 → DECID (𝑖 ∈ ω ↦
if(𝑖 ∈ 𝑁, 1o, ∅)) =
𝑋) |
|
13-Sep-2024 | nninfisollemne 7122 |
Lemma for nninfisol 7124. A case where 𝑁 is a successor and 𝑁
and 𝑋 are not equal. (Contributed by Jim
Kingdon,
13-Sep-2024.)
|
⊢ (𝜑 → 𝑋 ∈
ℕ∞)
& ⊢ (𝜑 → (𝑋‘𝑁) = ∅) & ⊢ (𝜑 → 𝑁 ∈ ω) & ⊢ (𝜑 → 𝑁 ≠ ∅) & ⊢ (𝜑 → (𝑋‘∪ 𝑁) =
∅) ⇒ ⊢ (𝜑 → DECID (𝑖 ∈ ω ↦
if(𝑖 ∈ 𝑁, 1o, ∅)) =
𝑋) |
|
13-Sep-2024 | nninfisollem0 7121 |
Lemma for nninfisol 7124. The case where 𝑁 is zero. (Contributed
by Jim Kingdon, 13-Sep-2024.)
|
⊢ (𝜑 → 𝑋 ∈
ℕ∞)
& ⊢ (𝜑 → (𝑋‘𝑁) = ∅) & ⊢ (𝜑 → 𝑁 ∈ ω) & ⊢ (𝜑 → 𝑁 = ∅) ⇒ ⊢ (𝜑 → DECID (𝑖 ∈ ω ↦
if(𝑖 ∈ 𝑁, 1o, ∅)) =
𝑋) |