P. 382 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Theorem

mptsnun 38101*

A class 𝐵 is equal to the union of the class of all singletons of elements of 𝐵. (Contributed by ML, 16-Jul-2020.)

⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ {𝑥})    &   ⊢ 𝑅 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}}    ⇒   ⊢ (𝐵 ⊆ 𝐴 → 𝐵 = ∪ (𝐹 “ 𝐵))

Theorem

dissneqlem 38102*

This is the core of the proof of dissneq 38103, but to avoid the distinct variables on the definitions, we split this proof into two. (Contributed by ML, 16-Jul-2020.)

⊢ 𝐶 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}}    ⇒   ⊢ ((𝐶 ⊆ 𝐵 ∧ 𝐵 ∈ (TopOn‘𝐴)) → 𝐵 = 𝒫 𝐴)

Theorem

dissneq 38103*

Any topology that contains every single-point set is the discrete topology. (Contributed by ML, 16-Jul-2020.)

⊢ 𝐶 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}}    ⇒   ⊢ ((𝐶 ⊆ 𝐵 ∧ 𝐵 ∈ (TopOn‘𝐴)) → 𝐵 = 𝒫 𝐴)

Theorem

exlimim 38104*

Closed form of exlimimd 38105. (Contributed by ML, 17-Jul-2020.)

⊢ ((∃𝑥𝜑 ∧ ∀𝑥(𝜑 → 𝜓)) → 𝜓)

Theorem

exlimimd 38105*

Existential elimination rule of natural deduction. (Contributed by ML, 17-Jul-2020.)

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

Theorem

exellim 38106*

Closed form of exellimddv 38107. See also exlimim 38104 for a more general theorem. (Contributed by ML, 17-Jul-2020.)

⊢ ((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) → 𝜑)

Theorem

exellimddv 38107*

Eliminate an antecedent when the antecedent is elementhood, deduction version. See exellim 38106 for the closed form, which requires the use of a universal quantifier. (Contributed by ML, 17-Jul-2020.)

⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))    ⇒   ⊢ (𝜑 → 𝜓)

Theorem

topdifinfindis 38108*

Part of Exercise 3 of [Munkres] p. 83. The topology of all subsets 𝑥 of 𝐴 such that the complement of 𝑥 in 𝐴 is infinite, or 𝑥 is the empty set, or 𝑥 is all of 𝐴, is the trivial topology when 𝐴 is finite. (Contributed by ML, 14-Jul-2020.)

⊢ 𝑇 = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))}    ⇒   ⊢ (𝐴 ∈ Fin → 𝑇 = {∅, 𝐴})

Theorem

topdifinffinlem 38109*

This is the core of the proof of topdifinffin 38110, but to avoid the distinct variables on the definition, we need to split this proof into two. (Contributed by ML, 17-Jul-2020.)

⊢ 𝑇 = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))}    ⇒   ⊢ (𝑇 ∈ (TopOn‘𝐴) → 𝐴 ∈ Fin)

Theorem

topdifinffin 38110*

Part of Exercise 3 of [Munkres] p. 83. The topology of all subsets 𝑥 of 𝐴 such that the complement of 𝑥 in 𝐴 is infinite, or 𝑥 is the empty set, or 𝑥 is all of 𝐴, is a topology only if 𝐴 is finite. (Contributed by ML, 17-Jul-2020.)

⊢ 𝑇 = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))}    ⇒   ⊢ (𝑇 ∈ (TopOn‘𝐴) → 𝐴 ∈ Fin)

Theorem

topdifinf 38111*

Part of Exercise 3 of [Munkres] p. 83. The topology of all subsets 𝑥 of 𝐴 such that the complement of 𝑥 in 𝐴 is infinite, or 𝑥 is the empty set, or 𝑥 is all of 𝐴, is a topology if and only if 𝐴 is finite, in which case it is the trivial topology. (Contributed by ML, 17-Jul-2020.)

⊢ 𝑇 = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))}    ⇒   ⊢ ((𝑇 ∈ (TopOn‘𝐴) ↔ 𝐴 ∈ Fin) ∧ (𝑇 ∈ (TopOn‘𝐴) → 𝑇 = {∅, 𝐴}))

Theorem

topdifinfeq 38112*

Two different ways of defining the collection from Exercise 3 of [Munkres] p. 83. (Contributed by ML, 18-Jul-2020.)

⊢ {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ ((𝐴 ∖ 𝑥) = ∅ ∨ (𝐴 ∖ 𝑥) = 𝐴))} = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))}

Theorem

icorempo 38113*

Closed-below, open-above intervals of reals. (Contributed by ML, 26-Jul-2020.)

⊢ 𝐹 = ([,) ↾ (ℝ × ℝ))    ⇒   ⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {𝑧 ∈ ℝ ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})

Theorem

icoreresf 38114

Closed-below, open-above intervals of reals map to subsets of reals. (Contributed by ML, 25-Jul-2020.)

⊢ ([,) ↾ (ℝ × ℝ)):(ℝ × ℝ)⟶𝒫 ℝ

