Most Recent Proofs - Intuitionistic Logic Explorer

Most recent proofs    These are the 100 (Unicode, GIF) or 1000 (Unicode, GIF) most recent proofs in the iset.mm database for the Intuitionistic Logic Explorer. The iset.mm database is maintained on GitHub with master (stable) and develop (development) versions. This page was created from the commit given on the MPE Most Recent Proofs page. The database from that commit is also available here: iset.mm.

See the MPE Most Recent Proofs page for news and some useful links.

Last updated on 5-Dec-2019 at 7:17 PM ET.

Recent Additions to the Intuitionistic Logic Explorer

Date	Label	Description
Theorem
3-Dec-2019	addassnq0lemcl 6302	A natural number closure law. Lemma for addassnq0 6303. (Contributed by Jim Kingdon, 3-Dec-2019.)
⊢ (((𝐼 ∈ 𝜔 ∧ 𝐽 ∈ N) ∧ (𝐾 ∈ 𝜔 ∧ 𝐿 ∈ N)) → (((𝐼 ·𝑜 𝐿) +𝑜 (𝐽 ·𝑜 𝐾)) ∈ 𝜔 ∧ (𝐽 ·𝑜 𝐿) ∈ N))
3-Dec-2019	nndir 5979	Distributive law for natural numbers (right-distributivity). (Contributed by Jim Kingdon, 3-Dec-2019.)
⊢ ((A ∈ 𝜔 ∧ B ∈ 𝜔 ∧ 𝐶 ∈ 𝜔) → ((A +𝑜 B) ·𝑜 𝐶) = ((A ·𝑜 𝐶) +𝑜 (B ·𝑜 𝐶)))
1-Dec-2019	nnanq0 6299	Addition of non-negative fractions with a common denominator. You can add two fractions with the same denominator by adding their numerators and keeping the same denominator. (Contributed by Jim Kingdon, 1-Dec-2019.)
⊢ ((𝑁 ∈ 𝜔 ∧ 𝑀 ∈ 𝜔 ∧ A ∈ N) → [⟨(𝑁 +𝑜 𝑀), A⟩] ~Q0 = ([⟨𝑁, A⟩] ~Q0 +Q0 [⟨𝑀, A⟩] ~Q0 ))
1-Dec-2019	archnqq 6261	For any fraction, there is an integer that is greater than it. This is also known as the "archimedean property". (Contributed by Jim Kingdon, 1-Dec-2019.)
⊢ (A ∈ Q → ∃x ∈ N A <Q [⟨x, 1𝑜⟩] ~Q )
30-Nov-2019	bj-2inf 6502	Two formulations of the axiom of infinity (see ax-infc 6504 and bj-omex 6506) . (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
⊢ (𝜔 ∈ V ↔ ∃x(Ind x ∧ ∀y(Ind y → x ⊆ y)))
30-Nov-2019	bj-om 6501	A set is equal to 𝜔 if and only if it is the smallest inductive set. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
⊢ (A ∈ 𝑉 → (A = 𝜔 ↔ (Ind A ∧ ∀x(Ind x → A ⊆ x))))
30-Nov-2019	bj-omssind 6500	𝜔 is included in all the inductive sets (but for the moment, we cannot prove that it is included in all the inductive classes). (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
⊢ (A ∈ 𝑉 → (Ind A → 𝜔 ⊆ A))
30-Nov-2019	bj-omind 6499	𝜔 is an inductive class. (Contributed by BJ, 30-Nov-2019.)
⊢ Ind 𝜔
30-Nov-2019	bj-dfom 6498	Alternate definition of 𝜔, as the intersection of all the inductive sets. Proposal: make this the definition. (Contributed by BJ, 30-Nov-2019.)
⊢ 𝜔 = ∩ {x ∣ Ind x}
30-Nov-2019	bj-indint 6497	The property of being an inductive class is closed under intersections. (Contributed by BJ, 30-Nov-2019.)
⊢ Ind ∩ {x ∈ A ∣ Ind x}
30-Nov-2019	bj-indeq 6496	Equality property for Ind. (Contributed by BJ, 30-Nov-2019.)
⊢ (A = B → (Ind A ↔ Ind B))
30-Nov-2019	bj-indsuc 6495	A direct consequence of the definition of Ind. (Contributed by BJ, 30-Nov-2019.)
⊢ (Ind A → (B ∈ A → suc B ∈ A))
30-Nov-2019	df-bj-ind 6494	Define the property of being an inductive class. (Contributed by BJ, 30-Nov-2019.)
⊢ (Ind A ↔ (∅ ∈ A ∧ ∀x ∈ A suc x ∈ A))
30-Nov-2019	bj-sseq 6387	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))
30-Nov-2019	nqpnq0nq 6294	A positive fraction plus a non-negative fraction is a positive fraction. (Contributed by Jim Kingdon, 30-Nov-2019.)
⊢ ((A ∈ Q ∧ B ∈ Q0) → (A +Q0 B) ∈ Q)
30-Nov-2019	mulclnq0 6293	Closure of multiplication on non-negative fractions. (Contributed by Jim Kingdon, 30-Nov-2019.)
⊢ ((A ∈ Q0 ∧ B ∈ Q0) → (A ·Q0 B) ∈ Q0)
30-Nov-2019	prarloclemarch 6262	A version of the Archimedean property. This variation is "stronger" than archnqq 6261 in the sense that we provide an integer which is larger than a given rational A even after being multiplied by a second rational B. (Contributed by Jim Kingdon, 30-Nov-2019.)
⊢ ((A ∈ Q ∧ B ∈ Q) → ∃x ∈ N A <Q ([⟨x, 1𝑜⟩] ~Q ·Q B))
29-Nov-2019	bj-elssuniab 6386	Version of elssuni 3581 using a class abstraction and explicit substitution. (Contributed by BJ, 29-Nov-2019.)
⊢ ℲxA    ⇒   ⊢ (A ∈ 𝑉 → ([A / x]φ → A ⊆ ∪ {x ∣ φ}))
29-Nov-2019	bj-intabssel1 6385	Version of intss1 3603 using a class abstraction and implicit substitution. Closed form of intmin3 3615. (Contributed by BJ, 29-Nov-2019.)
⊢ ℲxA    &   ⊢ Ⅎxψ    &   ⊢ (x = A → (ψ → φ))    ⇒   ⊢ (A ∈ 𝑉 → (ψ → ∩ {x ∣ φ} ⊆ A))
29-Nov-2019	bj-intabssel 6384	Version of intss1 3603 using a class abstraction and explicit substitution. (Contributed by BJ, 29-Nov-2019.)
⊢ ℲxA    ⇒   ⊢ (A ∈ 𝑉 → ([A / x]φ → ∩ {x ∣ φ} ⊆ A))
29-Nov-2019	nq02m 6305	Multiply a non-negative fraction by two. (Contributed by Jim Kingdon, 29-Nov-2019.)
⊢ (A ∈ Q0 → ([⟨2𝑜, 1𝑜⟩] ~Q0 ·Q0 A) = (A +Q0 A))
29-Nov-2019	distnq0r 6304	Multiplication of non-negative fractions is distributive. Version of distrnq0 6300 with the multiplications commuted. (Contributed by Jim Kingdon, 29-Nov-2019.)
⊢ ((A ∈ Q0 ∧ B ∈ Q0 ∧ 𝐶 ∈ Q0) → ((B +Q0 𝐶) ·Q0 A) = ((B ·Q0 A) +Q0 (𝐶 ·Q0 A)))
29-Nov-2019	addassnq0 6303	Addition of non-negaative fractions is associative. (Contributed by Jim Kingdon, 29-Nov-2019.)
⊢ ((A ∈ Q0 ∧ B ∈ Q0 ∧ 𝐶 ∈ Q0) → ((A +Q0 B) +Q0 𝐶) = (A +Q0 (B +Q0 𝐶)))
29-Nov-2019	addclnq0 6292	Closure of addition on non-negative fractions. (Contributed by Jim Kingdon, 29-Nov-2019.)
⊢ ((A ∈ Q0 ∧ B ∈ Q0) → (A +Q0 B) ∈ Q0)
29-Nov-2019	mulcanenq0ec 6286	Lemma for distributive law: cancellation of common factor. (Contributed by Jim Kingdon, 29-Nov-2019.)
⊢ ((A ∈ N ∧ B ∈ 𝜔 ∧ 𝐶 ∈ N) → [⟨(A ·𝑜 B), (A ·𝑜 𝐶)⟩] ~Q0 = [⟨B, 𝐶⟩] ~Q0 )
28-Nov-2019	ax-bdsetind 6527	Axiom of bounded set induction. (Contributed by BJ, 28-Nov-2019.)
⊢ BOUNDED φ    ⇒   ⊢ (∀𝑎(∀y ∈ 𝑎 [y / 𝑎]φ → φ) → ∀𝑎φ)
28-Nov-2019	bj-peano4 6522	Remove from peano4 4245 dependency on ax-setind 4202. Therefore, it only requires core constructive axioms (albeit more of them). (Contributed by BJ, 28-Nov-2019.) (Proof modification is discouraged.)
⊢ ((A ∈ 𝜔 ∧ B ∈ 𝜔) → (suc A = suc B ↔ A = B))
28-Nov-2019	bj-nnen2lp 6521	A version of en2lp 4214 for natural numbers, which does not require ax-setind 4202. Note: using this theorem and bj-nnelirr 6520, one can remove dependency on ax-setind 4202 from nntri2 5983 and nndcel 5986; one can actually remove more dependencies from these. (Contributed by BJ, 28-Nov-2019.) (Proof modification is discouraged.)
⊢ ((A ∈ 𝜔 ∧ B ∈ 𝜔) → ¬ (A ∈ B ∧ B ∈ A))
27-Nov-2019	mulcomnq0 6301	Multiplication of non-negative fractions is commutative. (Contributed by Jim Kingdon, 27-Nov-2019.)
⊢ ((A ∈ Q0 ∧ B ∈ Q0) → (A ·Q0 B) = (B ·Q0 A))
27-Nov-2019	distrnq0 6300	Multiplication of non-negative fractions is distributive. (Contributed by Jim Kingdon, 27-Nov-2019.)
⊢ ((A ∈ Q0 ∧ B ∈ Q0 ∧ 𝐶 ∈ Q0) → (A ·Q0 (B +Q0 𝐶)) = ((A ·Q0 B) +Q0 (A ·Q0 𝐶)))
25-Nov-2019	prcunqu 6324	An upper cut is closed upwards under the positive fractions. (Contributed by Jim Kingdon, 25-Nov-2019.)
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐶 ∈ 𝑈) → (𝐶 <Q B → B ∈ 𝑈))
25-Nov-2019	prarloclemarch2 6263	Like prarloclemarch 6262 but the integer must be at least two, and there is also B added to the right hand side. These details follow straightforwardly but are chosen to be helpful in the proof of prarloc 6340. (Contributed by Jim Kingdon, 25-Nov-2019.)
⊢ ((A ∈ Q ∧ B ∈ Q ∧ 𝐶 ∈ Q) → ∃x ∈ N (1𝑜 <N x ∧ A <Q (B +Q ([⟨x, 1𝑜⟩] ~Q ·Q 𝐶))))
25-Nov-2019	subhalfnqq 6258	There is a number which is less than half of any positive fraction. The case where A is one is Lemma 11.4 of [BauerTaylor], p. 50, and they use the word "approximate half" for such a number (since there may be constructions, for some structures other than the rationals themselves, which rely on such an approximate half but do not require division by two as seen at halfnqq 6254). (Contributed by Jim Kingdon, 25-Nov-2019.)
⊢ (A ∈ Q → ∃x ∈ Q (x +Q x) <Q A)
24-Nov-2019	bj-findeslem1 6530	Lemma for bj-findes (but probably useless). Constructive proof. (Contributed by BJ, 24-Nov-2019.) (Proof modification is discouraged.)
⊢ (ψ ↔ (x ∈ 𝜔 → φ))    ⇒   ⊢ ([suc x / x]ψ → (x ∈ 𝜔 → [suc x / x]φ))
24-Nov-2019	bj-findeslem1BAD 6529	Lemma for bj-findes . NOT YET constructive because of peano2b 4262. (Contributed by BJ, 24-Nov-2019.) (Proof modification is discouraged.)
⊢ (ψ ↔ (x ∈ 𝜔 → φ))    ⇒   ⊢ ((x ∈ 𝜔 → [suc x / x]φ) ↔ [suc x / x]ψ)
24-Nov-2019	bj-findeslem0 6528	Lemma for bj-findes . (Contributed by BJ, 24-Nov-2019.) (Proof modification is discouraged.)
⊢ (ψ ↔ (x ∈ 𝜔 → φ))    ⇒   ⊢ ([∅ / x]φ ↔ [∅ / x]ψ)
24-Nov-2019	bj-nnelirr 6520	A natural number does not belong to itself. Version of elirr 4206 for natural numbers, which does not require ax-setind 4202. (Contributed by BJ, 24-Nov-2019.) (Proof modification is discouraged.)
⊢ (A ∈ 𝜔 → ¬ A ∈ A)
24-Nov-2019	bdcriota 6454	A class given by a restricted definition binder is bounded, under the given hypotheses. (Contributed by BJ, 24-Nov-2019.)
⊢ BOUNDED φ    &   ⊢ ∃!x ∈ y φ    ⇒   ⊢ BOUNDED (℩x ∈ y φ)
24-Nov-2019	nq0nn 6283	Decomposition of a non-negative fraction into numerator and denominator. (Contributed by Jim Kingdon, 24-Nov-2019.)
⊢ (A ∈ Q0 → ∃w∃v((w ∈ 𝜔 ∧ v ∈ N) ∧ A = [⟨w, v⟩] ~Q0 ))
24-Nov-2019	enq0eceq 6278	Equivalence class equality of non-negative fractions in terms of natural numbers. (Contributed by Jim Kingdon, 24-Nov-2019.)
⊢ (((A ∈ 𝜔 ∧ B ∈ N) ∧ (𝐶 ∈ 𝜔 ∧ 𝐷 ∈ N)) → ([⟨A, B⟩] ~Q0 = [⟨𝐶, 𝐷⟩] ~Q0 ↔ (A ·𝑜 𝐷) = (B ·𝑜 𝐶)))
24-Nov-2019	dfplq0qs 6271	Addition on non-negative fractions. This definition is similar to df-plq0 6268 but expands Q0 (Contributed by Jim Kingdon, 24-Nov-2019.)
⊢ +Q0 = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ ((𝜔 × N) / ~Q0 ) ∧ y ∈ ((𝜔 × N) / ~Q0 )) ∧ ∃w∃v∃u∃f((x = [⟨w, v⟩] ~Q0 ∧ y = [⟨u, f⟩] ~Q0 ) ∧ z = [⟨((w ·𝑜 f) +𝑜 (v ·𝑜 u)), (v ·𝑜 f)⟩] ~Q0 ))}
23-Nov-2019	addnq0mo 6288	There is at most one result from adding non-negative fractions. (Contributed by Jim Kingdon, 23-Nov-2019.)
⊢ ((A ∈ ((𝜔 × N) / ~Q0 ) ∧ B ∈ ((𝜔 × N) / ~Q0 )) → ∃*z∃w∃v∃u∃𝑡((A = [⟨w, v⟩] ~Q0 ∧ B = [⟨u, 𝑡⟩] ~Q0 ) ∧ z = [⟨((w ·𝑜 𝑡) +𝑜 (v ·𝑜 u)), (v ·𝑜 𝑡)⟩] ~Q0 ))
23-Nov-2019	nnnq0lem1 6287	Decomposing non-negative fractions into natural numbers. Lemma for addnnnq0 6290 and mulnnnq0 6291. (Contributed by Jim Kingdon, 23-Nov-2019.)
⊢ (((A ∈ ((𝜔 × N) / ~Q0 ) ∧ B ∈ ((𝜔 × N) / ~Q0 )) ∧ (((A = [⟨w, v⟩] ~Q0 ∧ B = [⟨u, 𝑡⟩] ~Q0 ) ∧ z = [𝐶] ~Q0 ) ∧ ((A = [⟨𝑠, f⟩] ~Q0 ∧ B = [⟨g, ℎ⟩] ~Q0 ) ∧ 𝑞 = [𝐷] ~Q0 ))) → ((((w ∈ 𝜔 ∧ v ∈ N) ∧ (𝑠 ∈ 𝜔 ∧ f ∈ N)) ∧ ((u ∈ 𝜔 ∧ 𝑡 ∈ N) ∧ (g ∈ 𝜔 ∧ ℎ ∈ N))) ∧ ((w ·𝑜 f) = (v ·𝑜 𝑠) ∧ (u ·𝑜 ℎ) = (𝑡 ·𝑜 g))))
23-Nov-2019	addcmpblnq0 6284	Lemma showing compatibility of addition on non-negative fractions. (Contributed by Jim Kingdon, 23-Nov-2019.)
⊢ ((((A ∈ 𝜔 ∧ B ∈ N) ∧ (𝐶 ∈ 𝜔 ∧ 𝐷 ∈ N)) ∧ ((𝐹 ∈ 𝜔 ∧ 𝐺 ∈ N) ∧ (𝑅 ∈ 𝜔 ∧ 𝑆 ∈ N))) → (((A ·𝑜 𝐷) = (B ·𝑜 𝐶) ∧ (𝐹 ·𝑜 𝑆) = (𝐺 ·𝑜 𝑅)) → ⟨((A ·𝑜 𝐺) +𝑜 (B ·𝑜 𝐹)), (B ·𝑜 𝐺)⟩ ~Q0 ⟨((𝐶 ·𝑜 𝑆) +𝑜 (𝐷 ·𝑜 𝑅)), (𝐷 ·𝑜 𝑆)⟩))
23-Nov-2019	ee8anv 1793	Rearrange existential quantifiers. (Contributed by Jim Kingdon, 23-Nov-2019.)
⊢ (∃x∃y∃z∃w∃v∃u∃𝑡∃𝑠(φ ∧ ψ) ↔ (∃x∃y∃z∃wφ ∧ ∃v∃u∃𝑡∃𝑠ψ))
23-Nov-2019	19.42vvvv 1773	Theorem 19.42 of [Margaris] p. 90 with 4 quantifiers. (Contributed by Jim Kingdon, 23-Nov-2019.)
⊢ (∃w∃x∃y∃z(φ ∧ ψ) ↔ (φ ∧ ∃w∃x∃y∃zψ))
22-Nov-2019	setindis 6526	Axiom of set induction using implicit substitutions. (Contributed by BJ, 22-Nov-2019.)
⊢ Ⅎxψ    &   ⊢ Ⅎxχ    &   ⊢ Ⅎyφ    &   ⊢ Ⅎyψ    &   ⊢ (x = z → (φ ↔ ψ))    &   ⊢ (x = y → (χ ↔ φ))    ⇒   ⊢ (∀y(∀z ∈ y ψ → χ) → ∀xφ)
22-Nov-2019	setindf 6525	Axiom of set-induction with a DV condition replaced with a non-freeness hypothesis (Contributed by BJ, 22-Nov-2019.)
⊢ Ⅎyφ    ⇒   ⊢ (∀x(∀y ∈ x [y / x]φ → φ) → ∀xφ)
22-Nov-2019	setindft 6524	Axiom of set-induction with a DV condition replaced with a non-freeness hypothesis (Contributed by BJ, 22-Nov-2019.)
⊢ (∀xℲyφ → (∀x(∀y ∈ x [y / x]φ → φ) → ∀xφ))
22-Nov-2019	bj-nntrans2 6519	A natural number is a transitive set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
⊢ (A ∈ 𝜔 → (B ∈ A → B ⊆ A))
22-Nov-2019	bj-nntrans 6518	A natural number is a transitive set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
⊢ (A ∈ 𝜔 → ∀x ∈ A x ⊆ A)
22-Nov-2019	bdfind 6513	Bounded induction (principle of induction when A is assumed to be bounded), proved from basic constructive axioms. See find 4247 for a nonconstructive proof of the general case. See findset 6512 for a proof when A is assumed to be a set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
⊢ BOUNDED A    ⇒   ⊢ ((A ⊆ 𝜔 ∧ ∅ ∈ A ∧ ∀x ∈ A suc x ∈ A) → A = 𝜔)
22-Nov-2019	findset 6512	Bounded induction (principle of induction when A is assumed to be a set) allowing a proof from basic constructive axioms. See find 4247 for a nonconstructive proof of the general case. See bdfind 6513 for a proof when A is assumed to be bounded. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
⊢ (A ∈ 𝑉 → ((A ⊆ 𝜔 ∧ ∅ ∈ A ∧ ∀x ∈ A suc x ∈ A) → A = 𝜔))
22-Nov-2019	cbvrald 6383	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 χ))
22-Nov-2019	addnnnq0 6290	Addition of non-negative fractions in terms of natural numbers. (Contributed by Jim Kingdon, 22-Nov-2019.)
⊢ (((A ∈ 𝜔 ∧ B ∈ N) ∧ (𝐶 ∈ 𝜔 ∧ 𝐷 ∈ N)) → ([⟨A, B⟩] ~Q0 +Q0 [⟨𝐶, 𝐷⟩] ~Q0 ) = [⟨((A ·𝑜 𝐷) +𝑜 (B ·𝑜 𝐶)), (B ·𝑜 𝐷)⟩] ~Q0 )
22-Nov-2019	dfmq0qs 6270	Multiplication on non-negative fractions. This definition is similar to df-mq0 6269 but exapands Q0 (Contributed by Jim Kingdon, 22-Nov-2019.)
⊢ ·Q0 = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ ((𝜔 × N) / ~Q0 ) ∧ y ∈ ((𝜔 × N) / ~Q0 )) ∧ ∃w∃v∃u∃f((x = [⟨w, v⟩] ~Q0 ∧ y = [⟨u, f⟩] ~Q0 ) ∧ z = [⟨(w ·𝑜 u), (v ·𝑜 f)⟩] ~Q0 ))}
21-Nov-2019	bj-bdfindes 6516	Bounded induction, using explicit substitutions. Constructive proof. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
⊢ BOUNDED φ    ⇒   ⊢ (([∅ / x]φ ∧ ∀x ∈ 𝜔 (φ → [suc x / x]φ)) → ∀x ∈ 𝜔 φ)
21-Nov-2019	bj-bdfindisg 6515	Bounded induction (principle of induction for bounded formulas), using implicit substitutions (the biconditional versions of the hypotheses are implicit substitutions, and we have weakened them to implications). See finds 4248. From this version, it is easy to prove bounded versions of finds 4248, finds2 4249, finds1 4250. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
⊢ BOUNDED φ    &   ⊢ Ⅎxψ    &   ⊢ Ⅎxχ    &   ⊢ Ⅎxθ    &   ⊢ (x = ∅ → (ψ → φ))    &   ⊢ (x = y → (φ → χ))    &   ⊢ (x = suc y → (θ → φ))    &   ⊢ ℲxA    &   ⊢ Ⅎxτ    &   ⊢ (x = A → (φ → τ))    ⇒   ⊢ ((ψ ∧ ∀y ∈ 𝜔 (χ → θ)) → (A ∈ 𝜔 → τ))
21-Nov-2019	bj-bdfindis 6514	Bounded induction (principle of induction for bounded formulas), using implicit substitutions (the biconditional versions of the hypotheses are implicit substitutions, and we have weakened them to implications). See finds 4248. From this version, it is easy to prove bounded versions of finds 4248, finds2 4249, finds1 4250. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
⊢ BOUNDED φ    &   ⊢ Ⅎxψ    &   ⊢ Ⅎxχ    &   ⊢ Ⅎxθ    &   ⊢ (x = ∅ → (ψ → φ))    &   ⊢ (x = y → (φ → χ))    &   ⊢ (x = suc y → (θ → φ))    ⇒   ⊢ ((ψ ∧ ∀y ∈ 𝜔 (χ → θ)) → ∀x ∈ 𝜔 φ)
21-Nov-2019	bdeqsuc 6492	Boundedness lemma. (Contributed by BJ, 21-Nov-2019.)
⊢ BOUNDED x = suc y
21-Nov-2019	bdeq0 6491	Boundedness lemma. (Contributed by BJ, 21-Nov-2019.)
⊢ BOUNDED x = ∅
21-Nov-2019	bdop 6448	The ordered pair of two setvars is a bounded class. (Contributed by BJ, 21-Nov-2019.)
⊢ BOUNDED ⟨x, y⟩
21-Nov-2019	bj-rspg 6382	Restricted specialization, generalized. Weakens a hypothesis of rspccv 2629 and seems to have a shorter proof. (Contributed by BJ, 21-Nov-2019.)
⊢ ℲxA    &   ⊢ ℲxB    &   ⊢ Ⅎxψ    &   ⊢ (x = A → (φ → ψ))    ⇒   ⊢ (∀x ∈ B φ → (A ∈ B → ψ))
21-Nov-2019	bj-rspgt 6381	Restricted specialization, generalized. Weakens a hypothesis of rspccv 2629 and seems to have a shorter proof. (Contributed by BJ, 21-Nov-2019.)
⊢ ℲxA    &   ⊢ ℲxB    &   ⊢ Ⅎxψ    ⇒   ⊢ (∀x(x = A → (φ → ψ)) → (∀x ∈ B φ → (A ∈ B → ψ)))
21-Nov-2019	elabg2 6380	One implication of elabg 2664. (Contributed by BJ, 21-Nov-2019.)
⊢ (x = A → (ψ → φ))    ⇒   ⊢ (A ∈ 𝑉 → (ψ → A ∈ {x ∣ φ}))
21-Nov-2019	elab2a 6379	One implication of elab 2663. (Contributed by BJ, 21-Nov-2019.)
⊢ A ∈ V    &   ⊢ (x = A → (ψ → φ))    ⇒   ⊢ (ψ → A ∈ {x ∣ φ})
21-Nov-2019	elab1 6378	One implication of elab 2663. (Contributed by BJ, 21-Nov-2019.)
⊢ (x = A → (φ → ψ))    ⇒   ⊢ (A ∈ {x ∣ φ} → ψ)
21-Nov-2019	elabf2 6377	One implication of elabf 2662. (Contributed by BJ, 21-Nov-2019.)
⊢ Ⅎxψ    &   ⊢ A ∈ V    &   ⊢ (x = A → (ψ → φ))    ⇒   ⊢ (ψ → A ∈ {x ∣ φ})
21-Nov-2019	elabf1 6376	One implication of elabf 2662. (Contributed by BJ, 21-Nov-2019.)
⊢ Ⅎxψ    &   ⊢ (x = A → (φ → ψ))    ⇒   ⊢ (A ∈ {x ∣ φ} → ψ)
21-Nov-2019	elabgf2 6375	One implication of elabgf 2661. (Contributed by BJ, 21-Nov-2019.)
⊢ ℲxA    &   ⊢ Ⅎxψ    &   ⊢ (x = A → (ψ → φ))    ⇒   ⊢ (A ∈ B → (ψ → A ∈ {x ∣ φ}))
21-Nov-2019	elabgf1 6374	One implication of elabgf 2661. (Contributed by BJ, 21-Nov-2019.)
⊢ ℲxA    &   ⊢ Ⅎxψ    &   ⊢ (x = A → (φ → ψ))    ⇒   ⊢ (A ∈ {x ∣ φ} → ψ)
21-Nov-2019	elabgft1 6373	One implication of elabgf 2661, in closed form. (Contributed by BJ, 21-Nov-2019.)
⊢ ℲxA    &   ⊢ Ⅎxψ    ⇒   ⊢ (∀x(x = A → (φ → ψ)) → (A ∈ {x ∣ φ} → ψ))
21-Nov-2019	elabgf0 6372	Lemma for elabgf 2661. (Contributed by BJ, 21-Nov-2019.)
⊢ (x = A → (A ∈ {x ∣ φ} ↔ φ))
21-Nov-2019	bj-vtoclgf 6371	Weakening two hypotheses of vtoclgf 2588. (Contributed by BJ, 21-Nov-2019.)
⊢ ℲxA    &   ⊢ Ⅎxψ    &   ⊢ (x = A → φ)    &   ⊢ (x = A → (φ → ψ))    ⇒   ⊢ (A ∈ 𝑉 → ψ)
21-Nov-2019	bj-vtoclgft 6370	Weakening two hypotheses of vtoclgf 2588. (Contributed by BJ, 21-Nov-2019.)
⊢ ℲxA    &   ⊢ Ⅎxψ    &   ⊢ (x = A → φ)    ⇒   ⊢ (∀x(x = A → (φ → ψ)) → (A ∈ 𝑉 → ψ))
21-Nov-2019	bj-exlimmpi 6369	Lemma for bj-vtoclgf 6371. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
⊢ Ⅎxψ    &   ⊢ (χ → φ)    &   ⊢ (χ → (φ → ψ))    ⇒   ⊢ (∃xχ → ψ)
21-Nov-2019	bj-exlimmp 6368	Lemma for bj-vtoclgf 6371. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
⊢ Ⅎxψ    &   ⊢ (χ → φ)    ⇒   ⊢ (∀x(χ → (φ → ψ)) → (∃xχ → ψ))
20-Nov-2019	mulnq0mo 6289	There is at most one result from multiplying non-negative fractions. (Contributed by Jim Kingdon, 20-Nov-2019.)
⊢ ((A ∈ ((𝜔 × N) / ~Q0 ) ∧ B ∈ ((𝜔 × N) / ~Q0 )) → ∃*z∃w∃v∃u∃𝑡((A = [⟨w, v⟩] ~Q0 ∧ B = [⟨u, 𝑡⟩] ~Q0 ) ∧ z = [⟨(w ·𝑜 u), (v ·𝑜 𝑡)⟩] ~Q0 ))
20-Nov-2019	mulcmpblnq0 6285	Lemma showing compatibility of multiplication on non-negative fractions. (Contributed by Jim Kingdon, 20-Nov-2019.)
⊢ ((((A ∈ 𝜔 ∧ B ∈ N) ∧ (𝐶 ∈ 𝜔 ∧ 𝐷 ∈ N)) ∧ ((𝐹 ∈ 𝜔 ∧ 𝐺 ∈ N) ∧ (𝑅 ∈ 𝜔 ∧ 𝑆 ∈ N))) → (((A ·𝑜 𝐷) = (B ·𝑜 𝐶) ∧ (𝐹 ·𝑜 𝑆) = (𝐺 ·𝑜 𝑅)) → ⟨(A ·𝑜 𝐹), (B ·𝑜 𝐺)⟩ ~Q0 ⟨(𝐶 ·𝑜 𝑅), (𝐷 ·𝑜 𝑆)⟩))
19-Nov-2019	bj-nn0suc 6523	Proof of nn0suc 4252. NOT YET constructive because of omelon 4256 (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
⊢ (A ∈ 𝜔 → (A = ∅ ∨ ∃x ∈ 𝜔 A = suc x))
19-Nov-2019	bj-nn0suc0 6517	Constructive proof of an adaptation of nn0suc 4252. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
⊢ ∀x ∈ 𝜔 (x = ∅ ∨ ∃y ∈ x x = suc y)
19-Nov-2019	speano5 6511	Version of peano5 4246 when A is assumed to be a set, allowing a proof from the core axioms of CZF. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
⊢ ((A ∈ 𝑉 ∧ ∅ ∈ A ∧ ∀x ∈ 𝜔 (x ∈ A → suc x ∈ A)) → 𝜔 ⊆ A)
19-Nov-2019	bdpeano5 6510	Bounded version of peano5 4246. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
⊢ BOUNDED A    ⇒   ⊢ ((∅ ∈ A ∧ ∀x ∈ 𝜔 (x ∈ A → suc x ∈ A)) → 𝜔 ⊆ A)
19-Nov-2019	peano5set 6509	Version of peano5 4246 when 𝜔 ∩ A is assumed to be a set, allowing a proof from the core axioms of CZF. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
⊢ ((𝜔 ∩ A) ∈ 𝑉 → ((∅ ∈ A ∧ ∀x ∈ 𝜔 (x ∈ A → suc x ∈ A)) → 𝜔 ⊆ A))
19-Nov-2019	bj-inex 6474	The intersection of two sets is a set, from bounded separation. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → (A ∩ B) ∈ V)
19-Nov-2019	bdrabexg 6473	Bounded version of rabexg 3873. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
⊢ BOUNDED φ    &   ⊢ BOUNDED A    ⇒   ⊢ (A ∈ 𝑉 → {x ∈ A ∣ φ} ∈ V)
19-Nov-2019	bds 6426	Boundedness of a formula resulting from implicit substitution in a bounded formula. Note that the proof does not use ax-bdsb 6398; therefore, using implicit instead of explicit substitution when boundedness is important, one might avoid using ax-bdsb 6398. (Contributed by BJ, 19-Nov-2019.)
⊢ BOUNDED φ    &   ⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ BOUNDED ψ
19-Nov-2019	mulnnnq0 6291	Multiplication of non-negative fractions in terms of natural numbers. (Contributed by Jim Kingdon, 19-Nov-2019.)
⊢ (((A ∈ 𝜔 ∧ B ∈ N) ∧ (𝐶 ∈ 𝜔 ∧ 𝐷 ∈ N)) → ([⟨A, B⟩] ~Q0 ·Q0 [⟨𝐶, 𝐷⟩] ~Q0 ) = [⟨(A ·𝑜 𝐶), (B ·𝑜 𝐷)⟩] ~Q0 )
18-Nov-2019	bj-peano2 6503	Constructive proof of peano2 4243. Temporary note: another possibility is to simply replace sucexg 4172 with bj-sucexg 6489 in the proof of peano2 4243. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
⊢ (A ∈ 𝜔 → suc A ∈ 𝜔)
18-Nov-2019	bj-intnexr 6476	vnex 3863 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
⊢ (∩ A = V → ¬ ∩ A ∈ V)
18-Nov-2019	bj-intexr 6475	vnex 3863 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
⊢ (∩ A ∈ V → A ≠ ∅)
18-Nov-2019	bj-vnex 6465	vnex 3863 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
⊢ ¬ ∃x x = V
18-Nov-2019	bj-nvel 6464	nvel 3862 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
⊢ ¬ V ∈ A
18-Nov-2019	bj-vprc 6463	vprc 3861 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
⊢ ¬ V ∈ V
18-Nov-2019	bj-nalset 6462	nalset 3860 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
⊢ ¬ ∃x∀y y ∈ x
18-Nov-2019	nqnq0 6282	A positive fraction is a non-negative fraction. (Contributed by Jim Kingdon, 18-Nov-2019.)
⊢ Q ⊆ Q0
18-Nov-2019	nq0ex 6281	The class of positive fractions exists. (Contributed by Jim Kingdon, 18-Nov-2019.)
⊢ Q0 ∈ V
18-Nov-2019	enq0ex 6280	The equivalence relation for positive fractions exists. (Contributed by Jim Kingdon, 18-Nov-2019.)
⊢ ~Q0 ∈ V
14-Nov-2019	ax-infc2 6508	Another axiom of infinity in a constructive setting (see ax-infc 6504). (Contributed by BJ, 14-Nov-2019.)
⊢ ∃𝑎∀x(x ∈ 𝑎 ↔ (x = ∅ ∨ ∃y ∈ 𝑎 x = suc y))
14-Nov-2019	bj-omexALT 6507	Alternate proof of bj-omex 6506. (Contributed by BJ, 14-Nov-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜔 ∈ V