P. 383 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Theorem

isbasisrelowl 38201

The set of all closed-below, open-above intervals of reals form a basis. (Contributed by ML, 27-Jul-2020.)

⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ 𝐼 ∈ TopBases

Theorem

icoreunrn 38202

The union of all closed-below, open-above intervals of reals is the set of reals. (Contributed by ML, 27-Jul-2020.)

⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ ℝ = ∪ 𝐼

Theorem

istoprelowl 38203

The set of all closed-below, open-above intervals of reals generate a topology on the reals. (Contributed by ML, 27-Jul-2020.)

⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ (topGen‘𝐼) ∈ (TopOn‘ℝ)

Theorem

icoreelrn 38204*

A class abstraction which is an element of the set of closed-below, open-above intervals of reals. (Contributed by ML, 1-Aug-2020.)

⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → {𝑧 ∈ ℝ ∣ (𝐴 ≤ 𝑧 ∧ 𝑧 < 𝐵)} ∈ 𝐼)

Theorem

iooelexlt 38205*

An element of an open interval is not its smallest element. (Contributed by ML, 2-Aug-2020.)

⊢ (𝑋 ∈ (𝐴(,)𝐵) → ∃𝑦 ∈ (𝐴(,)𝐵)𝑦 < 𝑋)

Theorem

relowlssretop 38206

The lower limit topology on the reals is finer than the standard topology. (Contributed by ML, 1-Aug-2020.)

⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ (topGen‘ran (,)) ⊆ (topGen‘𝐼)

Theorem

relowlpssretop 38207

The lower limit topology on the reals is strictly finer than the standard topology. (Contributed by ML, 2-Aug-2020.)

⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ (topGen‘ran (,)) ⊊ (topGen‘𝐼)

Theorem

sucneqond 38208

Inequality of an ordinal set with its successor. Does not use the axiom of regularity. (Contributed by ML, 18-Oct-2020.)

⊢ (𝜑 → 𝑋 = suc 𝑌)    &   ⊢ (𝜑 → 𝑌 ∈ On)    ⇒   ⊢ (𝜑 → 𝑋 ≠ 𝑌)

Theorem

sucneqoni 38209

Inequality of an ordinal set with its successor. Does not use the axiom of regularity. (Contributed by ML, 18-Oct-2020.)

⊢ 𝑋 = suc 𝑌    &   ⊢ 𝑌 ∈ On    ⇒   ⊢ 𝑋 ≠ 𝑌

Theorem

onsucuni3 38210

If an ordinal number has a predecessor, then it is successor of that predecessor. (Contributed by ML, 17-Oct-2020.)

⊢ ((𝐵 ∈ On ∧ 𝐵 ≠ ∅ ∧ ¬ Lim 𝐵) → 𝐵 = suc ∪ 𝐵)

Theorem

1oequni2o 38211

The ordinal number 1_o is the predecessor of the ordinal number 2_o. (Contributed by ML, 19-Oct-2020.)

⊢ 1_o = ∪ 2_o

Theorem

rdgsucuni 38212

If an ordinal number has a predecessor, the value of the recursive definition generator at that number in terms of its predecessor. (Contributed by ML, 17-Oct-2020.)

⊢ ((𝐵 ∈ On ∧ 𝐵 ≠ ∅ ∧ ¬ Lim 𝐵) → (rec(𝐹, 𝐼)‘𝐵) = (𝐹‘(rec(𝐹, 𝐼)‘∪ 𝐵)))

Theorem

rdgeqoa 38213

If a recursive function with an initial value 𝐴 at step 𝑁 is equal to itself with an initial value 𝐵 at step 𝑀, then every finite number of successor steps will also be equal. (Contributed by ML, 21-Oct-2020.)

⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑋 ∈ ω) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +_o 𝑋)) = (rec(𝐹, 𝐵)‘(𝑀 +_o 𝑋))))

Theorem

elxp8 38214

Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp7 8019. (Contributed by ML, 19-Oct-2020.)

⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ((1^st ‘𝐴) ∈ 𝐵 ∧ 𝐴 ∈ (V × 𝐶)))

Theorem

cbveud 38215*

Deduction used to change bound variables in an existential uniqueness quantifier, using implicit substitution. (Contributed by ML, 27-Mar-2021.)

⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑦𝜒))

Theorem

cbvreud 38216*

Deduction used to change bound variables in a restricted existential uniqueness quantifier. (Contributed by ML, 27-Mar-2021.)

⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑦 ∈ 𝐴 𝜒))

Theorem

difunieq 38217

The difference of unions is a subset of the union of the difference. (Contributed by ML, 29-Mar-2021.)

⊢ (∪ 𝐴 ∖ ∪ 𝐵) ⊆ ∪ (𝐴 ∖ 𝐵)

Theorem

inunissunidif 38218