Theorem

icoreval 38115*

Value of the closed-below, open-above interval function on reals. (Contributed by ML, 26-Jul-2020.)

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

Theorem

icoreelrnab 38116*

Elementhood in the set of closed-below, open-above intervals of reals. (Contributed by ML, 27-Jul-2020.)

⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ (𝑋 ∈ 𝐼 ↔ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 𝑋 = {𝑧 ∈ ℝ ∣ (𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏)})

Theorem

isbasisrelowllem1 38117*

Lemma for isbasisrelowl 38120. (Contributed by ML, 27-Jul-2020.)

⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = {𝑧 ∈ ℝ ∣ (𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏)}) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = {𝑧 ∈ ℝ ∣ (𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑)})) ∧ (𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑)) → (𝑥 ∩ 𝑦) ∈ 𝐼)

Theorem

isbasisrelowllem2 38118*

Lemma for isbasisrelowl 38120. (Contributed by ML, 27-Jul-2020.)

⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = {𝑧 ∈ ℝ ∣ (𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏)}) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = {𝑧 ∈ ℝ ∣ (𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑)})) ∧ (𝑎 ≤ 𝑐 ∧ 𝑑 ≤ 𝑏)) → (𝑥 ∩ 𝑦) ∈ 𝐼)

Theorem

icoreclin 38119*

The set of closed-below, open-above intervals of reals is closed under finite intersection. (Contributed by ML, 27-Jul-2020.)

⊢ 𝐼 = ([,) “ (ℝ × ℝ))    ⇒   ⊢ ((𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼) → (𝑥 ∩ 𝑦) ∈ 𝐼)

Theorem

isbasisrelowl 38120

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

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

Theorem

icoreunrn 38121

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

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

Theorem

istoprelowl 38122

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 38123*

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 38124*

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

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

Theorem

relowlssretop 38125

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

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

Theorem

relowlpssretop 38126

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 38127

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 38128

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 38129

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 38130

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 38131

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 38132

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 38133

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

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

Theorem

cbveud 38134*

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

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

Theorem

cbvreud 38135*

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

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

Theorem

difunieq 38136

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

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

Theorem

inunissunidif 38137

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

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

Theorem

rdgellim 38138

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

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

Theorem

rdglimss 38139

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 38140*

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 38141*

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

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

Theorem

exrecfn 38142*

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

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

Theorem

exrecfnpw 38143*

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 38144

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 38145

Extend the definition of a class to include Cartesian exponentiation.

class (𝑈↑↑𝑁)

Definition

df-finxp 38146*

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 8909 or df-map 8832 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 5108 can be used on it, and df-fv 6545 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 38154 and finxpsuc 38160 for a more standard recursive experience. (Contributed by ML, 16-Oct-2020.)

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

Theorem

dffinxpf 38147*

This theorem is the same as Definition df-finxp 38146, 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 38148

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

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

Theorem

finxpeq2 38149

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

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

Theorem

csbfinxpg 38150*

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

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

Theorem

finxpreclem1 38151*

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

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

Theorem

finxpreclem2 38152*

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

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

Theorem

finxp0 38153

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

⊢ (𝑈↑↑∅) = ∅

Theorem

finxp1o 38154

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

⊢ (𝑈↑↑1_o) = 𝑈

Theorem

finxpreclem3 38155*

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 38156*

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 38157*

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

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

Theorem

finxpreclem6 38158*

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

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

Theorem

finxpsuclem 38159*

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

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

Theorem

finxpsuc 38160

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

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

Theorem

finxp2o 38161

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

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

Theorem

finxp3o 38162

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

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

Theorem

finxpnom 38163

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

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

Theorem

finxp00 38164

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 38165

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

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

Theorem

domalom 38166*

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

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

Theorem

isinf2 38167*

The converse of isinf 9239. 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 38168*

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

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

Theorem

ralssiun 38169*

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 38170*

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 38171*

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 38172*

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 38171 for a proof of this fact. (Contributed by ML, 23-Mar-2021.)

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

Theorem

fvineqsneu 38173*

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 38174*

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 38176 defines countably compact topologies. Proofs of theorems are similarly labeled pibtN, for example pibt2 38179.

Theorem

pibp16 38175*

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 23619. (Contributed by ML, 8-Dec-2020.)

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

Theorem

pibp19 38176*

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 38177*

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 38178*

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

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

Theorem

pibt2 38179*

Theorem T000002 of pi-base, a countably compact topology is also weakly countably compact. See pibp19 38176 and pibp21 38177 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 38180

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 38181, ax-luk2 38182 and ax-luk3 38183. 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 38181

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 38182

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 38183

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 38181, ax-luk2 38182 and pm2.21 124 result in phi1 or phi2, meaning they always hold. But for wl-luk-ax3 38195 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 38184

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 38185

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 38186

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 38187

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 38188

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 38189

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 38190

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 38191

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 38192

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 38193

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 38194

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 38195

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 38196

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 38197

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 38198

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 38199

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 38200

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.)

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