 Intuitionistic Logic Explorer Most Recent Proofs Mirrors  >  Home  >  ILE Home  >  Th. List  >  Recent MPE Most Recent             Other  >  MM 100

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.

 Color key: Intuitionistic Logic Explorer User Mathboxes

Last updated on 5-Dec-2019 at 7:17 PM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem

3-Dec-2019addassnq0lemcl 6302 A natural number closure law. Lemma for addassnq0 6303. (Contributed by Jim Kingdon, 3-Dec-2019.)
(((𝐼 𝜔 𝐽 N) (𝐾 𝜔 𝐿 N)) → (((𝐼 ·𝑜 𝐿) +𝑜 (𝐽 ·𝑜 𝐾)) 𝜔 (𝐽 ·𝑜 𝐿) N))

3-Dec-2019nndir 5979 Distributive law for natural numbers (right-distributivity). (Contributed by Jim Kingdon, 3-Dec-2019.)
((A 𝜔 B 𝜔 𝐶 𝜔) → ((A +𝑜 B) ·𝑜 𝐶) = ((A ·𝑜 𝐶) +𝑜 (B ·𝑜 𝐶)))

1-Dec-2019nnanq0 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-2019archnqq 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 Qx N A <Q [⟨x, 1𝑜⟩] ~Q )

30-Nov-2019bj-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 yxy)))

30-Nov-2019bj-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 xAx))))

30-Nov-2019bj-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-2019bj-omind 6499 𝜔 is an inductive class. (Contributed by BJ, 30-Nov-2019.)
Ind 𝜔

30-Nov-2019bj-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-2019bj-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-2019bj-indeq 6496 Equality property for Ind. (Contributed by BJ, 30-Nov-2019.)
(A = B → (Ind A ↔ Ind B))

30-Nov-2019bj-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-2019df-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-2019bj-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.)
(φ → (ψAB))    &   (φ → (χBA))       (φ → ((ψ χ) ↔ A = B))

30-Nov-2019nqpnq0nq 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-2019mulclnq0 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-2019prarloclemarch 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-2019bj-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-2019bj-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-2019bj-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-2019nq02m 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-2019distnq0r 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-2019addassnq0 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-2019addclnq0 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-2019mulcanenq0ec 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-2019ax-bdsetind 6527 Axiom of bounded set induction. (Contributed by BJ, 28-Nov-2019.)
BOUNDED φ       (𝑎(y 𝑎 [y / 𝑎]φφ) → 𝑎φ)

28-Nov-2019bj-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 BA = B))

28-Nov-2019bj-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-2019mulcomnq0 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-2019distrnq0 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-2019prcunqu 6324 An upper cut is closed upwards under the positive fractions. (Contributed by Jim Kingdon, 25-Nov-2019.)
((⟨𝐿, 𝑈 P 𝐶 𝑈) → (𝐶 <Q BB 𝑈))

25-Nov-2019prarloclemarch2 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-2019subhalfnqq 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 Qx Q (x +Q x) <Q A)

24-Nov-2019bj-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-2019bj-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-2019bj-findeslem0 6528 Lemma for bj-findes . (Contributed by BJ, 24-Nov-2019.) (Proof modification is discouraged.)
(ψ ↔ (x 𝜔 → φ))       ([∅ / x]φ[∅ / x]ψ)

24-Nov-2019bj-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-2019bdcriota 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-2019nq0nn 6283 Decomposition of a non-negative fraction into numerator and denominator. (Contributed by Jim Kingdon, 24-Nov-2019.)
(A Q0wv((w 𝜔 v N) A = [⟨w, v⟩] ~Q0 ))

24-Nov-2019enq0eceq 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-2019dfplq0qs 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 )) wvuf((x = [⟨w, v⟩] ~Q0 y = [⟨u, f⟩] ~Q0 ) z = [⟨((w ·𝑜 f) +𝑜 (v ·𝑜 u)), (v ·𝑜 f)⟩] ~Q0 ))}

23-Nov-2019addnq0mo 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 )) → ∃*zwvu𝑡((A = [⟨w, v⟩] ~Q0 B = [⟨u, 𝑡⟩] ~Q0 ) z = [⟨((w ·𝑜 𝑡) +𝑜 (v ·𝑜 u)), (v ·𝑜 𝑡)⟩] ~Q0 ))

23-Nov-2019nnnq0lem1 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-2019addcmpblnq0 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-2019ee8anv 1793 Rearrange existential quantifiers. (Contributed by Jim Kingdon, 23-Nov-2019.)
(xyzwvu𝑡𝑠(φ ψ) ↔ (xyzwφ vu𝑡𝑠ψ))

23-Nov-201919.42vvvv 1773 Theorem 19.42 of [Margaris] p. 90 with 4 quantifiers. (Contributed by Jim Kingdon, 23-Nov-2019.)
(wxyz(φ ψ) ↔ (φ wxyzψ))

22-Nov-2019setindis 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-2019setindf 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-2019setindft 6524 Axiom of set-induction with a DV condition replaced with a non-freeness hypothesis (Contributed by BJ, 22-Nov-2019.)
(xyφ → (x(y x [y / x]φφ) → xφ))

22-Nov-2019bj-nntrans2 6519 A natural number is a transitive set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
(A 𝜔 → (B ABA))

22-Nov-2019bj-nntrans 6518 A natural number is a transitive set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
(A 𝜔 → x A xA)

