P. 92 of Theorem List - Intuitionistic Logic Explorer

Type

Label

Description

Statement

Theorem

cjcli 9101

Closure law for complex conjugate. (Contributed by NM, 11-May-1999.)

⊢ A ∈ ℂ    ⇒   ⊢ (∗‘A) ∈ ℂ

Theorem

replimi 9102

Construct a complex number from its real and imaginary parts. (Contributed by NM, 1-Oct-1999.)

⊢ A ∈ ℂ    ⇒   ⊢ A = ((ℜ‘A) + (i · (ℑ‘A)))

Theorem

cjcji 9103

The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133. (Contributed by NM, 11-May-1999.)

⊢ A ∈ ℂ    ⇒   ⊢ (∗‘(∗‘A)) = A

Theorem

reim0bi 9104

A number is real iff its imaginary part is 0. (Contributed by NM, 29-May-1999.)

⊢ A ∈ ℂ    ⇒   ⊢ (A ∈ ℝ ↔ (ℑ‘A) = 0)

Theorem

rerebi 9105

A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 27-Oct-1999.)

⊢ A ∈ ℂ    ⇒   ⊢ (A ∈ ℝ ↔ (ℜ‘A) = A)

Theorem

cjrebi 9106

A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 11-Oct-1999.)

⊢ A ∈ ℂ    ⇒   ⊢ (A ∈ ℝ ↔ (∗‘A) = A)

Theorem

recji 9107

Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)

⊢ A ∈ ℂ    ⇒   ⊢ (ℜ‘(∗‘A)) = (ℜ‘A)

Theorem

imcji 9108

Imaginary part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)

⊢ A ∈ ℂ    ⇒   ⊢ (ℑ‘(∗‘A)) = -(ℑ‘A)

Theorem

cjmulrcli 9109

A complex number times its conjugate is real. (Contributed by NM, 11-May-1999.)

⊢ A ∈ ℂ    ⇒   ⊢ (A · (∗‘A)) ∈ ℝ

Theorem

cjmulvali 9110

A complex number times its conjugate. (Contributed by NM, 2-Oct-1999.)

⊢ A ∈ ℂ    ⇒   ⊢ (A · (∗‘A)) = (((ℜ‘A)↑2) + ((ℑ‘A)↑2))

Theorem

cjmulge0i 9111

A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999.)

⊢ A ∈ ℂ    ⇒   ⊢ 0 ≤ (A · (∗‘A))

Theorem

renegi 9112

Real part of negative. (Contributed by NM, 2-Aug-1999.)

⊢ A ∈ ℂ    ⇒   ⊢ (ℜ‘-A) = -(ℜ‘A)

Theorem

imnegi 9113

Imaginary part of negative. (Contributed by NM, 2-Aug-1999.)

⊢ A ∈ ℂ    ⇒   ⊢ (ℑ‘-A) = -(ℑ‘A)

Theorem

cjnegi 9114

Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.)

⊢ A ∈ ℂ    ⇒   ⊢ (∗‘-A) = -(∗‘A)

Theorem

addcji 9115

A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.)

⊢ A ∈ ℂ    ⇒   ⊢ (A + (∗‘A)) = (2 · (ℜ‘A))

Theorem

readdi 9116

Real part distributes over addition. (Contributed by NM, 28-Jul-1999.)

⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (ℜ‘(A + B)) = ((ℜ‘A) + (ℜ‘B))

Theorem

imaddi 9117

Imaginary part distributes over addition. (Contributed by NM, 28-Jul-1999.)

⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (ℑ‘(A + B)) = ((ℑ‘A) + (ℑ‘B))

Theorem

remuli 9118

Real part of a product. (Contributed by NM, 28-Jul-1999.)

⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (ℜ‘(A · B)) = (((ℜ‘A) · (ℜ‘B)) − ((ℑ‘A) · (ℑ‘B)))

Theorem

immuli 9119

Imaginary part of a product. (Contributed by NM, 28-Jul-1999.)

⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (ℑ‘(A · B)) = (((ℜ‘A) · (ℑ‘B)) + ((ℑ‘A) · (ℜ‘B)))

