P. 334 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

20.16  Mathbox for ML

Theorem

csbdif 33301

Distribution of class substitution over difference of two classes. (Contributed by ML, 14-Jul-2020.)

⊢ ⦋𝐴 / 𝑥⦌(𝐵 ∖ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∖ ⦋𝐴 / 𝑥⦌𝐶)

Theorem

csbpredg 33302

Move class substitution in and out of the predecessor class of a relationship. (Contributed by ML, 25-Oct-2020.)

⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌Pred(𝑅, 𝐷, 𝑋) = Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, ⦋𝐴 / 𝑥⦌𝑋))

Theorem

csbwrecsg 33303

Move class substitution in and out of the well-founded recursive function generator . (Contributed by ML, 25-Oct-2020.)

⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌wrecs(𝑅, 𝐷, 𝐹) = wrecs(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, ⦋𝐴 / 𝑥⦌𝐹))

Theorem

csbrecsg 33304

Move class substitution in and out of recs. (Contributed by ML, 25-Oct-2020.)

⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌recs(𝐹) = recs(⦋𝐴 / 𝑥⦌𝐹))

Theorem

csbrdgg 33305

Move class substitution in and out of the recursive function generator. (Contributed by ML, 25-Oct-2020.)

⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌rec(𝐹, 𝐼) = rec(⦋𝐴 / 𝑥⦌𝐹, ⦋𝐴 / 𝑥⦌𝐼))

Theorem

csboprabg 33306*

Move class substitution in and out of class abstractions of nested ordered pairs. (Contributed by ML, 25-Oct-2020.)

⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∣ 𝜑} = {⟨⟨𝑦, 𝑧⟩, 𝑑⟩ ∣ [𝐴 / 𝑥]𝜑})

Theorem

csbmpt22g 33307*

Move class substitution in and out of maps-to notation for operations. (Contributed by ML, 25-Oct-2020.)

⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝑦 ∈ 𝑌, 𝑧 ∈ 𝑍 ↦ 𝐷) = (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝑌, 𝑧 ∈ ⦋𝐴 / 𝑥⦌𝑍 ↦ ⦋𝐴 / 𝑥⦌𝐷))

Theorem

mpnanrd 33308

Eliminate the right side of a negated conjunction in an implication. (Contributed by ML, 17-Oct-2020.)

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

Theorem

con1bii2 33309

A contraposition inference. (Contributed by ML, 18-Oct-2020.)

⊢ (¬ 𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜑 ↔ ¬ 𝜓)

Theorem

con2bii2 33310

A contraposition inference. (Contributed by ML, 18-Oct-2020.)

⊢ (𝜑 ↔ ¬ 𝜓)    ⇒   ⊢ (¬ 𝜑 ↔ 𝜓)

Theorem

vtoclefex 33311*

Implicit substitution of a class for a setvar variable. (Contributed by ML, 17-Oct-2020.)

⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑥 = 𝐴 → 𝜑)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜑)

Theorem

rnmptsn 33312*

The range of a function mapping to singletons. (Contributed by ML, 15-Jul-2020.)

⊢ ran (𝑥 ∈ 𝐴 ↦ {𝑥}) = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}}

Theorem

f1omptsnlem 33313*

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

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

Theorem

f1omptsn 33314*

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

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

Theorem

mptsnunlem 33315*

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

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

Theorem

mptsnun 33316*

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

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

Theorem

dissneqlem 33317*

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

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

Theorem

dissneq 33318*

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

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

Theorem

exlimim 33319*

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

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

Theorem

exlimimd 33320*

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

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

Theorem

exlimimdd 33321

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

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

Theorem

exellim 33322*

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

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

Theorem

exellimddv 33323*

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

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

Theorem

topdifinfindis 33324*

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

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

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

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

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

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

Theorem

icorempt2 33329*

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

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

Theorem

icoreresf 33330

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

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

Theorem

icoreval 33331*

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

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

Theorem

icoreelrnab 33332*

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

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

Theorem

isbasisrelowllem1 33333*

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

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

Theorem

isbasisrelowllem2 33334*

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

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

Theorem

icoreclin 33335*

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

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

Theorem

isbasisrelowl 33336

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

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

Theorem

icoreunrn 33337

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

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

Theorem

istoprelowl 33338

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

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

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

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

Theorem

relowlssretop 33341

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

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

Theorem

relowlpssretop 33342

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 33343

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 33344

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 33345

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 33346

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

⊢ 1_𝑜 = ∪ 2_𝑜

Theorem