Theorem about subsets of the difference of unions. (Contributed by ML, 29-Mar-2021.)

⊢ ((𝐴 ∩ ∪ 𝐶) = ∅ → (𝐴 ⊆ ∪ 𝐵 ↔ 𝐴 ⊆ ∪ (𝐵 ∖ 𝐶)))

Theorem

rdgellim 38219

Elementhood in a recursive definition at a limit ordinal. (Contributed by ML, 30-Mar-2022.)

⊢ (((𝐵 ∈ On ∧ Lim 𝐵) ∧ 𝐶 ∈ 𝐵) → (𝑋 ∈ (rec(𝐹, 𝐴)‘𝐶) → 𝑋 ∈ (rec(𝐹, 𝐴)‘𝐵)))

Theorem

rdglimss 38220

A recursive definition at a limit ordinal is a superset of itself at any smaller ordinal. (Contributed by ML, 30-Mar-2022.)

⊢ (((𝐵 ∈ On ∧ Lim 𝐵) ∧ 𝐶 ∈ 𝐵) → (rec(𝐹, 𝐴)‘𝐶) ⊆ (rec(𝐹, 𝐴)‘𝐵))

Theorem

rdgssun 38221*

In a recursive definition where each step expands on the previous one using a union, every previous step is a subset of every later step. (Contributed by ML, 1-Apr-2022.)

⊢ 𝐹 = (𝑤 ∈ V ↦ (𝑤 ∪ 𝐵))    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝑋 ∈ On ∧ 𝑌 ∈ 𝑋) → (rec(𝐹, 𝐴)‘𝑌) ⊆ (rec(𝐹, 𝐴)‘𝑋))

Theorem

exrecfnlem 38222*

Lemma for exrecfn 38223. (Contributed by ML, 30-Mar-2022.)

⊢ 𝐹 = (𝑧 ∈ V ↦ (𝑧 ∪ ran (𝑦 ∈ 𝑧 ↦ 𝐵)))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦 𝐵 ∈ 𝑊) → ∃𝑥(𝐴 ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝐵 ∈ 𝑥))

Theorem

exrecfn 38223*

Theorem about the existence of infinite recursive sets. 𝑦 should usually be free in 𝐵. (Contributed by ML, 30-Mar-2022.)

⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦 𝐵 ∈ 𝑊) → ∃𝑥(𝐴 ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝐵 ∈ 𝑥))

Theorem

exrecfnpw 38224*

For any base set, a set which contains the powerset of all of its own elements exists. (Contributed by ML, 30-Mar-2022.)

⊢ (𝐴 ∈ 𝑉 → ∃𝑥(𝐴 ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝒫 𝑦 ∈ 𝑥))

Theorem

finorwe 38225

If the Axiom of Infinity is denied, every total order is a well-order. The notion of a well-order cannot be usefully expressed without the Axiom of Infinity due to the inability to quantify over proper classes. (Contributed by ML, 5-Oct-2023.)

⊢ (¬ ω ∈ V → ( < Or 𝐴 → < We 𝐴))

21.21.2  Cartesian exponentiation

Syntax

cfinxp 38226

Extend the definition of a class to include Cartesian exponentiation.

class (𝑈↑↑𝑁)

Definition

df-finxp 38227*

Define Cartesian exponentiation on a class.

Note that this definition is limited to finite exponents, since it is defined using nested ordered pairs. If tuples of infinite length are needed, or if they might be needed in the future, use df-ixp 8904 or df-map 8827 instead. The main advantage of this definition is that it integrates better with functions and relations. For example if 𝑅 is a subset of (𝐴↑↑2_o), then df-br 5103 can be used on it, and df-fv 6535 can also be used, and so on.

It's also worth keeping in mind that ((𝑈↑↑𝑀) × (𝑈↑↑𝑁)) is generally not equal to (𝑈↑↑(𝑀 +_o 𝑁)).

This definition is technical. Use finxp1o 38235 and finxpsuc 38241 for a more standard recursive experience. (Contributed by ML, 16-Oct-2020.)

⊢ (𝑈↑↑𝑁) = {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1_o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1^st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))}

Theorem

dffinxpf 38228*

This theorem is the same as Definition df-finxp 38227, except that the large function is replaced by a class variable for brevity. (Contributed by ML, 24-Oct-2020.)

⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1_o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1^st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))    ⇒   ⊢ (𝑈↑↑𝑁) = {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁))}

Theorem

finxpeq1 38229

Equality theorem for Cartesian exponentiation. (Contributed by ML, 19-Oct-2020.)

⊢ (𝑈 = 𝑉 → (𝑈↑↑𝑁) = (𝑉↑↑𝑁))

Theorem

finxpeq2 38230

Equality theorem for Cartesian exponentiation. (Contributed by ML, 19-Oct-2020.)

