P. 431 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43001-43100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	congneg 43001	If two integers are congruent mod 𝐴, so are their negatives. (Contributed by Stefan O'Rear, 1-Oct-2014.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ (𝐵 − 𝐶))) → 𝐴 ∥ (-𝐵 − -𝐶))
Theorem	congsub 43002	If two pairs of numbers are componentwise congruent, so are their differences. (Contributed by Stefan O'Rear, 2-Oct-2014.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − 𝐶) ∧ 𝐴 ∥ (𝐷 − 𝐸))) → 𝐴 ∥ ((𝐵 − 𝐷) − (𝐶 − 𝐸)))
Theorem	congid 43003	Every integer is congruent to itself mod every base. (Contributed by Stefan O'Rear, 1-Oct-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∥ (𝐵 − 𝐵))
Theorem	mzpcong 43004*	Polynomials commute with congruences. (Does this characterize them?) (Contributed by Stefan O'Rear, 5-Oct-2014.)
⊢ ((𝐹 ∈ (mzPoly‘𝑉) ∧ (𝑋 ∈ (ℤ ↑m 𝑉) ∧ 𝑌 ∈ (ℤ ↑m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) → 𝑁 ∥ ((𝐹‘𝑋) − (𝐹‘𝑌)))
Theorem	congrep 43005*	Every integer is congruent to some number in the fundamental domain. (Contributed by Stefan O'Rear, 2-Oct-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℤ) → ∃𝑎 ∈ (0...(𝐴 − 1))𝐴 ∥ (𝑎 − 𝑁))
Theorem	congabseq 43006	If two integers are congruent, they are either equal or separated by at least the congruence base. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 − 𝐶)) → ((abs‘(𝐵 − 𝐶)) < 𝐴 ↔ 𝐵 = 𝐶))
21.33.30  Alternating congruential equations
Theorem	acongid 43007	A wff like that in this theorem will be known as an "alternating congruence". A special symbol might be considered if more uses come up. They have many of the same properties as normal congruences, starting with reflexivity. JonesMatijasevic uses "a ≡ ± b (mod c)" for this construction. The disjunction of divisibility constraints seems to adequately capture the concept, but it's rather verbose and somewhat inelegant. Use of an explicit equivalence relation might also work. (Contributed by Stefan O'Rear, 2-Oct-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∥ (𝐵 − 𝐵) ∨ 𝐴 ∥ (𝐵 − -𝐵)))
Theorem	acongsym 43008	Symmetry of alternating congruence. (Contributed by Stefan O'Rear, 2-Oct-2014.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − 𝐶) ∨ 𝐴 ∥ (𝐵 − -𝐶))) → (𝐴 ∥ (𝐶 − 𝐵) ∨ 𝐴 ∥ (𝐶 − -𝐵)))
Theorem	acongneg2 43009	Negate right side of alternating congruence. Makes essential use of the "alternating" part. (Contributed by Stefan O'Rear, 3-Oct-2014.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − -𝐶) ∨ 𝐴 ∥ (𝐵 − --𝐶))) → (𝐴 ∥ (𝐵 − 𝐶) ∨ 𝐴 ∥ (𝐵 − -𝐶)))
Theorem	acongtr 43010	Transitivity of alternating congruence. (Contributed by Stefan O'Rear, 2-Oct-2014.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ ((𝐴 ∥ (𝐵 − 𝐶) ∨ 𝐴 ∥ (𝐵 − -𝐶)) ∧ (𝐴 ∥ (𝐶 − 𝐷) ∨ 𝐴 ∥ (𝐶 − -𝐷)))) → (𝐴 ∥ (𝐵 − 𝐷) ∨ 𝐴 ∥ (𝐵 − -𝐷)))
Theorem	acongeq12d 43011	Substitution deduction for alternating congruence. (Contributed by Stefan O'Rear, 3-Oct-2014.)
⊢ (𝜑 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐷 = 𝐸)    ⇒   ⊢ (𝜑 → ((𝐴 ∥ (𝐵 − 𝐷) ∨ 𝐴 ∥ (𝐵 − -𝐷)) ↔ (𝐴 ∥ (𝐶 − 𝐸) ∨ 𝐴 ∥ (𝐶 − -𝐸))))
Theorem	acongrep 43012*	Every integer is alternating-congruent to some number in the first half of the fundamental domain. (Contributed by Stefan O'Rear, 2-Oct-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℤ) → ∃𝑎 ∈ (0...𝐴)((2 · 𝐴) ∥ (𝑎 − 𝑁) ∨ (2 · 𝐴) ∥ (𝑎 − -𝑁)))
Theorem	fzmaxdif 43013	Bound on the difference between two integers constrained to two possibly overlapping finite ranges. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ (((𝐶 ∈ ℤ ∧ 𝐴 ∈ (𝐵...𝐶)) ∧ (𝐹 ∈ ℤ ∧ 𝐷 ∈ (𝐸...𝐹)) ∧ (𝐶 − 𝐸) ≤ (𝐹 − 𝐵)) → (abs‘(𝐴 − 𝐷)) ≤ (𝐹 − 𝐵))
Theorem	fzneg 43014	Reflection of a finite range of integers about 0. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 ∈ (𝐵...𝐶) ↔ -𝐴 ∈ (-𝐶...-𝐵)))
Theorem	acongeq 43015	Two numbers in the fundamental domain are alternating-congruent iff they are equal. TODO: could be used to shorten jm2.26 43034. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (𝐵 = 𝐶 ↔ ((2 · 𝐴) ∥ (𝐵 − 𝐶) ∨ (2 · 𝐴) ∥ (𝐵 − -𝐶))))
Theorem	dvdsacongtr 43016	Alternating congruence passes from a base to a dividing base. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝐷 ∥ 𝐴 ∧ (𝐴 ∥ (𝐵 − 𝐶) ∨ 𝐴 ∥ (𝐵 − -𝐶)))) → (𝐷 ∥ (𝐵 − 𝐶) ∨ 𝐷 ∥ (𝐵 − -𝐶)))
21.33.31  Additional theorems on integer divisibility
Theorem	coprmdvdsb 43017	Multiplication by a coprime number does not affect divisibility. (Contributed by Stefan O'Rear, 23-Sep-2014.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ (𝐾 gcd 𝑀) = 1)) → (𝐾 ∥ 𝑁 ↔ 𝐾 ∥ (𝑀 · 𝑁)))
Theorem	modabsdifz 43018	Divisibility in terms of modular reduction by the absolute value of the base. (Contributed by Stefan O'Rear, 26-Sep-2014.)
⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑀 ≠ 0) → ((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) ∈ ℤ)
Theorem	dvdsabsmod0 43019	Divisibility in terms of modular reduction by the absolute value of the base. (Contributed by Stefan O'Rear, 24-Sep-2014.) (Proof shortened by OpenAI, 3-Jul-2020.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≠ 0) → (𝑀 ∥ 𝑁 ↔ (𝑁 mod (abs‘𝑀)) = 0))
21.33.32  X and Y sequences 3: Divisibility properties
Theorem	jm2.18 43020	Theorem 2.18 of [JonesMatijasevic] p. 696. Direct relationship of the exponential function to X and Y sequences. (Contributed by Stefan O'Rear, 14-Oct-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑁) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑁))) − (𝐾↑𝑁)))
Theorem	jm2.19lem1 43021	Lemma for jm2.19 43025. X and Y values are coprime. (Contributed by Stefan O'Rear, 23-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ) → ((𝐴 Xrm 𝑀) gcd (𝐴 Yrm 𝑀)) = 1)
Theorem	jm2.19lem2 43022	Lemma for jm2.19 43025. (Contributed by Stefan O'Rear, 23-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + 𝑀))))
Theorem	jm2.19lem3 43023	Lemma for jm2.19 43025. (Contributed by Stefan O'Rear, 26-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐼 ∈ ℕ0) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + (𝐼 · 𝑀)))))
Theorem	jm2.19lem4 43024	Lemma for jm2.19 43025. Extend to ZZ by symmetry. TODO: use zindbi 42978. (Contributed by Stefan O'Rear, 26-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐼 ∈ ℤ) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + (𝐼 · 𝑀)))))
Theorem	jm2.19 43025	Lemma 2.19 of [JonesMatijasevic] p. 696. Transfer divisibility constraints between Y-values and their indices. (Contributed by Stefan O'Rear, 24-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁)))
Theorem	jm2.21 43026	Lemma for jm2.20nn 43029. Express X and Y values as a binomial. (Contributed by Stefan O'Rear, 26-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ) → ((𝐴 Xrm (𝑁 · 𝐽)) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm (𝑁 · 𝐽)))) = (((𝐴 Xrm 𝑁) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁)))↑𝐽))
Theorem	jm2.22 43027*	Lemma for jm2.20nn 43029. Applying binomial theorem and taking irrational part. (Contributed by Stefan O'Rear, 26-Sep-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ0) → (𝐴 Yrm (𝑁 · 𝐽)) = Σ𝑖 ∈ {𝑥 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑥} ((𝐽C𝑖) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑖)) · (((𝐴 Yrm 𝑁)↑𝑖) · (((𝐴↑2) − 1)↑((𝑖 − 1) / 2))))))
Theorem	jm2.23 43028	Lemma for jm2.20nn 43029. Truncate binomial expansion p-adicly. (Contributed by Stefan O'Rear, 26-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑3) ∥ ((𝐴 Yrm (𝑁 · 𝐽)) − (𝐽 · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (𝐴 Yrm 𝑁)))))
Theorem	jm2.20nn 43029	Lemma 2.20 of [JonesMatijasevic] p. 696, the "first step down lemma". (Contributed by Stefan O'Rear, 27-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀) ↔ (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀))
Theorem	jm2.25lem1 43030	Lemma for jm2.26 43034. (Contributed by Stefan O'Rear, 2-Oct-2014.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝐴 ∥ (𝐶 − 𝐷) ∨ 𝐴 ∥ (𝐶 − -𝐷))) → ((𝐴 ∥ (𝐷 − 𝐵) ∨ 𝐴 ∥ (𝐷 − -𝐵)) ↔ (𝐴 ∥ (𝐶 − 𝐵) ∨ 𝐴 ∥ (𝐶 − -𝐵))))
Theorem	jm2.25 43031	Lemma for jm2.26 43034. Remainders mod X(2n) are negaperiodic mod 2n. (Contributed by Stefan O'Rear, 2-Oct-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐼 ∈ ℤ) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀))))
Theorem	jm2.26a 43032	Lemma for jm2.26 43034. Reverse direction is required to prove forward direction, so do it separately. Induction on difference between K and M, together with the addition formula fact that adding 2N only inverts sign. (Contributed by Stefan O'Rear, 2-Oct-2014.)
⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (((2 · 𝑁) ∥ (𝐾 − 𝑀) ∨ (2 · 𝑁) ∥ (𝐾 − -𝑀)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))))
Theorem	jm2.26lem3 43033	Lemma for jm2.26 43034. Use acongrep 43012 to find K', M' ~ K, M in [ 0,N ]. Thus Y(K') ~ Y(M') and both are small; K' = M' on pain of contradicting 2.24, so K ~ M. (Contributed by Stefan O'Rear, 3-Oct-2014.)
⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝑀 ∈ (0...𝑁)) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → 𝐾 = 𝑀)
Theorem	jm2.26 43034	Lemma 2.26 of [JonesMatijasevic] p. 697, the "second step down lemma". (Contributed by Stefan O'Rear, 2-Oct-2014.)
⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀))) ↔ ((2 · 𝑁) ∥ (𝐾 − 𝑀) ∨ (2 · 𝑁) ∥ (𝐾 − -𝑀))))
Theorem	jm2.15nn0 43035	Lemma 2.15 of [JonesMatijasevic] p. 695. Yrm is a polynomial for fixed N, so has the expected congruence property. (Contributed by Stefan O'Rear, 1-Oct-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑁) − (𝐵 Yrm 𝑁)))
Theorem	jm2.16nn0 43036	Lemma 2.16 of [JonesMatijasevic] p. 695. This may be regarded as a special case of jm2.15nn0 43035 if Yrm is redefined as described in rmyluc 42969. (Contributed by Stefan O'Rear, 1-Oct-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → (𝐴 − 1) ∥ ((𝐴 Yrm 𝑁) − 𝑁))
21.33.33  X and Y sequences 4: Diophantine representability of Y
Theorem	jm2.27a 43037	Lemma for jm2.27 43040. Reverse direction after existential quantifiers are expanded. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ (𝜑 → 𝐴 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐸 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐹 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐺 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐻 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐽 ∈ ℕ0)    &   ⊢ (𝜑 → ((𝐷↑2) − (((𝐴↑2) − 1) · (𝐶↑2))) = 1)    &   ⊢ (𝜑 → ((𝐹↑2) − (((𝐴↑2) − 1) · (𝐸↑2))) = 1)    &   ⊢ (𝜑 → 𝐺 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → ((𝐼↑2) − (((𝐺↑2) − 1) · (𝐻↑2))) = 1)    &   ⊢ (𝜑 → 𝐸 = ((𝐽 + 1) · (2 · (𝐶↑2))))    &   ⊢ (𝜑 → 𝐹 ∥ (𝐺 − 𝐴))    &   ⊢ (𝜑 → (2 · 𝐶) ∥ (𝐺 − 1))    &   ⊢ (𝜑 → 𝐹 ∥ (𝐻 − 𝐶))    &   ⊢ (𝜑 → (2 · 𝐶) ∥ (𝐻 − 𝐵))    &   ⊢ (𝜑 → 𝐵 ≤ 𝐶)    &   ⊢ (𝜑 → 𝑃 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 = (𝐴 Xrm 𝑃))    &   ⊢ (𝜑 → 𝐶 = (𝐴 Yrm 𝑃))    &   ⊢ (𝜑 → 𝑄 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 = (𝐴 Xrm 𝑄))    &   ⊢ (𝜑 → 𝐸 = (𝐴 Yrm 𝑄))    &   ⊢ (𝜑 → 𝑅 ∈ ℤ)    &   ⊢ (𝜑 → 𝐼 = (𝐺 Xrm 𝑅))    &   ⊢ (𝜑 → 𝐻 = (𝐺 Yrm 𝑅))    ⇒   ⊢ (𝜑 → 𝐶 = (𝐴 Yrm 𝐵))
Theorem	jm2.27b 43038	Lemma for jm2.27 43040. Expand existential quantifiers for reverse direction. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ (𝜑 → 𝐴 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐸 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐹 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐺 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐻 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐼 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐽 ∈ ℕ0)    &   ⊢ (𝜑 → ((𝐷↑2) − (((𝐴↑2) − 1) · (𝐶↑2))) = 1)    &   ⊢ (𝜑 → ((𝐹↑2) − (((𝐴↑2) − 1) · (𝐸↑2))) = 1)    &   ⊢ (𝜑 → 𝐺 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → ((𝐼↑2) − (((𝐺↑2) − 1) · (𝐻↑2))) = 1)    &   ⊢ (𝜑 → 𝐸 = ((𝐽 + 1) · (2 · (𝐶↑2))))    &   ⊢ (𝜑 → 𝐹 ∥ (𝐺 − 𝐴))    &   ⊢ (𝜑 → (2 · 𝐶) ∥ (𝐺 − 1))    &   ⊢ (𝜑 → 𝐹 ∥ (𝐻 − 𝐶))    &   ⊢ (𝜑 → (2 · 𝐶) ∥ (𝐻 − 𝐵))    &   ⊢ (𝜑 → 𝐵 ≤ 𝐶)    ⇒   ⊢ (𝜑 → 𝐶 = (𝐴 Yrm 𝐵))
Theorem	jm2.27c 43039	Lemma for jm2.27 43040. Forward direction with substitutions. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ (𝜑 → 𝐴 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 = (𝐴 Yrm 𝐵))    &   ⊢ 𝐷 = (𝐴 Xrm 𝐵)    &   ⊢ 𝑄 = (𝐵 · (𝐴 Yrm 𝐵))    &   ⊢ 𝐸 = (𝐴 Yrm (2 · 𝑄))    &   ⊢ 𝐹 = (𝐴 Xrm (2 · 𝑄))    &   ⊢ 𝐺 = (𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴)))    &   ⊢ 𝐻 = (𝐺 Yrm 𝐵)    &   ⊢ 𝐼 = (𝐺 Xrm 𝐵)    &   ⊢ 𝐽 = ((𝐸 / (2 · (𝐶↑2))) − 1)    ⇒   ⊢ (𝜑 → (((𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ∧ 𝐹 ∈ ℕ0) ∧ (𝐺 ∈ ℕ0 ∧ 𝐻 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0)) ∧ (𝐽 ∈ ℕ0 ∧ (((((𝐷↑2) − (((𝐴↑2) − 1) · (𝐶↑2))) = 1 ∧ ((𝐹↑2) − (((𝐴↑2) − 1) · (𝐸↑2))) = 1 ∧ 𝐺 ∈ (ℤ≥‘2)) ∧ (((𝐼↑2) − (((𝐺↑2) − 1) · (𝐻↑2))) = 1 ∧ 𝐸 = ((𝐽 + 1) · (2 · (𝐶↑2))) ∧ 𝐹 ∥ (𝐺 − 𝐴))) ∧ (((2 · 𝐶) ∥ (𝐺 − 1) ∧ 𝐹 ∥ (𝐻 − 𝐶)) ∧ ((2 · 𝐶) ∥ (𝐻 − 𝐵) ∧ 𝐵 ≤ 𝐶))))))
Theorem	jm2.27 43040*	Lemma 2.27 of [JonesMatijasevic] p. 697; rmY is a diophantine relation. 0 was excluded from the range of B and the lower limit of G was imposed because the source proof does not seem to work otherwise; quite possible I'm just missing something. The source proof uses both i and I; i has been changed to j to avoid collision. This theorem is basically nothing but substitution instances, all the work is done in jm2.27a 43037 and jm2.27c 43039. Once Diophantine relations have been defined, the content of the theorem is "rmY is Diophantine". (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 = (𝐴 Yrm 𝐵) ↔ ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0 ∃𝑖 ∈ ℕ0 ∃𝑗 ∈ ℕ0 (((((𝑑↑2) − (((𝐴↑2) − 1) · (𝐶↑2))) = 1 ∧ ((𝑓↑2) − (((𝐴↑2) − 1) · (𝑒↑2))) = 1 ∧ 𝑔 ∈ (ℤ≥‘2)) ∧ (((𝑖↑2) − (((𝑔↑2) − 1) · (ℎ↑2))) = 1 ∧ 𝑒 = ((𝑗 + 1) · (2 · (𝐶↑2))) ∧ 𝑓 ∥ (𝑔 − 𝐴))) ∧ (((2 · 𝐶) ∥ (𝑔 − 1) ∧ 𝑓 ∥ (ℎ − 𝐶)) ∧ ((2 · 𝐶) ∥ (ℎ − 𝐵) ∧ 𝐵 ≤ 𝐶)))))
Theorem	jm2.27dlem1 43041*	Lemma for rmydioph 43046. Substitution of a tuple restriction into a projection that doesn't care. (Contributed by Stefan O'Rear, 11-Oct-2014.)
⊢ 𝐴 ∈ (1...𝐵)    ⇒   ⊢ (𝑎 = (𝑏 ↾ (1...𝐵)) → (𝑎‘𝐴) = (𝑏‘𝐴))
Theorem	jm2.27dlem2 43042	Lemma for rmydioph 43046. This theorem is used along with the next three to efficiently infer steps like 7 ∈ (1...;10). (Contributed by Stefan O'Rear, 11-Oct-2014.)
⊢ 𝐴 ∈ (1...𝐵)    &   ⊢ 𝐶 = (𝐵 + 1)    &   ⊢ 𝐵 ∈ ℕ    ⇒   ⊢ 𝐴 ∈ (1...𝐶)
Theorem	jm2.27dlem3 43043	Lemma for rmydioph 43046. Infer membership of the endpoint of a range. (Contributed by Stefan O'Rear, 11-Oct-2014.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ 𝐴 ∈ (1...𝐴)
Theorem	jm2.27dlem4 43044	Lemma for rmydioph 43046. Infer ℕ-hood of large numbers. (Contributed by Stefan O'Rear, 11-Oct-2014.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 = (𝐴 + 1)    ⇒   ⊢ 𝐵 ∈ ℕ
Theorem	jm2.27dlem5 43045	Lemma for rmydioph 43046. Used with sselii 3931 to infer membership of midpoints of range; jm2.27dlem2 43042 is deprecated. (Contributed by Stefan O'Rear, 11-Oct-2014.)
⊢ 𝐵 = (𝐴 + 1)    &   ⊢ (1...𝐵) ⊆ (1...𝐶)    ⇒   ⊢ (1...𝐴) ⊆ (1...𝐶)
Theorem	rmydioph 43046	jm2.27 43040 restated in terms of Diophantine sets. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ ((𝑎‘1) ∈ (ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))} ∈ (Dioph‘3)
21.33.34  X and Y sequences 5: Diophantine representability of X, ^, _C
Theorem	rmxdiophlem 43047*	X can be expressed in terms of Y, so it is also Diophantine. (Contributed by Stefan O'Rear, 15-Oct-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℕ0) → (𝑋 = (𝐴 Xrm 𝑁) ↔ ∃𝑦 ∈ ℕ0 (𝑦 = (𝐴 Yrm 𝑁) ∧ ((𝑋↑2) − (((𝐴↑2) − 1) · (𝑦↑2))) = 1)))
Theorem	rmxdioph 43048	X is a Diophantine function. (Contributed by Stefan O'Rear, 17-Oct-2014.)
⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ ((𝑎‘1) ∈ (ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2)))} ∈ (Dioph‘3)
Theorem	jm3.1lem1 43049	Lemma for jm3.1 43052. (Contributed by Stefan O'Rear, 16-Oct-2014.)
⊢ (𝜑 → 𝐴 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴)    ⇒   ⊢ (𝜑 → (𝐾↑𝑁) < 𝐴)
Theorem	jm3.1lem2 43050	Lemma for jm3.1 43052. (Contributed by Stefan O'Rear, 16-Oct-2014.)
⊢ (𝜑 → 𝐴 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴)    ⇒   ⊢ (𝜑 → (𝐾↑𝑁) < ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1))
Theorem	jm3.1lem3 43051	Lemma for jm3.1 43052. (Contributed by Stefan O'Rear, 17-Oct-2014.)
⊢ (𝜑 → 𝐴 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴)    ⇒   ⊢ (𝜑 → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∈ ℕ)
Theorem	jm3.1 43052	Diophantine expression for exponentiation. Lemma 3.1 of [JonesMatijasevic] p. 698. (Contributed by Stefan O'Rear, 16-Oct-2014.)
⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴) → (𝐾↑𝑁) = (((𝐴 Xrm 𝑁) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑁))) mod ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1)))
Theorem	expdiophlem1 43053*	Lemma for expdioph 43055. Fully expanded expression for exponential. (Contributed by Stefan O'Rear, 17-Oct-2014.)
⊢ (𝐶 ∈ ℕ0 → (((𝐴 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ ℕ) ∧ 𝐶 = (𝐴↑𝐵)) ↔ ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ ℕ) ∧ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑑 = (𝐴 Yrm (𝐵 + 1))) ∧ ((𝑑 ∈ (ℤ≥‘2) ∧ 𝑒 = (𝑑 Yrm 𝐵)) ∧ ((𝑑 ∈ (ℤ≥‘2) ∧ 𝑓 = (𝑑 Xrm 𝐵)) ∧ (𝐶 < ((((2 · 𝑑) · 𝐴) − (𝐴↑2)) − 1) ∧ ((((2 · 𝑑) · 𝐴) − (𝐴↑2)) − 1) ∥ ((𝑓 − ((𝑑 − 𝐴) · 𝑒)) − 𝐶))))))))
Theorem	expdiophlem2 43054	Lemma for expdioph 43055. Exponentiation on a restricted domain is Diophantine. (Contributed by Stefan O'Rear, 17-Oct-2014.)
⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (((𝑎‘1) ∈ (ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))} ∈ (Dioph‘3)
Theorem	expdioph 43055	The exponential function is Diophantine. This result completes and encapsulates our development using Pell equation solution sequences and is sometimes regarded as Matiyasevich's theorem properly. (Contributed by Stefan O'Rear, 17-Oct-2014.)
⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))} ∈ (Dioph‘3)
21.33.35  Uncategorized stuff not associated with a major project
Theorem	setindtr 43056*	Set induction for sets contained in a transitive set. If we are allowed to assume Infinity, then all sets have a transitive closure and this reduces to setind 9624; however, this version is useful without Infinity. (Contributed by Stefan O'Rear, 28-Oct-2014.)
⊢ (∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴) → (∃𝑦(Tr 𝑦 ∧ 𝐵 ∈ 𝑦) → 𝐵 ∈ 𝐴))
Theorem	setindtrs 43057*	Set induction scheme without Infinity. See comments at setindtr 43056. (Contributed by Stefan O'Rear, 28-Oct-2014.)
⊢ (∀𝑦 ∈ 𝑥 𝜓 → 𝜑)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    ⇒   ⊢ (∃𝑧(Tr 𝑧 ∧ 𝐵 ∈ 𝑧) → 𝜒)
Theorem	dford3lem1 43058*	Lemma for dford3 43060. (Contributed by Stefan O'Rear, 28-Oct-2014.)
⊢ ((Tr 𝑁 ∧ ∀𝑦 ∈ 𝑁 Tr 𝑦) → ∀𝑏 ∈ 𝑁 (Tr 𝑏 ∧ ∀𝑦 ∈ 𝑏 Tr 𝑦))
Theorem	dford3lem2 43059*	Lemma for dford3 43060. (Contributed by Stefan O'Rear, 28-Oct-2014.)
⊢ ((Tr 𝑥 ∧ ∀𝑦 ∈ 𝑥 Tr 𝑦) → 𝑥 ∈ On)
Theorem	dford3 43060*	Ordinals are precisely the hereditarily transitive classes. Definition 1.2 of [Schloeder] p. 1. (Contributed by Stefan O'Rear, 28-Oct-2014.)
⊢ (Ord 𝑁 ↔ (Tr 𝑁 ∧ ∀𝑥 ∈ 𝑁 Tr 𝑥))
Theorem	dford4 43061*	dford3 43060 expressed in primitives to demonstrate shortness. (Contributed by Stefan O'Rear, 28-Oct-2014.)
⊢ (Ord 𝑁 ↔ ∀𝑎∀𝑏∀𝑐((𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑎) → (𝑏 ∈ 𝑁 ∧ (𝑐 ∈ 𝑏 → 𝑐 ∈ 𝑎))))
Theorem	wopprc 43062	Unrelated: Wiener pairs treat proper classes symmetrically. (Contributed by Stefan O'Rear, 19-Sep-2014.)
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ ¬ 1o ∈ {{{𝐴}, ∅}, {{𝐵}}})
Theorem	rpnnen3lem 43063*	Lemma for rpnnen3 43064. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ 𝑎 < 𝑏) → {𝑐 ∈ ℚ ∣ 𝑐 < 𝑎} ≠ {𝑐 ∈ ℚ ∣ 𝑐 < 𝑏})
Theorem	rpnnen3 43064	Dedekind cut injection of ℝ into 𝒫 ℚ. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ ℝ ≼ 𝒫 ℚ
21.33.36  More equivalents of the Axiom of Choice
Theorem	axac10 43065	Characterization of choice similar to dffin1-5 10276. (Contributed by Stefan O'Rear, 6-Jan-2015.)
⊢ ( ≈ “ On) = V
Theorem	harinf 43066	The Hartogs number of an infinite set is at least ω. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.)
⊢ ((𝑆 ∈ 𝑉 ∧ ¬ 𝑆 ∈ Fin) → ω ⊆ (har‘𝑆))
Theorem	wdom2d2 43067*	Deduction for weak dominance by a Cartesian product. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝑥 = 𝑋)    ⇒   ⊢ (𝜑 → 𝐴 ≼* (𝐵 × 𝐶))
Theorem	ttac 43068	Tarski's theorem about choice: infxpidm 10450 is equivalent to ax-ac 10347. (Contributed by Stefan O'Rear, 4-Nov-2014.) (Proof shortened by Stefan O'Rear, 10-Jul-2015.)
⊢ (CHOICE ↔ ∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐))
Theorem	pw2f1ocnv 43069*	Define a bijection between characteristic functions and subsets. EDITORIAL: extracted from pw2en 8997, which can be easily reproved in terms of this. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Stefan O'Rear, 9-Jul-2015.)
⊢ 𝐹 = (𝑥 ∈ (2o ↑m 𝐴) ↦ (◡𝑥 “ {1o}))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐹:(2o ↑m 𝐴)–1-1-onto→𝒫 𝐴 ∧ ◡𝐹 = (𝑦 ∈ 𝒫 𝐴 ↦ (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)))))
Theorem	pw2f1o2 43070*	Define a bijection between characteristic functions and subsets. EDITORIAL: extracted from pw2en 8997, which can be easily reproved in terms of this. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ (2o ↑m 𝐴) ↦ (◡𝑥 “ {1o}))    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐹:(2o ↑m 𝐴)–1-1-onto→𝒫 𝐴)
Theorem	pw2f1o2val 43071*	Function value of the pw2f1o2 43070 bijection. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Stefan O'Rear, 6-May-2015.)
⊢ 𝐹 = (𝑥 ∈ (2o ↑m 𝐴) ↦ (◡𝑥 “ {1o}))    ⇒   ⊢ (𝑋 ∈ (2o ↑m 𝐴) → (𝐹‘𝑋) = (◡𝑋 “ {1o}))
Theorem	pw2f1o2val2 43072*	Membership in a mapped set under the pw2f1o2 43070 bijection. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Stefan O'Rear, 6-May-2015.)
⊢ 𝐹 = (𝑥 ∈ (2o ↑m 𝐴) ↦ (◡𝑥 “ {1o}))    ⇒   ⊢ ((𝑋 ∈ (2o ↑m 𝐴) ∧ 𝑌 ∈ 𝐴) → (𝑌 ∈ (𝐹‘𝑋) ↔ (𝑋‘𝑌) = 1o))
Theorem	limsuc2 43073	Limit ordinals in the sense inclusive of zero contain all successors of their members. (Contributed by Stefan O'Rear, 20-Jan-2015.)
⊢ ((Ord 𝐴 ∧ 𝐴 = ∪ 𝐴) → (𝐵 ∈ 𝐴 ↔ suc 𝐵 ∈ 𝐴))
Theorem	wepwsolem 43074*	Transfer an ordering on characteristic functions by isomorphism to the power set. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑧 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑥) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦)))}    &   ⊢ 𝑈 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧) E (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ 𝐹 = (𝑎 ∈ (2o ↑m 𝐴) ↦ (◡𝑎 “ {1o}))    ⇒   ⊢ (𝐴 ∈ V → 𝐹 Isom 𝑈, 𝑇 ((2o ↑m 𝐴), 𝒫 𝐴))
Theorem	wepwso 43075*	A well-ordering induces a strict ordering on the power set. EDITORIAL: when well-orderings are set like, this can be strengthened to remove 𝐴 ∈ 𝑉. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑧 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑥) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦)))}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 We 𝐴) → 𝑇 Or 𝒫 𝐴)
Theorem	dnnumch1 43076*	Define an enumeration of a set from a choice function; second part, it restricts to a bijection. EDITORIAL: overlaps dfac8a 9918. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ 𝐹 = recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧))))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝐺‘𝑦) ∈ 𝑦))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ On (𝐹 ↾ 𝑥):𝑥–1-1-onto→𝐴)
Theorem	dnnumch2 43077*	Define an enumeration (weak dominance version) of a set from a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ 𝐹 = recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧))))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝐺‘𝑦) ∈ 𝑦))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ ran 𝐹)
Theorem	dnnumch3lem 43078*	Value of the ordinal injection function. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ 𝐹 = recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧))))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝐺‘𝑦) ∈ 𝑦))    ⇒   ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) = ∩ (◡𝐹 “ {𝑤}))
Theorem	dnnumch3 43079*	Define an injection from a set into the ordinals using a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ 𝐹 = recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧))))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝐺‘𝑦) ∈ 𝑦))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴–1-1→On)
Theorem	dnwech 43080*	Define a well-ordering from a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ 𝐹 = recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧))))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝐺‘𝑦) ∈ 𝑦))    &   ⊢ 𝐻 = {⟨𝑣, 𝑤⟩ ∣ ∩ (◡𝐹 “ {𝑣}) ∈ ∩ (◡𝐹 “ {𝑤})}    ⇒   ⊢ (𝜑 → 𝐻 We 𝐴)
Theorem	fnwe2val 43081*	Lemma for fnwe2 43085. Substitute variables. (Contributed by Stefan O'Rear, 19-Jan-2015.)
⊢ (𝑧 = (𝐹‘𝑥) → 𝑆 = 𝑈)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑈𝑦))}    ⇒   ⊢ (𝑎𝑇𝑏 ↔ ((𝐹‘𝑎)𝑅(𝐹‘𝑏) ∨ ((𝐹‘𝑎) = (𝐹‘𝑏) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏)))
Theorem	fnwe2lem1 43082*	Lemma for fnwe2 43085. Substitution in well-ordering hypothesis. (Contributed by Stefan O'Rear, 19-Jan-2015.)
⊢ (𝑧 = (𝐹‘𝑥) → 𝑆 = 𝑈)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑈𝑦))}    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑈 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑥)})    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)})
Theorem	fnwe2lem2 43083*	Lemma for fnwe2 43085. An element which is in a minimal fiber and minimal within its fiber is minimal globally; thus 𝑇 is well-founded. (Contributed by Stefan O'Rear, 19-Jan-2015.)
⊢ (𝑧 = (𝐹‘𝑥) → 𝑆 = 𝑈)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑈𝑦))}    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑈 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑥)})    &   ⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝑅 We 𝐵)    &   ⊢ (𝜑 → 𝑎 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝑎 ≠ ∅)    ⇒   ⊢ (𝜑 → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏)
Theorem	fnwe2lem3 43084*	Lemma for fnwe2 43085. Trichotomy. (Contributed by Stefan O'Rear, 19-Jan-2015.)
⊢ (𝑧 = (𝐹‘𝑥) → 𝑆 = 𝑈)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑈𝑦))}    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑈 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑥)})    &   ⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝑅 We 𝐵)    &   ⊢ (𝜑 → 𝑎 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑏 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎))
Theorem	fnwe2 43085*	A well-ordering can be constructed on a partitioned set by patching together well-orderings on each partition using a well-ordering on the partitions themselves. Similar to fnwe 8062 but does not require the within-partition ordering to be globally well. (Contributed by Stefan O'Rear, 19-Jan-2015.)
⊢ (𝑧 = (𝐹‘𝑥) → 𝑆 = 𝑈)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑈𝑦))}    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑈 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑥)})    &   ⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝑅 We 𝐵)    ⇒   ⊢ (𝜑 → 𝑇 We 𝐴)
Theorem	aomclem1 43086*	Lemma for dfac11 43094. This is the beginning of the proof that multiple choice is equivalent to choice. Our goal is to construct, by transfinite recursion, a well-ordering of (𝑅1‘𝐴). In what follows, 𝐴 is the index of the rank we wish to well-order, 𝑧 is the collection of well-orderings constructed so far, dom 𝑧 is the set of ordinal indices of constructed ranks i.e. the next rank to construct, and 𝑦 is a postulated multiple-choice function. Successor case 1, define a simple ordering from the well-ordered predecessor. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ 𝐵 = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ (𝑅1‘∪ dom 𝑧)((𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎) ∧ ∀𝑑 ∈ (𝑅1‘∪ dom 𝑧)(𝑑(𝑧‘∪ dom 𝑧)𝑐 → (𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏)))}    &   ⊢ (𝜑 → dom 𝑧 ∈ On)    &   ⊢ (𝜑 → dom 𝑧 = suc ∪ dom 𝑧)    &   ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑧(𝑧‘𝑎) We (𝑅1‘𝑎))    ⇒   ⊢ (𝜑 → 𝐵 Or (𝑅1‘dom 𝑧))
Theorem	aomclem2 43087*	Lemma for dfac11 43094. Successor case 2, a choice function for subsets of (𝑅1‘dom 𝑧). (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ 𝐵 = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ (𝑅1‘∪ dom 𝑧)((𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎) ∧ ∀𝑑 ∈ (𝑅1‘∪ dom 𝑧)(𝑑(𝑧‘∪ dom 𝑧)𝑐 → (𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏)))}    &   ⊢ 𝐶 = (𝑎 ∈ V ↦ sup((𝑦‘𝑎), (𝑅1‘dom 𝑧), 𝐵))    &   ⊢ (𝜑 → dom 𝑧 ∈ On)    &   ⊢ (𝜑 → dom 𝑧 = suc ∪ dom 𝑧)    &   ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑧(𝑧‘𝑎) We (𝑅1‘𝑎))    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → dom 𝑧 ⊆ 𝐴)    &   ⊢ (𝜑 → ∀𝑎 ∈ 𝒫 (𝑅1‘𝐴)(𝑎 ≠ ∅ → (𝑦‘𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅})))    ⇒   ⊢ (𝜑 → ∀𝑎 ∈ 𝒫 (𝑅1‘dom 𝑧)(𝑎 ≠ ∅ → (𝐶‘𝑎) ∈ 𝑎))
Theorem	aomclem3 43088*	Lemma for dfac11 43094. Successor case 3, our required well-ordering. (Contributed by Stefan O'Rear, 19-Jan-2015.)
⊢ 𝐵 = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ (𝑅1‘∪ dom 𝑧)((𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎) ∧ ∀𝑑 ∈ (𝑅1‘∪ dom 𝑧)(𝑑(𝑧‘∪ dom 𝑧)𝑐 → (𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏)))}    &   ⊢ 𝐶 = (𝑎 ∈ V ↦ sup((𝑦‘𝑎), (𝑅1‘dom 𝑧), 𝐵))    &   ⊢ 𝐷 = recs((𝑎 ∈ V ↦ (𝐶‘((𝑅1‘dom 𝑧) ∖ ran 𝑎))))    &   ⊢ 𝐸 = {⟨𝑎, 𝑏⟩ ∣ ∩ (◡𝐷 “ {𝑎}) ∈ ∩ (◡𝐷 “ {𝑏})}    &   ⊢ (𝜑 → dom 𝑧 ∈ On)    &   ⊢ (𝜑 → dom 𝑧 = suc ∪ dom 𝑧)    &   ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑧(𝑧‘𝑎) We (𝑅1‘𝑎))    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → dom 𝑧 ⊆ 𝐴)    &   ⊢ (𝜑 → ∀𝑎 ∈ 𝒫 (𝑅1‘𝐴)(𝑎 ≠ ∅ → (𝑦‘𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅})))    ⇒   ⊢ (𝜑 → 𝐸 We (𝑅1‘dom 𝑧))
Theorem	aomclem4 43089*	Lemma for dfac11 43094. Limit case. Patch together well-orderings constructed so far using fnwe2 43085 to cover the limit rank. (Contributed by Stefan O'Rear, 20-Jan-2015.)
⊢ 𝐹 = {⟨𝑎, 𝑏⟩ ∣ ((rank‘𝑎) E (rank‘𝑏) ∨ ((rank‘𝑎) = (rank‘𝑏) ∧ 𝑎(𝑧‘suc (rank‘𝑎))𝑏))}    &   ⊢ (𝜑 → dom 𝑧 ∈ On)    &   ⊢ (𝜑 → dom 𝑧 = ∪ dom 𝑧)    &   ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑧(𝑧‘𝑎) We (𝑅1‘𝑎))    ⇒   ⊢ (𝜑 → 𝐹 We (𝑅1‘dom 𝑧))
Theorem	aomclem5 43090*	Lemma for dfac11 43094. Combine the successor case with the limit case. (Contributed by Stefan O'Rear, 20-Jan-2015.)
⊢ 𝐵 = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ (𝑅1‘∪ dom 𝑧)((𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎) ∧ ∀𝑑 ∈ (𝑅1‘∪ dom 𝑧)(𝑑(𝑧‘∪ dom 𝑧)𝑐 → (𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏)))}    &   ⊢ 𝐶 = (𝑎 ∈ V ↦ sup((𝑦‘𝑎), (𝑅1‘dom 𝑧), 𝐵))    &   ⊢ 𝐷 = recs((𝑎 ∈ V ↦ (𝐶‘((𝑅1‘dom 𝑧) ∖ ran 𝑎))))    &   ⊢ 𝐸 = {⟨𝑎, 𝑏⟩ ∣ ∩ (◡𝐷 “ {𝑎}) ∈ ∩ (◡𝐷 “ {𝑏})}    &   ⊢ 𝐹 = {⟨𝑎, 𝑏⟩ ∣ ((rank‘𝑎) E (rank‘𝑏) ∨ ((rank‘𝑎) = (rank‘𝑏) ∧ 𝑎(𝑧‘suc (rank‘𝑎))𝑏))}    &   ⊢ 𝐺 = (if(dom 𝑧 = ∪ dom 𝑧, 𝐹, 𝐸) ∩ ((𝑅1‘dom 𝑧) × (𝑅1‘dom 𝑧)))    &   ⊢ (𝜑 → dom 𝑧 ∈ On)    &   ⊢ (𝜑 → ∀𝑎 ∈ dom 𝑧(𝑧‘𝑎) We (𝑅1‘𝑎))    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → dom 𝑧 ⊆ 𝐴)    &   ⊢ (𝜑 → ∀𝑎 ∈ 𝒫 (𝑅1‘𝐴)(𝑎 ≠ ∅ → (𝑦‘𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅})))    ⇒   ⊢ (𝜑 → 𝐺 We (𝑅1‘dom 𝑧))
Theorem	aomclem6 43091*	Lemma for dfac11 43094. Transfinite induction, close over 𝑧. (Contributed by Stefan O'Rear, 20-Jan-2015.)
⊢ 𝐵 = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ (𝑅1‘∪ dom 𝑧)((𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎) ∧ ∀𝑑 ∈ (𝑅1‘∪ dom 𝑧)(𝑑(𝑧‘∪ dom 𝑧)𝑐 → (𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏)))}    &   ⊢ 𝐶 = (𝑎 ∈ V ↦ sup((𝑦‘𝑎), (𝑅1‘dom 𝑧), 𝐵))    &   ⊢ 𝐷 = recs((𝑎 ∈ V ↦ (𝐶‘((𝑅1‘dom 𝑧) ∖ ran 𝑎))))    &   ⊢ 𝐸 = {⟨𝑎, 𝑏⟩ ∣ ∩ (◡𝐷 “ {𝑎}) ∈ ∩ (◡𝐷 “ {𝑏})}    &   ⊢ 𝐹 = {⟨𝑎, 𝑏⟩ ∣ ((rank‘𝑎) E (rank‘𝑏) ∨ ((rank‘𝑎) = (rank‘𝑏) ∧ 𝑎(𝑧‘suc (rank‘𝑎))𝑏))}    &   ⊢ 𝐺 = (if(dom 𝑧 = ∪ dom 𝑧, 𝐹, 𝐸) ∩ ((𝑅1‘dom 𝑧) × (𝑅1‘dom 𝑧)))    &   ⊢ 𝐻 = recs((𝑧 ∈ V ↦ 𝐺))    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → ∀𝑎 ∈ 𝒫 (𝑅1‘𝐴)(𝑎 ≠ ∅ → (𝑦‘𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅})))    ⇒   ⊢ (𝜑 → (𝐻‘𝐴) We (𝑅1‘𝐴))
Theorem	aomclem7 43092*	Lemma for dfac11 43094. (𝑅1‘𝐴) is well-orderable. (Contributed by Stefan O'Rear, 20-Jan-2015.)
⊢ 𝐵 = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ (𝑅1‘∪ dom 𝑧)((𝑐 ∈ 𝑏 ∧ ¬ 𝑐 ∈ 𝑎) ∧ ∀𝑑 ∈ (𝑅1‘∪ dom 𝑧)(𝑑(𝑧‘∪ dom 𝑧)𝑐 → (𝑑 ∈ 𝑎 ↔ 𝑑 ∈ 𝑏)))}    &   ⊢ 𝐶 = (𝑎 ∈ V ↦ sup((𝑦‘𝑎), (𝑅1‘dom 𝑧), 𝐵))    &   ⊢ 𝐷 = recs((𝑎 ∈ V ↦ (𝐶‘((𝑅1‘dom 𝑧) ∖ ran 𝑎))))    &   ⊢ 𝐸 = {⟨𝑎, 𝑏⟩ ∣ ∩ (◡𝐷 “ {𝑎}) ∈ ∩ (◡𝐷 “ {𝑏})}    &   ⊢ 𝐹 = {⟨𝑎, 𝑏⟩ ∣ ((rank‘𝑎) E (rank‘𝑏) ∨ ((rank‘𝑎) = (rank‘𝑏) ∧ 𝑎(𝑧‘suc (rank‘𝑎))𝑏))}    &   ⊢ 𝐺 = (if(dom 𝑧 = ∪ dom 𝑧, 𝐹, 𝐸) ∩ ((𝑅1‘dom 𝑧) × (𝑅1‘dom 𝑧)))    &   ⊢ 𝐻 = recs((𝑧 ∈ V ↦ 𝐺))    &   ⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → ∀𝑎 ∈ 𝒫 (𝑅1‘𝐴)(𝑎 ≠ ∅ → (𝑦‘𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅})))    ⇒   ⊢ (𝜑 → ∃𝑏 𝑏 We (𝑅1‘𝐴))
Theorem	aomclem8 43093*	Lemma for dfac11 43094. Perform variable substitutions. This is the most we can say without invoking regularity. (Contributed by Stefan O'Rear, 20-Jan-2015.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → ∀𝑎 ∈ 𝒫 (𝑅1‘𝐴)(𝑎 ≠ ∅ → (𝑦‘𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅})))    ⇒   ⊢ (𝜑 → ∃𝑏 𝑏 We (𝑅1‘𝐴))
Theorem	dfac11 43094*	The right-hand side of this theorem (compare with ac4 10363), sometimes known as the "axiom of multiple choice", is a choice equivalent. Curiously, this statement cannot be proved without ax-reg 9478, despite not mentioning the cumulative hierarchy in any way as most consequences of regularity do. This is definition (MC) of [Schechter] p. 141. EDITORIAL: the proof is not original with me of course but I lost my reference sometime after writing it. A multiple choice function allows any total order to be extended to a choice function, which in turn defines a well-ordering. Since a well-ordering on a set defines a simple ordering of the power set, this allows the trivial well-ordering of the empty set to be transfinitely bootstrapped up the cumulative hierarchy to any desired level. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Stefan O'Rear, 1-Jun-2015.)
⊢ (CHOICE ↔ ∀𝑥∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ ((𝒫 𝑧 ∩ Fin) ∖ {∅})))
Theorem	kelac1 43095*	Kelley's choice, basic form: if a collection of sets can be cast as closed sets in the factors of a topology, and there is a definable element in each topology (which need not be in the closed set - if it were this would be trivial), then compactness (via finite intersection) guarantees that the final product is nonempty. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ≠ ∅)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐽 ∈ Top)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐶 ∈ (Clsd‘𝐽))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐵:𝑆–1-1-onto→𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑈 ∈ ∪ 𝐽)    &   ⊢ (𝜑 → (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Comp)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐼 𝑆 ≠ ∅)
Theorem	kelac2lem 43096	Lemma for kelac2 43097 and dfac21 43098: knob topologies are compact. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ (𝑆 ∈ 𝑉 → (topGen‘{𝑆, {𝒫 ∪ 𝑆}}) ∈ Comp)
Theorem	kelac2 43097*	Kelley's choice, most common form: compactness of a product of knob topologies recovers choice. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ≠ ∅)    &   ⊢ (𝜑 → (∏t‘(𝑥 ∈ 𝐼 ↦ (topGen‘{𝑆, {𝒫 ∪ 𝑆}}))) ∈ Comp)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐼 𝑆 ≠ ∅)
Theorem	dfac21 43098	Tychonoff's theorem is a choice equivalent. Definition AC21 of Schechter p. 461. (Contributed by Stefan O'Rear, 22-Feb-2015.) (Revised by Mario Carneiro, 27-Aug-2015.)
⊢ (CHOICE ↔ ∀𝑓(𝑓:dom 𝑓⟶Comp → (∏t‘𝑓) ∈ Comp))
21.33.37  Finitely generated left modules
Syntax	clfig 43099	Extend class notation with the class of finitely generated left modules.
class LFinGen
Definition	df-lfig 43100	Define the class of finitely generated left modules. Finite generation of subspaces can be interpreted using ↾s. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ LFinGen = {𝑤 ∈ LMod ∣ (Base‘𝑤) ∈ ((LSpan‘𝑤) “ (𝒫 (Base‘𝑤) ∩ Fin))}