 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 21-Jan-2020 at 12:30 AM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem

((A B ℂ) → (A + B) = (B + A))

17-Jan-2020ax-addcom 6590 Addition commutes. Axiom for real and complex numbers, justified by theorem axaddcom 6564. Proofs should normally use addcom 6737 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 17-Jan-2020.)
((A B ℂ) → (A + B) = (B + A))

17-Jan-2020axaddcom 6564 Addition commutes. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addcom 6590 be used later. Instead, use addcom 6737.

In the Metamath Proof Explorer this is not a complex number axiom but is instead proved from other axioms. That proof relies on real number trichotomy and it is not known whether it is possible to prove this from the other axioms without it. (Contributed by Jim Kingdon, 17-Jan-2020.) (New usage is discouraged.)

((A B ℂ) → (A + B) = (B + A))

16-Jan-2020addid1 6738 0 is an additive identity. (Contributed by Jim Kingdon, 16-Jan-2020.)
(A ℂ → (A + 0) = A)

16-Jan-2020ax-0id 6598 0 is an identity element for real addition. Axiom for real and complex numbers, justified by theorem ax0id 6572.

Proofs should normally use addid1 6738 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.)

(A ℂ → (A + 0) = A)

16-Jan-2020ax0id 6572 0 is an identity element for real addition. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-0id 6598.

In the Metamath Proof Explorer this is not a complex number axiom but is instead proved from other axioms. That proof relies on excluded middle and it is not known whether it is possible to prove this from the other axioms without excluded middle. (Contributed by Jim Kingdon, 16-Jan-2020.) (New usage is discouraged.)

(A ℂ → (A + 0) = A)

15-Jan-2020axltwlin 6688 Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltwlin 6603 with ordering on the extended reals. (Contributed by Jim Kingdon, 15-Jan-2020.)
((A B 𝐶 ℝ) → (A < B → (A < 𝐶 𝐶 < B)))

15-Jan-2020axltirr 6687 Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltirr 6602 with ordering on the extended reals. New proofs should use ltnr 6695 instead for naming consistency. (New usage is discouraged.) (Contributed by Jim Kingdon, 15-Jan-2020.)
(A ℝ → ¬ A < A)

14-Jan-20202pwuninelg 5820 The power set of the power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set. (Contributed by Jim Kingdon, 14-Jan-2020.)
(A 𝑉 → ¬ 𝒫 𝒫 A A)

13-Jan-20201re 6628 1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.)
1

13-Jan-2020ax-1re 6584 1 is a real number. Axiom for real and complex numbers, justified by theorem ax1re 6558. Proofs should use 1re 6628 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.)
1

13-Jan-2020ax1re 6558 1 is a real number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1re 6584.

In the Metamath Proof Explorer, this is not a complex number axiom but is proved from ax-1cn 6583 and the other axioms. It is not known whether we can do so here, but the Metamath Proof Explorer proof (accessed 13-Jan-2020) uses excluded middle. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.)

1

12-Jan-2020ax-pre-ltwlin 6603 Real number less-than is weakly linear. Axiom for real and complex numbers, justified by theorem axpre-ltwlin 6577. (Contributed by Jim Kingdon, 12-Jan-2020.)
((A B 𝐶 ℝ) → (A < B → (A < 𝐶 𝐶 < B)))

12-Jan-2020ax-pre-ltirr 6602 Real number less-than is irreflexive. Axiom for real and complex numbers, justified by theorem ax-pre-ltirr 6602. (Contributed by Jim Kingdon, 12-Jan-2020.)
(A ℝ → ¬ A < A)

12-Jan-2020ax-precex 6600 Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by theorem axprecex 6574.

In treatments which assume excluded middle, the 0 < A condition is generally replaced by A ≠ 0. (Contributed by Jim Kingdon, 12-Jan-2020.)

((A 0 < A) → x ℝ (A · x) = 1)

12-Jan-2020ax-0lt1 6596 0 is less than 1. Axiom for real and complex numbers, justified by theorem ax0lt1 6570. (Contributed by Jim Kingdon, 12-Jan-2020.)
0 < 1

12-Jan-2020axpre-ltwlin 6577 Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltwlin 6603. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
((A B 𝐶 ℝ) → (A < B → (A < 𝐶 𝐶 < B)))

12-Jan-2020axpre-ltirr 6576 Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltirr 6602. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
(A ℝ → ¬ A < A)

12-Jan-2020axprecex 6574 Existence of reciprocal of positive real number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-precex 6600.

In treatments which assume excluded middle, the 0 < A condition is generally replaced by A ≠ 0. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)

((A 0 < A) → x ℝ (A · x) = 1)

12-Jan-2020ax0lt1 6570 0 is less than 1. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-0lt1 6596.

The version of this axiom in the Metamath Proof Explorer reads 1 ≠ 0; here we change it to 0 < 1. The proof of 0 < 1 from 1 ≠ 0 in the Metamath Proof Explorer (accessed 12-Jan-2020) relies on real number trichotomy. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)

0 < 1

8-Jan-2020ecidg 6081 A set is equal to its converse epsilon coset. (Note: converse epsilon is not an equivalence relation.) (Contributed by Jim Kingdon, 8-Jan-2020.)
(A 𝑉 → [A] E = A)

5-Jan-20201idsr 6515 1 is an identity element for multiplication. (Contributed by Jim Kingdon, 5-Jan-2020.)
(A R → (A ·R 1R) = A)

4-Jan-2020distrsrg 6506 Multiplication of signed reals is distributive. (Contributed by Jim Kingdon, 4-Jan-2020.)
((A R B R 𝐶 R) → (A ·R (B +R 𝐶)) = ((A ·R B) +R (A ·R 𝐶)))

3-Jan-2020mulasssrg 6505 Multiplication of signed reals is associative. (Contributed by Jim Kingdon, 3-Jan-2020.)
((A R B R 𝐶 R) → ((A ·R B) ·R 𝐶) = (A ·R (B ·R 𝐶)))

3-Jan-2020mulcomsrg 6504 Multiplication of signed reals is commutative. (Contributed by Jim Kingdon, 3-Jan-2020.)
((A R B R) → (A ·R B) = (B ·R A))

3-Jan-2020addasssrg 6503 Addition of signed reals is associative. (Contributed by Jim Kingdon, 3-Jan-2020.)
((A R B R 𝐶 R) → ((A +R B) +R 𝐶) = (A +R (B +R 𝐶)))

3-Jan-2020addcomsrg 6502 Addition of signed reals is commutative. (Contributed by Jim Kingdon, 3-Jan-2020.)
((A R B R) → (A +R B) = (B +R A))

3-Jan-2020caovlem2d 5616 Rearrangement of expression involving multiplication (𝐺) and addition (𝐹). (Contributed by Jim Kingdon, 3-Jan-2020.)
((φ (x 𝑆 y 𝑆)) → (x𝐺y) = (y𝐺x))    &   ((φ (x 𝑆 y 𝑆 z 𝑆)) → ((x𝐹y)𝐺z) = ((x𝐺z)𝐹(y𝐺z)))    &   ((φ (x 𝑆 y 𝑆 z 𝑆)) → ((x𝐺y)𝐺z) = (x𝐺(y𝐺z)))    &   ((φ (x 𝑆 y 𝑆)) → (x𝐺y) 𝑆)    &   (φA 𝑆)    &   (φB 𝑆)    &   (φ𝐶 𝑆)    &   (φ𝐷 𝑆)    &   (φ𝐻 𝑆)    &   (φ𝑅 𝑆)    &   ((φ (x 𝑆 y 𝑆)) → (x𝐹y) = (y𝐹x))    &   ((φ (x 𝑆 y 𝑆 z 𝑆)) → ((x𝐹y)𝐹z) = (x𝐹(y𝐹z)))    &   ((φ (x 𝑆 y 𝑆)) → (x𝐹y) 𝑆)       (φ → ((((A𝐺𝐶)𝐹(B𝐺𝐷))𝐺𝐻)𝐹(((A𝐺𝐷)𝐹(B𝐺𝐶))𝐺𝑅)) = ((A𝐺((𝐶𝐺𝐻)𝐹(𝐷𝐺𝑅)))𝐹(B𝐺((𝐶𝐺𝑅)𝐹(𝐷𝐺𝐻)))))

2-Jan-2020bj-d0clsepcl 7148 Δ0-classical logic and separation implies classical logic. (Contributed by BJ, 2-Jan-2020.) (Proof modification is discouraged.)
(φ ¬ φ)

2-Jan-2020ax-bj-d0cl 7147 Axiom for Δ0-classical logic. (Contributed by BJ, 2-Jan-2020.)
BOUNDED φ       (φ ¬ φ)

1-Jan-2020mulcmpblnrlemg 6487 Lemma used in lemma showing compatibility of multiplication. (Contributed by Jim Kingdon, 1-Jan-2020.)
((((A P B P) (𝐶 P 𝐷 P)) ((𝐹 P 𝐺 P) (𝑅 P 𝑆 P))) → (((A +P 𝐷) = (B +P 𝐶) (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → ((𝐷 ·P 𝐹) +P (((A ·P 𝐹) +P (B ·P 𝐺)) +P ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅)))) = ((𝐷 ·P 𝐹) +P (((A ·P 𝐺) +P (B ·P 𝐹)) +P ((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆))))))

31-Dec-2019eceq1d 6053 Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.)
(φA = B)       (φ → [A]𝐶 = [B]𝐶)

30-Dec-2019mulsrmo 6491 There is at most one result from multiplying signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.)
((A ((P × P) / ~R ) B ((P × P) / ~R )) → ∃*zwvu𝑡((A = [⟨w, v⟩] ~R B = [⟨u, 𝑡⟩] ~R ) z = [⟨((w ·P u) +P (v ·P 𝑡)), ((w ·P 𝑡) +P (v ·P u))⟩] ~R ))

30-Dec-2019addsrmo 6490 There is at most one result from adding signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.)
((A ((P × P) / ~R ) B ((P × P) / ~R )) → ∃*zwvu𝑡((A = [⟨w, v⟩] ~R B = [⟨u, 𝑡⟩] ~R ) z = [⟨(w +P u), (v +P 𝑡)⟩] ~R ))

30-Dec-2019prsrlem1 6489 Decomposing signed reals into positive reals. Lemma for addsrpr 6492 and mulsrpr 6493. (Contributed by Jim Kingdon, 30-Dec-2019.)
(((A ((P × P) / ~R ) B ((P × P) / ~R )) ((A = [⟨w, v⟩] ~R B = [⟨u, 𝑡⟩] ~R ) (A = [⟨𝑠, f⟩] ~R B = [⟨g, ⟩] ~R ))) → ((((w P v P) (𝑠 P f P)) ((u P 𝑡 P) (g P P))) ((w +P f) = (v +P 𝑠) (u +P ) = (𝑡 +P g))))

29-Dec-2019bj-omelon 7181 The set 𝜔 is an ordinal. Constructive proof of omelon 4258. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.)
𝜔 On

29-Dec-2019bj-omord 7180 The set 𝜔 is an ordinal. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.)
Ord 𝜔

29-Dec-2019bj-omtrans2 7179 The set 𝜔 is transitive. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.)
Tr 𝜔

29-Dec-2019bj-omtrans 7178 The set 𝜔 is transitive. A natural number is included in 𝜔.

The idea is to use bounded induction with the formula x ⊆ 𝜔. This formula, in a logic with terms, is bounded. So in our logic without terms, we need to temporarily replace it with x𝑎 and then deduce the original claim. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.)

(A 𝜔 → A ⊆ 𝜔)

29-Dec-2019ltrnqg 6277 Ordering property of reciprocal for positive fractions. For a simplified version of the forward implication, see ltrnqi 6278. (Contributed by Jim Kingdon, 29-Dec-2019.)
((A Q B Q) → (A <Q B ↔ (*QB) <Q (*QA)))

29-Dec-2019rec1nq 6254 Reciprocal of positive fraction one. (Contributed by Jim Kingdon, 29-Dec-2019.)
(*Q‘1Q) = 1Q

28-Dec-2019recexprlemupu 6462 The upper cut of B is upper. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 28-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       ((A P 𝑟 Q) → (𝑞 Q (𝑞 <Q 𝑟 𝑞 (2ndB)) → 𝑟 (2ndB)))

28-Dec-2019recexprlemopu 6461 The upper cut of B is open. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 28-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       ((A P 𝑟 Q 𝑟 (2ndB)) → 𝑞 Q (𝑞 <Q 𝑟 𝑞 (2ndB)))

28-Dec-2019recexprlemlol 6460 The lower cut of B is lower. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 28-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       ((A P 𝑞 Q) → (𝑟 Q (𝑞 <Q 𝑟 𝑟 (1stB)) → 𝑞 (1stB)))

28-Dec-2019recexprlemopl 6459 The lower cut of B is open. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 28-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       ((A P 𝑞 Q 𝑞 (1stB)) → 𝑟 Q (𝑞 <Q 𝑟 𝑟 (1stB)))

28-Dec-2019prmuloc2 6411 Positive reals are multiplicatively located. This is a variation of prmuloc 6410 which only constructs one (named) point and is therefore often easier to work with. It states that given a ratio B, there are elements of the lower and upper cut which have exactly that ratio between them. (Contributed by Jim Kingdon, 28-Dec-2019.)
((⟨𝐿, 𝑈 P 1Q <Q B) → x 𝐿 (x ·Q B) 𝑈)

28-Dec-20191pru 6406 The upper cut of the positive real number 'one'. (Contributed by Jim Kingdon, 28-Dec-2019.)
(2nd ‘1P) = {x ∣ 1Q <Q x}

28-Dec-20191prl 6405 The lower cut of the positive real number 'one'. (Contributed by Jim Kingdon, 28-Dec-2019.)
(1st ‘1P) = {xx <Q 1Q}

27-Dec-2019recexprlemex 6471 B is the reciprocal of A. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P → (A ·P B) = 1P)

27-Dec-2019recexprlemss1u 6470 The upper cut of A ·P B is a subset of the upper cut of one. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P → (2nd ‘(A ·P B)) ⊆ (2nd ‘1P))

27-Dec-2019recexprlemss1l 6469 The lower cut of A ·P B is a subset of the lower cut of one. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P → (1st ‘(A ·P B)) ⊆ (1st ‘1P))

27-Dec-2019recexprlem1ssu 6468 The upper cut of one is a subset of the upper cut of A ·P B. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P → (2nd ‘1P) ⊆ (2nd ‘(A ·P B)))

27-Dec-2019recexprlem1ssl 6467 The lower cut of one is a subset of the lower cut of A ·P B. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P → (1st ‘1P) ⊆ (1st ‘(A ·P B)))

27-Dec-2019recexprlempr 6466 B is a positive real. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A PB P)

27-Dec-2019recexprlemloc 6465 B is located. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 (1stB) 𝑟 (2ndB))))

27-Dec-2019recexprlemdisj 6464 B is disjoint. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P𝑞 Q ¬ (𝑞 (1stB) 𝑞 (2ndB)))

27-Dec-2019recexprlemrnd 6463 B is rounded. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P → (𝑞 Q (𝑞 (1stB) ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 (1stB))) 𝑟 Q (𝑟 (2ndB) ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 (2ndB)))))

27-Dec-2019recexprlemm 6458 B is inhabited. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (A P → (𝑞 Q 𝑞 (1stB) 𝑟 Q 𝑟 (2ndB)))

27-Dec-2019recexprlemelu 6457 Membership in the upper cut of B. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (𝐶 (2ndB) ↔ y(y <Q 𝐶 (*Qy) (1stA)))

27-Dec-2019recexprlemell 6456 Membership in the lower cut of B. Lemma for recexpr 6472. (Contributed by Jim Kingdon, 27-Dec-2019.)
B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩       (𝐶 (1stB) ↔ y(𝐶 <Q y (*Qy) (2ndA)))

26-Dec-2019ltaprg 6455 Ordering property of addition. Proposition 9-3.5(v) of [Gleason] p. 123. Part of Definition 11.2.7(vi) of [HoTT]], p. (varies). (Contributed by Jim Kingdon, 26-Dec-2019.)
((A P B P 𝐶 P) → (A<P B ↔ (𝐶 +P A)<P (𝐶 +P B)))

26-Dec-2019prarloc2 6358 A Dedekind cut is arithmetically located. This is a variation of prarloc 6357 which only constructs one (named) point and is therefore often easier to work with. It states that given a tolerance 𝑃, there are elements of the lower and upper cut which are exactly that tolerance from each other. (Contributed by Jim Kingdon, 26-Dec-2019.)
((⟨𝐿, 𝑈 P 𝑃 Q) → 𝑎 𝐿 (𝑎 +Q 𝑃) 𝑈)

(((A P B P 𝐶 P) (A +P B) = (A +P 𝐶)) → (2ndB) ⊆ (2nd𝐶))

(((A P B P 𝐶 P) (A +P B) = (A +P 𝐶)) → (1stB) ⊆ (1st𝐶))

24-Dec-2019addcanprg 6453 Addition cancellation law for positive reals. Proposition 9-3.5(vi) of [Gleason] p. 123. (Contributed by Jim Kingdon, 24-Dec-2019.)
((A P B P 𝐶 P) → ((A +P B) = (A +P 𝐶) → B = 𝐶))

23-Dec-2019ltprordil 6428 If a positive real is less than a second positive real, its lower cut is a subset of the second's lower cut. (Contributed by Jim Kingdon, 23-Dec-2019.)
(A<P B → (1stA) ⊆ (1stB))

22-Dec-2019bj-findis 7197 Principle of induction, using implicit substitutions (the biconditional versions of the hypotheses are implicit substitutions, and we have weakened them to implications). Constructive proof (from CZF). See bj-bdfindis 7169 for a bounded version not requiring ax-setind 4204. See finds 4250 for a proof in IZF. From this version, it is easy to prove of finds 4250, finds2 4251, finds1 4252. (Contributed by BJ, 22-Dec-2019.) (Proof modification is discouraged.)
xψ    &   xχ    &   xθ    &   (x = ∅ → (ψφ))    &   (x = y → (φχ))    &   (x = suc y → (θφ))       ((ψ y 𝜔 (χθ)) → x 𝜔 φ)

21-Dec-2019ltexprlemupu 6441 The upper cut of our constructed difference is upper. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 21-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       ((A<P B 𝑟 Q) → (𝑞 Q (𝑞 <Q 𝑟 𝑞 (2nd𝐶)) → 𝑟 (2nd𝐶)))

21-Dec-2019ltexprlemopu 6440 The upper cut of our constructed difference is open. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 21-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       ((A<P B 𝑟 Q 𝑟 (2nd𝐶)) → 𝑞 Q (𝑞 <Q 𝑟 𝑞 (2nd𝐶)))

21-Dec-2019ltexprlemlol 6439 The lower cut of our constructed difference is lower. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 21-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       ((A<P B 𝑞 Q) → (𝑟 Q (𝑞 <Q 𝑟 𝑟 (1st𝐶)) → 𝑞 (1st𝐶)))

21-Dec-2019ltexprlemopl 6438 The lower cut of our constructed difference is open. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 21-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       ((A<P B 𝑞 Q 𝑞 (1st𝐶)) → 𝑟 Q (𝑞 <Q 𝑟 𝑟 (1st𝐶)))

21-Dec-2019ltexprlemelu 6436 Element in upper cut of the constructed difference. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 21-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (𝑟 (2nd𝐶) ↔ (𝑟 Q y(y (1stA) (y +Q 𝑟) (2ndB))))

21-Dec-2019ltexprlemell 6435 Element in lower cut of the constructed difference. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 21-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (𝑞 (1st𝐶) ↔ (𝑞 Q y(y (2ndA) (y +Q 𝑞) (1stB))))

17-Dec-2019ltexprlemru 6449 Lemma for ltexpri 6450. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (A<P B → (2ndB) ⊆ (2nd ‘(A +P 𝐶)))

17-Dec-2019ltexprlemfu 6448 Lemma for ltexpri 6450. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (A<P B → (2nd ‘(A +P 𝐶)) ⊆ (2ndB))

17-Dec-2019ltexprlemrl 6447 Lemma for ltexpri 6450. Reverse directon of our result for lower cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (A<P B → (1stB) ⊆ (1st ‘(A +P 𝐶)))

17-Dec-2019ltexprlemfl 6446 Lemma for ltexpri 6450. One directon of our result for lower cuts. (Contributed by Jim Kingdon, 17-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (A<P B → (1st ‘(A +P 𝐶)) ⊆ (1stB))

17-Dec-2019ltexprlempr 6445 Our constructed difference is a positive real. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 17-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (A<P B𝐶 P)

17-Dec-2019ltexprlemloc 6444 Our constructed difference is located. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 17-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (A<P B𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 (1st𝐶) 𝑟 (2nd𝐶))))

17-Dec-2019ltexprlemdisj 6443 Our constructed difference is disjoint. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 17-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (A<P B𝑞 Q ¬ (𝑞 (1st𝐶) 𝑞 (2nd𝐶)))

17-Dec-2019ltexprlemrnd 6442 Our constructed difference is rounded. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 17-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (A<P B → (𝑞 Q (𝑞 (1st𝐶) ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 (1st𝐶))) 𝑟 Q (𝑟 (2nd𝐶) ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 (2nd𝐶)))))

17-Dec-2019ltexprlemm 6437 Our constructed difference is inhabited. Lemma for ltexpri 6450. (Contributed by Jim Kingdon, 17-Dec-2019.)
𝐶 = ⟨{x Qy(y (2ndA) (y +Q x) (1stB))}, {x Qy(y (1stA) (y +Q x) (2ndB))}⟩       (A<P B → (𝑞 Q 𝑞 (1st𝐶) 𝑟 Q 𝑟 (2nd𝐶)))

16-Dec-2019bj-sbime 7020 A strengthening of sbie 1656 (same proof). (Contributed by BJ, 16-Dec-2019.)
xψ    &   (x = y → (φψ))       ([y / x]φψ)

16-Dec-2019bj-sbimeh 7019 A strengthening of sbieh 1655 (same proof). (Contributed by BJ, 16-Dec-2019.)
(ψxψ)    &   (x = y → (φψ))       ([y / x]φψ)

16-Dec-2019bj-sbimedh 7018 A strengthening of sbiedh 1652 (same proof). (Contributed by BJ, 16-Dec-2019.)
(φxφ)    &   (φ → (χxχ))    &   (φ → (x = y → (ψχ)))       (φ → ([y / x]ψχ))

16-Dec-2019ltsopr 6433 Positive real 'less than' is a weak linear order (in the sense of df-iso 4008). Proposition 11.2.3 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 16-Dec-2019.)
<P Or P

15-Dec-2019ltpopr 6432 Positive real 'less than' is a partial ordering. Remark ("< is transitive and irreflexive") preceding Proposition 11.2.3 of [HoTT], p. (varies). Lemma for ltsopr 6433. (Contributed by Jim Kingdon, 15-Dec-2019.)
<P Po P

15-Dec-2019ltdfpr 6360 More convenient form of df-iltp 6324. (Contributed by Jim Kingdon, 15-Dec-2019.)
((A P B P) → (A<P B𝑞 Q (𝑞 (2ndA) 𝑞 (1stB))))

15-Dec-2019prdisj 6346 A Dedekind cut is disjoint. (Contributed by Jim Kingdon, 15-Dec-2019.)
((⟨𝐿, 𝑈 P A Q) → ¬ (A 𝐿 A 𝑈))

13-Dec-20191idpru 6430 Lemma for 1idpr 6431. (Contributed by Jim Kingdon, 13-Dec-2019.)
(A P → (2nd ‘(A ·P 1P)) = (2ndA))

13-Dec-20191idprl 6429 Lemma for 1idpr 6431. (Contributed by Jim Kingdon, 13-Dec-2019.)
(A P → (1st ‘(A ·P 1P)) = (1stA))

13-Dec-2019gtnqex 6403 The class of rationals greater than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.)
{xA <Q x} V

13-Dec-2019ltnqex 6402 The class of rationals less than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.)
{xx <Q A} V

13-Dec-2019sotritrieq 4036 A trichotomy relationship, given a trichotomous order. (Contributed by Jim Kingdon, 13-Dec-2019.)
𝑅 Or A    &   ((B A 𝐶 A) → (B𝑅𝐶 B = 𝐶 𝐶𝑅B))       ((B A 𝐶 A) → (B = 𝐶 ↔ ¬ (B𝑅𝐶 𝐶𝑅B)))

12-Dec-2019distrprg 6427 Multiplication of positive reals is distributive. Proposition 9-3.7(iii) of [Gleason] p. 124. (Contributed by Jim Kingdon, 12-Dec-2019.)
((A P B P 𝐶 P) → (A ·P (B +P 𝐶)) = ((A ·P B) +P (A ·P 𝐶)))

12-Dec-2019distrlem5pru 6426 Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
((A P B P 𝐶 P) → (2nd ‘((A ·P B) +P (A ·P 𝐶))) ⊆ (2nd ‘(A ·P (B +P 𝐶))))

12-Dec-2019distrlem5prl 6425 Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
((A P B P 𝐶 P) → (1st ‘((A ·P B) +P (A ·P 𝐶))) ⊆ (1st ‘(A ·P (B +P 𝐶))))

12-Dec-2019distrlem4pru 6424 Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
(((A P B P 𝐶 P) ((x (2ndA) y (2ndB)) (f (2ndA) z (2nd𝐶)))) → ((x ·Q y) +Q (f ·Q z)) (2nd ‘(A ·P (B +P 𝐶))))

12-Dec-2019distrlem4prl 6423 Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
(((A P B P 𝐶 P) ((x (1stA) y (1stB)) (f (1stA) z (1st𝐶)))) → ((x ·Q y) +Q (f ·Q z)) (1st ‘(A ·P (B +P 𝐶))))

12-Dec-2019distrlem1pru 6422 Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
((A P B P 𝐶 P) → (2nd ‘(A ·P (B +P 𝐶))) ⊆ (2nd ‘((A ·P B) +P (A ·P 𝐶))))

12-Dec-2019distrlem1prl 6421 Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
((A P B P 𝐶 P) → (1st ‘(A ·P (B +P 𝐶))) ⊆ (1st ‘((A ·P B) +P (A ·P 𝐶))))

12-Dec-2019ltdcnq 6256 Less-than for positive fractions is decidable. (Contributed by Jim Kingdon, 12-Dec-2019.)
((A Q B Q) → DECID A <Q B)

12-Dec-2019ltdcpi 6183 Less-than for positive integers is decidable. (Contributed by Jim Kingdon, 12-Dec-2019.)
((A N B N) → DECID A <N B)

11-Dec-2019mulassprg 6420 Multiplication of positive reals is associative. Proposition 9-3.7(i) of [Gleason] p. 124. (Contributed by Jim Kingdon, 11-Dec-2019.)
((A P B P 𝐶 P) → ((A ·P B) ·P 𝐶) = (A ·P (B ·P 𝐶)))

11-Dec-2019mulcomprg 6419 Multiplication of positive reals is commutative. Proposition 9-3.7(ii) of [Gleason] p. 124. (Contributed by Jim Kingdon, 11-Dec-2019.)
((A P B P) → (A ·P B) = (B ·P A))

11-Dec-2019addassprg 6418 Addition of positive reals is associative. Proposition 9-3.5(i) of [Gleason] p. 123. (Contributed by Jim Kingdon, 11-Dec-2019.)
((A P B P 𝐶 P) → ((A +P B) +P 𝐶) = (A +P (B +P 𝐶)))

11-Dec-2019addcomprg 6417 Addition of positive reals is commutative. Proposition 9-3.5(ii) of [Gleason] p. 123. (Contributed by Jim Kingdon, 11-Dec-2019.)
((A P B P) → (A +P B) = (B +P A))

11-Dec-2019genpassg 6381 Associativity of an operation on reals. (Contributed by Jim Kingdon, 11-Dec-2019.)
𝐹 = (w P, v P ↦ ⟨{x Qy Q z Q (y (1stw) z (1stv) x = (y𝐺z))}, {x Qy Q z Q (y (2ndw) z (2ndv) x = (y𝐺z))}⟩)    &   ((y Q z Q) → (y𝐺z) Q)    &   dom 𝐹 = (P × P)    &   ((f P g P) → (f𝐹g) P)    &   ((f Q g Q Q) → ((f𝐺g)𝐺) = (f𝐺(g𝐺)))       ((A P B P 𝐶 P) → ((A𝐹B)𝐹𝐶) = (A𝐹(B𝐹𝐶)))

11-Dec-2019genpassu 6380 Associativity of upper cuts. Lemma for genpassg 6381. (Contributed by Jim Kingdon, 11-Dec-2019.)
𝐹 = (w P, v P ↦ ⟨{x Qy Q z Q (y (1stw) z (1stv) x = (y𝐺z))}, {x Qy Q z Q (y (2ndw) z (2ndv) x = (y𝐺z))}⟩)    &   ((y Q z Q) → (y𝐺z) Q)    &   dom 𝐹 = (P × P)    &   ((f P g P) → (f𝐹g) P)    &   ((f Q g Q Q) → ((f𝐺g)𝐺) = (f𝐺(g𝐺)))       ((A P B P 𝐶 P) → (2nd ‘((A𝐹B)𝐹𝐶)) = (2nd ‘(A𝐹(B𝐹𝐶))))

11-Dec-2019genpassl 6379 Associativity of lower cuts. Lemma for genpassg 6381. (Contributed by Jim Kingdon, 11-Dec-2019.)
𝐹 = (w P, v P ↦ ⟨{x Qy Q z Q (y (1stw) z (1stv) x = (y𝐺z))}, {x Qy Q z Q (y (2ndw) z (2ndv) x = (y𝐺z))}⟩)    &   ((y Q z Q) → (y𝐺z) Q)    &   dom 𝐹 = (P × P)    &   ((f P g P) → (f𝐹g) P)    &   ((f Q g Q Q) → ((f𝐺g)𝐺) = (f𝐺(g𝐺)))       ((A P B P 𝐶 P) → (1st ‘((A𝐹B)𝐹𝐶)) = (1st ‘(A𝐹(B𝐹𝐶))))

11-Dec-2019preqlu 6326 Two reals are equal if and only if their lower and upper cuts are. (Contributed by Jim Kingdon, 11-Dec-2019.)
((A P B P) → (A = B ↔ ((1stA) = (1stB) (2ndA) = (2ndB))))

10-Dec-2019mullocprlem 6414 Calculations for mullocpr 6415. (Contributed by Jim Kingdon, 10-Dec-2019.)
(φ → (A P B P))    &   (φ → (𝑈 ·Q 𝑄) <Q (𝐸 ·Q (𝐷 ·Q 𝑈)))    &   (φ → (𝐸 ·Q (𝐷 ·Q 𝑈)) <Q (𝑇 ·Q (𝐷 ·Q 𝑈)))    &   (φ → (𝑇 ·Q (𝐷 ·Q 𝑈)) <Q (𝐷 ·Q 𝑅))    &   (φ → (𝑄 Q 𝑅 Q))    &   (φ → (𝐷 Q 𝑈 Q))    &   (φ → (𝐷 (1stA) 𝑈 (2ndA)))    &   (φ → (𝐸 Q 𝑇 Q))       (φ → (𝑄 (1st ‘(A ·P B)) 𝑅 (2nd ‘(A ·P B))))

10-Dec-2019mulnqpru 6413 Lemma to prove upward closure in positive real multiplication. (Contributed by Jim Kingdon, 10-Dec-2019.)
((((A P 𝐺 (2ndA)) (B P 𝐻 (2ndB))) 𝑋 Q) → ((𝐺 ·Q 𝐻) <Q 𝑋𝑋 (2nd ‘(A ·P B))))

10-Dec-2019mulnqprl 6412 Lemma to prove downward closure in positive real multiplication. (Contributed by Jim Kingdon, 10-Dec-2019.)
((((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) 𝑋 Q) → (𝑋 <Q (𝐺 ·Q 𝐻) → 𝑋 (1st ‘(A ·P B))))

9-Dec-2019prmuloclemcalc 6409 Calculations for prmuloc 6410. (Contributed by Jim Kingdon, 9-Dec-2019.)
(φ𝑅 <Q 𝑈)    &   (φ𝑈 <Q (𝐷 +Q 𝑃))    &   (φ → (A +Q 𝑋) = B)    &   (φ → (𝑃 ·Q B) <Q (𝑅 ·Q 𝑋))    &   (φA Q)    &   (φB Q)    &   (φ𝐷 Q)    &   (φ𝑃 Q)    &   (φ𝑋 Q)       (φ → (𝑈 ·Q A) <Q (𝐷 ·Q B))

9-Dec-2019appdiv0nq 6408 Approximate division for positive rationals. This can be thought of as a variation of appdivnq 6407 in which A is zero, although it can be stated and proved in terms of positive rationals alone, without zero as such. (Contributed by Jim Kingdon, 9-Dec-2019.)
((B Q 𝐶 Q) → 𝑚 Q (𝑚 ·Q 𝐶) <Q B)

9-Dec-2019ltmnqi 6262 Ordering property of multiplication for positive fractions. One direction of ltmnqg 6260. (Contributed by Jim Kingdon, 9-Dec-2019.)
((A <Q B 𝐶 Q) → (𝐶 ·Q A) <Q (𝐶 ·Q B))

9-Dec-2019ltanqi 6261 Ordering property of addition for positive fractions. One direction of ltanqg 6259. (Contributed by Jim Kingdon, 9-Dec-2019.)
((A <Q B 𝐶 Q) → (𝐶 +Q A) <Q (𝐶 +Q B))

8-Dec-2019bj-nn0sucALT 7196 Alternate proof of bj-nn0suc 7182, also constructive but from ax-inf2 7194, hence requiring ax-bdsetind 7186. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
(A 𝜔 ↔ (A = ∅ x 𝜔 A = suc x))

8-Dec-2019bj-omex2 7195 Using bounded set induction and the strong axiom of infinity, 𝜔 is a set, that is, we recover ax-infvn 7163 (see bj-2inf 7160 for the equivalence of the latter with bj-omex 7164). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
𝜔 V

8-Dec-2019bj-inf2vn2 7193 A sufficient condition for 𝜔 to be a set; unbounded version of bj-inf2vn 7192. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
(A 𝑉 → (x(x A ↔ (x = ∅ y A x = suc y)) → A = 𝜔))

8-Dec-2019bj-inf2vn 7192 A sufficient condition for 𝜔 to be a set. See bj-inf2vn2 7193 for the unbounded version from full set induction. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
BOUNDED A       (A 𝑉 → (x(x A ↔ (x = ∅ y A x = suc y)) → A = 𝜔))

8-Dec-2019bj-inf2vnlem4 7191 Lemma for bj-inf2vn2 7193. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
(x A (x = ∅ y A x = suc y) → (Ind 𝑍A𝑍))

8-Dec-2019bj-inf2vnlem3 7190 Lemma for bj-inf2vn 7192. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
BOUNDED A    &   BOUNDED 𝑍       (x A (x = ∅ y A x = suc y) → (Ind 𝑍A𝑍))

8-Dec-2019bj-inf2vnlem2 7189 Lemma for bj-inf2vnlem3 7190 and bj-inf2vnlem4 7191. Remark: unoptimized proof (have to use more deduction style). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
(x A (x = ∅ y A x = suc y) → (Ind 𝑍u(𝑡 u (𝑡 A𝑡 𝑍) → (u Au 𝑍))))

8-Dec-2019bj-inf2vnlem1 7188 Lemma for bj-inf2vn 7192. Remark: unoptimized proof (have to use more deduction style). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.)
(x(x A ↔ (x = ∅ y A x = suc y)) → Ind A)

8-Dec-2019bj-bdcel 7064 Boundedness of a membership formula. (Contributed by BJ, 8-Dec-2019.)
BOUNDED y = A       BOUNDED A x

8-Dec-2019bj-ex 7009 Existential generalization. (Contributed by BJ, 8-Dec-2019.) Proof modification is discouraged because there are shorter proofs, but using less basic results (like exlimiv 1471 and 19.9ht 1514 or 19.23ht 1367). (Proof modification is discouraged.)
(xφφ)

8-Dec-2019mullocpr 6415 Locatedness of multiplication on positive reals. Lemma 12.9 in [BauerTaylor], p. 56 (but where both A and B are positive, not just A). (Contributed by Jim Kingdon, 8-Dec-2019.)
((A P B P) → 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 (1st ‘(A ·P B)) 𝑟 (2nd ‘(A ·P B)))))

8-Dec-2019prmuloc 6410 Positive reals are multiplicatively located. Lemma 12.8 of [BauerTaylor], p. 56. (Contributed by Jim Kingdon, 8-Dec-2019.)
((⟨𝐿, 𝑈 P A <Q B) → 𝑑 Q u Q (𝑑 𝐿 u 𝑈 (u ·Q A) <Q (𝑑 ·Q B)))

8-Dec-2019appdivnq 6407 Approximate division for positive rationals. Proposition 12.7 of [BauerTaylor], p. 55 (a special case where A and B are positive, as well as 𝐶). Our proof is simpler than the one in BauerTaylor because we have reciprocals. (Contributed by Jim Kingdon, 8-Dec-2019.)
((A <Q B 𝐶 Q) → 𝑚 Q (A <Q (𝑚 ·Q 𝐶) (𝑚 ·Q 𝐶) <Q B))

8-Dec-2019nqprlu 6401 The canonical embedding of the rationals into the reals. (Contributed by Jim Kingdon, 8-Dec-2019.)
(A Q → ⟨{xx <Q A}, {xA <Q x}⟩ P)

8-Dec-2019nqprloc 6400 A cut produced from a rational is located. Lemma for nqprlu 6401. (Contributed by Jim Kingdon, 8-Dec-2019.)
(A Q𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 {xx <Q A} 𝑟 {xA <Q x})))

8-Dec-2019nqprdisj 6399 A cut produced from a rational is disjoint. Lemma for nqprlu 6401. (Contributed by Jim Kingdon, 8-Dec-2019.)
(A Q𝑞 Q ¬ (𝑞 {xx <Q A} 𝑞 {xA <Q x}))

8-Dec-2019nqprrnd 6398 A cut produced from a rational is rounded. Lemma for nqprlu 6401. (Contributed by Jim Kingdon, 8-Dec-2019.)
(A Q → (𝑞 Q (𝑞 {xx <Q A} ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 {xx <Q A})) 𝑟 Q (𝑟 {xA <Q x} ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 {xA <Q x}))))

8-Dec-2019nqprm 6397 A cut produced from a rational is inhabited. Lemma for nqprlu 6401. (Contributed by Jim Kingdon, 8-Dec-2019.)
(A Q → (𝑞 Q 𝑞 {xx <Q A} 𝑟 Q 𝑟 {xA <Q x}))

8-Dec-2019mpvlu 6394 Value of multiplication on positive reals. (Contributed by Jim Kingdon, 8-Dec-2019.)
((A P B P) → (A ·P B) = ⟨{x Qy (1stA)z (1stB)x = (y ·Q z)}, {x Qy (2ndA)z (2ndB)x = (y ·Q z)}⟩)

8-Dec-2019plpvlu 6393 Value of addition on positive reals. (Contributed by Jim Kingdon, 8-Dec-2019.)
((A P B P) → (A +P B) = ⟨{x Qy (1stA)z (1stB)x = (y +Q z)}, {x Qy (2ndA)z (2ndB)x = (y +Q z)}⟩)

7-Dec-2019addlocprlemeqgt 6387 Lemma for addlocpr 6391. This is a step used in both the 𝑄 = (𝐷 +Q 𝐸) and (𝐷 +Q 𝐸) <Q 𝑄 cases. (Contributed by Jim Kingdon, 7-Dec-2019.)
(φA P)    &   (φB P)    &   (φ𝑄 <Q 𝑅)    &   (φ𝑃 Q)    &   (φ → (𝑄 +Q (𝑃 +Q 𝑃)) = 𝑅)    &   (φ𝐷 (1stA))    &   (φ𝑈 (2ndA))    &   (φ𝑈 <Q (𝐷 +Q 𝑃))    &   (φ𝐸 (1stB))    &   (φ𝑇 (2ndB))    &   (φ𝑇 <Q (𝐸 +Q 𝑃))       (φ → (𝑈 +Q 𝑇) <Q ((𝐷 +Q 𝐸) +Q (𝑃 +Q 𝑃)))

7-Dec-2019addnqprulem 6383 Lemma to prove upward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.)
(((⟨𝐿, 𝑈 P 𝐺 𝑈) 𝑋 Q) → (𝑆 <Q 𝑋 → ((𝑋 ·Q (*Q𝑆)) ·Q 𝐺) 𝑈))

7-Dec-2019addnqprllem 6382 Lemma to prove downward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.)
(((⟨𝐿, 𝑈 P 𝐺 𝐿) 𝑋 Q) → (𝑋 <Q 𝑆 → ((𝑋 ·Q (*Q𝑆)) ·Q 𝐺) 𝐿))