⊢ (𝑀 = 𝑁 → (𝑈↑↑𝑀) = (𝑈↑↑𝑁))

Theorem

csbfinxpg 38231*

Distribute proper substitution through Cartesian exponentiation. (Contributed by ML, 25-Oct-2020.)

⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝑈↑↑𝑁) = (⦋𝐴 / 𝑥⦌𝑈↑↑⦋𝐴 / 𝑥⦌𝑁))

Theorem

finxpreclem1 38232*

Lemma for ↑↑ recursion theorems. (Contributed by ML, 17-Oct-2020.)

⊢ (𝑋 ∈ 𝑈 → ∅ = ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1_o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1^st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))‘⟨1_o, 𝑋⟩))

Theorem

finxpreclem2 38233*

Lemma for ↑↑ recursion theorems. (Contributed by ML, 17-Oct-2020.)

⊢ ((𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) → ¬ ∅ = ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1_o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1^st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))‘⟨1_o, 𝑋⟩))

Theorem

finxp0 38234

The value of Cartesian exponentiation at zero. (Contributed by ML, 24-Oct-2020.)

⊢ (𝑈↑↑∅) = ∅

Theorem

finxp1o 38235

The value of Cartesian exponentiation at one. (Contributed by ML, 17-Oct-2020.)

⊢ (𝑈↑↑1_o) = 𝑈

Theorem

finxpreclem3 38236*

Lemma for ↑↑ recursion theorems. (Contributed by ML, 20-Oct-2020.)

⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1_o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1^st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))    ⇒   ⊢ (((𝑁 ∈ ω ∧ 2_o ⊆ 𝑁) ∧ 𝑋 ∈ (V × 𝑈)) → ⟨∪ 𝑁, (1^st ‘𝑋)⟩ = (𝐹‘⟨𝑁, 𝑋⟩))

Theorem

finxpreclem4 38237*

Lemma for ↑↑ recursion theorems. (Contributed by ML, 23-Oct-2020.)

⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1_o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1^st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))    ⇒   ⊢ (((𝑁 ∈ ω ∧ 2_o ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, ⟨𝑁, 𝑦⟩)‘𝑁) = (rec(𝐹, ⟨∪ 𝑁, (1^st ‘𝑦)⟩)‘∪ 𝑁))

Theorem

finxpreclem5 38238*

Lemma for ↑↑ recursion theorems. (Contributed by ML, 24-Oct-2020.)

⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1_o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1^st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))    ⇒   ⊢ ((𝑛 ∈ ω ∧ 1_o ∈ 𝑛) → (¬ 𝑥 ∈ (V × 𝑈) → (𝐹‘⟨𝑛, 𝑥⟩) = ⟨𝑛, 𝑥⟩))

Theorem

finxpreclem6 38239*

Lemma for ↑↑ recursion theorems. (Contributed by ML, 24-Oct-2020.)

⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1_o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1^st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))    ⇒   ⊢ ((𝑁 ∈ ω ∧ 1_o ∈ 𝑁) → (𝑈↑↑𝑁) ⊆ (V × 𝑈))

Theorem

finxpsuclem 38240*

Lemma for finxpsuc 38241. (Contributed by ML, 24-Oct-2020.)

⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1_o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1^st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))    ⇒   ⊢ ((𝑁 ∈ ω ∧ 1_o ⊆ 𝑁) → (𝑈↑↑suc 𝑁) = ((𝑈↑↑𝑁) × 𝑈))

Theorem

finxpsuc 38241

The value of Cartesian exponentiation at a successor. (Contributed by ML, 24-Oct-2020.)

⊢ ((𝑁 ∈ ω ∧ 𝑁 ≠ ∅) → (𝑈↑↑suc 𝑁) = ((𝑈↑↑𝑁) × 𝑈))

Theorem

finxp2o 38242

The value of Cartesian exponentiation at two. (Contributed by ML, 19-Oct-2020.)

⊢ (𝑈↑↑2_o) = (𝑈 × 𝑈)

Theorem

finxp3o 38243

The value of Cartesian exponentiation at three. (Contributed by ML, 24-Oct-2020.)

⊢ (𝑈↑↑3_o) = ((𝑈 × 𝑈) × 𝑈)

Theorem

finxpnom 38244

Cartesian exponentiation when the exponent is not a natural number defaults to the empty set. (Contributed by ML, 24-Oct-2020.)

⊢ (¬ 𝑁 ∈ ω → (𝑈↑↑𝑁) = ∅)

Theorem

finxp00 38245

Cartesian exponentiation of the empty set to any power is the empty set. (Contributed by ML, 24-Oct-2020.)

⊢ (∅↑↑𝑁) = ∅

21.21.3  Topology

Theorem

iunctb2 38246

Using the axiom of countable choice ax-cc 10485, the countable union of countable sets is countable. See iunctb 10631 for a somewhat more general theorem. (Contributed by ML, 10-Dec-2020.)

⊢ (∀𝑥 ∈ ω 𝐵 ≼ ω → ∪ 𝑥 ∈ ω 𝐵 ≼ ω)

Theorem

domalom 38247*

A class which dominates every natural number is not finite. (Contributed by ML, 14-Dec-2020.)

⊢ (∀𝑛 ∈ ω 𝑛 ≼ 𝐴 → ¬ 𝐴 ∈ Fin)

Theorem

isinf2 38248*

The converse of isinf 9234. 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 ML, 14-Dec-2020.)

⊢ (∀𝑛 ∈ ω ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛) → ¬ 𝐴 ∈ Fin)

Theorem

ctbssinf 38249*

Using the axiom of choice, any infinite class has a countable subset. (Contributed by ML, 14-Dec-2020.)

⊢ (¬ 𝐴 ∈ Fin → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ω))

Theorem

ralssiun 38250*

The index set of an indexed union is a subset of the union when each 𝐵 contains its index. (Contributed by ML, 16-Dec-2020.)

⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 → 𝐴 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)

Theorem

nlpineqsn 38251*

For every point 𝑝 of a subset 𝐴 of 𝑋 with no limit points, there exists an open set 𝑛 that intersects 𝐴 only at 𝑝. (Contributed by ML, 23-Mar-2021.)

⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝐴) = ∅) → ∀𝑝 ∈ 𝐴 ∃𝑛 ∈ 𝐽 (𝑝 ∈ 𝑛 ∧ (𝑛 ∩ 𝐴) = {𝑝}))

Theorem

nlpfvineqsn 38252*

Given a subset 𝐴 of 𝑋 with no limit points, there exists a function from each point 𝑝 of 𝐴 to an open set intersecting 𝐴 only at 𝑝. This proof uses the axiom of choice. (Contributed by ML, 23-Mar-2021.)

⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐴 ∈ 𝑉 → ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝐴) = ∅) → ∃𝑓(𝑓:𝐴⟶𝐽 ∧ ∀𝑝 ∈ 𝐴 ((𝑓‘𝑝) ∩ 𝐴) = {𝑝})))

Theorem

fvineqsnf1 38253*

A theorem about functions where the image of every point intersects the domain only at that point. If 𝐽 is a topology and 𝐴 is a set with no limit points, then there exists an 𝐹 such that this antecedent is true. See nlpfvineqsn 38252 for a proof of this fact. (Contributed by ML, 23-Mar-2021.)

⊢ ((𝐹:𝐴⟶𝐽 ∧ ∀𝑝 ∈ 𝐴 ((𝐹‘𝑝) ∩ 𝐴) = {𝑝}) → 𝐹:𝐴–1-1→𝐽)

Theorem

fvineqsneu 38254*

A theorem about functions where the image of every point intersects the domain only at that point. (Contributed by ML, 27-Mar-2021.)

⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑝 ∈ 𝐴 ((𝐹‘𝑝) ∩ 𝐴) = {𝑝}) → ∀𝑞 ∈ 𝐴 ∃!𝑥 ∈ ran 𝐹 𝑞 ∈ 𝑥)

Theorem

fvineqsneq 38255*

A theorem about functions where the image of every point intersects the domain only at that point. (Contributed by ML, 28-Mar-2021.)

⊢ (((𝐹 Fn 𝐴 ∧ ∀𝑝 ∈ 𝐴 ((𝐹‘𝑝) ∩ 𝐴) = {𝑝}) ∧ (𝑍 ⊆ ran 𝐹 ∧ 𝐴 ⊆ ∪ 𝑍)) → 𝑍 = ran 𝐹)

21.21.3.1  Pi-base theorems

This section contains a few proofs of theorems found in the pi-base database. The pi-base site can be found at https://topology.pi-base.org.

Definitions of topological properties are theorems labeled pibpN, where N is the property number in pi-base. For example, pibp19 38257 defines countably compact topologies. Proofs of theorems are similarly labeled pibtN, for example pibt2 38260.

Theorem

pibp16 38256*

Property P000016 of pi-base. The class of compact topologies. A space 𝑋 is compact if every open cover of 𝑋 has a finite subcover. This theorem is just a relabeled copy of iscmp 23668. (Contributed by ML, 8-Dec-2020.)

⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))

Theorem

pibp19 38257*

Property P000019 of pi-base. The class of countably compact topologies. A space 𝑋 is countably compact if every countable open cover of 𝑋 has a finite subcover. (Contributed by ML, 8-Dec-2020.)

⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐶 = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥((∪ 𝑥 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧)}    ⇒   ⊢ (𝐽 ∈ 𝐶 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))

Theorem

pibp21 38258*

Property P000021 of pi-base. The class of weakly countably compact topologies, or limit point compact topologies. A space 𝑋 is weakly countably compact if every infinite subset of 𝑋 has a limit point. (Contributed by ML, 9-Dec-2020.)

⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑊 = {𝑥 ∈ Top ∣ ∀𝑦 ∈ (𝒫 ∪ 𝑥 ∖ Fin)∃𝑧 ∈ ∪ 𝑥𝑧 ∈ ((limPt‘𝑥)‘𝑦)}    ⇒   ⊢ (𝐽 ∈ 𝑊 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧 ∈ 𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦)))

Theorem

pibt1 38259*

Theorem T000001 of pi-base. A compact topology is also countably compact. See pibp16 38256 and pibp19 38257 for the definitions of the relevant properties. (Contributed by ML, 8-Dec-2020.)

⊢ 𝐶 = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥((∪ 𝑥 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧)}    ⇒   ⊢ (𝐽 ∈ Comp → 𝐽 ∈ 𝐶)

Theorem

pibt2 38260*

Theorem T000002 of pi-base, a countably compact topology is also weakly countably compact. See pibp19 38257 and pibp21 38258 for the definitions of the relevant properties. This proof uses the axiom of choice. (Contributed by ML, 30-Mar-2021.)

⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐶 = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥((∪ 𝑥 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧)}    &   ⊢ 𝑊 = {𝑥 ∈ Top ∣ ∀𝑦 ∈ (𝒫 ∪ 𝑥 ∖ Fin)∃𝑧 ∈ ∪ 𝑥𝑧 ∈ ((limPt‘𝑥)‘𝑦)}    ⇒   ⊢ (𝐽 ∈ 𝐶 → 𝐽 ∈ 𝑊)

21.22  Mathbox for Wolf Lammen

Theorem

wl-section-prop 38261

Intuitionistic logic is now developed separately, so we need not first focus on intuitionally valid axioms ax-1 6 and ax-2 7 any longer.

Alternatively, I start from Jan Lukasiewicz's axiom system here, i.e., ax-mp 5, ax-luk1 38262, ax-luk2 38263 and ax-luk3 38264. I rather copy this system than use luk-1 1688 to luk-3 1690, since the latter are theorems, while we need axioms here.

(Contributed by Wolf Lammen, 23-Feb-2018.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ 𝜑    ⇒   ⊢ 𝜑

Axiom

ax-luk1 38262

1 of 3 axioms for propositional calculus due to Lukasiewicz. Copy of luk-1 1688 and imim1 84, but introduced as an axiom. It focuses on a basic property of a valid implication, namely that the consequent has to be true whenever the antecedent is. So if 𝜑 and 𝜓 are somehow parametrized expressions, then 𝜑 → 𝜓 states that 𝜑 strengthen 𝜓, in that 𝜑 holds only for a (often proper) subset of those parameters making 𝜓 true. We easily accept, that when 𝜓 is stronger than 𝜒 and, at the same time 𝜑 is stronger than 𝜓, then 𝜑 must be stronger than 𝜒. This transitivity is expressed in this axiom.

A particular result of this strengthening property comes into play if the antecedent holds unconditionally. Then the consequent must hold unconditionally as well. This specialization is the foundational idea behind logical conclusion. Such conclusion is best expressed in so-called immediate versions of this axiom like imim1i 64 or syl 18. Note that these forms are weaker replacements (i.e. just frequent specialization) of the closed form presented here, hence a mere convenience.

We can identify in this axiom up to three antecedents, followed by a consequent. The number of antecedents is not really fixed; the fewer we are willing to "see", the more complex the consequent grows. On the other side, since 𝜒 is a variable capable of assuming an implication itself, we might find even more antecedents after some substitution of 𝜒. This shows that the ideas of antecedent and consequent in expressions like this depends on, and can adapt to, our current interpretation of the whole expression.

In this axiom, up to two antecedents happen to be of complex nature themselves, i.e. are an embedded implication. Logically, this axiom is a compact notion of simpler expressions, which I will later coin implication chains. Herein all antecedents and the consequent appear as simple variables, or their negation. Any propositional expression is equivalent to a set of such chains. This axiom, for example, is dissected into following chains, from which it can be recovered losslessly:

(𝜓 → (𝜒 → (𝜑 → 𝜒))); (¬ 𝜑 → (𝜒 → (𝜑 → 𝜒))); (𝜓 → (¬ 𝜓 → (𝜑 → 𝜒))); (¬ 𝜑 → (¬ 𝜓 → (𝜑 → 𝜒))). (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.)

⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))

Axiom

ax-luk2 38263

2 of 3 axioms for propositional calculus due to Lukasiewicz. Copy of luk-2 1689 or pm2.18 129, but introduced as an axiom. The core idea behind this axiom is, that if something can be implied from both an antecedent, and separately from its negation, then the antecedent is irrelevant to the consequent, and can safely be dropped. This is perhaps better seen from the following slightly extended version (related to pm2.65 195):

((𝜑 → 𝜑) → ((¬ 𝜑 → 𝜑) → 𝜑)). (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.)

⊢ ((¬ 𝜑 → 𝜑) → 𝜑)

Axiom

ax-luk3 38264

3 of 3 axioms for propositional calculus due to Lukasiewicz. Copy of luk-3 1690 and pm2.24 125, but introduced as an axiom. One might think that the similar pm2.21 124 (¬ 𝜑 → (𝜑 → 𝜓)) is a valid replacement for this axiom. But this is not true, ax-3 8 is not derivable from this modification. This can be shown by designing carefully operators ¬ and → on a finite set of primitive statements. In propositional logic such statements are ⊤ and ⊥, but we can assume more and other primitives in our universe of statements. So we denote our primitive statements as phi0 , phi1 and phi2. The actual meaning of the statements are not important in this context, it rather counts how they behave under our operations ¬ and →, and which of them we assume to hold unconditionally (phi1, phi2). For our disproving model, I give that information in tabular form below. The interested reader may check by hand, that all possible interpretations of ax-mp 5, ax-luk1 38262, ax-luk2 38263 and pm2.21 124 result in phi1 or phi2, meaning they always hold. But for wl-luk-ax3 38276 we can find a counter example resulting in phi0, not a statement always true. The verification of a particular set of axioms in a given model is tedious and error prone, so I wrote a computer program, first checking this for me, and second, hunting for a counter example. Here is the result, after 9165 fruitlessly computer generated models:

ax-3 fails for phi2, phi2
number of statements: 3
always true phi1 phi2

Negation is defined as
----------------------------------------------------------------------

-. phi0	-. phi1	-. phi2
phi1	phi0	phi1

Implication is defined as
----------------------------------------------------------------------

p->q	q: phi0	q: phi1	q: phi2
p: phi0	phi1	phi1	phi1
p: phi1	phi0	phi1	phi1
p: phi2	phi0	phi0	phi0

(Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.)

⊢ (𝜑 → (¬ 𝜑 → 𝜓))

21.22.1  1. Bootstrapping

Theorem

wl-section-boot 38265

In this section, I provide the first steps needed for convenient proving. The presented theorems follow no common concept other than being useful in themselves, and apt to rederive ax-1 6, ax-2 7 and ax-3 8. (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ 𝜑    ⇒   ⊢ 𝜑

Theorem

wl-luk-imim1i 38266

Inference adding common consequents in an implication, thereby interchanging the original antecedent and consequent. Copy of imim1i 64 with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018.)

⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜓 → 𝜒) → (𝜑 → 𝜒))

Theorem

wl-luk-syl 38267

An inference version of the transitive laws for implication luk-1 1688. Copy of syl 18 with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)

Theorem

wl-luk-imtrid 38268

A syllogism rule of inference. The first premise is used to replace the second antecedent of the second premise. Copy of syl5 35 with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → (𝜓 → 𝜃))    ⇒   ⊢ (𝜒 → (𝜑 → 𝜃))

Theorem

wl-luk-pm2.18d 38269

Deduction based on reductio ad absurdum. Copy of pm2.18d 128 with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ (𝜑 → (¬ 𝜓 → 𝜓))    ⇒   ⊢ (𝜑 → 𝜓)

Theorem

wl-luk-con4i 38270

Inference rule. Copy of con4i 115 with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ (¬ 𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜓 → 𝜑)

Theorem

wl-luk-pm2.24i 38271

Inference rule. Copy of pm2.24i 151 with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ 𝜑    ⇒   ⊢ (¬ 𝜑 → 𝜓)

Theorem

wl-luk-a1i 38272

Inference rule. Copy of a1i 11 with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ 𝜑    ⇒   ⊢ (𝜓 → 𝜑)

Theorem

wl-luk-mpi 38273

A nested modus ponens inference. Copy of mpi 21 with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ 𝜓    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → 𝜒)

Theorem

wl-luk-imim2i 38274

Inference adding common antecedents in an implication. Copy of imim2i 17 with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜒 → 𝜑) → (𝜒 → 𝜓))

Theorem

wl-luk-imtrdi 38275

A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. Copy of syl6 36 with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜒 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → 𝜃))

Theorem

wl-luk-ax3 38276

ax-3 8 proved from Lukasiewicz's axioms. (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑))

Theorem

wl-luk-ax1 38277

ax-1 6 proved from Lukasiewicz's axioms. (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ (𝜑 → (𝜓 → 𝜑))

Theorem

wl-luk-pm2.27 38278

This theorem, called "Assertion", can be thought of as closed form of modus ponens ax-mp 5. Theorem *2.27 of [WhiteheadRussell] p. 104. Copy of pm2.27 43 with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))

Theorem

wl-luk-com12 38279