22-Nov-2019bdfind 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-2019findset 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-2019cbvrald 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-2019addnnnq0 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-2019dfmq0qs 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 )) wvuf((x = [⟨w, v⟩] ~Q0 y = [⟨u, f⟩] ~Q0 ) z = [⟨(w ·𝑜 u), (v ·𝑜 f)⟩] ~Q0 ))}

21-Nov-2019bj-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-2019bj-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-2019bj-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-2019bdeqsuc 6492 Boundedness lemma. (Contributed by BJ, 21-Nov-2019.)
BOUNDED x = suc y

21-Nov-2019bdeq0 6491 Boundedness lemma. (Contributed by BJ, 21-Nov-2019.)
BOUNDED x = ∅

21-Nov-2019bdop 6448 The ordered pair of two setvars is a bounded class. (Contributed by BJ, 21-Nov-2019.)
BOUNDEDx, y

21-Nov-2019bj-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-2019bj-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-2019elabg2 6380 One implication of elabg 2664. (Contributed by BJ, 21-Nov-2019.)
(x = A → (ψφ))       (A 𝑉 → (ψA {xφ}))

21-Nov-2019elab2a 6379 One implication of elab 2663. (Contributed by BJ, 21-Nov-2019.)
A V    &   (x = A → (ψφ))       (ψA {xφ})

21-Nov-2019elab1 6378 One implication of elab 2663. (Contributed by BJ, 21-Nov-2019.)
(x = A → (φψ))       (A {xφ} → ψ)

21-Nov-2019elabf2 6377 One implication of elabf 2662. (Contributed by BJ, 21-Nov-2019.)
xψ    &   A V    &   (x = A → (ψφ))       (ψA {xφ})

21-Nov-2019elabf1 6376 One implication of elabf 2662. (Contributed by BJ, 21-Nov-2019.)
xψ    &   (x = A → (φψ))       (A {xφ} → ψ)

21-Nov-2019elabgf2 6375 One implication of elabgf 2661. (Contributed by BJ, 21-Nov-2019.)
xA    &   xψ    &   (x = A → (ψφ))       (A B → (ψA {xφ}))

21-Nov-2019elabgf1 6374 One implication of elabgf 2661. (Contributed by BJ, 21-Nov-2019.)
xA    &   xψ    &   (x = A → (φψ))       (A {xφ} → ψ)

21-Nov-2019elabgft1 6373 One implication of elabgf 2661, in closed form. (Contributed by BJ, 21-Nov-2019.)
xA    &   xψ       (x(x = A → (φψ)) → (A {xφ} → ψ))

21-Nov-2019elabgf0 6372 Lemma for elabgf 2661. (Contributed by BJ, 21-Nov-2019.)
(x = A → (A {xφ} ↔ φ))

21-Nov-2019bj-vtoclgf 6371 Weakening two hypotheses of vtoclgf 2588. (Contributed by BJ, 21-Nov-2019.)
xA    &   xψ    &   (x = Aφ)    &   (x = A → (φψ))       (A 𝑉ψ)

21-Nov-2019bj-vtoclgft 6370 Weakening two hypotheses of vtoclgf 2588. (Contributed by BJ, 21-Nov-2019.)
xA    &   xψ    &   (x = Aφ)       (x(x = A → (φψ)) → (A 𝑉ψ))

21-Nov-2019bj-exlimmpi 6369 Lemma for bj-vtoclgf 6371. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
xψ    &   (χφ)    &   (χ → (φψ))       (xχψ)

21-Nov-2019bj-exlimmp 6368 Lemma for bj-vtoclgf 6371. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
xψ    &   (χφ)       (x(χ → (φψ)) → (xχψ))

20-Nov-2019mulnq0mo 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 )) → ∃*zwvu𝑡((A = [⟨w, v⟩] ~Q0 B = [⟨u, 𝑡⟩] ~Q0 ) z = [⟨(w ·𝑜 u), (v ·𝑜 𝑡)⟩] ~Q0 ))

20-Nov-2019mulcmpblnq0 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-2019bj-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-2019bj-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-2019speano5 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-2019bdpeano5 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-2019peano5set 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-2019bj-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 𝑊) → (AB) V)

19-Nov-2019bdrabexg 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-2019bds 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-2019mulnnnq0 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-2019bj-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-2019bj-intnexr 6476 vnex 3863 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
( A = V → ¬ A V)

18-Nov-2019bj-intexr 6475 vnex 3863 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
( A V → A ≠ ∅)

18-Nov-2019bj-vnex 6465 vnex 3863 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
¬ x x = V

18-Nov-2019bj-nvel 6464 nvel 3862 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
¬ V A

18-Nov-2019bj-vprc 6463 vprc 3861 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
¬ V V

18-Nov-2019bj-nalset 6462 nalset 3860 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
¬ xy y x

18-Nov-2019nqnq0 6282 A positive fraction is a non-negative fraction. (Contributed by Jim Kingdon, 18-Nov-2019.)
QQ0

18-Nov-2019nq0ex 6281 The class of positive fractions exists. (Contributed by Jim Kingdon, 18-Nov-2019.)
Q0 V

18-Nov-2019enq0ex 6280 The equivalence relation for positive fractions exists. (Contributed by Jim Kingdon, 18-Nov-2019.)
~Q0 V

14-Nov-2019ax-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-2019bj-omexALT 6507 Alternate proof of bj-omex 6506. (Contributed by BJ, 14-Nov-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
𝜔 V

 Copyright terms: Public domain W3C HTML validation [external]