7-Dec-2019lt2addnq 6263 Ordering property of addition for positive fractions. (Contributed by Jim Kingdon, 7-Dec-2019.)
(((A Q B Q) (𝐶 Q 𝐷 Q)) → ((A <Q B 𝐶 <Q 𝐷) → (A +Q 𝐶) <Q (B +Q 𝐷)))

6-Dec-2019addlocprlem 6390 Lemma for addlocpr 6391. The result, in deduction form. (Contributed by Jim Kingdon, 6-Dec-2019.)
(φA P)    &   (φB P)    &   (φ𝑄 <Q 𝑅)    &   (φ𝑃 Q)    &   (φ → (𝑄 +Q (𝑃 +Q 𝑃)) = 𝑅)    &   (φ𝐷 (1stA))    &   (φ𝑈 (2ndA))    &   (φ𝑈 <Q (𝐷 +Q 𝑃))    &   (φ𝐸 (1stB))    &   (φ𝑇 (2ndB))    &   (φ𝑇 <Q (𝐸 +Q 𝑃))       (φ → (𝑄 (1st ‘(A +P B)) 𝑅 (2nd ‘(A +P B))))

6-Dec-2019addlocprlemgt 6389 Lemma for addlocpr 6391. The (𝐷 +Q 𝐸) <Q 𝑄 case. (Contributed by Jim Kingdon, 6-Dec-2019.)
(φA P)    &   (φB P)    &   (φ𝑄 <Q 𝑅)    &   (φ𝑃 Q)    &   (φ → (𝑄 +Q (𝑃 +Q 𝑃)) = 𝑅)    &   (φ𝐷 (1stA))    &   (φ𝑈 (2ndA))    &   (φ𝑈 <Q (𝐷 +Q 𝑃))    &   (φ𝐸 (1stB))    &   (φ𝑇 (2ndB))    &   (φ𝑇 <Q (𝐸 +Q 𝑃))       (φ → ((𝐷 +Q 𝐸) <Q 𝑄𝑅 (2nd ‘(A +P B))))

6-Dec-2019addlocprlemeq 6388 Lemma for addlocpr 6391. The 𝑄 = (𝐷 +Q 𝐸) case. (Contributed by Jim Kingdon, 6-Dec-2019.)
(φA P)    &   (φB P)    &   (φ𝑄 <Q 𝑅)    &   (φ𝑃 Q)    &   (φ → (𝑄 +Q (𝑃 +Q 𝑃)) = 𝑅)    &   (φ𝐷 (1stA))    &   (φ𝑈 (2ndA))    &   (φ𝑈 <Q (𝐷 +Q 𝑃))    &   (φ𝐸 (1stB))    &   (φ𝑇 (2ndB))    &   (φ𝑇 <Q (𝐸 +Q 𝑃))       (φ → (𝑄 = (𝐷 +Q 𝐸) → 𝑅 (2nd ‘(A +P B))))

6-Dec-2019addlocprlemlt 6386 Lemma for addlocpr 6391. The 𝑄 <Q (𝐷 +Q 𝐸) case. (Contributed by Jim Kingdon, 6-Dec-2019.)
(φA P)    &   (φB P)    &   (φ𝑄 <Q 𝑅)    &   (φ𝑃 Q)    &   (φ → (𝑄 +Q (𝑃 +Q 𝑃)) = 𝑅)    &   (φ𝐷 (1stA))    &   (φ𝑈 (2ndA))    &   (φ𝑈 <Q (𝐷 +Q 𝑃))    &   (φ𝐸 (1stB))    &   (φ𝑇 (2ndB))    &   (φ𝑇 <Q (𝐸 +Q 𝑃))       (φ → (𝑄 <Q (𝐷 +Q 𝐸) → 𝑄 (1st ‘(A +P B))))

5-Dec-2019addlocpr 6391 Locatedness of addition on positive reals. Lemma 11.16 in [BauerTaylor], p. 53. The proof in BauerTaylor relies on signed rationals, so we replace it with another proof which applies prarloc 6357 to both A and B, and uses nqtri3or 6255 rather than prloc 6345 to decide whether 𝑞 is too big to be in the lower cut of A +P B (and deduce that if it is, then 𝑟 must be in the upper cut). What the two proofs have in common is that they take the difference between 𝑞 and 𝑟 to determine how tight a range they need around the real numbers. (Contributed by Jim Kingdon, 5-Dec-2019.)
((A P B P) → 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 (1st ‘(A +P B)) 𝑟 (2nd ‘(A +P B)))))

5-Dec-2019addnqpru 6385 Lemma to prove upward closure in positive real addition. (Contributed by Jim Kingdon, 5-Dec-2019.)
((((A P 𝐺 (2ndA)) (B P 𝐻 (2ndB))) 𝑋 Q) → ((𝐺 +Q 𝐻) <Q 𝑋𝑋 (2nd ‘(A +P B))))

5-Dec-2019addnqprl 6384 Lemma to prove downward closure in positive real addition. (Contributed by Jim Kingdon, 5-Dec-2019.)
((((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) 𝑋 Q) → (𝑋 <Q (𝐺 +Q 𝐻) → 𝑋 (1st ‘(A +P B))))

5-Dec-2019genpmu 6373 The upper cut produced by addition or multiplication on positive reals is inhabited. (Contributed by Jim Kingdon, 5-Dec-2019.)
𝐹 = (w P, v P ↦ ⟨{x Qy Q z Q (y (1stw) z (1stv) x = (y𝐺z))}, {x Qy Q z Q (y (2ndw) z (2ndv) x = (y𝐺z))}⟩)    &   ((y Q z Q) → (y𝐺z) Q)       ((A P B P) → 𝑞 Q 𝑞 (2nd ‘(A𝐹B)))

5-Dec-2019genpelxp 6365 Set containing the result of adding or multiplying positive reals. (Contributed by Jim Kingdon, 5-Dec-2019.)
𝐹 = (w P, v P ↦ ⟨{x Qy Q z Q (y (1stw) z (1stv) x = (y𝐺z))}, {x Qy Q z Q (y (2ndw) z (2ndv) x = (y𝐺z))}⟩)       ((A P B P) → (A𝐹B) (𝒫 Q × 𝒫 Q))

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

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

1-Dec-2019nnanq0 6313 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 6274 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 7160 Two formulations of the axiom of infinity (see ax-infvn 7163 and bj-omex 7164) . (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
(𝜔 V ↔ x(Ind x y(Ind yxy)))

30-Nov-2019bj-om 7159 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-ssom 7158 A characterization of subclasses of 𝜔. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.)
(x(Ind xAx) ↔ A ⊆ 𝜔)

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

30-Nov-2019bj-dfom 7155 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 7154 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-bdind 7153 Boundedness of the formula "the setvar x is an inductive class". (Contributed by BJ, 30-Nov-2019.)
BOUNDED Ind x

30-Nov-2019bj-indeq 7152 Equality property for Ind. (Contributed by BJ, 30-Nov-2019.)
(A = B → (Ind A ↔ Ind B))

30-Nov-2019bj-indsuc 7151 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 7150 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-bdsucel 7109 Boundedness of the formula "the successor of the setvar x belongs to the setvar y". (Contributed by BJ, 30-Nov-2019.)
BOUNDED suc x y

30-Nov-2019bj-bd0el 7095 Boundedness of the formula "the empty set belongs to the setvar x". (Contributed by BJ, 30-Nov-2019.)
BOUNDED x

30-Nov-2019bj-sseq 7038 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 6308 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 6307 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 6275 A version of the Archimedean property. This variation is "stronger" than archnqq 6274 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 7037 Version of elssuni 3582 using a class abstraction and explicit substitution. (Contributed by BJ, 29-Nov-2019.)
xA       (A 𝑉 → ([A / x]φA {xφ}))

29-Nov-2019bj-intabssel1 7036 Version of intss1 3604 using a class abstraction and implicit substitution. Closed form of intmin3 3616. (Contributed by BJ, 29-Nov-2019.)
xA    &   xψ    &   (x = A → (ψφ))       (A 𝑉 → (ψ {xφ} ⊆ A))

29-Nov-2019bj-intabssel 7035 Version of intss1 3604 using a class abstraction and explicit substitution. (Contributed by BJ, 29-Nov-2019.)
xA       (A 𝑉 → ([A / x]φ {xφ} ⊆ A))

29-Nov-2019nq02m 6319 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 6318 Multiplication of non-negative fractions is distributive. Version of distrnq0 6314 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 6317 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 6306 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 6300 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 7186 Axiom of bounded set induction. (Contributed by BJ, 28-Nov-2019.)
BOUNDED φ       (𝑎(y 𝑎 [y / 𝑎]φφ) → 𝑎φ)

28-Nov-2019bj-peano4 7177 Remove from peano4 4247 dependency on ax-setind 4204. 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 7176 A version of en2lp 4216 for natural numbers, which does not require ax-setind 4204.

Note: using this theorem and bj-nnelirr 7175, one can remove dependency on ax-setind 4204 from nntri2 5988 and nndcel 5991; 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 6315 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 6314 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 6339 An upper cut is closed upwards under the positive fractions. (Contributed by Jim Kingdon, 25-Nov-2019.)
((⟨𝐿, 𝑈 P 𝐶 𝑈) → (𝐶 <Q BB 𝑈))

25-Nov-2019prarloclemarch2 6276 Like prarloclemarch 6275 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 6357. (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 6271 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 6267). (Contributed by Jim Kingdon, 25-Nov-2019.)
(A Qx Q (x +Q x) <Q A)

24-Nov-2019bj-nnelirr 7175 A natural number does not belong to itself. Version of elirr 4208 for natural numbers, which does not require ax-setind 4204. (Contributed by BJ, 24-Nov-2019.) (Proof modification is discouraged.)
(A 𝜔 → ¬ A A)

24-Nov-2019bdcriota 7110 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 6297 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 6292 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 6285 Addition on non-negative fractions. This definition is similar to df-plq0 6282 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 6302 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 6301 Decomposing non-negative fractions into natural numbers. Lemma for addnnnq0 6304 and mulnnnq0 6305. (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 6298 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 1792 Rearrange existential quantifiers. (Contributed by Jim Kingdon, 23-Nov-2019.)
(xyzwvu𝑡𝑠(φ ψ) ↔ (xyzwφ vu𝑡𝑠ψ))

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

22-Nov-2019bdsetindis 7187 Axiom of bounded set induction using implicit substitutions. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
BOUNDED φ    &   xψ    &   xχ    &   yφ    &   yψ    &   (x = z → (φψ))    &   (x = y → (χφ))       (y(z y ψχ) → xφ)

22-Nov-2019setindis 7185 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 7184 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 7183 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 7174 A natural number is a transitive set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.)
(A 𝜔 → Tr A)

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

22-Nov-2019bdfind 7168 Bounded induction (principle of induction when A is assumed to be bounded), proved from basic constructive axioms. See find 4249 for a nonconstructive proof of the general case. See findset 7167 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 7167 Bounded induction (principle of induction when A is assumed to be a set) allowing a proof from basic constructive axioms. See find 4249 for a nonconstructive proof of the general case. See bdfind 7168 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 7034 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 6304 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 6284 Multiplication on non-negative fractions. This definition is similar to df-mq0 6283 but expands 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-findes 7199 Principle of induction, using explicit substitutions. Constructive proof (from CZF). See the comment of bj-findis 7197 for explanations. From this version, it is easy to prove findes 4253. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
(([∅ / x]φ x 𝜔 (φ[suc x / x]φ)) → x 𝜔 φ)

21-Nov-2019bj-findisg 7198 Version of bj-findis 7197 using a class term in the consequent. Constructive proof (from CZF). See the comment of bj-findis 7197 for explanations. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
xψ    &   xχ    &   xθ    &   (x = ∅ → (ψφ))    &   (x = y → (φχ))    &   (x = suc y → (θφ))    &   xA    &   xτ    &   (x = A → (φτ))       ((ψ y 𝜔 (χθ)) → (A 𝜔 → τ))

21-Nov-2019bj-bdfindes 7171 Bounded induction (principle of induction for bounded formulas), using explicit substitutions. Constructive proof (from CZF). See the comment of bj-bdfindis 7169 for explanations. From this version, it is easy to prove the bounded version of findes 4253. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
BOUNDED φ       (([∅ / x]φ x 𝜔 (φ[suc x / x]φ)) → x 𝜔 φ)

21-Nov-2019bj-bdfindisg 7170 Version of bj-bdfindis 7169 using a class term in the consequent. Constructive proof (from CZF). See the comment of bj-bdfindis 7169 for explanations. (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 7169 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). Constructive proof (from CZF). See finds 4250 for a proof of full induction in IZF. From this version, it is easy to prove bounded versions of finds 4250, finds2 4251, finds1 4252. (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 7108 Boundedness of the formula expressing that a setvar is equal to the successor of another. (Contributed by BJ, 21-Nov-2019.)
BOUNDED x = suc y

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

21-Nov-2019bdeq0 7094 Boundedness of the formula expressing that a setvar is equal to the empty class. (Contributed by BJ, 21-Nov-2019.)
BOUNDED x = ∅

21-Nov-2019bj-rspg 7033 Restricted specialization, generalized. Weakens a hypothesis of rspccv 2630 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 7032 Restricted specialization, generalized. Weakens a hypothesis of rspccv 2630 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 7031 One implication of elabg 2665. (Contributed by BJ, 21-Nov-2019.)
(x = A → (ψφ))       (A 𝑉 → (ψA {xφ}))

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

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

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

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

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

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

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

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

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

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

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

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

20-Nov-2019mulnq0mo 6303 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 6299 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 7182 Proof of (biconditional form of) nn0suc 4254 from the core axioms of CZF. See also bj-nn0sucALT 7196. As a characterization of the elements of 𝜔, this could be labeled "elom". (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
(A 𝜔 ↔ (A = ∅ x 𝜔 A = suc x))

19-Nov-2019bj-nn0suc0 7172 Constructive proof of a variant of nn0suc 4254. For a constructive proof of nn0suc 4254, see bj-nn0suc 7182. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
(A 𝜔 → (A = ∅ x A A = suc x))

19-Nov-2019speano5 7166 Version of peano5 4248 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 7165 Bounded version of peano5 4248. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
BOUNDED A       ((∅ A x 𝜔 (x A → suc x A)) → 𝜔 ⊆ A)

19-Nov-2019peano5set 7162 Version of peano5 4248 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 7130 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 7129 Bounded version of rabexg 3874. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
BOUNDED φ    &   BOUNDED A       (A 𝑉 → {x Aφ} V)

19-Nov-2019bds 7078 Boundedness of a formula resulting from implicit substitution in a bounded formula. Note that the proof does not use ax-bdsb 7049; therefore, using implicit instead of explicit substitution when boundedness is important, one might avoid using ax-bdsb 7049. (Contributed by BJ, 19-Nov-2019.)
BOUNDED φ    &   (x = y → (φψ))       BOUNDED ψ

19-Nov-2019mulnnnq0 6305 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 7161 Constructive proof of peano2 4245. Temporary note: another possibility is to simply replace sucexg 4174 with bj-sucexg 7145 in the proof of peano2 4245. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
(A 𝜔 → suc A 𝜔)

18-Nov-2019bj-intnexr 7132 vnex 3864 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
( A = V → ¬ A V)

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

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

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

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

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

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

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

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

14-Nov-2019ax-inf2 7194 Another axiom of infinity in a constructive setting (see ax-infvn 7163). (Contributed by BJ, 14-Nov-2019.) (New usage is discouraged.)
𝑎x(x 𝑎 ↔ (x = ∅ y 𝑎 x = suc y))

14-Nov-2019bj-omex 7164 Proof of omex 4243 from ax-infvn 7163. (Contributed by BJ, 14-Nov-2019.) (Proof modification is discouraged.)
𝜔 V

14-Nov-2019ax-infvn 7163 Axiom of infinity in a constructive setting. This asserts the existence of the special set we want (the set of natural numbers), instead of the existence of a set with some properties (ax-iinf 4238) from which one then proves (omex 4243) using full separation that the wanted set exists. "vn" is for "Von Neumann". (Contributed by BJ, 14-Nov-2019.)
x(Ind x y(Ind yxy))

14-Nov-2019enq0tr 6289 The equivalence relation for non-negative fractions is transitive. Lemma for enq0er 6290. (Contributed by Jim Kingdon, 14-Nov-2019.)
((f ~Q0 g g ~Q0 ) → f ~Q0 )

14-Nov-2019enq0ref 6288 The equivalence relation for non-negative fractions is reflexive. Lemma for enq0er 6290. (Contributed by Jim Kingdon, 14-Nov-2019.)
(f (𝜔 × N) ↔ f ~Q0 f)

14-Nov-2019enq0sym 6287 The equivalence relation for non-negative fractions is symmetric. Lemma for enq0er 6290. (Contributed by Jim Kingdon, 14-Nov-2019.)
(f ~Q0 gg ~Q0 f)

13-Nov-2019bj-sucex 7146 sucex 4175 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
A V       suc A V

13-Nov-2019bj-sucexg 7145 sucexg 4174 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
(A 𝑉 → suc A V)

13-Nov-2019bj-unexg 7144 unexg 4128 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
((A 𝑉 B 𝑊) → (AB) V)

13-Nov-2019bdunexb 7143 Bounded version of unexb 4127. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
BOUNDED A    &   BOUNDED B       ((A V B V) ↔ (AB) V)

13-Nov-2019bj-unex 7142 unex 4126 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
A V    &   B V       (AB) V

13-Nov-2019bj-uniexg 7141 uniexg 4125 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
(A 𝑉 A V)

13-Nov-2019bj-uniex 7140 uniex 4124 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
A V        A V

13-Nov-2019bdssexd 7128 Bounded version of ssexd 3871. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
(φB 𝐶)    &   (φAB)    &   BOUNDED A       (φA V)

13-Nov-2019bdssexg 7127 Bounded version of ssexg 3870. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
BOUNDED A       ((AB B 𝐶) → A V)

13-Nov-2019bdssexi 7126 Bounded version of ssexi 3869. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
BOUNDED A    &   B V    &   AB       A V

13-Nov-2019bdssex 7125 Bounded version of ssex 3868. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
BOUNDED A    &   B V       (ABA V)

13-Nov-2019bdinex1g 7124 Bounded version of inex1g 3867. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
BOUNDED B       (A 𝑉 → (AB) V)

13-Nov-2019bdinex2 7123 Bounded version of inex2 3866. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
BOUNDED B    &   A V       (BA) V

13-Nov-2019bdinex1 7122 Bounded version of inex1 3865. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
BOUNDED B    &   A V       (AB) V

13-Nov-2019bdzfauscl 7116 Closed form of the version of zfauscl 3851 for bounded formulas using bounded separation. (Contributed by BJ, 13-Nov-2019.)
BOUNDED φ       (A 𝑉yx(x y ↔ (x A φ)))

12-Nov-2019enq0er 6290 The equivalence relation for non-negative fractions is an equivalence relation. (Contributed by Jim Kingdon, 12-Nov-2019.)
~Q0 Er (𝜔 × N)

12-Nov-2019enq0enq 6286 Equivalence on positive fractions in terms of equivalence on non-negative fractions. (Contributed by Jim Kingdon, 12-Nov-2019.)
~Q = ( ~Q0 ∩ ((N × N) × (N × N)))

10-Nov-2019prarloclemup 6349 Contracting the upper side of an interval which straddles a Dedekind cut. Lemma for prarloc 6357. (Contributed by Jim Kingdon, 10-Nov-2019.)
(((𝑋 𝜔 (⟨𝐿, 𝑈 P A 𝐿 𝑃 Q)) y 𝜔) → ((A +Q ([⟨((y +𝑜 2𝑜) +𝑜 𝑋), 1𝑜⟩] ~Q ·Q 𝑃)) 𝑈 → (((A +Q0 ([⟨y, 1𝑜⟩] ~Q0 ·Q0 𝑃)) 𝐿 (A +Q ([⟨((y +𝑜 2𝑜) +𝑜 suc 𝑋), 1𝑜⟩] ~Q ·Q 𝑃)) 𝑈) → y 𝜔 ((A +Q0 ([⟨y, 1𝑜⟩] ~Q0 ·Q0 𝑃)) 𝐿 (A +Q ([⟨((y +𝑜 2𝑜) +𝑜 𝑋), 1𝑜⟩] ~Q ·Q 𝑃)) 𝑈))))

10-Nov-2019prarloclemlo 6348 Contracting the lower side of an interval which straddles a Dedekind cut. Lemma for prarloc 6357. (Contributed by Jim Kingdon, 10-Nov-2019.)
(((𝑋 𝜔 (⟨𝐿, 𝑈 P A 𝐿 𝑃 Q)) y 𝜔) → ((A +Q ([⟨(y +𝑜 1𝑜), 1𝑜⟩] ~Q ·Q 𝑃)) 𝐿 → (((A +Q0 ([⟨y, 1𝑜⟩] ~Q0 ·Q0 𝑃)) 𝐿 (A +Q ([⟨((y +𝑜 2𝑜) +𝑜 suc 𝑋), 1𝑜⟩] ~Q ·Q 𝑃)) 𝑈) → y 𝜔 ((A +Q0 ([⟨y, 1𝑜⟩] ~Q0 ·Q0 𝑃)) 𝐿 (A +Q ([⟨((y +𝑜 2𝑜) +𝑜 𝑋), 1𝑜⟩] ~Q ·Q 𝑃)) 𝑈))))

10-Nov-2019prarloclemlt 6347 Two possible ways of contracting an interval which straddles a Dedekind cut. Lemma for prarloc 6357. (Contributed by Jim Kingdon, 10-Nov-2019.)
(((𝑋 𝜔 (⟨𝐿, 𝑈 P A 𝐿 𝑃 Q)) y 𝜔) → (A +Q ([⟨(y +𝑜 1𝑜), 1𝑜⟩] ~Q ·Q 𝑃)) <Q (A +Q ([⟨((y +𝑜 2𝑜) +𝑜 𝑋), 1𝑜⟩] ~Q ·Q 𝑃)))

10-Nov-2019nqnq0m 6310 Multiplication of positive fractions is equal with ·Q or ·Q0. (Contributed by Jim Kingdon, 10-Nov-2019.)
((A Q B Q) → (A ·Q B) = (A ·Q0 B))

10-Nov-2019nqnq0a 6309 Addition of positive fractions is equal with +Q or +Q0. (Contributed by Jim Kingdon, 10-Nov-2019.)
((A Q B Q) → (A +Q B) = (A +Q0 B))

10-Nov-2019nqnq0pi 6293 A non-negative fraction is a positive fraction if its numerator and denominator are positive integers. (Contributed by Jim Kingdon, 10-Nov-2019.)
((A N B N) → [⟨A, B⟩] ~Q0 = [⟨A, B⟩] ~Q )

10-Nov-2019nnppipi 6202 A natural number plus a positive integer is a positive integer. (Contributed by Jim Kingdon, 10-Nov-2019.)
((A 𝜔 B N) → (A +𝑜 B) N)

9-Nov-2019prarloclem3step 6350 Induction step for prarloclem3 6351. (Contributed by Jim Kingdon, 9-Nov-2019.)
(((𝑋 𝜔 (⟨𝐿, 𝑈 P A 𝐿 𝑃 Q)) y 𝜔 ((A +Q0 ([⟨y, 1𝑜⟩] ~Q0 ·Q0 𝑃)) 𝐿 (A +Q ([⟨((y +𝑜 2𝑜) +𝑜 suc 𝑋), 1𝑜⟩] ~Q ·Q 𝑃)) 𝑈)) → y 𝜔 ((A +Q0 ([⟨y, 1𝑜⟩] ~Q0 ·Q0 𝑃)) 𝐿 (A +Q ([⟨((y +𝑜 2𝑜) +𝑜 𝑋), 1𝑜⟩] ~Q ·Q 𝑃)) 𝑈))

8-Nov-2019genpcuu 6375 Upward closure of an operation on positive reals. (Contributed by Jim Kingdon, 8-Nov-2019.)
𝐹 = (w P, v P ↦ ⟨{x Qy Q z Q (y (1stw) z (1stv) x = (y𝐺z))}, {x Qy Q z Q (y (2ndw) z (2ndv) x = (y𝐺z))}⟩)    &   ((y Q z Q) → (y𝐺z) Q)    &   ((((A P g (2ndA)) (B P (2ndB))) x Q) → ((g𝐺) <Q xx (2nd ‘(A𝐹B))))       ((A P B P) → (f (2nd ‘(A𝐹B)) → (f <Q xx (2nd ‘(A𝐹B)))))

7-Nov-2019genppreclu 6369 Pre-closure law for general operation on upper cuts. (Contributed by Jim Kingdon, 7-Nov-2019.)
𝐹 = (w P, v P ↦ ⟨{x Qy Q z Q (y (1stw) z (1stv) x = (y𝐺z))}, {x Qy Q z Q (y (2ndw) z (2ndv) x = (y𝐺z))}⟩)    &   ((y Q z Q) → (y𝐺z) Q)       ((A P B P) → ((𝐶 (2ndA) 𝐷 (2ndB)) → (𝐶𝐺𝐷) (2nd ‘(A𝐹B))))

7-Nov-2019prnminu 6343 An upper cut has no smallest member. (Contributed by Jim Kingdon, 7-Nov-2019.)
((⟨𝐿, 𝑈 P B 𝑈) → x 𝑈 x <Q B)

5-Nov-2019prarloclemn 6353 Subtracting two from a positive integer. Lemma for prarloc 6357. (Contributed by Jim Kingdon, 5-Nov-2019.)
((𝑁 N 1𝑜 <N 𝑁) → x 𝜔 (2𝑜 +𝑜 x) = 𝑁)

5-Nov-2019nq0a0 6312 Addition with zero for non-negative fractions. (Contributed by Jim Kingdon, 5-Nov-2019.)
(A Q0 → (A +Q0 0Q0) = A)

5-Nov-2019nq0m0r 6311 Multiplication with zero for non-negative fractions. (Contributed by Jim Kingdon, 5-Nov-2019.)
(A Q0 → (0Q0 ·Q0 A) = 0Q0)

5-Nov-2019df-0nq0 6281 Define non-negative fraction constant 0. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 5-Nov-2019.)
0Q0 = [⟨∅, 1𝑜⟩] ~Q0

4-Nov-2019prarloclem5 6354 A substitution of zero for y and 𝑁 minus two for x. Lemma for prarloc 6357. (Contributed by Jim Kingdon, 4-Nov-2019.)
(((⟨𝐿, 𝑈 P A 𝐿) (𝑁 N 𝑃 Q 1𝑜 <N 𝑁) (A +Q ([⟨𝑁, 1𝑜⟩] ~Q ·Q 𝑃)) 𝑈) → x 𝜔 y 𝜔 ((A +Q0 ([⟨y, 1𝑜⟩] ~Q0 ·Q0 𝑃)) 𝐿 (A +Q ([⟨((y +𝑜 2𝑜) +𝑜 x), 1𝑜⟩] ~Q ·Q 𝑃)) 𝑈))

4-Nov-2019prarloclem4 6352 A slight rearrangement of prarloclem3 6351. Lemma for prarloc 6357. (Contributed by Jim Kingdon, 4-Nov-2019.)
(((⟨𝐿, 𝑈 P A 𝐿) 𝑃 Q) → (x 𝜔 y 𝜔 ((A +Q0 ([⟨y, 1𝑜⟩] ~Q0 ·Q0 𝑃)) 𝐿 (A +Q ([⟨((y +𝑜 2𝑜) +𝑜 x), 1𝑜⟩] ~Q ·Q 𝑃)) 𝑈) → 𝑗 𝜔 ((A +Q0 ([⟨𝑗, 1𝑜⟩] ~Q0 ·Q0 𝑃)) 𝐿 (A +Q ([⟨(𝑗 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑃)) 𝑈)))

2-Nov-2019df-mq0 6283 Define multiplication on non-negative fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 2-Nov-2019.)
·Q0 = {⟨⟨x, y⟩, z⟩ ∣ ((x Q0 y Q0) wvuf((x = [⟨w, v⟩] ~Q0 y = [⟨u, f⟩] ~Q0 ) z = [⟨(w ·𝑜 u), (v ·𝑜 f)⟩] ~Q0 ))}

2-Nov-2019df-plq0 6282 Define addition on non-negative fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 2-Nov-2019.)
+Q0 = {⟨⟨x, y⟩, z⟩ ∣ ((x Q0 y Q0) wvuf((x = [⟨w, v⟩] ~Q0 y = [⟨u, f⟩] ~Q0 ) z = [⟨((w ·𝑜 f) +𝑜 (v ·𝑜 u)), (v ·𝑜 f)⟩] ~Q0 ))}

2-Nov-2019df-nq0 6280 Define class of non-negative fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 2-Nov-2019.)
Q0 = ((𝜔 × N) / ~Q0 )

2-Nov-2019df-enq0 6279 Define equivalence relation for non-negative fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 2-Nov-2019.)
~Q0 = {⟨x, y⟩ ∣ ((x (𝜔 × N) y (𝜔 × N)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)))}