Inference that swaps (commutes) antecedents in an implication. Copy of com12 33 with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜓 → (𝜑 → 𝜒))

Theorem

wl-luk-pm2.21 38280

From a wff and its negation, anything follows. Theorem *2.21 of [WhiteheadRussell] p. 104. Also called the Duns Scotus law. Copy of pm2.21 124 with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ (¬ 𝜑 → (𝜑 → 𝜓))

Theorem

wl-luk-con1i 38281

A contraposition inference. Copy of con1i 148 with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ (¬ 𝜑 → 𝜓)    ⇒   ⊢ (¬ 𝜓 → 𝜑)

Theorem

wl-luk-ja 38282

Inference joining the antecedents of two premises. Copy of ja 188 with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ (¬ 𝜑 → 𝜒)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ ((𝜑 → 𝜓) → 𝜒)

Theorem

wl-luk-imim2 38283

A closed form of syllogism (see syl 18). Theorem *2.05 of [WhiteheadRussell] p. 100. Copy of imim2 59 with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ ((𝜑 → 𝜓) → ((𝜒 → 𝜑) → (𝜒 → 𝜓)))

Theorem

wl-luk-a1d 38284

Deduction introducing an embedded antecedent. Copy of imim2 59 with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (𝜒 → 𝜓))

Theorem

wl-luk-ax2 38285

ax-2 7 proved from Lukasiewicz's axioms. (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))

Theorem

wl-luk-id 38286

Principle of identity. Theorem *2.08 of [WhiteheadRussell] p. 101. Copy of id 23 with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ (𝜑 → 𝜑)

Theorem

wl-luk-notnotr 38287

Converse of double negation. Theorem *2.14 of [WhiteheadRussell] p. 102. In classical logic (our logic) this is always true. In intuitionistic logic this is not always true; in intuitionistic logic, when this is true for some 𝜑, then 𝜑 is stable. Copy of notnotr 131 with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ (¬ ¬ 𝜑 → 𝜑)

Theorem

wl-luk-pm2.04 38288

Swap antecedents. Theorem *2.04 of [WhiteheadRussell] p. 100. This was the third axiom in Frege's logic system, specifically Proposition 8 of [Frege1879] p. 35. Copy of pm2.04 91 with a different proof. (Contributed by Wolf Lammen, 7-Jul-2019.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒)))

21.22.2  Implication chains

Theorem

wl-section-impchain 38289

An implication like (𝜓 → 𝜑) with one antecedent can easily be extended by prepending more and more antecedents, as in (𝜒 → (𝜓 → 𝜑)) or (𝜃 → (𝜒 → (𝜓 → 𝜑))). I call these expressions implication chains, and the number of antecedents (number of nodes minus one) denotes their length. A given length often marks just a required minimum value, since the consequent 𝜑 itself may represent an implication, or even an implication chain, such hiding part of the whole chain. As an extension, it is useful to consider a single variable 𝜑 as a degenerate implication chain of length zero.

Implication chains play a particular role in logic, as all propositional expressions turn out to be convertible to one or more implication chains, their nodes as simple as a variable, or its negation.

So there is good reason to focus on implication chains as a sort of normalized expressions, and build some general theorems around them, with proofs using recursive patterns. This allows for theorems referring to longer and longer implication chains in an automated way.