Theorem

cjaddi 9120

Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.)

⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (∗‘(A + B)) = ((∗‘A) + (∗‘B))

Theorem

cjmuli 9121

Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.)

⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (∗‘(A · B)) = ((∗‘A) · (∗‘B))

Theorem

ipcni 9122

Standard inner product on complex numbers. (Contributed by NM, 2-Oct-1999.)

⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (ℜ‘(A · (∗‘B))) = (((ℜ‘A) · (ℜ‘B)) + ((ℑ‘A) · (ℑ‘B)))

Theorem

cjdivapi 9123

Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.)

⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ (B # 0 → (∗‘(A / B)) = ((∗‘A) / (∗‘B)))

Theorem

crrei 9124

The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.)

⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (ℜ‘(A + (i · B))) = A

Theorem

crimi 9125

The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.)

⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ (ℑ‘(A + (i · B))) = B

Theorem

recld 9126

The real part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (ℜ‘A) ∈ ℝ)

Theorem

imcld 9127

The imaginary part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (ℑ‘A) ∈ ℝ)

Theorem

cjcld 9128

Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (∗‘A) ∈ ℂ)

Theorem

replimd 9129

Construct a complex number from its real and imaginary parts. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → A = ((ℜ‘A) + (i · (ℑ‘A))))

Theorem

remimd 9130

Value of the conjugate of a complex number. The value is the real part minus i times the imaginary part. Definition 10-3.2 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (∗‘A) = ((ℜ‘A) − (i · (ℑ‘A))))

Theorem

cjcjd 9131

The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (∗‘(∗‘A)) = A)

Theorem

reim0bd 9132

A number is real iff its imaginary part is 0. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → (ℑ‘A) = 0)    ⇒   ⊢ (φ → A ∈ ℝ)

Theorem

rerebd 9133

A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → (ℜ‘A) = A)    ⇒   ⊢ (φ → A ∈ ℝ)

Theorem

cjrebd 9134

A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → (∗‘A) = A)    ⇒   ⊢ (φ → A ∈ ℝ)

Theorem

cjne0d 9135

A number is nonzero iff its complex conjugate is nonzero. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → A ≠ 0)    ⇒   ⊢ (φ → (∗‘A) ≠ 0)

Theorem

recjd 9136

Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (ℜ‘(∗‘A)) = (ℜ‘A))

Theorem

imcjd 9137

Imaginary part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (ℑ‘(∗‘A)) = -(ℑ‘A))

Theorem

cjmulrcld 9138

A complex number times its conjugate is real. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (A · (∗‘A)) ∈ ℝ)

Theorem

cjmulvald 9139

A complex number times its conjugate. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (A · (∗‘A)) = (((ℜ‘A)↑2) + ((ℑ‘A)↑2)))

Theorem

cjmulge0d 9140

A complex number times its conjugate is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → 0 ≤ (A · (∗‘A)))

Theorem

renegd 9141

Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (ℜ‘-A) = -(ℜ‘A))

Theorem

imnegd 9142

Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (ℑ‘-A) = -(ℑ‘A))

Theorem

cjnegd 9143

Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (∗‘-A) = -(∗‘A))

Theorem

addcjd 9144

A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (A + (∗‘A)) = (2 · (ℜ‘A)))

Theorem

cjexpd 9145

Complex conjugate of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → 𝑁 ∈ ℕ₀)    ⇒   ⊢ (φ → (∗‘(A↑𝑁)) = ((∗‘A)↑𝑁))

Theorem

readdd 9146

Real part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (ℜ‘(A + B)) = ((ℜ‘A) + (ℜ‘B)))

Theorem

imaddd 9147

Imaginary part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (ℑ‘(A + B)) = ((ℑ‘A) + (ℑ‘B)))

Theorem

resubd 9148

Real part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (ℜ‘(A − B)) = ((ℜ‘A) − (ℜ‘B)))

Theorem

imsubd 9149

Imaginary part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (ℑ‘(A − B)) = ((ℑ‘A) − (ℑ‘B)))