29-Oct-2019nford 1441 If in a context x is not free in ψ and χ, it is not free in (ψ χ). (Contributed by Jim Kingdon, 29-Oct-2019.)
(φ → Ⅎxψ)    &   (φ → Ⅎxχ)       (φ → Ⅎx(ψ χ))

27-Oct-2019prarloclem3 6351 Contracting an interval which straddles a Dedekind cut. Lemma for prarloc 6357. (Contributed by Jim Kingdon, 27-Oct-2019.)
(((⟨𝐿, 𝑈 P A 𝐿) (𝑋 𝜔 𝑃 Q) y 𝜔 ((A +Q0 ([⟨y, 1𝑜⟩] ~Q0 ·Q0 𝑃)) 𝐿 (A +Q ([⟨((y +𝑜 2𝑜) +𝑜 𝑋), 1𝑜⟩] ~Q ·Q 𝑃)) 𝑈)) → 𝑗 𝜔 ((A +Q0 ([⟨𝑗, 1𝑜⟩] ~Q0 ·Q0 𝑃)) 𝐿 (A +Q ([⟨(𝑗 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑃)) 𝑈))

26-Oct-2019prarloclemcalc 6356 Some calculations for prarloc 6357. (Contributed by Jim Kingdon, 26-Oct-2019.)
(((A = (𝑋 +Q0 ([⟨𝑀, 1𝑜⟩] ~Q0 ·Q0 𝑄)) B = (𝑋 +Q ([⟨(𝑀 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑄))) ((𝑄 Q (𝑄 +Q 𝑄) <Q 𝑃) (𝑋 Q 𝑀 𝜔))) → B <Q (A +Q 𝑃))

23-Oct-2019prloc 6345 A Dedekind cut is located. (Contributed by Jim Kingdon, 23-Oct-2019.)
((⟨𝐿, 𝑈 P A <Q B) → (A 𝐿 B 𝑈))

22-Oct-2019prarloc 6357 A Dedekind cut is arithmetically located. Part of Proposition 11.15 of [BauerTaylor], p. 52, slightly modified. It states that given a tolerance 𝑃, there are elements of the lower and upper cut which are within that tolerance of each other. (Contributed by Jim Kingdon, 22-Oct-2019.)
((⟨𝐿, 𝑈 P 𝑃 Q) → 𝑎 𝐿 𝑏 𝑈 𝑏 <Q (𝑎 +Q 𝑃))

22-Oct-2019prarloclem 6355 A special case of Lemma 6.16 from [BauerTaylor], p. 32. Given evenly spaced rational numbers from A to A +Q (𝑁 ·Q 𝑃) (which are in the lower and upper cuts, respectively, of a real number), there are a pair of numbers, two positions apart in the even spacing, which straddle the cut. (Contributed by Jim Kingdon, 22-Oct-2019.)
(((⟨𝐿, 𝑈 P A 𝐿) (𝑁 N 𝑃 Q 1𝑜 <N 𝑁) (A +Q ([⟨𝑁, 1𝑜⟩] ~Q ·Q 𝑃)) 𝑈) → 𝑗 𝜔 ((A +Q0 ([⟨𝑗, 1𝑜⟩] ~Q0 ·Q0 𝑃)) 𝐿 (A +Q ([⟨(𝑗 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑃)) 𝑈))

21-Oct-2019strcollnf 7203 Version of ax-strcoll 7200 with one DV condition removed, the other DV condition replaced by a non-freeness hypothesis, and without initial universal quantifier. (Contributed by BJ, 21-Oct-2019.)
𝑏φ       (x 𝑎 yφ𝑏y(y 𝑏x 𝑎 φ))

21-Oct-2019strcollnft 7202 Closed form of strcollnf 7203. Version of ax-strcoll 7200 with one DV condition removed, the other DV condition replaced by a non-freeness antecedent, and without initial universal quantifier. (Contributed by BJ, 21-Oct-2019.)
(xy𝑏φ → (x 𝑎 yφ𝑏y(y 𝑏x 𝑎 φ)))

19-Oct-2019bdsepnft 7113 Closed form of bdsepnf 7114. Version of ax-bdsep 7111 with one DV condition removed, the other DV condition replaced by a non-freeness antecedent, and without initial universal quantifier. (Contributed by BJ, 19-Oct-2019.)
BOUNDED φ       (x𝑏φ𝑏x(x 𝑏 ↔ (x 𝑎 φ)))

17-Oct-2019ch2varv 7015 Version of ch2var 7014 with non-freeness hypotheses replaced by DV conditions. (Contributed by BJ, 17-Oct-2019.)
((x = y z = 𝑡) → (φψ))    &   φ       ψ

17-Oct-2019ch2var 7014 Implicit substitution of y for x and 𝑡 for z into a theorem. (Contributed by BJ, 17-Oct-2019.)
xψ    &   zψ    &   ((x = y z = 𝑡) → (φψ))    &   φ       ψ

17-Oct-20192spim 7013 Double substitution, as in spim 1608. (Contributed by BJ, 17-Oct-2019.)
xχ    &   zχ    &   ((x = y z = 𝑡) → (ψχ))       (zxψχ)

17-Oct-2019spimd 7012 Deduction form of spim 1608. (Contributed by BJ, 17-Oct-2019.)
(φ → Ⅎxχ)    &   (φx(x = y → (ψχ)))       (φ → (xψχ))

16-Oct-2019bdcsuc 7107 The successor of a setvar is a bounded class. (Contributed by BJ, 16-Oct-2019.)
BOUNDED suc x

16-Oct-2019bdciin 7106 The indexed intersection of a bounded class with a setvar indexing set is a bounded class. (Contributed by BJ, 16-Oct-2019.)
BOUNDED A       BOUNDED x y A

16-Oct-2019bdciun 7105 The indexed union of a bounded class with a setvar indexing set is a bounded class. (Contributed by BJ, 16-Oct-2019.)
BOUNDED A       BOUNDED x y A

16-Oct-2019bdcint 7104 The intersection of a setvar is a bounded class. (Contributed by BJ, 16-Oct-2019.)
BOUNDED x

16-Oct-2019bdvsn 7101 Equality of a setvar with a singleton of a setvar is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
BOUNDED x = {y}

16-Oct-2019bdsnss 7100 Inclusion of a singleton of a setvar in a bounded class is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
BOUNDED A       BOUNDED {x} ⊆ A

16-Oct-2019bdctp 7099 The unordered triple of three setvars is bounded. (Contributed by BJ, 16-Oct-2019.)
BOUNDED {x, y, z}

16-Oct-2019bdcpr 7098 The pair of two setvars is bounded. (Contributed by BJ, 16-Oct-2019.)
BOUNDED {x, y}

16-Oct-2019bdcsn 7097 The singleton of a setvar is bounded. (Contributed by BJ, 16-Oct-2019.)
BOUNDED {x}

16-Oct-2019bdccsb 7087 A class resulting from proper substitution of a setvar for a setvar in a bounded class is bounded. (Contributed by BJ, 16-Oct-2019.)
BOUNDED A       BOUNDED y / xA

16-Oct-2019bdsbcALT 7086 Alternate proof of bdsbc 7085. (Contributed by BJ, 16-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
BOUNDED φ       BOUNDED [y / x]φ

16-Oct-2019bdsbc 7085 A formula resulting from proper substitution of a setvar for a setvar in a bounded formula is bounded. See also bdsbcALT 7086. (Contributed by BJ, 16-Oct-2019.)
BOUNDED φ       BOUNDED [y / x]φ

16-Oct-2019bdrmo 7083 Boundedness of existential at-most-one. (Contributed by BJ, 16-Oct-2019.)
BOUNDED φ       BOUNDED ∃*x y φ

16-Oct-2019bdreu 7082 Boundedness of existential uniqueness.

Remark regarding restricted quantifiers: the formula x Aφ need not be bounded even if A and φ are. Indeed, V is bounded by bdcvv 7084, and (x Vφxφ) (in minimal propositional calculus), so by bd0 7051, if x Vφ were bounded when φ is bounded, then xφ would be bounded as well when φ is bounded, which is not the case. The same remark holds with , ∃!, ∃*. (Contributed by BJ, 16-Oct-2019.)

BOUNDED φ       BOUNDED ∃!x y φ

16-Oct-2019bdnel 7081 Non-membership of a setvar in a bounded formula is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
BOUNDED A       BOUNDED xA

16-Oct-2019bdne 7080 Inequality of two setvars is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
BOUNDED xy

16-Oct-2019bdcdeq 7066 Conditional equality of a bounded formula is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
BOUNDED φ       BOUNDED CondEq(x = yφ)

15-Oct-2019bj-uniex2 7139 uniex2 4123 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.)
y y = x

15-Oct-2019bj-axun2 7138 axun2 4122 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.)
yz(z yw(z w w x))

15-Oct-2019bdcuni 7103 The union of a setvar is a bounded class. (Contributed by BJ, 15-Oct-2019.)
BOUNDED x

15-Oct-2019genpdisj 6378 The lower and upper cuts produced by addition or multiplication on positive reals are disjoint. (Contributed by Jim Kingdon, 15-Oct-2019.)
𝐹 = (w P, v P ↦ ⟨{x Qy Q z Q (y (1stw) z (1stv) x = (y𝐺z))}, {x Qy Q z Q (y (2ndw) z (2ndv) x = (y𝐺z))}⟩)    &   ((y Q z Q) → (y𝐺z) Q)    &   ((x Q y Q z Q) → (x <Q y ↔ (z𝐺x) <Q (z𝐺y)))    &   ((x Q y Q) → (x𝐺y) = (y𝐺x))       ((A P B P) → 𝑞 Q ¬ (𝑞 (1st ‘(A𝐹B)) 𝑞 (2nd ‘(A𝐹B))))

15-Oct-2019genpelvu 6367 Membership in upper cut of general operation (addition or multiplication) on positive reals. (Contributed by Jim Kingdon, 15-Oct-2019.)
𝐹 = (w P, v P ↦ ⟨{x Qy Q z Q (y (1stw) z (1stv) x = (y𝐺z))}, {x Qy Q z Q (y (2ndw) z (2ndv) x = (y𝐺z))}⟩)    &   ((y Q z Q) → (y𝐺z) Q)       ((A P B P) → (𝐶 (2nd ‘(A𝐹B)) ↔ g (2ndA) (2ndB)𝐶 = (g𝐺)))

15-Oct-2019prltlu 6341 An element of a lower cut is less than an element of the corresponding upper cut. (Contributed by Jim Kingdon, 15-Oct-2019.)
((⟨𝐿, 𝑈 P B 𝐿 𝐶 𝑈) → B <Q 𝐶)

14-Oct-2019genpcdl 6374 Downward closure of an operation on positive reals. (Contributed by Jim Kingdon, 14-Oct-2019.)
𝐹 = (w P, v P ↦ ⟨{x Qy Q z Q (y (1stw) z (1stv) x = (y𝐺z))}, {x Qy Q z Q (y (2ndw) z (2ndv) x = (y𝐺z))}⟩)    &   ((y Q z Q) → (y𝐺z) Q)    &   ((((A P g (1stA)) (B P (1stB))) x Q) → (x <Q (g𝐺) → x (1st ‘(A𝐹B))))       ((A P B P) → (f (1st ‘(A𝐹B)) → (x <Q fx (1st ‘(A𝐹B)))))

9-Oct-2019bj-df-test 7008 Definition of the testability predicate TEST. This definition is not very useful in terms of number of tokens saved and readability added, since one can replace everywhere the string TEST with the string DECID ¬. (Contributed by BJ, 9-Oct-2019.)
(TEST φDECID ¬ φ)

9-Oct-2019dcdc 7007 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 φ)

9-Oct-2019dcnbidcnn 7006 The decidability of ¬ φ is equivalent to that of ¬ ¬ φ. (Contributed by BJ, 9-Oct-2019.)
(DECID ¬ φDECID ¬ ¬ φ)

9-Oct-2019nndc 7005 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 φ

9-Oct-2019nnexmid 7004 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.)
¬ ¬ (φ ¬ φ)

7-Oct-2019genprndu 6377 The upper cut produced by addition or multiplication on positive reals is rounded. (Contributed by Jim Kingdon, 7-Oct-2019.)
𝐹 = (w P, v P ↦ ⟨{x Qy Q z Q (y (1stw) z (1stv) x = (y𝐺z))}, {x Qy Q z Q (y (2ndw) z (2ndv) x = (y𝐺z))}⟩)    &   ((y Q z Q) → (y𝐺z) Q)    &   ((x Q y Q z Q) → (x <Q y ↔ (z𝐺x) <Q (z𝐺y)))    &   ((x Q y Q) → (x𝐺y) = (y𝐺x))    &   ((((A P g (2ndA)) (B P (2ndB))) x Q) → ((g𝐺) <Q xx (2nd ‘(A𝐹B))))       ((A P B P) → 𝑟 Q (𝑟 (2nd ‘(A𝐹B)) ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 (2nd ‘(A𝐹B)))))

7-Oct-2019genprndl 6376 The lower cut produced by addition or multiplication on positive reals is rounded. (Contributed by Jim Kingdon, 7-Oct-2019.)
𝐹 = (w P, v P ↦ ⟨{x Qy Q z Q (y (1stw) z (1stv) x = (y𝐺z))}, {x Qy Q z Q (y (2ndw) z (2ndv) x = (y𝐺z))}⟩)    &   ((y Q z Q) → (y𝐺z) Q)    &   ((x Q y Q z Q) → (x <Q y ↔ (z𝐺x) <Q (z𝐺y)))    &   ((x Q y Q) → (x𝐺y) = (y𝐺x))    &   ((((A P g (1stA)) (B P (1stB))) x Q) → (x <Q (g𝐺) → x (1st ‘(A𝐹B))))       ((A P B P) → 𝑞 Q (𝑞 (1st ‘(A𝐹B)) ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 (1st ‘(A𝐹B)))))

6-Oct-2019bdph 7077 A formula which defines (by class abstraction) a bounded class is bounded. (Contributed by BJ, 6-Oct-2019.)
BOUNDED {xφ}       BOUNDED φ

6-Oct-2019bdcab 7076 A class defined by class abstraction using a bounded formula is bounded. (Contributed by BJ, 6-Oct-2019.)
BOUNDED φ       BOUNDED {xφ}

6-Oct-2019bdnthALT 7062 Alternate proof of bdnth 7061 not using bdfal 7060. Then, bdfal 7060 can be proved from this theorem, using fal 1235. The total number of proof steps would be 17 (for bdnthALT 7062) + 3 = 20, which is more than 8 (for bdfal 7060) + 9 (for bdnth 7061) = 17. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
¬ φ       BOUNDED φ

6-Oct-2019bdnth 7061 A falsity is a bounded formula. (Contributed by BJ, 6-Oct-2019.)
¬ φ       BOUNDED φ

6-Oct-2019bdth 7058 A truth (a (closed) theorem) is a bounded formula. (Contributed by BJ, 6-Oct-2019.)
φ       BOUNDED φ

6-Oct-2019genplt2i 6364 Operating on both sides of two inequalities, when the operation is consistent with <Q. (Contributed by Jim Kingdon, 6-Oct-2019.)
((x Q y Q z Q) → (x <Q y ↔ (z𝐺x) <Q (z𝐺y)))    &   ((x Q y Q) → (x𝐺y) = (y𝐺x))       ((A <Q B 𝐶 <Q 𝐷) → (A𝐺𝐶) <Q (B𝐺𝐷))

5-Oct-2019sscoll2 7206 Version of ax-sscoll 7205 with two DV conditions removed and without initial universal quantifiers. (Contributed by BJ, 5-Oct-2019.)
𝑐z(x 𝑎 y 𝑏 φ𝑑 𝑐 y(y 𝑑x 𝑎 φ))

5-Oct-2019ax-sscoll 7205 Axiom scheme of subset collection. It is stated with all possible disjoint variable conditions, to show that this weak form is sufficient. (Contributed by BJ, 5-Oct-2019.)
𝑎𝑏𝑐z(x 𝑎 y 𝑏 φ𝑑 𝑐 y(y 𝑑x 𝑎 φ))

5-Oct-2019strcollnfALT 7204 Alternate proof of strcollnf 7203, not using strcollnft 7202. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
𝑏φ       (x 𝑎 yφ𝑏y(y 𝑏x 𝑎 φ))

5-Oct-2019strcoll2 7201 Version of ax-strcoll 7200 with one DV condition removed and without initial universal quantifier. (Contributed by BJ, 5-Oct-2019.)
(x 𝑎 yφ𝑏y(y 𝑏x 𝑎 φ))

5-Oct-2019ax-strcoll 7200 Axiom scheme of strong collection. It is stated with all possible disjoint variable conditions, to show that this weak form is sufficient. (Contributed by BJ, 5-Oct-2019.)
𝑎(x 𝑎 yφ𝑏y(y 𝑏x 𝑎 φ))

5-Oct-2019bj-snex 7136 snex 3911 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
A V       {A} V

5-Oct-2019bj-snexg 7135 snexg 3910 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
(A 𝑉 → {A} V)

5-Oct-2019bj-prexg 7134 Proof of prexg 3921 using only bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
((A 𝑉 B 𝑊) → {A, B} V)

5-Oct-2019bj-zfpair2 7133 Proof of zfpair2 3919 using only bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
{x, y} V

5-Oct-2019bdbm1.3ii 7117 Bounded version of bm1.3ii 3852. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
BOUNDED φ    &   xy(φy x)       xy(y xφ)

5-Oct-2019bdsepnfALT 7115 Alternate proof of bdsepnf 7114, not using bdsepnft 7113. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
𝑏φ    &   BOUNDED φ       𝑏x(x 𝑏 ↔ (x 𝑎 φ))

5-Oct-2019bdsepnf 7114 Version of ax-bdsep 7111 with one DV condition removed, the other DV condition replaced by a non-freeness hypothesis, and without initial universal quantifier. See also bdsepnfALT 7115. (Contributed by BJ, 5-Oct-2019.)
𝑏φ    &   BOUNDED φ       𝑏x(x 𝑏 ↔ (x 𝑎 φ))

5-Oct-2019bdsep2 7112 Version of ax-bdsep 7111 with one DV condition removed and without initial universal quantifier. (Contributed by BJ, 5-Oct-2019.)
BOUNDED φ       𝑏x(x 𝑏 ↔ (x 𝑎 φ))

5-Oct-2019ax-bdsep 7111 Axiom scheme of bounded (or restricted, or Δ0) separation. It is stated with all possible disjoint variable conditions, to show that this weak form is sufficient. For the full axiom of separation, see ax-sep 3849. (Contributed by BJ, 5-Oct-2019.)
BOUNDED φ       𝑎𝑏x(x 𝑏 ↔ (x 𝑎 φ))

5-Oct-2019genpml 6372 The lower cut produced by addition or multiplication on positive reals is inhabited. (Contributed by Jim Kingdon, 5-Oct-2019.)
𝐹 = (w P, v P ↦ ⟨{x Qy Q z Q (y (1stw) z (1stv) x = (y𝐺z))}, {x Qy Q z Q (y (2ndw) z (2ndv) x = (y𝐺z))}⟩)    &   ((y Q z Q) → (y𝐺z) Q)       ((A P B P) → 𝑞 Q 𝑞 (1st ‘(A𝐹B)))

4-Oct-2019genpelpw 6371 Result of general operation on positive reals is an ordered pair of sets of positive fractions. (Contributed by Jim Kingdon, 4-Oct-2019.)
𝐹 = (w P, v P ↦ ⟨{x Qy Q z Q (y (1stw) z (1stv) x = (y𝐺z))}, {x Qy Q z Q (y (2ndw) z (2ndv) x = (y𝐺z))}⟩)    &   ((y Q z Q) → (y𝐺z) Q)       ((A P B P) → (A𝐹B) (𝒫 Q × 𝒫 Q))

3-Oct-2019bdcpw 7096 The power class of a bounded class is bounded. (Contributed by BJ, 3-Oct-2019.)
BOUNDED A       BOUNDED 𝒫 A

3-Oct-2019bdcnulALT 7093 Alternate proof of bdcnul 7092. Similarly, for the next few theorems proving boundedness of a class, one can either use their definition followed by bdceqir 7071, or use the corresponding characterizations of its elements followed by bdelir 7074. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
BOUNDED

3-Oct-2019bdcnul 7092 The empty class is bounded. See also bdcnulALT 7093. (Contributed by BJ, 3-Oct-2019.)
BOUNDED

3-Oct-2019bdss 7091 The inclusion of a setvar in a bounded class is a bounded formula. Note: apparently, we cannot prove from the present axioms that equality of two bounded classes is a bounded formula. (Contributed by BJ, 3-Oct-2019.)
BOUNDED A       BOUNDED xA

3-Oct-2019bdcin 7090 The intersection of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.)
BOUNDED A    &   BOUNDED B       BOUNDED (AB)

