P. 359 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Theorem

csboprabg 35801*

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

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

Theorem

csbmpo123 35802*

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

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

Theorem

con1bii2 35803

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

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

Theorem

con2bii2 35804

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

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

Theorem

vtoclefex 35805*

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

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

Theorem

rnmptsn 35806*

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

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

Theorem

f1omptsnlem 35807*

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

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

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

Theorem

mptsnunlem 35809*

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

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

Theorem

mptsnun 35810*

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

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

Theorem

dissneqlem 35811*

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

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

Theorem

dissneq 35812*

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

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

Theorem

exlimim 35813*

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

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

Theorem

exlimimd 35814*

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

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

Theorem

exellim 35815*

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

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

Theorem

exellimddv 35816*

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

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

Theorem

topdifinfindis 35817*

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

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

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

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

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

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

Theorem

icorempo 35822*

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

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

Theorem

icoreresf 35823

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

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

Theorem

icoreval 35824*

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

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

Theorem

icoreelrnab 35825*

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

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

Theorem

isbasisrelowllem1 35826*

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

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

Theorem

isbasisrelowllem2 35827*

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

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

Theorem

icoreclin 35828*

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

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

Theorem

isbasisrelowl 35829

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

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

Theorem

icoreunrn 35830

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

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

Theorem

istoprelowl 35831

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

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

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

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

Theorem

relowlssretop 35834

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

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

Theorem

relowlpssretop 35835

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 35836

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 35837

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 35838

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 35839

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 35840

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 35841

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 35842

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

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

Theorem

cbveud 35843*

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

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

Theorem

cbvreud 35844*

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

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

Theorem

difunieq 35845

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

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

Theorem

inunissunidif 35846

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

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

Theorem

rdgellim 35847

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

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

Theorem

rdglimss 35848

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

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

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

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

Theorem

exrecfn 35851*

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

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

Theorem

exrecfnpw 35852*

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 35853

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.17.2  Cartesian exponentiation

Syntax

cfinxp 35854

Extend the definition of a class to include Cartesian exponentiation.

class (𝑈↑↑𝑁)

Definition

df-finxp 35855*

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 8836 or df-map 8767 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 5106 can be used on it, and df-fv 6504 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 35863 and finxpsuc 35869 for a more standard recursive experience. (Contributed by ML, 16-Oct-2020.)

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

Theorem

dffinxpf 35856*

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

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

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

Theorem

finxpeq2 35858

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

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

Theorem

csbfinxpg 35859*

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

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

Theorem

finxpreclem1 35860*

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

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

Theorem

finxpreclem2 35861*

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

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

Theorem

finxp0 35862

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

⊢ (𝑈↑↑∅) = ∅

Theorem

finxp1o 35863

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

⊢ (𝑈↑↑1_o) = 𝑈

Theorem

finxpreclem3 35864*

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

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

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

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

Theorem

finxpreclem6 35867*

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

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

Theorem

finxpsuclem 35868*

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

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

Theorem

finxpsuc 35869

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

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

Theorem

finxp2o 35870

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

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

Theorem

finxp3o 35871

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

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

Theorem

finxpnom 35872

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

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

Theorem

finxp00 35873

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

⊢ (∅↑↑𝑁) = ∅

21.17.3  Topology

Theorem

iunctb2 35874

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

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

Theorem

domalom 35875*

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

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

Theorem

isinf2 35876*

The converse of isinf 9204. 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 35877*

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

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

Theorem

ralssiun 35878*

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

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

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

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

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

Theorem

fvineqsneu 35882*

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

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

Theorem

pibp16 35884*

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

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

Theorem

pibp19 35885*

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

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

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

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

Theorem

pibt2 35888*

Theorem T000002 of pi-base, a countably compact topology is also weakly countably compact. See pibp19 35885 and pibp21 35886 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.18  Mathbox for Wolf Lammen

Theorem

wl-section-prop 35889

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 35890, ax-luk2 35891 and ax-luk3 35892. I rather copy this system than use luk-1 1657 to luk-3 1659, 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 35890

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

2 of 3 axioms for propositional calculus due to Lukasiewicz. Copy of luk-2 1658 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 192):

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

⊢ ((¬ 𝜑 → 𝜑) → 𝜑)

Axiom

ax-luk3 35892

3 of 3 axioms for propositional calculus due to Lukasiewicz. Copy of luk-3 1659 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 35890, ax-luk2 35891 and pm2.21 123 result in phi1 or phi2, meaning they always hold. But for wl-luk-ax3 35904 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.18.1  1. Bootstrapping

Theorem

wl-section-boot 35893

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 35894

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 35895

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

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 35897

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 35898

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 35899

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 35900

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

⊢ 𝜑    ⇒   ⊢ (𝜓 → 𝜑)