Theorem

remuld 9150

Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (ℜ‘(A · B)) = (((ℜ‘A) · (ℜ‘B)) − ((ℑ‘A) · (ℑ‘B))))

Theorem

immuld 9151

Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (ℑ‘(A · B)) = (((ℜ‘A) · (ℑ‘B)) + ((ℑ‘A) · (ℜ‘B))))

Theorem

cjaddd 9152

Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (∗‘(A + B)) = ((∗‘A) + (∗‘B)))

Theorem

cjmuld 9153

Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (∗‘(A · B)) = ((∗‘A) · (∗‘B)))

Theorem

ipcnd 9154

Standard inner product on complex numbers. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (ℜ‘(A · (∗‘B))) = (((ℜ‘A) · (ℜ‘B)) + ((ℑ‘A) · (ℑ‘B))))

Theorem

cjdivapd 9155

Complex conjugate distributes over division. (Contributed by Jim Kingdon, 15-Jun-2020.)

⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → B ∈ ℂ)    &   ⊢ (φ → B # 0)    ⇒   ⊢ (φ → (∗‘(A / B)) = ((∗‘A) / (∗‘B)))

Theorem

rered 9156

A real number equals its real part. One direction of Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℝ)    ⇒   ⊢ (φ → (ℜ‘A) = A)

Theorem

reim0d 9157

The imaginary part of a real number is 0. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℝ)    ⇒   ⊢ (φ → (ℑ‘A) = 0)

Theorem

cjred 9158

A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℝ)    ⇒   ⊢ (φ → (∗‘A) = A)

Theorem

remul2d 9159

Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (ℜ‘(A · B)) = (A · (ℜ‘B)))

Theorem

immul2d 9160

Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℂ)    ⇒   ⊢ (φ → (ℑ‘(A · B)) = (A · (ℑ‘B)))

Theorem

redivapd 9161

Real part of a division. Related to remul2 9061. (Contributed by Jim Kingdon, 15-Jun-2020.)

⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℂ)    &   ⊢ (φ → A # 0)    ⇒   ⊢ (φ → (ℜ‘(B / A)) = ((ℜ‘B) / A))

Theorem

imdivapd 9162

Imaginary part of a division. Related to remul2 9061. (Contributed by Jim Kingdon, 15-Jun-2020.)

⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℂ)    &   ⊢ (φ → A # 0)    ⇒   ⊢ (φ → (ℑ‘(B / A)) = ((ℑ‘B) / A))

Theorem

crred 9163

The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    ⇒   ⊢ (φ → (ℜ‘(A + (i · B))) = A)

Theorem

crimd 9164

The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.)

⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℝ)    ⇒   ⊢ (φ → (ℑ‘(A + (i · B))) = B)

PART 4  GUIDES AND MISCELLANEA

4.1  Guides (conventions, explanations, and examples)

4.1.1  Conventions

This section describes the conventions we use. However, these conventions often refer to existing mathematical practices, which are discussed in more detail in other references. The following sources lay out how mathematics is developed without the law of the excluded middle. Of course, there are a greater number of sources which assume excluded middle and most of what is in them applies here too (especially in a treatment such as ours which is built on first order logic and set theory, rather than, say, type theory). Studying how a topic is treated in the Metamath Proof Explorer and the references therein is often a good place to start (and is easy to compare with the Intuitionistic Logic Explorer). The textbooks provide a motivation for what we are doing, whereas Metamath lets you see in detail all hidden and implicit steps. Most standard theorems are accompanied by citations. Some closely followed texts include the following:

• Axioms of propositional calculus - Stanford Encyclopedia of Philosophy or [Heyting].
• Axioms of predicate calculus - our axioms are adapted from the ones in the Metamath Proof Explorer.
• Theorems of propositional calculus - [Heyting].
• Theorems of pure predicate calculus - Metamath Proof Explorer.
• Theorems of equality and substitution - Metamath Proof Explorer.
• Axioms of set theory - [Crosilla].
• Development of set theory - Chapter 10 of [HoTT].
• Construction of real and complex numbers - Chapter 11 of [HoTT]; [BauerTaylor].
• Theorems about real numbers - [Geuvers].