3-Oct-2019bdcun 7089 The union of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.)
BOUNDED A    &   BOUNDED B       BOUNDED (AB)

3-Oct-2019bdcdif 7088 The difference of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.)
BOUNDED A    &   BOUNDED B       BOUNDED (AB)

3-Oct-2019bdcvv 7084 The universal class is bounded. The formulation may sound strange, but recall that here, "bounded" means "Δ0". (Contributed by BJ, 3-Oct-2019.)
BOUNDED V

3-Oct-2019bdcrab 7079 A class defined by restricted abstraction from a bounded class and a bounded formula is bounded. (Contributed by BJ, 3-Oct-2019.)
BOUNDED A    &   BOUNDED φ       BOUNDED {x Aφ}

3-Oct-2019bdcv 7075 A setvar is a bounded class. (Contributed by BJ, 3-Oct-2019.)
BOUNDED x

3-Oct-2019bdelir 7074 Inference associated with df-bdc 7068. Its converse is bdeli 7073. (Contributed by BJ, 3-Oct-2019.)
BOUNDED x A       BOUNDED A

3-Oct-2019bdeli 7073 Inference associated with bdel 7072. Its converse is bdelir 7074. (Contributed by BJ, 3-Oct-2019.)
BOUNDED A       BOUNDED x A

3-Oct-2019bdel 7072 The belonging of a setvar in a bounded class is a bounded formula. (Contributed by BJ, 3-Oct-2019.)
(BOUNDED ABOUNDED x A)

3-Oct-2019bdceqir 7071 A class equal to a bounded one is bounded. Stated with a commuted (compared with bdceqi 7070) equality in the hypothesis, to work better with definitions (B is the definiendum that one wants to prove bounded; see comment of bd0r 7052). (Contributed by BJ, 3-Oct-2019.)
BOUNDED A    &   B = A       BOUNDED B

3-Oct-2019bdceqi 7070 A class equal to a bounded one is bounded. Note the use of ax-ext 2004. See also bdceqir 7071. (Contributed by BJ, 3-Oct-2019.)
BOUNDED A    &   A = B       BOUNDED B

3-Oct-2019bdceq 7069 Equality property for the predicate BOUNDED. (Contributed by BJ, 3-Oct-2019.)
A = B       (BOUNDED ABOUNDED B)

3-Oct-2019df-bdc 7068 Define a bounded class as one such that membership in this class is a bounded formula. (Contributed by BJ, 3-Oct-2019.)
(BOUNDED AxBOUNDED x A)

3-Oct-2019bdab 7065 Membership in a class defined by class abstraction using a bounded formula, is a bounded formula. (Contributed by BJ, 3-Oct-2019.)
BOUNDED φ       BOUNDED x {yφ}

3-Oct-2019bdxor 7063 The exclusive disjunction of two bounded formulas is bounded. (Contributed by BJ, 3-Oct-2019.)
BOUNDED φ    &   BOUNDED ψ       BOUNDED (φψ)

3-Oct-2019bdfal 7060 The truth value is bounded. (Contributed by BJ, 3-Oct-2019.)
BOUNDED

3-Oct-2019bdtru 7059 The truth value is bounded. (Contributed by BJ, 3-Oct-2019.)
BOUNDED

3-Oct-2019bd3an 7057 A conjunction of three bounded formulas is bounded. (Contributed by BJ, 3-Oct-2019.)
BOUNDED φ    &   BOUNDED ψ    &   BOUNDED χ       BOUNDED (φ ψ χ)

3-Oct-2019bd3or 7056 A disjunction of three bounded formulas is bounded. (Contributed by BJ, 3-Oct-2019.)
BOUNDED φ    &   BOUNDED ψ    &   BOUNDED χ       BOUNDED (φ ψ χ)

3-Oct-2019bddc 7055 Decidability of a bounded formula is bounded. (Contributed by BJ, 3-Oct-2019.)
BOUNDED φ       BOUNDED DECID φ

3-Oct-2019bdstab 7054 Stability of a bounded formula is bounded. (Contributed by BJ, 3-Oct-2019.)
BOUNDED φ       BOUNDED STAB φ

3-Oct-2019bdbi 7053 A biconditional between two bounded formulas is bounded. (Contributed by BJ, 3-Oct-2019.)
BOUNDED φ    &   BOUNDED ψ       BOUNDED (φψ)

3-Oct-2019bd0r 7052 A formula equivalent to a bounded one is bounded. Stated with a commuted (compared with bd0 7051) biconditional in the hypothesis, to work better with definitions (ψ is the definiendum that one wants to prove bounded). (Contributed by BJ, 3-Oct-2019.)
BOUNDED φ    &   (ψφ)       BOUNDED ψ

3-Oct-2019bd0 7051 A formula equivalent to a bounded one is bounded. See also bd0r 7052. (Contributed by BJ, 3-Oct-2019.)
BOUNDED φ    &   (φψ)       BOUNDED ψ

3-Oct-2019bdeq 7050 Equality property for the predicate BOUNDED. (Contributed by BJ, 3-Oct-2019.)
(φψ)       (BOUNDED φBOUNDED ψ)

3-Oct-2019ax-bdsb 7049 A formula resulting from proper substitution in a bounded formula is bounded. This probably cannot be proved from the other axioms, since neither the definiens in df-sb 1628, nor probably any other equivalent formula, is syntactically bounded. (Contributed by BJ, 3-Oct-2019.)
BOUNDED φ       BOUNDED [y / x]φ

3-Oct-2019ax-bdel 7048 An atomic formula is bounded (membership predicate). (Contributed by BJ, 3-Oct-2019.)
BOUNDED x y

3-Oct-2019ax-bdeq 7047 An atomic formula is bounded (equality predicate). (Contributed by BJ, 3-Oct-2019.)
BOUNDED x = y

3-Oct-2019ax-bd0 7040 If two formulas are equivalent, then boundedness of one implies boundedness of the other. (Contributed by BJ, 3-Oct-2019.)
(φψ)       (BOUNDED φBOUNDED ψ)

3-Oct-2019genipv 6363 Value of general operation (addition or multiplication) on positive reals. (Contributed by Jim Kingon, 3-Oct-2019.)
𝐹 = (w P, v P ↦ ⟨{x Qy Q z Q (y (1stw) z (1stv) x = (y𝐺z))}, {x Qy Q z Q (y (2ndw) z (2ndv) x = (y𝐺z))}⟩)    &   ((y Q z Q) → (y𝐺z) Q)       ((A P B P) → (A𝐹B) = ⟨{𝑞 Q𝑟 (1stA)𝑠 (1stB)𝑞 = (𝑟𝐺𝑠)}, {𝑞 Q𝑟 (2ndA)𝑠 (2ndB)𝑞 = (𝑟𝐺𝑠)}⟩)

3-Oct-2019elnp1st2nd 6330 Membership in positive reals, using 1st and 2nd to refer to the lower and upper cut. (Contributed by Jim Kingdon, 3-Oct-2019.)
(A P ↔ ((A (𝒫 Q × 𝒫 Q) (𝑞 Q 𝑞 (1stA) 𝑟 Q 𝑟 (2ndA))) ((𝑞 Q (𝑞 (1stA) ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 (1stA))) 𝑟 Q (𝑟 (2ndA) ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 (2ndA)))) 𝑞 Q ¬ (𝑞 (1stA) 𝑞 (2ndA)) 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 (1stA) 𝑟 (2ndA))))))

2-Oct-2019genipdm 6370 Domain of general operation on positive reals. (Contributed by Jim Kingdon, 2-Oct-2019.)
𝐹 = (w P, v P ↦ ⟨{x Qy Q z Q (y (1stw) z (1stv) x = (y𝐺z))}, {x Qy Q z Q (y (2ndw) z (2ndv) x = (y𝐺z))}⟩)    &   ((y Q z Q) → (y𝐺z) Q)       dom 𝐹 = (P × P)

2-Oct-2019genpprecll 6368 Pre-closure law for general operation on lower cuts. (Contributed by Jim Kingdon, 2-Oct-2019.)
𝐹 = (w P, v P ↦ ⟨{x Qy Q z Q (y (1stw) z (1stv) x = (y𝐺z))}, {x Qy Q z Q (y (2ndw) z (2ndv) x = (y𝐺z))}⟩)    &   ((y Q z Q) → (y𝐺z) Q)       ((A P B P) → ((𝐶 (1stA) 𝐷 (1stB)) → (𝐶𝐺𝐷) (1st ‘(A𝐹B))))

2-Oct-2019genpelvl 6366 Membership in lower cut of general operation (addition or multiplication) on positive reals. (Contributed by Jim Kingdon, 2-Oct-2019.)
𝐹 = (w P, v P ↦ ⟨{x Qy Q z Q (y (1stw) z (1stv) x = (y𝐺z))}, {x Qy Q z Q (y (2ndw) z (2ndv) x = (y𝐺z))}⟩)    &   ((y Q z Q) → (y𝐺z) Q)       ((A P B P) → (𝐶 (1st ‘(A𝐹B)) ↔ g (1stA) (1stB)𝐶 = (g𝐺)))

30-Sep-2019genpdf 6362 Simplified definition of addition or multiplication on positive reals. (Contributed by Jim Kingdon, 30-Sep-2019.)
𝐹 = (w P, v P ↦ ⟨{𝑞 Q𝑟 Q 𝑠 Q (𝑟 (1stw) 𝑠 (1stv) 𝑞 = (𝑟𝐺𝑠))}, {𝑞 Q𝑟 Q 𝑠 Q (𝑟 (2ndw) 𝑠 (2ndv) 𝑞 = (𝑟𝐺𝑠))}⟩)       𝐹 = (w P, v P ↦ ⟨{𝑞 Q𝑟 (1stw)𝑠 (1stv)𝑞 = (𝑟𝐺𝑠)}, {𝑞 Q𝑟 (2ndw)𝑠 (2ndv)𝑞 = (𝑟𝐺𝑠)}⟩)

30-Sep-2019genpdflem 6361 Simplification of upper or lower cut expression. Lemma for genpdf 6362. (Contributed by Jim Kingdon, 30-Sep-2019.)
((φ 𝑟 A) → 𝑟 Q)    &   ((φ 𝑠 B) → 𝑠 Q)       (φ → {𝑞 Q𝑟 Q 𝑠 Q (𝑟 A 𝑠 B 𝑞 = (𝑟𝐺𝑠))} = {𝑞 Q𝑟 A 𝑠 B 𝑞 = (𝑟𝐺𝑠)})

29-Sep-2019prnmaddl 6344 A lower cut has no largest member. Addition version. (Contributed by Jim Kingdon, 29-Sep-2019.)
((⟨𝐿, 𝑈 P B 𝐿) → x Q (B +Q x) 𝐿)

29-Sep-2019prnmaxl 6342 A lower cut has no largest member. (Contributed by Jim Kingdon, 29-Sep-2019.)
((⟨𝐿, 𝑈 P B 𝐿) → x 𝐿 B <Q x)

29-Sep-2019prubl 6340 A positive fraction not in a lower cut is an upper bound. (Contributed by Jim Kingdon, 29-Sep-2019.)
(((⟨𝐿, 𝑈 P B 𝐿) 𝐶 Q) → (¬ 𝐶 𝐿B <Q 𝐶))

29-Sep-2019df-iltp 6324 Define ordering on positive reals. We define x<P y if there is a positive fraction 𝑞 which is an element of the upper cut of x and the lower cut of y. From the definition of < in Section 11.2.1 of [HoTT], p. (varies).

This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 29-Sep-2019.)

<P = {⟨x, y⟩ ∣ ((x P y P) 𝑞 Q (𝑞 (2ndx) 𝑞 (1sty)))}

29-Sep-2019df-imp 6323 Define multiplication on positive reals. Here we use a simple definition which is similar to df-iplp 6322 or the definition of multiplication on positive reals in Metamath Proof Explorer. This is as opposed to the more complicated definition of multiplication given in Section 11.2.1 of [HoTT], p. (varies), which appears to be motivated by handling negative numbers or handling modified Dedekind cuts in which locatedness is omitted.