The theorem names in this section contain the text fragment 'impchain' to point out their relevance to implication chains, followed by a number indicating the (minimal) length of the longest chain involved. (Contributed by Wolf Lammen, 6-Jul-2019.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ 𝜑    ⇒   ⊢ 𝜑

Theorem

wl-impchain-mp-x 38290

This series of theorems provide a means of exchanging the consequent of an implication chain via a simple implication. In the main part, Theorems ax-mp 5, syl 18, syl6 36, syl8 77 form the beginning of this series. These theorems are replicated here, but with proofs that aim at a recursive scheme, allowing to base a proof on that of the previous one in the series. (Contributed by Wolf Lammen, 17-Nov-2019.)

⊢ ⊤

Theorem

wl-impchain-mp-0 38291

This theorem is the start of a proof recursion scheme where we replace the consequent of an implication chain. The number '0' in the theorem name indicates that the modified chain has no antecedents.

This theorem is in fact a copy of ax-mp 5, and is repeated here to emphasize the recursion using similar theorem names. (Contributed by Wolf Lammen, 6-Jul-2019.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ 𝜓    &   ⊢ (𝜓 → 𝜑)    ⇒   ⊢ 𝜑

Theorem

wl-impchain-mp-1 38292

This theorem is in fact a copy of wl-luk-syl 38267, and repeated here to demonstrate a recursive proof scheme. The number '1' in the theorem name indicates that a chain of length 1 is modified. (Contributed by Wolf Lammen, 6-Jul-2019.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ (𝜒 → 𝜓)    &   ⊢ (𝜓 → 𝜑)    ⇒   ⊢ (𝜒 → 𝜑)

Theorem

wl-impchain-mp-2 38293

This theorem is in fact a copy of wl-luk-imtrdi 38275, and repeated here to demonstrate a recursive proof scheme. The number '2' in the theorem name indicates that a chain of length 2 is modified. (Contributed by Wolf Lammen, 6-Jul-2019.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ (𝜃 → (𝜒 → 𝜓))    &   ⊢ (𝜓 → 𝜑)    ⇒   ⊢ (𝜃 → (𝜒 → 𝜑))

Theorem

wl-impchain-com-1.x 38294

It is often convenient to have the antecedent under focus in first position, so we can apply immediate theorem forms (as opposed to deduction, tautology form). This series of theorems swaps the first with the last antecedent in an implication chain. This kind of swapping is self-inverse, whence we prefer it over, say, rotating theorems. A consequent can hide a tail of a longer chain, so theorems of this series appear as swapping a pair of antecedents with fixed offsets. This form of swapping antecedents is flexible enough to allow for any permutation of antecedents in an implication chain.

The first elements of this series correspond to com12 33, com13 89, com14 97 and com15 102 in the main part.

The proofs of this series aim at automated proving using a simple recursive scheme. It employs the previous theorem in the series along with a sample from the wl-impchain-mp-x 38290 series developed before. (Contributed by Wolf Lammen, 17-Nov-2019.)

⊢ ⊤

Theorem

wl-impchain-com-1.1 38295

A degenerate form of antecedent swapping. The number '1' in the theorem name indicates that it handles a chain of length 1.

Since there is just one antecedent in the chain, there is nothing to swap. Nondegenerated forms begin with wl-impchain-com-1.2 38296, for more see there. (Contributed by Wolf Lammen, 7-Jul-2019.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ (𝜓 → 𝜑)    ⇒   ⊢ (𝜓 → 𝜑)

Theorem

wl-impchain-com-1.2 38296

This theorem is in fact a copy of wl-luk-com12 38279, and repeated here to demonstrate a simple proof scheme. The number '2' in the theorem name indicates that a chain of length 2 is modified.

See wl-impchain-com-1.x 38294 for more information how this proof is generated. (Contributed by Wolf Lammen, 7-Jul-2019.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ (𝜒 → (𝜓 → 𝜑))    ⇒   ⊢ (𝜓 → (𝜒 → 𝜑))

Theorem

wl-impchain-com-1.3 38297

This theorem is in fact a copy of com13 89, and repeated here to demonstrate a simple proof scheme. The number '3' in the theorem name indicates that a chain of length 3 is modified.

See wl-impchain-com-1.x 38294 for more information how this proof is generated. (Contributed by Wolf Lammen, 7-Jul-2019.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ (𝜃 → (𝜒 → (𝜓 → 𝜑)))    ⇒   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜑)))

Theorem

wl-impchain-com-1.4 38298

This theorem is in fact a copy of com14 97, and repeated here to demonstrate a simple proof scheme. The number '4' in the theorem name indicates that a chain of length 4 is modified.

See wl-impchain-com-1.x 38294 for more information how this proof is generated. (Contributed by Wolf Lammen, 7-Jul-2019.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ (𝜂 → (𝜃 → (𝜒 → (𝜓 → 𝜑))))    ⇒   ⊢ (𝜓 → (𝜃 → (𝜒 → (𝜂 → 𝜑))))

Theorem

wl-impchain-com-n.m 38299

This series of theorems allow swapping any two antecedents in an implication chain. The theorem names follow a pattern wl-impchain-com-n.m with integral numbers n < m, that swaps the m-th antecedent with n-th one in an implication chain. It is sufficient to restrict the length of the chain to m, too, since the consequent can be assumed to be the tail right of the m-th antecedent of any arbitrary sized implication chain. We further assume n > 1, since the wl-impchain-com-1.x 38294 series already covers the special case n = 1.

Being able to swap any two antecedents in an implication chain lays the foundation of permuting its antecedents arbitrarily.

The proofs of this series aim at automated proofing using a simple scheme. Any instance of this series is a triple step of swapping the first and n-th antecedent, then the first and the m-th, then the first and the n-th antecedent again. Each of these steps is an instance of the wl-impchain-com-1.x 38294 series. (Contributed by Wolf Lammen, 17-Nov-2019.)

⊢ ⊤

Theorem

wl-impchain-com-2.3 38300

This theorem is in fact a copy of com23 87. It starts a series of theorems named after wl-impchain-com-n.m 38299. For more information see there. (Contributed by Wolf Lammen, 12-Nov-2019.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ (𝜃 → (𝜒 → (𝜓 → 𝜑)))    ⇒   ⊢ (𝜃 → (𝜓 → (𝜒 → 𝜑)))