Theorem

conventions 9165

Unless there is a reason to diverge, we follow the conventions of the Metamath Proof Explorer (aka "set.mm"). This list of conventions is intended to be read in conjunction with the corresponding conventions in the Metamath Proof Explorer, and only the differences are described below.

• Minimizing axioms and the axiom of choice. We prefer proofs that depend on fewer and/or weaker axioms, even if the proofs are longer. In particular, our choice of IZF (Intuitionistic Zermelo-Fraenkel) over CZF (Constructive Zermelo-Fraenkel, a weaker system) was just an expedient choice because IZF is easier to formalize in metamath. You can find some development using CZF in BJ's mathbox starting at ax-bd0 9202 (and the section header just above it). As for the axiom of choice, the full axiom of choice implies excluded middle as seen at acexmid 5454, although some authors will use countable choice or dependent choice. For example, countable choice or excluded middle is needed to show that the Cauchy reals coincide with the Dedekind reals - Corollary 11.4.3 of [HoTT], p. (varies).
• Junk/undefined results. Much of the discussion of this topic in the Metamath Proof Explorer applies except that certain techniques are not available to us. For example, the Metamath Proof Explorer will often say "if a function is evaluated within its domain, a certain result follows; if the function is evaluated outside its domain, the same result follows. Since the function must be evaluated within its domain or outside it, the result follows unconditionally" (the use of excluded middle in this argument is perhaps obvious when stated this way). For this reason, we generally need to prove we are evaluating functions within their domains and avoid the reverse closure theorems of the Metamath Proof Explorer.
• Bibliography references. The bibliography for the Intuitionistic Logic Explorer is separate from the one for the Metamath Proof Explorer but feel free to copy-paste a citation in either direction in order to cite it.

Label naming conventions

Here are a few of the label naming conventions:

• Suffixes. We follow the conventions of the Metamath Proof Explorer with a few additions. A biconditional in set.mm which is an implication in iset.mm should have a "r" (for the reverse direction), or "i"/"im" (for the forward direction) appended. A theorem in set.mm which has a decidability condition added should add "dc" to the theorem name. A theorem in set.mm where "nonempty class" is changed to "inhabited class" should add "m" (for member) to the theorem name.

The following table shows some commonly-used abbreviations in labels which are not found in the Metamath Proof Explorer, in alphabetical order. For each abbreviation we provide a mnenomic to help you remember it, the source theorem/assumption defining it, an expression showing what it looks like, whether or not it is a "syntax fragment" (an abbreviation that indicates a particular kind of syntax), and hyperlinks to label examples that use the abbreviation. The abbreviation is bolded if there is a df-NAME definition but the label fragment is not NAME.

Abbreviation	Mnenomic	Source	Expression	Syntax?	Example(s)
ap	apart	df-ap 7326		Yes	apadd1 7352, apne 7367

Community. The Metamath mailing list also covers the Intuitionistic Logic Explorer and is at: https://groups.google.com/forum/#!forum/metamath.

(Contributed by Jim Kingdon, 24-Feb-2020.)

⊢ φ    ⇒   ⊢ φ

PART 5  SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)

5.1  Mathboxes for user contributions

5.1.1  Mathbox guidelines

Theorem

mathbox 9166

(This theorem is a dummy placeholder for these guidelines. The name of this theorem, "mathbox", is hard-coded into the Metamath program to identify the start of the mathbox section for web page generation.)

A "mathbox" is a user-contributed section that is maintained by its contributor independently from the main part of set.mm.

For contributors:

By making a contribution, you agree to release it into the public domain, according to the statement at the beginning of set.mm.

Mathboxes are provided to help keep your work synchronized with changes in set.mm, but they shouldn't be depended on as a permanent archive. If you want to preserve your original contribution, it is your responsibility to keep your own copy of it along with the version of set.mm that works with it.

Guidelines:

1. If at all possible, please use only 0-ary class constants for new definitions.

