P. 374 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Theorem

f1omptsn 37301*

A function mapping to singletons is bijective onto a set of singletons. (Contributed by ML, 16-Jul-2020.)

⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ {𝑥})    &   ⊢ 𝑅 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}}    ⇒   ⊢ 𝐹:𝐴–1-1-onto→𝑅

Theorem

mptsnunlem 37302*

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

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

Theorem

mptsnun 37303*

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

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

Theorem

dissneqlem 37304*

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

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

Theorem

dissneq 37305*

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

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

Theorem

exlimim 37306*

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

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

Theorem

exlimimd 37307*

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

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

Theorem

exellim 37308*

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

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

Theorem

exellimddv 37309*

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

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

Theorem

topdifinfindis 37310*

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

This is the core of the proof of topdifinffin 37312, 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 37312*

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

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

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

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

Theorem

icorempo 37315*

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

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

Theorem

icoreresf 37316

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

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

Theorem

icoreval 37317*

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

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

Theorem

icoreelrnab 37318*

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

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

Theorem

isbasisrelowllem1 37319*

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

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

Theorem

isbasisrelowllem2 37320*

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

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

Theorem

icoreclin 37321*

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

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

Theorem

isbasisrelowl 37322

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

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

Theorem

icoreunrn 37323

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

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

Theorem

istoprelowl 37324

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

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

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

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

Theorem

relowlssretop 37327

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

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

Theorem

relowlpssretop 37328

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 37329

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 37330

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 37331

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 37332

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 37333

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 37334

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 37335

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

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

Theorem

cbveud 37336*

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

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

Theorem

cbvreud 37337*

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

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

Theorem

difunieq 37338

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

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

Theorem

inunissunidif 37339

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

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

Theorem

rdgellim 37340

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

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

Theorem

rdglimss 37341

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

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

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

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

Theorem

exrecfn 37344*

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

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

Theorem

exrecfnpw 37345*

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 37346

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 37347

Extend the definition of a class to include Cartesian exponentiation.

class (𝑈↑↑𝑁)

Definition

df-finxp 37348*

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 8910 or df-map 8840 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 5120 can be used on it, and df-fv 6538 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 37356 and finxpsuc 37362 for a more standard recursive experience. (Contributed by ML, 16-Oct-2020.)

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

Theorem

dffinxpf 37349*

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

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

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

Theorem

finxpeq2 37351

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

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

Theorem

csbfinxpg 37352*

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

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

Theorem

finxpreclem1 37353*

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

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

Theorem

finxpreclem2 37354*

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

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

Theorem

finxp0 37355

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

⊢ (𝑈↑↑∅) = ∅

Theorem

finxp1o 37356

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

⊢ (𝑈↑↑1_o) = 𝑈

Theorem

finxpreclem3 37357*

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

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

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

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

Theorem

finxpreclem6 37360*

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

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

Theorem

finxpsuclem 37361*

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

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

Theorem

finxpsuc 37362

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

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

Theorem

finxp2o 37363

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

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

Theorem

finxp3o 37364

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

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

Theorem

finxpnom 37365

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

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

Theorem

finxp00 37366

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 37367

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

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

Theorem

domalom 37368*

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

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

Theorem

isinf2 37369*

The converse of isinf 9266. 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 37370*

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

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

Theorem

ralssiun 37371*

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

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

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

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

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

Theorem

fvineqsneu 37375*

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

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

Theorem

pibp16 37377*

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

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

Theorem

pibp19 37378*

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

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

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

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

Theorem

pibt2 37381*

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

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 37383, ax-luk2 37384 and ax-luk3 37385. I rather copy this system than use luk-1 1655 to luk-3 1657, 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 37383

1 of 3 axioms for propositional calculus due to Lukasiewicz. Copy of luk-1 1655 and imim1 83, 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 63 or syl 17. 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 37384

2 of 3 axioms for propositional calculus due to Lukasiewicz. Copy of luk-2 1656 or pm2.18 128, 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 193):

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

⊢ ((¬ 𝜑 → 𝜑) → 𝜑)

Axiom

ax-luk3 37385

3 of 3 axioms for propositional calculus due to Lukasiewicz. Copy of luk-3 1657 and pm2.24 124, but introduced as an axiom. One might think that the similar pm2.21 123 (¬ 𝜑 → (𝜑 → 𝜓)) 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 37383, ax-luk2 37384 and pm2.21 123 result in phi1 or phi2, meaning they always hold. But for wl-luk-ax3 37397 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 37386

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 37387

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

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

Theorem

wl-luk-syl 37388

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

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

Theorem

wl-luk-imtrid 37389

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

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

Theorem

wl-luk-pm2.18d 37390

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

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

Theorem

wl-luk-con4i 37391

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

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

Theorem

wl-luk-pm2.24i 37392

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

⊢ 𝜑    ⇒   ⊢ (¬ 𝜑 → 𝜓)

Theorem

wl-luk-a1i 37393

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 37394

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

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

Theorem

wl-luk-imim2i 37395

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

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

Theorem

wl-luk-imtrdi 37396

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

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

Theorem

wl-luk-ax3 37397

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 37398

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 37399

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 42 with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.) (Proof modification is discouraged.)

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

Theorem

wl-luk-com12 37400

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

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