rdgsucuni 33347

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 33348

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(𝐹, 𝐴)‘(𝑁 +_𝑜 𝑋)) = (rec(𝐹, 𝐵)‘(𝑀 +_𝑜 𝑋))))

Theorem

elxp8 33349

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

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

Syntax

cfinxp 33350

Extend the definition of a class to include Cartesian exponentiation.

class (𝑈↑↑𝑁)

Definition

df-finxp 33351*

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 7951 or df-map 7901 instead. The main advantage of this definition is that it integrates better with functions and relations. For example if 𝑅 is a subset of (𝐴↑↑2_𝑜), then df-br 4686 can be used on it, and df-fv 5934 can also be used, and so on.

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

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

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

Theorem

dffinxpf 33352*

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

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

Theorem

finxpeq1 33353

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

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

Theorem

finxpeq2 33354

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

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

Theorem

csbfinxpg 33355*

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

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

Theorem

finxpreclem1 33356*

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

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

Theorem

finxpreclem2 33357*

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

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

Theorem

finxp0 33358

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

⊢ (𝑈↑↑∅) = ∅

Theorem

finxp1o 33359

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

⊢ (𝑈↑↑1_𝑜) = 𝑈

Theorem

finxpreclem3 33360*

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

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

Theorem

finxpreclem4 33361*

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

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

Theorem

finxpreclem5 33362*

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

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

Theorem

finxpreclem6 33363*

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

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

Theorem

finxpsuclem 33364*

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

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

Theorem

finxpsuc 33365

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

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

Theorem

finxp2o 33366

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

⊢ (𝑈↑↑2_𝑜) = (𝑈 × 𝑈)

Theorem

finxp3o 33367

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

⊢ (𝑈↑↑3_𝑜) = ((𝑈 × 𝑈) × 𝑈)

Theorem

finxpnom 33368

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

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

Theorem

finxp00 33369

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

⊢ (∅↑↑𝑁) = ∅

20.17  Mathbox for Wolf Lammen

Theorem

wl-section-prop 33370

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 33371, ax-luk2 33372 and ax-luk3 33373. I rather copy this system than use luk-1 1620 to luk-3 1622, 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 33371

1 of 3 axioms for propositional calculus due to Lukasiewicz. Copy of luk-1 1620 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 33372

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

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

⊢ ((¬ 𝜑 → 𝜑) → 𝜑)

Axiom

ax-luk3 33373

3 of 3 axioms for propositional calculus due to Lukasiewicz. Copy of luk-3 1622 and pm2.24 121, but introduced as an axiom. One might think that the similar pm2.21 120 (¬ 𝜑 → (𝜑 → 𝜓)) 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 per hand, that all possible interpretations of ax-mp 5, ax-luk1 33371, ax-luk2 33372 and pm2.21 120 result in phi1 or phi2, meaning they always hold. But for wl-ax3 33385 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.)

⊢ (𝜑 → (¬ 𝜑 → 𝜓))

20.17.1  1. Bootstrapping

Theorem

wl-section-boot 33374

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-imim1i 33375

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-syl 33376

An inference version of the transitive laws for implication luk-1 1620. 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-syl5 33377

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-pm2.18d 33378

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

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

Theorem

wl-con4i 33379

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

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

Theorem

wl-pm2.24i 33380

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

⊢ 𝜑    ⇒   ⊢ (¬ 𝜑 → 𝜓)

Theorem

wl-a1i 33381

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-mpi 33382

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-imim2i 33383

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-syl6 33384

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-ax3 33385

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-ax1 33386

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-pm2.27 33387

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-com12 33388

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

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

Theorem

wl-pm2.21 33389

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

⊢ (¬ 𝜑 → (𝜑 → 𝜓))

Theorem

wl-con1i 33390

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

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

Theorem

wl-ja 33391

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

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

Theorem

wl-imim2 33392

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

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

Theorem

wl-a1d 33393

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

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

Theorem

wl-ax2 33394

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-id 33395

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

⊢ (𝜑 → 𝜑)

Theorem

wl-notnotr 33396

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

⊢ (¬ ¬ 𝜑 → 𝜑)

Theorem

wl-pm2.04 33397

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 90 with a different proof. (Contributed by Wolf Lammen, 7-Jul-2019.) (New usage is discouraged.) (Proof modification is discouraged.)

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

20.17.2  Implication chains

Theorem

wl-section-impchain 33398

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 33399

This series of theorems provide a means of exchanging the consequent of an implication chain via a simple implication. In the main part, the theorems ax-mp 5, syl 17, syl6 35, syl8 76 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 33400

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

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