2. Try to follow the style of the rest of set.mm. Each $p and $a statement must be immediately preceded with the comment that will be shown on its web page description. The metamath program command "write source set.mm /rewrap" will take care of wrapping comment lines and indentation conventions. All mathbox content will be on public display and should hopefully reflect the overall quality of the website.

3. Before submitting a revised mathbox, please make sure it verifies against the current set.mm.

4. Mathboxes should be independent i.e. the proofs should verify with all other mathboxes removed. If you need a theorem from another mathbox, that is fine (and encouraged), but let me know, so I can move the theorem to the main section. One way avoid undesired accidental use of other mathbox theorems is to develop your mathbox using a modified set.mm that has mathboxes removed.

Notes:

1. We may decide to move some theorems to the main part of set.mm for general use.

2. We may make changes to mathboxes to maintain the overall quality of set.mm. Normally we will let you know if a change might impact what you are working on.

3. If you use theorems from another user's mathbox, we don't provide assurance that they are based on correct or consistent $a statements. (If you find such a problem, please let us know so it can be corrected.) (Contributed by NM, 20-Feb-2007.) (New usage is discouraged.)

⊢ x = x

5.2  Mathbox for Mykola Mostovenko

Theorem

ax1hfs 9167

Heyting's formal system Axiom #1 from [Heyting] p. 127. (Contributed by MM, 11-Aug-2018.)

⊢ (φ → (φ ∧ φ))

5.3  Mathbox for BJ

5.3.1  Propositional calculus

Theorem

nnexmid 9168

Double negation of excluded middle. Intuitionistic logic refutes the negation of excluded middle (but, of course, does not prove excluded middle) for any formula. (Contributed by BJ, 9-Oct-2019.)

⊢ ¬ ¬ (φ ∨ ¬ φ)

Theorem

nndc 9169

Double negation of decidability of a formula. Intuitionistic logic refutes undecidability (but, of course, does not prove decidability) of any formula. (Contributed by BJ, 9-Oct-2019.)

⊢ ¬ ¬ DECID φ

Theorem

dcdc 9170

Decidability of a proposition is decidable if and only if that proposition is decidable. DECID is idempotent. (Contributed by BJ, 9-Oct-2019.)

⊢ (DECID DECID φ ↔ DECID φ)

5.3.2  Predicate calculus

Theorem

bj-ex 9171*

Existential generalization. (Contributed by BJ, 8-Dec-2019.) Proof modification is discouraged because there are shorter proofs, but using less basic results (like exlimiv 1486 and 19.9ht 1529 or 19.23ht 1383). (Proof modification is discouraged.)

⊢ (∃xφ → φ)

Theorem

bj-hbalt 9172

Closed form of hbal 1363 (copied from set.mm). (Contributed by BJ, 2-May-2019.)

⊢ (∀y(φ → ∀xφ) → (∀yφ → ∀x∀yφ))

Theorem

bj-nfalt 9173

Closed form of nfal 1465 (copied from set.mm). (Contributed by BJ, 2-May-2019.)

⊢ (∀xℲyφ → Ⅎy∀xφ)

Theorem

spimd 9174

Deduction form of spim 1623. (Contributed by BJ, 17-Oct-2019.)

⊢ (φ → Ⅎxχ)    &   ⊢ (φ → ∀x(x = y → (ψ → χ)))    ⇒   ⊢ (φ → (∀xψ → χ))

Theorem

2spim 9175*

Double substitution, as in spim 1623. (Contributed by BJ, 17-Oct-2019.)

⊢ Ⅎxχ    &   ⊢ Ⅎzχ    &   ⊢ ((x = y ∧ z = 𝑡) → (ψ → χ))    ⇒   ⊢ (∀z∀xψ → χ)

Theorem

ch2var 9176*

Implicit substitution of y for x and 𝑡 for z into a theorem. (Contributed by BJ, 17-Oct-2019.)

⊢ Ⅎxψ    &   ⊢ Ⅎzψ    &   ⊢ ((x = y ∧ z = 𝑡) → (φ ↔ ψ))    &   ⊢ φ    ⇒   ⊢ ψ