This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 29-Sep-2019.)

·P = (x P, y P ↦ ⟨{𝑞 Q𝑟 Q 𝑠 Q (𝑟 (1stx) 𝑠 (1sty) 𝑞 = (𝑟 ·Q 𝑠))}, {𝑞 Q𝑟 Q 𝑠 Q (𝑟 (2ndx) 𝑠 (2ndy) 𝑞 = (𝑟 ·Q 𝑠))}⟩)

28-Sep-2019prcdnql 6338 A lower cut is closed downwards under the positive fractions. (Contributed by Jim Kingdon, 28-Sep-2019.)
((⟨𝐿, 𝑈 P B 𝐿) → (𝐶 <Q B𝐶 𝐿))

28-Sep-2019elprnqu 6336 An element of a positive real's upper cut is a positive fraction. (Contributed by Jim Kingdon, 28-Sep-2019.)
((⟨𝐿, 𝑈 P B 𝑈) → B Q)

28-Sep-2019elprnql 6335 An element of a positive real's lower cut is a positive fraction. (Contributed by Jim Kingdon, 28-Sep-2019.)
((⟨𝐿, 𝑈 P B 𝐿) → B Q)

28-Sep-2019prssnqu 6334 A positive real's upper cut is a subset of the positive fractions. It would presumably be possible to also prove 𝑈Q, but we only need 𝑈Q so far. (Contributed by Jim Kingdon, 28-Sep-2019.)
(⟨𝐿, 𝑈 P𝑈Q)

28-Sep-2019prssnql 6333 A positive real's lower cut is a subset of the positive fractions. It would presumably be possible to also prove 𝐿Q, but we only need 𝐿Q so far. (Contributed by Jim Kingdon, 28-Sep-2019.)
(⟨𝐿, 𝑈 P𝐿Q)

28-Sep-2019sotritric 4035 A trichotomy relationship, given a trichotomous order. (Contributed by Jim Kingdon, 28-Sep-2019.)
𝑅 Or A    &   ((B A 𝐶 A) → (B𝑅𝐶 B = 𝐶 𝐶𝑅B))       ((B A 𝐶 A) → (B𝑅𝐶 ↔ ¬ (B = 𝐶 𝐶𝑅B)))

28-Sep-2019sotricim 4034 One direction of sotritric 4035 holds for all weakly linear orders. (Contributed by Jim Kingdon, 28-Sep-2019.)
((𝑅 Or A (B A 𝐶 A)) → (B𝑅𝐶 → ¬ (B = 𝐶 𝐶𝑅B)))

27-Sep-2019prmu 6332 A positive real's upper cut is inhabited. (Contributed by Jim Kingdon, 27-Sep-2019.)
(⟨𝐿, 𝑈 Px Q x 𝑈)

27-Sep-2019prml 6331 A positive real's lower cut is inhabited. (Contributed by Jim Kingdon, 27-Sep-2019.)
(⟨𝐿, 𝑈 Px Q x 𝐿)

27-Sep-2019prop 6329 A positive real is an ordered pair of a lower cut and an upper cut. (Contributed by Jim Kingdon, 27-Sep-2019.)
(A P → ⟨(1stA), (2ndA)⟩ P)

27-Sep-2019elinp 6328 Membership in positive reals. (Contributed by Jim Kingdon, 27-Sep-2019.)
(⟨𝐿, 𝑈 P ↔ (((𝐿Q 𝑈Q) (𝑞 Q 𝑞 𝐿 𝑟 Q 𝑟 𝑈)) ((𝑞 Q (𝑞 𝐿𝑟 Q (𝑞 <Q 𝑟 𝑟 𝐿)) 𝑟 Q (𝑟 𝑈𝑞 Q (𝑞 <Q 𝑟 𝑞 𝑈))) 𝑞 Q ¬ (𝑞 𝐿 𝑞 𝑈) 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 𝐿 𝑟 𝑈)))))

27-Sep-2019npsspw 6325 Lemma for proving existence of reals. (Contributed by Jim Kingdon, 27-Sep-2019.)
P ⊆ (𝒫 Q × 𝒫 Q)

26-Sep-2019df-iplp 6322 Define addition on positive reals. From Section 11.2.1 of [HoTT], p. (varies). We write this definition to closely resemble the definition in HoTT although some of the conditions (for example, 𝑟 Q and 𝑟 (1stx)) conditions are redundant and can be simplified as shown at genpdf 6362.

This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 26-Sep-2019.)

+P = (x P, y P ↦ ⟨{𝑞 Q𝑟 Q 𝑠 Q (𝑟 (1stx) 𝑠 (1sty) 𝑞 = (𝑟 +Q 𝑠))}, {𝑞 Q𝑟 Q 𝑠 Q (𝑟 (2ndx) 𝑠 (2ndy) 𝑞 = (𝑟 +Q 𝑠))}⟩)

25-Sep-2019ax-bdex 7046 A bounded existential quantification of a bounded formula is bounded. Note the DV condition on x, y. (Contributed by BJ, 25-Sep-2019.)
BOUNDED φ       BOUNDED x y φ

25-Sep-2019ax-bdal 7045 A bounded universal quantification of a bounded formula is bounded. Note the DV condition on x, y. (Contributed by BJ, 25-Sep-2019.)
BOUNDED φ       BOUNDED x y φ

25-Sep-2019ax-bdn 7044 The negation of a bounded formula is bounded. (Contributed by BJ, 25-Sep-2019.)
BOUNDED φ       BOUNDED ¬ φ

25-Sep-2019ax-bdor 7043 The disjunction of two bounded formulas is bounded. (Contributed by BJ, 25-Sep-2019.)
BOUNDED φ    &   BOUNDED ψ       BOUNDED (φ ψ)

25-Sep-2019ax-bdan 7042 The conjunction of two bounded formulas is bounded. (Contributed by BJ, 25-Sep-2019.)
BOUNDED φ    &   BOUNDED ψ       BOUNDED (φ ψ)

25-Sep-2019ax-bdim 7041 An implication between two bounded formulas is bounded. (Contributed by BJ, 25-Sep-2019.)
BOUNDED φ    &   BOUNDED ψ       BOUNDED (φψ)

25-Sep-2019df-i1p 6321 Define the positive real constant 1. This is a "temporary" set used in the construction of complex numbers and is intended to be used only by the construction. (Contributed by Jim Kingdon, 25-Sep-2019.)
1P = ⟨{𝑙𝑙 <Q 1Q}, {u ∣ 1Q <Q u}⟩

25-Sep-2019df-inp 6320 Define the set of positive reals. A "Dedekind cut" is a partition of the positive rational numbers into two classes such that all the numbers of one class are less than all the numbers of the other.

Here we follow the definition of a Dedekind cut from Definition 11.2.1 of [HoTT], p. (varies) with the one exception that we define it over positive rational numbers rather than all rational numbers.

A Dedekind cut is an ordered pair of a lower set 𝑙 and an upper set u which is inhabited (𝑞 Q𝑞 𝑙 𝑟 Q𝑟 u), rounded (𝑞 Q(𝑞 𝑙𝑟 Q(𝑞 <Q 𝑟 𝑟 𝑙)) and likewise for u), disjoint (𝑞 Q¬ (𝑞 𝑙 𝑞 u)) and located (𝑞 Q𝑟 Q(𝑞 <Q 𝑟 → (𝑞 𝑙 𝑟 u))). See HoTT for more discussion of those terms and different ways of defining Dedekind cuts.

(Note: This is a "temporary" definition used in the construction of complex numbers, and is intended to be used only by the construction.) (Contributed by Jim Kingdon, 25-Sep-2019.)

P = {⟨𝑙, u⟩ ∣ (((𝑙Q uQ) (𝑞 Q 𝑞 𝑙 𝑟 Q 𝑟 u)) ((𝑞 Q (𝑞 𝑙𝑟 Q (𝑞 <Q 𝑟 𝑟 𝑙)) 𝑟 Q (𝑟 u𝑞 Q (𝑞 <Q 𝑟 𝑞 u))) 𝑞 Q ¬ (𝑞 𝑙 𝑞 u) 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 𝑙 𝑟 u))))}

24-Sep-2019ltrnqi 6278 Ordering property of reciprocal for positive fractions. For the converse, see ltrnqg 6277. (Contributed by Jim Kingdon, 24-Sep-2019.)
(A <Q B → (*QB) <Q (*QA))

24-Sep-2019ltbtwnnqq 6272 There exists a number between any two positive fractions. Proposition 9-2.6(i) of [Gleason] p. 120. (Contributed by Jim Kingdon, 24-Sep-2019.)
(A <Q Bx Q (A <Q x x <Q B))

24-Sep-2019nsmallnqq 6269 There is no smallest positive fraction. (Contributed by Jim Kingdon, 24-Sep-2019.)
(A Qx Q x <Q A)

23-Sep-2019halfnqq 6267 One-half of any positive fraction is a fraction. (Contributed by Jim Kingdon, 23-Sep-2019.)
(A Qx Q (x +Q x) = A)

23-Sep-2019ltexnqq 6266 Ordering on positive fractions in terms of existence of sum. Definition in Proposition 9-2.6 of [Gleason] p. 119. (Contributed by Jim Kingdon, 23-Sep-2019.)
((A Q B Q) → (A <Q Bx Q (A +Q x) = B))

22-Sep-2019ltmnqg 6260 Ordering property of multiplication for positive fractions. Proposition 9-2.6(iii) of [Gleason] p. 120. (Contributed by Jim Kingdon, 22-Sep-2019.)
((A Q B Q 𝐶 Q) → (A <Q B ↔ (𝐶 ·Q A) <Q (𝐶 ·Q B)))

22-Sep-2019ltanqg 6259 Ordering property of addition for positive fractions. Proposition 9-2.6(ii) of [Gleason] p. 120. (Contributed by Jim Kingdon, 22-Sep-2019.)
((A Q B Q 𝐶 Q) → (A <Q B ↔ (𝐶 +Q A) <Q (𝐶 +Q B)))

21-Sep-2019nqtric 6258 Trichotomy for positive integers. (Contributed by Jim Kingdon, 21-Sep-2019.)
((A Q B Q) → (A <Q B ↔ ¬ (A = B B <Q A)))

21-Sep-2019nqtri3or 6255 Trichotomy for positive fractions. (Contributed by Jim Kingdon, 21-Sep-2019.)
((A Q B Q) → (A <Q B A = B B <Q A))

21-Sep-2019pitri3or 6182 Trichotomy for positive integers. (Contributed by Jim Kingdon, 21-Sep-2019.)
((A N B N) → (A <N B A = B B <N A))

21-Sep-2019pitric 6181 Trichotomy for positive integers. (Contributed by Jim Kingdon, 21-Sep-2019.)
((A N B N) → (A <N B ↔ ¬ (A = B B <N A)))

20-Sep-2019recex 6249 Existence of positive fraction reciprocal. (Contributed by Jim Kingdon, 20-Sep-2019.)
(A Qy(y Q (A ·Q y) = 1Q))

20-Sep-2019nqpi 6237 Decomposition of a positive fraction into numerator and denominator. Similar to dmaddpqlem 6236 but also shows that the numerator and denominator are positive integers. (Contributed by Jim Kingdon, 20-Sep-2019.)
(A Qwv((w N v N) A = [⟨w, v⟩] ~Q ))

20-Sep-2019df-rq 6211 Define reciprocal on positive fractions. It means the same thing as one divided by the argument (although we don't define full division since we will never need it). This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-2.5 of [Gleason] p. 119, who uses an asterisk to denote this unary operation. (Contributed by Jim Kingdon, 20-Sep-2019.)
*Q = {⟨x, y⟩ ∣ (x Q y Q (x ·Q y) = 1Q)}

19-Sep-2019recmulnqg 6250 Relationship between reciprocal and multiplication on positive fractions. (Contributed by Jim Kingdon, 19-Sep-2019.)
((A Q B Q) → ((*QA) = B ↔ (A ·Q B) = 1Q))

18-Sep-2019caovimo 5617 Uniqueness of inverse element in commutative, associative operation with identity. The identity element is B. (Contributed by Jim Kingdon, 18-Sep-2019.)
B 𝑆    &   ((x 𝑆 y 𝑆) → (x𝐹y) = (y𝐹x))    &   ((x 𝑆 y 𝑆 z 𝑆) → ((x𝐹y)𝐹z) = (x𝐹(y𝐹z)))    &   (x 𝑆 → (x𝐹B) = x)       (A 𝑆∃*w(w 𝑆 (A𝐹w) = B))

17-Sep-2019distrnqg 6246 Multiplication of positive fractions is distributive. (Contributed by Jim Kingdon, 17-Sep-2019.)
((A Q B Q 𝐶 Q) → (A ·Q (B +Q 𝐶)) = ((A ·Q B) +Q (A ·Q 𝐶)))

17-Sep-2019mulcanenqec 6245 Lemma for distributive law: cancellation of common factor. (Contributed by Jim Kingdon, 17-Sep-2019.)
((A N B N 𝐶 N) → [⟨(A ·N B), (A ·N 𝐶)⟩] ~Q = [⟨B, 𝐶⟩] ~Q )

17-Sep-2019mulassnqg 6243 Multiplication of positive fractions is associative. (Contributed by Jim Kingdon, 17-Sep-2019.)
((A Q B Q 𝐶 Q) → ((A ·Q B) ·Q 𝐶) = (A ·Q (B ·Q 𝐶)))

17-Sep-2019mulcomnqg 6242 Multiplication of positive fractions is commutative. (Contributed by Jim Kingdon, 17-Sep-2019.)
((A Q B Q) → (A ·Q B) = (B ·Q A))

17-Sep-2019ecovidi 6129 Lemma used to transfer a distributive law via an equivalence relation. (Contributed by Jim Kingdon, 17-Sep-2019.)
𝐷 = ((𝑆 × 𝑆) / )    &   (((z 𝑆 w 𝑆) (v 𝑆 u 𝑆)) → ([⟨z, w⟩] + [⟨v, u⟩] ) = [⟨𝑀, 𝑁⟩] )    &   (((x 𝑆 y 𝑆) (𝑀 𝑆 𝑁 𝑆)) → ([⟨x, y⟩] · [⟨𝑀, 𝑁⟩] ) = [⟨𝐻, 𝐽⟩] )    &   (((x 𝑆 y 𝑆) (z 𝑆 w 𝑆)) → ([⟨x, y⟩] · [⟨z, w⟩] ) = [⟨𝑊, 𝑋⟩] )    &   (((x 𝑆 y 𝑆) (v 𝑆 u 𝑆)) → ([⟨x, y⟩] · [⟨v, u⟩] ) = [⟨𝑌, 𝑍⟩] )    &   (((𝑊 𝑆 𝑋 𝑆) (𝑌 𝑆 𝑍 𝑆)) → ([⟨𝑊, 𝑋⟩] + [⟨𝑌, 𝑍⟩] ) = [⟨𝐾, 𝐿⟩] )    &   (((z 𝑆 w 𝑆) (v 𝑆 u 𝑆)) → (𝑀 𝑆 𝑁 𝑆))    &   (((x 𝑆 y 𝑆) (z 𝑆 w 𝑆)) → (𝑊 𝑆 𝑋 𝑆))    &   (((x 𝑆 y 𝑆) (v 𝑆 u 𝑆)) → (𝑌 𝑆 𝑍 𝑆))    &   (((x 𝑆 y 𝑆) (z 𝑆 w 𝑆) (v 𝑆 u 𝑆)) → 𝐻 = 𝐾)    &   (((x 𝑆 y 𝑆) (z 𝑆 w 𝑆) (v 𝑆 u 𝑆)) → 𝐽 = 𝐿)       ((A 𝐷 B 𝐷 𝐶 𝐷) → (A · (B + 𝐶)) = ((A · B) + (A · 𝐶)))

16-Sep-2019addassnqg 6241 Addition of positive fractions is associative. (Contributed by Jim Kingdon, 16-Sep-2019.)
((A Q B Q 𝐶 Q) → ((A +Q B) +Q 𝐶) = (A +Q (B +Q 𝐶)))

16-Sep-2019ecoviass 6127 Lemma used to transfer an associative law via an equivalence relation. (Contributed by Jim Kingdon, 16-Sep-2019.)
𝐷 = ((𝑆 × 𝑆) / )    &   (((x 𝑆 y 𝑆) (z 𝑆 w 𝑆)) → ([⟨x, y⟩] + [⟨z, w⟩] ) = [⟨𝐺, 𝐻⟩] )    &   (((z 𝑆 w 𝑆) (v 𝑆 u 𝑆)) → ([⟨z, w⟩] + [⟨v, u⟩] ) = [⟨𝑁, 𝑄⟩] )    &   (((𝐺 𝑆 𝐻 𝑆) (v 𝑆 u 𝑆)) → ([⟨𝐺, 𝐻⟩] + [⟨v, u⟩] ) = [⟨𝐽, 𝐾⟩] )    &   (((x 𝑆 y 𝑆) (𝑁 𝑆 𝑄 𝑆)) → ([⟨x, y⟩] + [⟨𝑁, 𝑄⟩] ) = [⟨𝐿, 𝑀⟩] )    &   (((x 𝑆 y 𝑆) (z 𝑆 w 𝑆)) → (𝐺 𝑆 𝐻 𝑆))    &   (((z 𝑆 w 𝑆) (v 𝑆 u 𝑆)) → (𝑁 𝑆 𝑄 𝑆))    &   (((x 𝑆 y 𝑆) (z 𝑆 w 𝑆) (v 𝑆 u 𝑆)) → 𝐽 = 𝐿)    &   (((x 𝑆 y 𝑆) (z 𝑆 w 𝑆) (v 𝑆 u 𝑆)) → 𝐾 = 𝑀)       ((A 𝐷 B 𝐷 𝐶 𝐷) → ((A + B) + 𝐶) = (A + (B + 𝐶)))

16-Sep-2019caovdilemd 5615 Lemma used by real number construction. (Contributed by Jim Kingdon, 16-Sep-2019.)
((φ (x 𝑆 y 𝑆)) → (x𝐺y) = (y𝐺x))    &   ((φ (x 𝑆 y 𝑆 z 𝑆)) → ((x𝐹y)𝐺z) = ((x𝐺z)𝐹(y𝐺z)))    &   ((φ (x 𝑆 y 𝑆 z 𝑆)) → ((x𝐺y)𝐺z) = (x𝐺(y𝐺z)))    &   ((φ (x 𝑆 y 𝑆)) → (x𝐺y) 𝑆)    &   (φA 𝑆)    &   (φB 𝑆)    &   (φ𝐶 𝑆)    &   (φ𝐷 𝑆)    &   (φ𝐻 𝑆)       (φ → (((A𝐺𝐶)𝐹(B𝐺𝐷))𝐺𝐻) = ((A𝐺(𝐶𝐺𝐻))𝐹(B𝐺(𝐷𝐺𝐻))))

15-Sep-2019addcomnqg 6240 Addition of positive fractions is commutative. (Contributed by Jim Kingdon, 15-Sep-2019.)
((A Q B Q) → (A +Q B) = (B +Q A))

15-Sep-2019dmaddpqlem 6236 Decomposition of a positive fraction into numerator and denominator. Lemma for dmaddpq 6238. (Contributed by Jim Kingdon, 15-Sep-2019.)
(x Qwv x = [⟨w, v⟩] ~Q )

15-Sep-2019ecovicom 6125 Lemma used to transfer a commutative law via an equivalence relation. (Contributed by Jim Kingdon, 15-Sep-2019.)
𝐶 = ((𝑆 × 𝑆) / )    &   (((x 𝑆 y 𝑆) (z 𝑆 w 𝑆)) → ([⟨x, y⟩] + [⟨z, w⟩] ) = [⟨𝐷, 𝐺⟩] )    &   (((z 𝑆 w 𝑆) (x 𝑆 y 𝑆)) → ([⟨z, w⟩] + [⟨x, y⟩] ) = [⟨𝐻, 𝐽⟩] )    &   (((x 𝑆 y 𝑆) (z 𝑆 w 𝑆)) → 𝐷 = 𝐻)    &   (((x 𝑆 y 𝑆) (z 𝑆 w 𝑆)) → 𝐺 = 𝐽)       ((A 𝐶 B 𝐶) → (A + B) = (B + A))

14-Sep-2019ordpipqqs 6233 Ordering of positive fractions in terms of positive integers. (Contributed by Jim Kingdon, 14-Sep-2019.)
(((A N B N) (𝐶 N 𝐷 N)) → ([⟨A, B⟩] ~Q <Q [⟨𝐶, 𝐷⟩] ~Q ↔ (A ·N 𝐷) <N (B ·N 𝐶)))

13-Sep-2019dfmpq2 6214 Alternative definition of pre-multiplication on positive fractions. (Contributed by Jim Kingdon, 13-Sep-2019.)
·pQ = {⟨⟨x, y⟩, z⟩ ∣ ((x (N × N) y (N × N)) wvuf((x = ⟨w, v y = ⟨u, f⟩) z = ⟨(w ·N u), (v ·N f)⟩))}

12-Sep-2019dfplpq2 6213 Alternative definition of pre-addition on positive fractions. (Contributed by Jim Kingdon, 12-Sep-2019.)
+pQ = {⟨⟨x, y⟩, z⟩ ∣ ((x (N × N) y (N × N)) wvuf((x = ⟨w, v y = ⟨u, f⟩) z = ⟨((w ·N f) +N (v ·N u)), (v ·N f)⟩))}

(((A N B N) (𝐶 N 𝐷 N)) → ⟨((A ·N 𝐷) +N (B ·N 𝐶)), (B ·N 𝐷)⟩ (N × N))

7-Sep-2019enqdc1 6221 The equivalence relation for positive fractions is decidable. (Contributed by Jim Kingdon, 7-Sep-2019.)
(((A N B N) 𝐶 (N × N)) → DECIDA, B⟩ ~Q 𝐶)

7-Sep-2019enqdc 6220 The equivalence relation for positive fractions is decidable. (Contributed by Jim Kingdon, 7-Sep-2019.)
(((A N B N) (𝐶 N 𝐷 N)) → DECIDA, B⟩ ~Q𝐶, 𝐷⟩)

7-Sep-2019dcbid 739 The equivalent of a decidable proposition is decidable. (Contributed by Jim Kingdon, 7-Sep-2019.)
(φ → (ψχ))       (φ → (DECID ψDECID χ))

6-Sep-2019nndcel 5991 Set membership between two natural numbers is decidable. (Contributed by Jim Kingdon, 6-Sep-2019.)
((A 𝜔 B 𝜔) → DECID A B)

6-Sep-2019nnregexmid 4269 If inhabited sets of natural numbers always have minimal elements, excluded middle follows. The argument is essentially the same as regexmid 4203 and the larger lesson is that although natural numbers may behave "non-constructively" even in a constructive set theory (for example see nndceq 5990 or nntri3or 5987), sets of natural numbers are a different animal. (Contributed by Jim Kingdon, 6-Sep-2019.)
((x ⊆ 𝜔 y y x) → y(y x z(z y → ¬ z x)))       (φ ¬ φ)

3-Sep-2019regexmid 4203 The axiom of foundation implies excluded middle.

By foundation (or regularity), we mean the principle that every inhabited set has an element which is minimal (when arranged by ). The statement of foundation here is taken from Metamath Proof Explorer's ax-reg, and is identical (modulo one unnecessary quantifier) to the statement of foundation in Theorem "Foundation implies instances of EM" of [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic".

For this reason, IZF does not adopt foundation as an axiom and instead replaces it with ax-setind 4204. (Contributed by Jim Kingdon, 3-Sep-2019.)

(y y xy(y x z(z y → ¬ z x)))       (φ ¬ φ)

3-Sep-2019regexmidlem1 4202 Lemma for regexmid 4203. If A has a minimal element, excluded middle follows. (Contributed by Jim Kingdon, 3-Sep-2019.)
A = {x {∅, {∅}} ∣ (x = {∅} (x = ∅ φ))}       (y(y A z(z y → ¬ z A)) → (φ ¬ φ))

3-Sep-2019regexmidlemm 4201 Lemma for regexmid 4203. A is inhabited. (Contributed by Jim Kingdon, 3-Sep-2019.)
A = {x {∅, {∅}} ∣ (x = {∅} (x = ∅ φ))}       y y A

1-Sep-2019ecopoverg 6118 Assuming that operation 𝐹 is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation , specified by the first hypothesis, is an equivalence relation. (Contributed by Jim Kingdon, 1-Sep-2019.)
= {⟨x, y⟩ ∣ ((x (𝑆 × 𝑆) y (𝑆 × 𝑆)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z + u) = (w + v)))}    &   ((x 𝑆 y 𝑆) → (x + y) = (y + x))    &   ((x 𝑆 y 𝑆) → (x + y) 𝑆)    &   ((x 𝑆 y 𝑆 z 𝑆) → ((x + y) + z) = (x + (y + z)))    &   ((x 𝑆 y 𝑆 z 𝑆) → ((x + y) = (x + z) → y = z))        Er (𝑆 × 𝑆)