Theorem

ch2varv 9177*

Version of ch2var 9176 with non-freeness hypotheses replaced by DV conditions. (Contributed by BJ, 17-Oct-2019.)

⊢ ((x = y ∧ z = 𝑡) → (φ ↔ ψ))    &   ⊢ φ    ⇒   ⊢ ψ

Theorem

bj-exlimmp 9178

Lemma for bj-vtoclgf 9184. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)

⊢ Ⅎxψ    &   ⊢ (χ → φ)    ⇒   ⊢ (∀x(χ → (φ → ψ)) → (∃xχ → ψ))

Theorem

bj-exlimmpi 9179

Lemma for bj-vtoclgf 9184. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)

⊢ Ⅎxψ    &   ⊢ (χ → φ)    &   ⊢ (χ → (φ → ψ))    ⇒   ⊢ (∃xχ → ψ)

Theorem

bj-sbimedh 9180

A strengthening of sbiedh 1667 (same proof). (Contributed by BJ, 16-Dec-2019.)

⊢ (φ → ∀xφ)    &   ⊢ (φ → (χ → ∀xχ))    &   ⊢ (φ → (x = y → (ψ → χ)))    ⇒   ⊢ (φ → ([y / x]ψ → χ))

Theorem

bj-sbimeh 9181

A strengthening of sbieh 1670 (same proof). (Contributed by BJ, 16-Dec-2019.)

⊢ (ψ → ∀xψ)    &   ⊢ (x = y → (φ → ψ))    ⇒   ⊢ ([y / x]φ → ψ)

Theorem

bj-sbime 9182

A strengthening of sbie 1671 (same proof). (Contributed by BJ, 16-Dec-2019.)

⊢ Ⅎxψ    &   ⊢ (x = y → (φ → ψ))    ⇒   ⊢ ([y / x]φ → ψ)

5.3.3  Extensionality

Various utility theorems using FOL and extensionality.

Theorem

bj-vtoclgft 9183

Weakening two hypotheses of vtoclgf 2606. (Contributed by BJ, 21-Nov-2019.)

⊢ ℲxA    &   ⊢ Ⅎxψ    &   ⊢ (x = A → φ)    ⇒   ⊢ (∀x(x = A → (φ → ψ)) → (A ∈ 𝑉 → ψ))

Theorem

bj-vtoclgf 9184

Weakening two hypotheses of vtoclgf 2606. (Contributed by BJ, 21-Nov-2019.)

⊢ ℲxA    &   ⊢ Ⅎxψ    &   ⊢ (x = A → φ)    &   ⊢ (x = A → (φ → ψ))    ⇒   ⊢ (A ∈ 𝑉 → ψ)

Theorem

elabgf0 9185

Lemma for elabgf 2679. (Contributed by BJ, 21-Nov-2019.)

⊢ (x = A → (A ∈ {x ∣ φ} ↔ φ))

Theorem

elabgft1 9186

One implication of elabgf 2679, in closed form. (Contributed by BJ, 21-Nov-2019.)

⊢ ℲxA    &   ⊢ Ⅎxψ    ⇒   ⊢ (∀x(x = A → (φ → ψ)) → (A ∈ {x ∣ φ} → ψ))

Theorem

elabgf1 9187

One implication of elabgf 2679. (Contributed by BJ, 21-Nov-2019.)

⊢ ℲxA    &   ⊢ Ⅎxψ    &   ⊢ (x = A → (φ → ψ))    ⇒   ⊢ (A ∈ {x ∣ φ} → ψ)

Theorem

elabgf2 9188

One implication of elabgf 2679. (Contributed by BJ, 21-Nov-2019.)

⊢ ℲxA    &   ⊢ Ⅎxψ    &   ⊢ (x = A → (ψ → φ))    ⇒   ⊢ (A ∈ B → (ψ → A ∈ {x ∣ φ}))

Theorem

elabf1 9189*

One implication of elabf 2680. (Contributed by BJ, 21-Nov-2019.)