1-Sep-2019ecopovtrng 6117 Assuming that operation 𝐹 is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation , specified by the first hypothesis, is transitive. (Contributed by Jim Kingdon, 1-Sep-2019.)
= {⟨x, y⟩ ∣ ((x (𝑆 × 𝑆) y (𝑆 × 𝑆)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z + u) = (w + v)))}    &   ((x 𝑆 y 𝑆) → (x + y) = (y + x))    &   ((x 𝑆 y 𝑆) → (x + y) 𝑆)    &   ((x 𝑆 y 𝑆 z 𝑆) → ((x + y) + z) = (x + (y + z)))    &   ((x 𝑆 y 𝑆 z 𝑆) → ((x + y) = (x + z) → y = z))       ((A B B 𝐶) → A 𝐶)

1-Sep-2019ecopovsymg 6116 Assuming the operation 𝐹 is commutative, show that the relation , specified by the first hypothesis, is symmetric. (Contributed by Jim Kingdon, 1-Sep-2019.)
= {⟨x, y⟩ ∣ ((x (𝑆 × 𝑆) y (𝑆 × 𝑆)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z + u) = (w + v)))}    &   ((x 𝑆 y 𝑆) → (x + y) = (y + x))       (A BB A)

31-Aug-2019nlt1pig 6201 No positive integer is less than one. (Contributed by Jim Kingdon, 31-Aug-2019.)
(A N → ¬ A <N 1𝑜)

31-Aug-2019ltmpig 6199 Ordering property of multiplication for positive integers. (Contributed by Jim Kingdon, 31-Aug-2019.)
((A N B N 𝐶 N) → (A <N B ↔ (𝐶 ·N A) <N (𝐶 ·N B)))

31-Aug-2019ltapig 6198 Ordering property of addition for positive integers. (Contributed by Jim Kingdon, 31-Aug-2019.)
((A N B N 𝐶 N) → (A <N B ↔ (𝐶 +N A) <N (𝐶 +N B)))

31-Aug-2019nndceq 5990 Equality of natural numbers is decidable. Theorem 7.2.6 of [HoTT], p. (varies). For the specific case where B is zero, see nndceq0 4266. (Contributed by Jim Kingdon, 31-Aug-2019.)
((A 𝜔 B 𝜔) → DECID A = B)

29-Aug-2019mulcanpig 6195 Multiplication cancellation law for positive integers. (Contributed by Jim Kingdon, 29-Aug-2019.)
((A N B N 𝐶 N) → ((A ·N B) = (A ·N 𝐶) ↔ B = 𝐶))

29-Aug-2019frecrdg 5908 Transfinite recursion restricted to omega.

Given a suitable characteristic function, df-frec 5898 produces the same results as df-irdg 5878 restricted to 𝜔. (Contributed by Jim Kingdon, 29-Aug-2019.)

(φ𝐹 Fn V)    &   (φA 𝑉)    &   (φx x ⊆ (𝐹x))       (φ → frec(𝐹, A) = (rec(𝐹, A) ↾ 𝜔))

29-Aug-2019rdgisucinc 5892 Value of the recursive definition generator at a successor.

This can be thought of as a generalization of oasuc 5959 and omsuc 5966. (Contributed by Jim Kingdon, 29-Aug-2019.)

(φ𝐹 Fn V)    &   (φA 𝑉)    &   (φB On)    &   (φx x ⊆ (𝐹x))       (φ → (rec(𝐹, A)‘suc B) = (𝐹‘(rec(𝐹, A)‘B)))

28-Aug-2019nntri1 5989 A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 28-Aug-2019.)
((A 𝜔 B 𝜔) → (AB ↔ ¬ B A))

28-Aug-2019nntri2 5988 A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 28-Aug-2019.)
((A 𝜔 B 𝜔) → (A B ↔ ¬ (A = B B A)))

28-Aug-2019nn0eln0 4268 A natural number is nonempty iff it contains the empty set. Although in constructive mathematics it is generally more natural to work with inhabited sets and ignore the whole concept of nonempty sets, in the specific case of natural numbers this theorem may be helpful in converting proofs which were written assuming excluded middle. (Contributed by Jim Kingdon, 28-Aug-2019.)
(A 𝜔 → (∅ AA ≠ ∅))

27-Aug-2019addcanpig 6194 Addition cancellation law for positive integers. (Contributed by Jim Kingdon, 27-Aug-2019.)
((A N B N 𝐶 N) → ((A +N B) = (A +N 𝐶) ↔ B = 𝐶))

26-Aug-2019distrpig 6193 Multiplication of positive integers is distributive. (Contributed by Jim Kingdon, 26-Aug-2019.)
((A N B N 𝐶 N) → (A ·N (B +N 𝐶)) = ((A ·N B) +N (A ·N 𝐶)))

26-Aug-2019mulasspig 6192 Multiplication of positive integers is associative. (Contributed by Jim Kingdon, 26-Aug-2019.)
((A N B N 𝐶 N) → ((A ·N B) ·N 𝐶) = (A ·N (B ·N 𝐶)))

26-Aug-2019mulcompig 6191 Multiplication of positive integers is commutative. (Contributed by Jim Kingdon, 26-Aug-2019.)
((A N B N) → (A ·N B) = (B ·N A))

26-Aug-2019addasspig 6190 Addition of positive integers is associative. (Contributed by Jim Kingdon, 26-Aug-2019.)
((A N B N 𝐶 N) → ((A +N B) +N 𝐶) = (A +N (B +N 𝐶)))

26-Aug-2019addcompig 6189 Addition of positive integers is commutative. (Contributed by Jim Kingdon, 26-Aug-2019.)
((A N B N) → (A +N B) = (B +N A))

25-Aug-2019nntri3or 5987 Trichotomy for natural numbers. (Contributed by Jim Kingdon, 25-Aug-2019.)
((A 𝜔 B 𝜔) → (A B A = B B A))

25-Aug-2019nnsucsssuc 5986 Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucsssucr 4184, but the forward direction, for all ordinals, implies excluded middle as seen as onsucsssucexmid 4196. (Contributed by Jim Kingdon, 25-Aug-2019.)
((A 𝜔 B 𝜔) → (AB ↔ suc A ⊆ suc B))

25-Aug-2019nnsucelsuc 5985 Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucelsucr 4183, but the forward direction, for all ordinals, implies excluded middle as seen as onsucelsucexmid 4199. (Contributed by Jim Kingdon, 25-Aug-2019.)
(B 𝜔 → (A B ↔ suc A suc B))

23-Aug-2019omv2 5960 Value of ordinal multiplication. (Contributed by Jim Kingdon, 23-Aug-2019.)
((A On B On) → (A ·𝑜 B) = x B ((A ·𝑜 x) +𝑜 A))

23-Aug-2019omfnex 5944 The characteristic function for ordinal multiplication is defined everywhere. (Contributed by Jim Kingdon, 23-Aug-2019.)
(A 𝑉 → (x V ↦ (x +𝑜 A)) Fn V)

23-Aug-20190elnn 4267 A natural number is either the empty set or has the empty set as an element. (Contributed by Jim Kingdon, 23-Aug-2019.)
(A 𝜔 → (A = ∅ A))

22-Aug-2019xpiderm 6088 A square Cartesian product is an equivalence relation (in general it's not a poset). (Contributed by Jim Kingdon, 22-Aug-2019.)
(x x A → (A × A) Er A)

21-Aug-2019elqsn0m 6085 An element of a quotient set is inhabited. (Contributed by Jim Kingdon, 21-Aug-2019.)
((dom 𝑅 = A B (A / 𝑅)) → x x B)

21-Aug-2019ecdmn0m 6059 A representative of an inhabited equivalence class belongs to the domain of the equivalence relation. (Contributed by Jim Kingdon, 21-Aug-2019.)
(A dom 𝑅x x [A]𝑅)

18-Aug-2019unisucg 4100 A transitive class is equal to the union of its successor. Combines Theorem 4E of [Enderton] p. 72 and Exercise 6 of [Enderton] p. 73. (Contributed by Jim Kingdon, 18-Aug-2019.)
(A 𝑉 → (Tr A suc A = A))

16-Aug-2019frecabex 5899 The class abstraction from df-frec 5898 exists. This is a lemma for several other finite recursion proofs. (Contributed by Jim Kingdon, 16-Aug-2019.)
(φ𝑆 𝑉)    &   (φ𝐹 Fn V)    &   (φA 𝑊)       (φ → {x ∣ (𝑚 𝜔 (dom 𝑆 = suc 𝑚 x (𝐹‘(𝑆𝑚))) (dom 𝑆 = ∅ x A))} V)

15-Aug-2019frecsuc 5907 The successor value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 15-Aug-2019.)
((𝐹 Fn V A 𝑉 B 𝜔) → (frec(𝐹, A)‘suc B) = (𝐹‘(frec(𝐹, A)‘B)))

15-Aug-2019frecsuclem3 5906 Lemma for frecsuc 5907. (Contributed by Jim Kingdon, 15-Aug-2019.)
𝐺 = (g V ↦ {x ∣ (𝑚 𝜔 (dom g = suc 𝑚 x (𝐹‘(g𝑚))) (dom g = ∅ x A))})       ((𝐹 Fn V A 𝑉 B 𝜔) → (frec(𝐹, A)‘suc B) = (𝐹‘(frec(𝐹, A)‘B)))

15-Aug-2019frecsuclem2 5905 Lemma for frecsuc 5907. (Contributed by Jim Kingdon, 15-Aug-2019.)
𝐺 = (g V ↦ {x ∣ (𝑚 𝜔 (dom g = suc 𝑚 x (𝐹‘(g𝑚))) (dom g = ∅ x A))})       ((𝐹 Fn V A 𝑉 B 𝜔) → ((recs(𝐺) ↾ suc B)‘B) = (frec(𝐹, A)‘B))

15-Aug-2019frecsuclemdm 5904 Lemma for frecsuc 5907. (Contributed by Jim Kingdon, 15-Aug-2019.)
𝐺 = (g V ↦ {x ∣ (𝑚 𝜔 (dom g = suc 𝑚 x (𝐹‘(g𝑚))) (dom g = ∅ x A))})       ((𝐹 Fn V A 𝑉 B 𝜔) → dom (recs(𝐺) ↾ suc B) = suc B)

15-Aug-2019frectfr 5900 Lemma to connect transfinite recursion theorems with finite recursion. That is, given the conditions 𝐹 Fn V and A 𝑉 on frec(𝐹, A), we want to be able to apply tfri1d 5871 or tfri2d 5872, and this lemma lets us satisfy hypotheses of those theorems.

(Contributed by Jim Kingdon, 15-Aug-2019.)

𝐺 = (g V ↦ {x ∣ (𝑚 𝜔 (dom g = suc 𝑚 x (𝐹‘(g𝑚))) (dom g = ∅ x A))})       ((𝐹 Fn V A 𝑉) → y(Fun 𝐺 (𝐺y) V))

13-Aug-2019frecsuclem1 5903 Lemma for frecsuc 5907. (Contributed by Jim Kingdon, 13-Aug-2019.)
𝐺 = (g V ↦ {x ∣ (𝑚 𝜔 (dom g = suc 𝑚 x (𝐹‘(g𝑚))) (dom g = ∅ x A))})       ((𝐹 Fn V A 𝑉 B 𝜔) → (frec(𝐹, A)‘suc B) = (𝐺‘(recs(𝐺) ↾ suc B)))

12-Aug-2019oav2 5958 Value of ordinal addition. (Contributed by Mario Carneiro and Jim Kingdon, 12-Aug-2019.)
((A On B On) → (A +𝑜 B) = (A x B suc (A +𝑜 x)))

11-Aug-2019frec0g 5902 The initial value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 11-Aug-2019.)
((𝐹 Fn V A 𝑉) → (frec(𝐹, A)‘∅) = A)

11-Aug-2019frecfnom 5901 The function generated by finite recursive definition generation is a function on omega. (Contributed by Jim Kingdon, 11-Aug-2019.)
((𝐹 Fn V A 𝑉) → frec(𝐹, A) Fn 𝜔)

10-Aug-2019df-frec 5898 Define a recursive definition generator on 𝜔 (the class of finite ordinals) with characteristic function 𝐹 and initial value 𝐼. This rather amazing operation allows us to define, with compact direct definitions, functions that are usually defined in textbooks only with indirect self-referencing recursive definitions. A recursive definition requires advanced metalogic to justify - in particular, eliminating a recursive definition is very difficult and often not even shown in textbooks. On the other hand, the elimination of a direct definition is a matter of simple mechanical substitution. The price paid is the daunting complexity of our frec operation (especially when df-recs 5842 that it is built on is also eliminated). But once we get past this hurdle, definitions that would otherwise be recursive become relatively simple; see frec0g 5902 and frecsuc 5907.

Unlike with transfinite recursion, finite recurson can readily divide definitions and proofs into zero and successor cases, because even without excluded middle we have theorems such as nn0suc 4254. The analogous situation with transfinite recursion - being able to say that an ordinal is zero, successor, or limit - is enabled by excluded middle and thus is not available to us. For the characteristic functions which satisfy the conditions given at frecrdg 5908, this definition and df-irdg 5878 restricted to 𝜔 produce the same result.

Note: We introduce frec with the philosophical goal of being able to eliminate all definitions with direct mechanical substitution and to verify easily the soundness of definitions. Metamath itself has no built-in technical limitation that prevents multiple-part recursive definitions in the traditional textbook style. (Contributed by Mario Carneiro and Jim Kingdon, 10-Aug-2019.)

frec(𝐹, 𝐼) = (recs((g V ↦ {x ∣ (𝑚 𝜔 (dom g = suc 𝑚 x (𝐹‘(g𝑚))) (dom g = ∅ x 𝐼))})) ↾ 𝜔)

7-Aug-2019acexmidlem1 5432 Lemma for acexmid 5435. List the cases identified in acexmidlemcase 5431 and hook them up to the lemmas which handle each case. (Contributed by Jim Kingdon, 7-Aug-2019.)
A = {x {∅, {∅}} ∣ (x = ∅ φ)}    &   B = {x {∅, {∅}} ∣ (x = {∅} φ)}    &   𝐶 = {A, B}       (z 𝐶 ∃!v z u y (z u v u) → (φ ¬ φ))

7-Aug-2019acexmidlemcase 5431 Lemma for acexmid 5435. Here we divide the proof into cases (based on the disjunction implicit in an unordered pair, not the sort of case elimination which relies on excluded middle).

The cases are (1) the choice function evaluated at A equals {∅}, (2) the choice function evaluated at B equals , and (3) the choice function evaluated at A equals and the choice function evaluated at B equals {∅}.

Because of the way we represent the choice function y, the choice function evaluated at A is (v Au y(A u v u)) and the choice function evaluated at B is (v Bu y(B u v u)). Other than the difference in notation these work just as (yA) and (yB) would if y were a function as defined by df-fun 4831.

Although it isn't exactly about the division into cases, it is also convenient for this lemma to also include the step that if the choice function evaluated at A equals {∅}, then {∅} A and likewise for B.

(Contributed by Jim Kingdon, 7-Aug-2019.)

A = {x {∅, {∅}} ∣ (x = ∅ φ)}    &   B = {x {∅, {∅}} ∣ (x = {∅} φ)}    &   𝐶 = {A, B}       (z 𝐶 ∃!v z u y (z u v u) → ({∅} A B ((v A u y (A u v u)) = ∅ (v B u y (B u v u)) = {∅})))

6-Aug-2019acexmidlemv 5434 Lemma for acexmid 5435.

This is acexmid 5435 with additional distinct variable constraints, most notably between φ and x.

(Contributed by Jim Kingdon, 6-Aug-2019.)

yz x w z ∃!v z u y (z u v u)       (φ ¬ φ)

6-Aug-2019acexmidlemab 5430 Lemma for acexmid 5435. (Contributed by Jim Kingdon, 6-Aug-2019.)
A = {x {∅, {∅}} ∣ (x = ∅ φ)}    &   B = {x {∅, {∅}} ∣ (x = {∅} φ)}    &   𝐶 = {A, B}       (((v A u y (A u v u)) = ∅ (v B u y (B u v u)) = {∅}) → ¬ φ)