⊢ Ⅎxψ    &   ⊢ (x = A → (φ → ψ))    ⇒   ⊢ (A ∈ {x ∣ φ} → ψ)

Theorem

elabf2 9190*

One implication of elabf 2680. (Contributed by BJ, 21-Nov-2019.)

⊢ Ⅎxψ    &   ⊢ A ∈ V    &   ⊢ (x = A → (ψ → φ))    ⇒   ⊢ (ψ → A ∈ {x ∣ φ})

Theorem

elab1 9191*

One implication of elab 2681. (Contributed by BJ, 21-Nov-2019.)

⊢ (x = A → (φ → ψ))    ⇒   ⊢ (A ∈ {x ∣ φ} → ψ)

Theorem

elab2a 9192*

One implication of elab 2681. (Contributed by BJ, 21-Nov-2019.)

⊢ A ∈ V    &   ⊢ (x = A → (ψ → φ))    ⇒   ⊢ (ψ → A ∈ {x ∣ φ})

Theorem

elabg2 9193*

One implication of elabg 2682. (Contributed by BJ, 21-Nov-2019.)

⊢ (x = A → (ψ → φ))    ⇒   ⊢ (A ∈ 𝑉 → (ψ → A ∈ {x ∣ φ}))

Theorem

bj-rspgt 9194

Restricted specialization, generalized. Weakens a hypothesis of rspccv 2647 and seems to have a shorter proof. (Contributed by BJ, 21-Nov-2019.)

⊢ ℲxA    &   ⊢ ℲxB    &   ⊢ Ⅎxψ    ⇒   ⊢ (∀x(x = A → (φ → ψ)) → (∀x ∈ B φ → (A ∈ B → ψ)))

Theorem

bj-rspg 9195

Restricted specialization, generalized. Weakens a hypothesis of rspccv 2647 and seems to have a shorter proof. (Contributed by BJ, 21-Nov-2019.)

⊢ ℲxA    &   ⊢ ℲxB    &   ⊢ Ⅎxψ    &   ⊢ (x = A → (φ → ψ))    ⇒   ⊢ (∀x ∈ B φ → (A ∈ B → ψ))

Theorem

cbvrald 9196*

Rule used to change bound variables, using implicit substitution. (Contributed by BJ, 22-Nov-2019.)

⊢ Ⅎxφ    &   ⊢ Ⅎyφ    &   ⊢ (φ → Ⅎyψ)    &   ⊢ (φ → Ⅎxχ)    &   ⊢ (φ → (x = y → (ψ ↔ χ)))    ⇒   ⊢ (φ → (∀x ∈ A ψ ↔ ∀y ∈ A χ))

Theorem

bj-intabssel 9197

Version of intss1 3621 using a class abstraction and explicit substitution. (Contributed by BJ, 29-Nov-2019.)

⊢ ℲxA    ⇒   ⊢ (A ∈ 𝑉 → ([A / x]φ → ∩ {x ∣ φ} ⊆ A))

Theorem

bj-intabssel1 9198

Version of intss1 3621 using a class abstraction and implicit substitution. Closed form of intmin3 3633. (Contributed by BJ, 29-Nov-2019.)

⊢ ℲxA    &   ⊢ Ⅎxψ    &   ⊢ (x = A → (ψ → φ))    ⇒   ⊢ (A ∈ 𝑉 → (ψ → ∩ {x ∣ φ} ⊆ A))

Theorem

bj-elssuniab 9199

Version of elssuni 3599 using a class abstraction and explicit substitution. (Contributed by BJ, 29-Nov-2019.)

⊢ ℲxA    ⇒   ⊢ (A ∈ 𝑉 → ([A / x]φ → A ⊆ ∪ {x ∣ φ}))

Theorem

bj-sseq 9200

If two converse inclusions are characterized each by a formula, then equality is characterized by the conjunction of these formulas. (Contributed by BJ, 30-Nov-2019.)

⊢ (φ → (ψ ↔ A ⊆ B))    &   ⊢ (φ → (χ ↔ B ⊆ A))    ⇒   ⊢ (φ → ((ψ ∧ χ) ↔ A = B))