6-Aug-2019acexmidlemph 5429 Lemma for acexmid 5435. (Contributed by Jim Kingdon, 6-Aug-2019.)
A = {x {∅, {∅}} ∣ (x = ∅ φ)}    &   B = {x {∅, {∅}} ∣ (x = {∅} φ)}    &   𝐶 = {A, B}       (φA = B)

6-Aug-2019acexmidlemb 5428 Lemma for acexmid 5435. (Contributed by Jim Kingdon, 6-Aug-2019.)
A = {x {∅, {∅}} ∣ (x = ∅ φ)}    &   B = {x {∅, {∅}} ∣ (x = {∅} φ)}    &   𝐶 = {A, B}       (∅ Bφ)

6-Aug-2019acexmidlema 5427 Lemma for acexmid 5435. (Contributed by Jim Kingdon, 6-Aug-2019.)
A = {x {∅, {∅}} ∣ (x = ∅ φ)}    &   B = {x {∅, {∅}} ∣ (x = {∅} φ)}    &   𝐶 = {A, B}       ({∅} Aφ)

5-Aug-2019acexmidlem2 5433 Lemma for acexmid 5435. This builds on acexmidlem1 5432 by noting that every element of 𝐶 is inhabited.

(Note that y is not quite a function in the df-fun 4831 sense because it uses ordered pairs as described in opthreg 4218 rather than df-op 3359).

The set A is also found in onsucelsucexmidlem 4198.

(Contributed by Jim Kingdon, 5-Aug-2019.)

A = {x {∅, {∅}} ∣ (x = ∅ φ)}    &   B = {x {∅, {∅}} ∣ (x = {∅} φ)}    &   𝐶 = {A, B}       (z 𝐶 w z ∃!v z u y (z u v u) → (φ ¬ φ))

4-Aug-2019acexmid 5435 The axiom of choice implies excluded middle. Theorem 1.3 in [Bauer] p. 483.

The statement of the axiom of choice given here is ac2 in the Metamath Proof Explorer (version of 3-Aug-2019). In particular, note that the choice function y provides a value when z is inhabited (as opposed to non-empty as in some statements of the axiom of choice).

Essentially the same proof can also be found at "The axiom of choice implies instances of EM", [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic".

Often referred to as Diaconescu's theorem, or Diaconescu-Goodman-Myhill theorem, after Radu Diaconescu who discovered it in 1975 in the framework of topos theory and N. D. Goodman and John Myhill in 1978 in the framework of set theory (although it already appeared as an exercise in Errett Bishop's book Foundations of Constructive Analysis from 1967).

(Contributed by Jim Kingdon, 4-Aug-2019.)

yz x w z ∃!v z u y (z u v u)       (φ ¬ φ)

2-Aug-2019ordsucunielexmid 4200 The converse of sucunielr 4185 (where B is an ordinal) implies excluded middle. (Contributed by Jim Kingdon, 2-Aug-2019.)
x On y On (x y → suc x y)       (φ ¬ φ)

2-Aug-2019onsucelsucexmid 4199 The converse of onsucelsucr 4183 implies excluded middle. On the other hand, if y is constrained to be a natural number, instead of an arbitrary ordinal, then the converse of onsucelsucr 4183 does hold, as seen at nnsucelsuc 5985. (Contributed by Jim Kingdon, 2-Aug-2019.)
x On y On (x y → suc x suc y)       (φ ¬ φ)

2-Aug-2019onsucelsucexmidlem 4198 Lemma for onsucelsucexmid 4199. The set {x {∅, {∅}} ∣ (x = ∅ φ)} appears as A in the proof of Theorem 1.3 in [Bauer] p. 483 (see acexmidlema 5427), and similar sets also appear in other proofs that various propositions imply excluded middle, for example in ordtriexmidlem 4192. (Contributed by Jim Kingdon, 2-Aug-2019.)
{x {∅, {∅}} ∣ (x = ∅ φ)} On

2-Aug-2019onsucelsucexmidlem1 4197 Lemma for onsucelsucexmid 4199. (Contributed by Jim Kingdon, 2-Aug-2019.)
{x {∅, {∅}} ∣ (x = ∅ φ)}

2-Aug-2019onuniss2 4187 The union of the ordinal subsets of an ordinal number is that number. (Contributed by Jim Kingdon, 2-Aug-2019.)
(A On → {x On ∣ xA} = A)

2-Aug-2019sucunielr 4185 Successor and union. The converse (where B is an ordinal) implies excluded middle, as seen at ordsucunielexmid 4200. (Contributed by Jim Kingdon, 2-Aug-2019.)
(suc A BA B)

31-Jul-2019ordtri2orexmid 4195 Ordinal trichotomy implies excluded middle. (Contributed by Jim Kingdon, 31-Jul-2019.)
x On y On (x y yx)       (φ ¬ φ)

30-Jul-2019ordpwsucexmid 4230 The subset in ordpwsucss 4227 cannot be equality. That is, strengthening it to equality implies excluded middle. (Contributed by Jim Kingdon, 30-Jul-2019.)
x On suc x = (𝒫 x ∩ On)       (φ ¬ φ)

29-Jul-2019onsucsssucexmid 4196 The converse of onsucsssucr 4184 implies excluded middle. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2019.)
x On y On (xy → suc x ⊆ suc y)       (φ ¬ φ)

29-Jul-2019onsucsssucr 4184 The subclass relationship between two ordinals is inherited by their predecessors. The converse implies excluded middle, as shown at onsucsssucexmid 4196. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2019.)
((A On Ord B) → (suc A ⊆ suc BAB))

27-Jul-2019oawordi 5964 Weak ordering property of ordinal addition. (Contributed by Jim Kingdon, 27-Jul-2019.)
((A On B On 𝐶 On) → (AB → (𝐶 +𝑜 A) ⊆ (𝐶 +𝑜 B)))

27-Jul-2019oafnex 5939 The characteristic function for ordinal addition is defined everywhere. (Contributed by Jim Kingdon, 27-Jul-2019.)
(x V ↦ suc x) Fn V

26-Jul-2019oeicl 5957 Closure law for ordinal exponentiation. (Contributed by Jim Kingdon, 26-Jul-2019.)
((A On B On) → (A𝑜 B) On)

26-Jul-2019rdgon 5893 Evaluating the recursive definition generator produces an ordinal. There is a hypothesis that the characteristic function produces ordinals on ordinal arguments. (Contributed by Jim Kingdon, 26-Jul-2019.)
(φ𝐹 Fn V)    &   (φA On)    &   (φx On (𝐹x) On)       ((φ B On) → (rec(𝐹, A)‘B) On)

26-Jul-2019rdgival 5889 Value of the recursive definition generator. (Contributed by Jim Kingdon, 26-Jul-2019.)
((𝐹 Fn V A 𝑉 B On) → (rec(𝐹, A)‘B) = (A x B (𝐹‘(rec(𝐹, A)‘x))))

25-Jul-2019onun2 4166 The union of two ordinal numbers is an ordinal number. (Contributed by Jim Kingdon, 25-Jul-2019.)
((A On B On) → (AB) On)

25-Jul-2019prexgOLD 3920 The Axiom of Pairing using class variables. Theorem 7.13 of [Quine] p. 51, but restricted to classes which exist. For proper classes, see prprc 3454, prprc1 3452, and prprc2 3453. This is a special case of prexg 3921 and new proofs should use prexg 3921 instead. (Contributed by Jim Kingdon, 25-Jul-2019.) (New usage is discouraged.) TODO: remove in favor of prexg 3921.
((A V B V) → {A, B} V)

24-Jul-2019nfnt 1528 If x is not free in φ, then it is not free in ¬ φ. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 28-Dec-2017.) (Revised by BJ, 24-Jul-2019.)
(Ⅎxφ → Ⅎx ¬ φ)

22-Jul-2019ssnel 4229 Relationship between subset and elementhood. In the context of ordinals this can be seen as an ordering law. (Contributed by Jim Kingdon, 22-Jul-2019.)
(AB → ¬ B A)

21-Jul-2019ordpwsucss 4227 The collection of ordinals in the power class of an ordinal is a superset of its successor.

We can think of (𝒫 A ∩ On) as another possible definition of successor, which would be equivalent to df-suc 4057 given excluded middle. It is an ordinal, and has some successor-like properties. For example, if A On then both suc A = A (onunisuci 4119) and {x On ∣ xA} = A (onuniss2 4187).

Constructively (𝒫 A ∩ On) and suc A cannot be shown to be equivalent (as proved at ordpwsucexmid 4230). (Contributed by Jim Kingdon, 21-Jul-2019.)

(Ord A → suc A ⊆ (𝒫 A ∩ On))

21-Jul-2019dfnot 1247 Given falsum, we can define the negation of a wff φ as the statement that a contradiction follows from assuming φ. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof shortened by Wolf Lammen, 21-Jul-2019.)
φ ↔ (φ → ⊥ ))

21-Jul-2019truan 1245 True can be removed from a conjunction. (Contributed by FL, 20-Mar-2011.) (Proof shortened by Wolf Lammen, 21-Jul-2019.)
(( ⊤ φ) ↔ φ)

17-Jul-2019onsucelsucr 4183 Membership is inherited by predecessors. The converse, for all ordinals, implies excluded middle, as shown at onsucelsucexmid 4199. However, the converse does hold where B is a natural number, as seen at nnsucelsuc 5985. (Contributed by Jim Kingdon, 17-Jul-2019.)
(B On → (suc A suc BA B))

15-Jul-2019rdgss 5890 Subset and recursive definition generator. (Contributed by Jim Kingdon, 15-Jul-2019.)
(φ𝐹 Fn V)    &   (φ𝐼 𝑉)    &   (φA On)    &   (φB On)    &   (φAB)       (φ → (rec(𝐹, 𝐼)‘A) ⊆ (rec(𝐹, 𝐼)‘B))

14-Jul-2019sucinc2 5941 Successor is increasing. (Contributed by Jim Kingdon, 14-Jul-2019.)
𝐹 = (z V ↦ suc z)       ((B On A B) → (𝐹A) ⊆ (𝐹B))

13-Jul-2019rdgivallem 5888 Value of the recursive definition generator. Lemma for rdgival 5889 which simplifies the value further. (Contributed by Jim Kingdon, 13-Jul-2019.) (New usage is discouraged.)
((𝐹 Fn V A 𝑉 B On) → (rec(𝐹, A)‘B) = (A x B (𝐹‘((rec(𝐹, A) ↾ B)‘x))))

13-Jul-2019rdgifnon 5887 The recursive definition generator is a function on ordinal numbers. The 𝐹 Fn V condition states that the characteristic function is defined for all sets (being defined for all ordinals might be enough, but being defined for all sets will generally hold for the characteristic functions we need to use this with). (Contributed by Jim Kingdon, 13-Jul-2019.)
((𝐹 Fn V A 𝑉) → rec(𝐹, A) Fn On)

12-Jul-2019dftru2 1236 An alternate definition of "true". (Contributed by Anthony Hart, 13-Oct-2010.) (Revised by BJ, 12-Jul-2019.) (New usage is discouraged.)
( ⊤ ↔ (φφ))

11-Jul-2019df-tru 1231 Definition of the truth value "true", or "verum", denoted by . This is a tautology, as proved by tru 1232. In this definition, an instance of id 19 is used as the definiens, although any tautology, such as an axiom, can be used in its place. This particular id 19 instance was chosen so this definition can be checked by the same algorithm that is used for predicate calculus. This definition should be referenced directly only by tru 1232, and other proofs should depend on tru 1232 (directly or indirectly) instead of this definition, since there are many alternative ways to define . (Contributed by Anthony Hart, 13-Oct-2010.) (Revised by NM, 11-Jul-2019.) (New usage is discouraged.)
( ⊤ ↔ (x x = xx x = x))

11-Jul-2019trujust 1230 Soundness justification theorem for df-tru 1231. (Contributed by Mario Carneiro, 17-Nov-2013.) (Revised by NM, 11-Jul-2019.)
((x x = xx x = x) ↔ (y y = yy y = y))

10-Jul-2019rdgi0g 5886 The initial value of the recursive definition generator. (Contributed by Jim Kingdon, 10-Jul-2019.)
((𝐹 Fn V A 𝑉) → (rec(𝐹, A)‘∅) = A)

9-Jul-2019oeiv 5951 Value of ordinal exponentiation. (Contributed by Jim Kingdon, 9-Jul-2019.)
((A On B On) → (A𝑜 B) = (rec((x V ↦ (x ·𝑜 A)), 1𝑜)‘B))

9-Jul-2019tfrlemi14d 5868 The domain of recs is all ordinals (lemma for transfinite recursion). (Contributed by Jim Kingdon, 9-Jul-2019.)
A = {fx On (f Fn x y x (fy) = (𝐹‘(fy)))}    &   (φx(Fun 𝐹 (𝐹x) V))       (φ → dom recs(𝐹) = On)

9-Jul-2019opeldmg 4467 Membership of first of an ordered pair in a domain. (Contributed by Jim Kingdon, 9-Jul-2019.)
((A 𝑉 B 𝑊) → (⟨A, B 𝐶A dom 𝐶))

4-Jul-2019df-oexpi 5922 Define the ordinal exponentiation operation.

This definition is similar to a conventional definition of exponentiation except that it defines ∅ ↑𝑜 A to be 1𝑜 for all A On, in order to avoid having different cases for whether the base is or not. (Contributed by Mario Carneiro, 4-Jul-2019.)

𝑜 = (x On, y On ↦ (rec((z V ↦ (z ·𝑜 x)), 1𝑜)‘y))

4-Jul-2019rdgexgg 5885 The recursive definition generator produces a set on a set input. (Contributed by Jim Kingdon, 4-Jul-2019.)
𝐹 Fn V       ((A 𝑉 B 𝑊) → (rec(𝐹, A)‘B) V)

4-Jul-2019rdgexggg 5884 The recursive definition generator produces a set on a set input. (Contributed by Jim Kingdon, 4-Jul-2019.)
((𝐹 Fn V A 𝑉 B 𝑊) → (rec(𝐹, A)‘B) V)

4-Jul-2019rdgruledefg 5883 The recursion rule for the recursive definition generator is defined everywhere. (Contributed by Jim Kingdon, 4-Jul-2019.)
𝐹 Fn V       (A 𝑉 → (Fun (g V ↦ (A x dom g(𝐹‘(gx)))) ((g V ↦ (A x dom g(𝐹‘(gx))))‘f) V))

4-Jul-2019rdgruledefgg 5882 The recursion rule for the recursive definition generator is defined everywhere. (Contributed by Jim Kingdon, 4-Jul-2019.)
((𝐹 Fn V A 𝑉) → (Fun (g V ↦ (A x dom g(𝐹‘(gx)))) ((g V ↦ (A x dom g(𝐹‘(gx))))‘f) V))

3-Jul-2019oeiexg 5948 Ordinal exponentiation is a set. (Contributed by Mario Carneiro, 3-Jul-2019.)
((A 𝑉 B 𝑊) → (A𝑜 B) V)

3-Jul-2019fnoei 5947 Functionality and domain of ordinal exponentiation. (Contributed by Mario Carneiro, 29-May-2015.) (Revised by Mario Carneiro, 3-Jul-2019.)
𝑜 Fn (On × On)

3-Jul-2019omexg 5946 Ordinal multiplication is a set. (Contributed by Mario Carneiro, 3-Jul-2019.)
((A 𝑉 B 𝑊) → (A ·𝑜 B) V)

3-Jul-2019fnom 5945 Functionality and domain of ordinal multiplication. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 3-Jul-2019.)
·𝑜 Fn (On × On)

3-Jul-2019oaexg 5943 Ordinal addition is a set. (Contributed by Mario Carneiro, 3-Jul-2019.)
((A 𝑉 B 𝑊) → (A +𝑜 B) V)

3-Jul-2019fnoa 5942 Functionality and domain of ordinal addition. (Contributed by NM, 26-Aug-1995.) (Proof shortened by Mario Carneiro, 3-Jul-2019.)
+𝑜 Fn (On × On)

3-Jul-2019rdgexg 5896 The recursive definition generator produces a set on a set input. (Contributed by Mario Carneiro, 3-Jul-2019.)
A V    &   𝐹 Fn V       (B 𝑉 → (rec(𝐹, A)‘B) V)

3-Jul-2019tfrex 5876 The transfinite recursion function is set-like if the input is. (Contributed by Mario Carneiro, 3-Jul-2019.)
𝐹 = recs(𝐺)    &   (φx(Fun 𝐺 (𝐺x) V))       ((φ A 𝑉) → (𝐹A) V)

3-Jul-2019tfrexlem 5870 The transfinite recursion function is set-like if the input is. (Contributed by Mario Carneiro, 3-Jul-2019.)
A = {fx On (f Fn x y x (fy) = (𝐹‘(fy)))}    &   (φx(Fun 𝐹 (𝐹x) V))       ((φ 𝐶 𝑉) → (recs(𝐹)‘𝐶) V)

3-Jul-2019mpt2fvexi 5755 Sufficient condition for an operation maps-to notation to be set-like. (Contributed by Mario Carneiro, 3-Jul-2019.)
𝐹 = (x A, y B𝐶)    &   𝐶 V    &   𝑅 V    &   𝑆 V       (𝑅𝐹𝑆) V

3-Jul-2019mpt2fvex 5752 Sufficient condition for an operation maps-to notation to be set-like. (Contributed by Mario Carneiro, 3-Jul-2019.)
𝐹 = (x A, y B𝐶)       ((xy 𝐶 𝑉 𝑅 𝑊 𝑆 𝑋) → (𝑅𝐹𝑆) V)

3-Jul-2019mptfvex 5181 Sufficient condition for a maps-to notation to be set-like. (Contributed by Mario Carneiro, 3-Jul-2019.)
𝐹 = (x AB)       ((x B 𝑉 𝐶 𝑊) → (𝐹𝐶) V)

3-Jul-2019fvmptss2 5172 A mapping always evaluates to a subset of the substituted expression in the mapping, even if this is a proper class, or we are out of the domain. (Contributed by Mario Carneiro, 13-Feb-2015.) (Revised by Mario Carneiro, 3-Jul-2019.)
(x = 𝐷B = 𝐶)    &   𝐹 = (x AB)       (𝐹𝐷) ⊆ 𝐶

2-Jul-2019tfrlemisucfn 5859 We can extend an acceptable function by one element to produce a function. Lemma for tfrlemi1 5867. (Contributed by Jim Kingdon, 2-Jul-2019.)
A = {fx On (f Fn x y x (fy) = (𝐹‘(fy)))}    &   (φx(Fun 𝐹 (𝐹x) V))    &   (φz On)    &   (φg Fn z)    &   (φg A)       (φ → (g ∪ {⟨z, (𝐹g)⟩}) Fn suc z)

2-Jul-2019tfrlem3-2d 5850 Lemma for transfinite recursion which changes a bound variable (Contributed by Jim Kingdon, 2-Jul-2019.)
(φx(Fun 𝐹 (𝐹x) V))       (φ → (Fun 𝐹 (𝐹g) V))

26-Jun-2019ordge1n0im 5934 An ordinal greater than or equal to 1 is nonzero. (Contributed by Jim Kingdon, 26-Jun-2019.)
(Ord A → (1𝑜AA ≠ ∅))

25-Jun-2019sucinc 5940 Successor is increasing. (Contributed by Jim Kingdon, 25-Jun-2019.)
𝐹 = (z V ↦ suc z)       x x ⊆ (𝐹x)

9-Jun-2019rdgisuc1 5891 One way of describing the value of the recursive definition generator at a successor. There is no condition on the characteristic function 𝐹 other than 𝐹 Fn V. Given that, the resulting expression encompasses both the expected successor term (𝐹‘(rec(𝐹, A)‘B)) but also terms that correspond to the initial value A and to limit ordinals x B(𝐹‘(rec(𝐹, A)‘x)).

If we add conditions on the characteristic function, we can show tighter results such as rdgisucinc 5892. (Contributed by Jim Kingdon, 9-Jun-2019.)

(φ𝐹 Fn V)    &   (φA 𝑉)    &   (φB On)       (φ → (rec(𝐹, A)‘suc B) = (A ∪ ( x B (𝐹‘(rec(𝐹, A)‘x)) ∪ (𝐹‘(rec(𝐹, A)‘B)))))

29-May-2019rdgruledef 5894 The recursion rule for the recursive definition generator is defined everywhere. Lemma for rdg0 5895. (Contributed by Jim Kingdon, 29-May-2019.)
A V    &   𝐹 Fn V       (Fun (g V ↦ (A x dom g(𝐹‘(gx))))