P. 438 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43701-43800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	jm2.16nn0 43701	Lemma 2.16 of [JonesMatijasevic] p. 695. This may be regarded as a special case of jm2.15nn0 43700 if Yrm is redefined as described in rmyluc 43634. (Contributed by Stefan O'Rear, 1-Oct-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → (𝐴 − 1) ∥ ((𝐴 Yrm 𝑁) − 𝑁))
21.34.33  X and Y sequences 4: Diophantine representability of Y
Theorem	jm2.27a 43702	Lemma for jm2.27 43705. 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 43703	Lemma for jm2.27 43705. 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 43704	Lemma for jm2.27 43705. 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 43705*	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 43702 and jm2.27c 43704. 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 43706*	Lemma for rmydioph 43711. 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 43707	Lemma for rmydioph 43711. 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 43708	Lemma for rmydioph 43711. Infer membership of the endpoint of a range. (Contributed by Stefan O'Rear, 11-Oct-2014.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ 𝐴 ∈ (1...𝐴)
Theorem	jm2.27dlem4 43709	Lemma for rmydioph 43711. Infer ℕ-hood of large numbers. (Contributed by Stefan O'Rear, 11-Oct-2014.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 = (𝐴 + 1)    ⇒   ⊢ 𝐵 ∈ ℕ
Theorem	jm2.27dlem5 43710	Lemma for rmydioph 43711. Used with sselii 3933 to infer membership of midpoints of range; jm2.27dlem2 43707 is deprecated. (Contributed by Stefan O'Rear, 11-Oct-2014.)
⊢ 𝐵 = (𝐴 + 1)    &   ⊢ (1...𝐵) ⊆ (1...𝐶)    ⇒   ⊢ (1...𝐴) ⊆ (1...𝐶)
Theorem	rmydioph 43711	jm2.27 43705 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.34.34  X and Y sequences 5: Diophantine representability of X, ^, _C
Theorem	rmxdiophlem 43712*	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 43713	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 43714	Lemma for jm3.1 43717. (Contributed by Stefan O'Rear, 16-Oct-2014.)
⊢ (𝜑 → 𝐴 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴)    ⇒   ⊢ (𝜑 → (𝐾↑𝑁) < 𝐴)
Theorem	jm3.1lem2 43715	Lemma for jm3.1 43717. (Contributed by Stefan O'Rear, 16-Oct-2014.)
⊢ (𝜑 → 𝐴 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴)    ⇒   ⊢ (𝜑 → (𝐾↑𝑁) < ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1))
Theorem	jm3.1lem3 43716	Lemma for jm3.1 43717. (Contributed by Stefan O'Rear, 17-Oct-2014.)
⊢ (𝜑 → 𝐴 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴)    ⇒   ⊢ (𝜑 → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∈ ℕ)
Theorem	jm3.1 43717	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 43718*	Lemma for expdioph 43720. 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 43719	Lemma for expdioph 43720. 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 43720	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.34.35  Uncategorized stuff not associated with a major project
Theorem	setindtr 43721*	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 9715; however, this version is useful without Infinity. (Contributed by Stefan O'Rear, 28-Oct-2014.)
⊢ (∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴) → (∃𝑦(Tr 𝑦 ∧ 𝐵 ∈ 𝑦) → 𝐵 ∈ 𝐴))
Theorem	setindtrs 43722*	Set induction scheme without Infinity. See comments at setindtr 43721. (Contributed by Stefan O'Rear, 28-Oct-2014.)
⊢ (∀𝑦 ∈ 𝑥 𝜓 → 𝜑)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    ⇒   ⊢ (∃𝑧(Tr 𝑧 ∧ 𝐵 ∈ 𝑧) → 𝜒)
Theorem	dford3lem1 43723*	Lemma for dford3 43725. (Contributed by Stefan O'Rear, 28-Oct-2014.)
⊢ ((Tr 𝑁 ∧ ∀𝑦 ∈ 𝑁 Tr 𝑦) → ∀𝑏 ∈ 𝑁 (Tr 𝑏 ∧ ∀𝑦 ∈ 𝑏 Tr 𝑦))
Theorem	dford3lem2 43724*	Lemma for dford3 43725. (Contributed by Stefan O'Rear, 28-Oct-2014.)
⊢ ((Tr 𝑥 ∧ ∀𝑦 ∈ 𝑥 Tr 𝑦) → 𝑥 ∈ On)
Theorem	dford3 43725*	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 43726*	dford3 43725 expressed in primitives to demonstrate shortness. (Contributed by Stefan O'Rear, 28-Oct-2014.)
⊢ (Ord 𝑁 ↔ ∀𝑎∀𝑏∀𝑐((𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑎) → (𝑏 ∈ 𝑁 ∧ (𝑐 ∈ 𝑏 → 𝑐 ∈ 𝑎))))
Theorem	wopprc 43727	Unrelated: Wiener pairs treat proper classes symmetrically. (Contributed by Stefan O'Rear, 19-Sep-2014.)
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ ¬ 1o ∈ {{{𝐴}, ∅}, {{𝐵}}})
Theorem	rpnnen3lem 43728*	Lemma for rpnnen3 43729. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ 𝑎 < 𝑏) → {𝑐 ∈ ℚ ∣ 𝑐 < 𝑎} ≠ {𝑐 ∈ ℚ ∣ 𝑐 < 𝑏})
Theorem	rpnnen3 43729	Dedekind cut injection of ℝ into 𝒫 ℚ. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ ℝ ≼ 𝒫 ℚ
21.34.36  More equivalents of the Axiom of Choice
Theorem	axac10 43730	Characterization of choice similar to dffin1-5 10371. (Contributed by Stefan O'Rear, 6-Jan-2015.)
⊢ ( ≈ “ On) = V
Theorem	harinf 43731	The Hartogs number of an infinite set is at least ω. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.)
⊢ ((𝑆 ∈ 𝑉 ∧ ¬ 𝑆 ∈ Fin) → ω ⊆ (har‘𝑆))
Theorem	wdom2d2 43732*	Deduction for weak dominance by a Cartesian product. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝑥 = 𝑋)    ⇒   ⊢ (𝜑 → 𝐴 ≼* (𝐵 × 𝐶))
Theorem	ttac 43733	Tarski's theorem about choice: infxpidm 10545 is equivalent to ax-ac 10442. (Contributed by Stefan O'Rear, 4-Nov-2014.) (Proof shortened by Stefan O'Rear, 10-Jul-2015.)
⊢ (CHOICE ↔ ∀𝑐(ω ≼ 𝑐 → (𝑐 × 𝑐) ≈ 𝑐))
Theorem	pw2f1ocnv 43734*	Define a bijection between characteristic functions and subsets. EDITORIAL: extracted from pw2en 9071, 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 43735*	Define a bijection between characteristic functions and subsets. EDITORIAL: extracted from pw2en 9071, 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 43736*	Function value of the pw2f1o2 43735 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 43737*	Membership in a mapped set under the pw2f1o2 43735 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 43738	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 43739*	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 43740*	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 43741*	Define an enumeration of a set from a choice function; second part, it restricts to a bijection. EDITORIAL: overlaps dfac8a 10013. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ 𝐹 = recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧))))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝐺‘𝑦) ∈ 𝑦))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ On (𝐹 ↾ 𝑥):𝑥–1-1-onto→𝐴)
Theorem	dnnumch2 43742*	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 43743*	Value of the ordinal injection function. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ 𝐹 = recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧))))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝐺‘𝑦) ∈ 𝑦))    ⇒   ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) = ∩ (◡𝐹 “ {𝑤}))
Theorem	dnnumch3 43744*	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 43745*	Define a well-ordering from a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ 𝐹 = recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧))))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝐺‘𝑦) ∈ 𝑦))    &   ⊢ 𝐻 = {⟨𝑣, 𝑤⟩ ∣ ∩ (◡𝐹 “ {𝑣}) ∈ ∩ (◡𝐹 “ {𝑤})}    ⇒   ⊢ (𝜑 → 𝐻 We 𝐴)
Theorem	fnwe2val 43746*	Lemma for fnwe2 43750. Substitute variables. (Contributed by Stefan O'Rear, 19-Jan-2015.)
⊢ (𝑧 = (𝐹‘𝑥) → 𝑆 = 𝑈)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑈𝑦))}    ⇒   ⊢ (𝑎𝑇𝑏 ↔ ((𝐹‘𝑎)𝑅(𝐹‘𝑏) ∨ ((𝐹‘𝑎) = (𝐹‘𝑏) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏)))
Theorem	fnwe2lem1 43747*	Lemma for fnwe2 43750. Substitution in well-ordering hypothesis. (Contributed by Stefan O'Rear, 19-Jan-2015.)
⊢ (𝑧 = (𝐹‘𝑥) → 𝑆 = 𝑈)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑈𝑦))}    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑈 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑥)})    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)})
Theorem	fnwe2lem2 43748*	Lemma for fnwe2 43750. 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 43749*	Lemma for fnwe2 43750. Trichotomy. (Contributed by Stefan O'Rear, 19-Jan-2015.)
⊢ (𝑧 = (𝐹‘𝑥) → 𝑆 = 𝑈)    &   ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑈𝑦))}    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑈 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑥)})    &   ⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝑅 We 𝐵)    &   ⊢ (𝜑 → 𝑎 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑏 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎))
Theorem	fnwe2 43750*	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 8127 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 43751*	Lemma for dfac11 43759. 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 43752*	Lemma for dfac11 43759. 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 43753*	Lemma for dfac11 43759. 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 43754*	Lemma for dfac11 43759. Limit case. Patch together well-orderings constructed so far using fnwe2 43750 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 43755*	Lemma for dfac11 43759. 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 43756*	Lemma for dfac11 43759. 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 43757*	Lemma for dfac11 43759. (𝑅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 43758*	Lemma for dfac11 43759. 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 43759*	The right-hand side of this theorem (compare with ac4 10458), sometimes known as the "axiom of multiple choice", is a choice equivalent. Curiously, this statement cannot be proved without ax-reg 9553, 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 43760*	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 43761	Lemma for kelac2 43762 and dfac21 43763: knob topologies are compact. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ (𝑆 ∈ 𝑉 → (topGen‘{𝑆, {𝒫 ∪ 𝑆}}) ∈ Comp)
Theorem	kelac2 43762*	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 43763	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.34.37  Finitely generated left modules
Syntax	clfig 43764	Extend class notation with the class of finitely generated left modules.
class LFinGen
Definition	df-lfig 43765	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))}
Theorem	islmodfg 43766*	Property of a finitely generated left module. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ (𝑊 ∈ LMod → (𝑊 ∈ LFinGen ↔ ∃𝑏 ∈ 𝒫 𝐵(𝑏 ∈ Fin ∧ (𝑁‘𝑏) = 𝐵)))
Theorem	islssfg 43767*	Property of a finitely generated left (sub)module. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑋 ∈ LFinGen ↔ ∃𝑏 ∈ 𝒫 𝑈(𝑏 ∈ Fin ∧ (𝑁‘𝑏) = 𝑈)))
Theorem	islssfg2 43768*	Property of a finitely generated left (sub)module, with a relaxed constraint on the spanning vectors. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑋 ∈ LFinGen ↔ ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)(𝑁‘𝑏) = 𝑈))
Theorem	islssfgi 43769	Finitely spanned subspaces are finitely generated. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑁 = (LSpan‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑋 = (𝑊 ↾s (𝑁‘𝐵))    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝐵 ⊆ 𝑉 ∧ 𝐵 ∈ Fin) → 𝑋 ∈ LFinGen)
Theorem	fglmod 43770	Finitely generated left modules are left modules. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ (𝑀 ∈ LFinGen → 𝑀 ∈ LMod)
Theorem	lsmfgcl 43771	The sum of two finitely generated submodules is finitely generated. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑈 = (LSubSp‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝐷 = (𝑊 ↾s 𝐴)    &   ⊢ 𝐸 = (𝑊 ↾s 𝐵)    &   ⊢ 𝐹 = (𝑊 ↾s (𝐴 ⊕ 𝐵))    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐷 ∈ LFinGen)    &   ⊢ (𝜑 → 𝐸 ∈ LFinGen)    ⇒   ⊢ (𝜑 → 𝐹 ∈ LFinGen)
21.34.38  Noetherian left modules I
Syntax	clnm 43772	Extend class notation with the class of Noetherian left modules.
class LNoeM
Definition	df-lnm 43773*	A left-module is Noetherian iff it is hereditarily finitely generated. (Contributed by Stefan O'Rear, 12-Dec-2014.)
⊢ LNoeM = {𝑤 ∈ LMod ∣ ∀𝑖 ∈ (LSubSp‘𝑤)(𝑤 ↾s 𝑖) ∈ LFinGen}
Theorem	islnm 43774*	Property of being a Noetherian left module. (Contributed by Stefan O'Rear, 12-Dec-2014.)
⊢ 𝑆 = (LSubSp‘𝑀)    ⇒   ⊢ (𝑀 ∈ LNoeM ↔ (𝑀 ∈ LMod ∧ ∀𝑖 ∈ 𝑆 (𝑀 ↾s 𝑖) ∈ LFinGen))
Theorem	islnm2 43775*	Property of being a Noetherian left module with finite generation expanded in terms of spans. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑆 = (LSubSp‘𝑀)    &   ⊢ 𝑁 = (LSpan‘𝑀)    ⇒   ⊢ (𝑀 ∈ LNoeM ↔ (𝑀 ∈ LMod ∧ ∀𝑖 ∈ 𝑆 ∃𝑔 ∈ (𝒫 𝐵 ∩ Fin)𝑖 = (𝑁‘𝑔)))
Theorem	lnmlmod 43776	A Noetherian left module is a left module. (Contributed by Stefan O'Rear, 12-Dec-2014.)
⊢ (𝑀 ∈ LNoeM → 𝑀 ∈ LMod)
Theorem	lnmlssfg 43777	A submodule of Noetherian module is finitely generated. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑀)    &   ⊢ 𝑅 = (𝑀 ↾s 𝑈)    ⇒   ⊢ ((𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆) → 𝑅 ∈ LFinGen)
Theorem	lnmlsslnm 43778	All submodules of a Noetherian module are Noetherian. (Contributed by Stefan O'Rear, 1-Jan-2015.)
⊢ 𝑆 = (LSubSp‘𝑀)    &   ⊢ 𝑅 = (𝑀 ↾s 𝑈)    ⇒   ⊢ ((𝑀 ∈ LNoeM ∧ 𝑈 ∈ 𝑆) → 𝑅 ∈ LNoeM)
Theorem	lnmfg 43779	A Noetherian left module is finitely generated. (Contributed by Stefan O'Rear, 12-Dec-2014.)
⊢ (𝑀 ∈ LNoeM → 𝑀 ∈ LFinGen)
Theorem	kercvrlsm 43780	The domain of a linear function is the subspace sum of the kernel and any subspace which covers the range. (Contributed by Stefan O'Rear, 24-Jan-2015.) (Revised by Stefan O'Rear, 6-May-2015.)
⊢ 𝑈 = (LSubSp‘𝑆)    &   ⊢ ⊕ = (LSSum‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    &   ⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇))    &   ⊢ (𝜑 → 𝐷 ∈ 𝑈)    &   ⊢ (𝜑 → (𝐹 “ 𝐷) = ran 𝐹)    ⇒   ⊢ (𝜑 → (𝐾 ⊕ 𝐷) = 𝐵)
Theorem	lmhmfgima 43781	A homomorphism maps finitely generated submodules to finitely generated submodules. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑇 ↾s (𝐹 “ 𝐴))    &   ⊢ 𝑋 = (𝑆 ↾s 𝐴)    &   ⊢ 𝑈 = (LSubSp‘𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ LFinGen)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇))    ⇒   ⊢ (𝜑 → 𝑌 ∈ LFinGen)
Theorem	lnmepi 43782	Epimorphic images of Noetherian modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝐵 = (Base‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑆 ∈ LNoeM ∧ ran 𝐹 = 𝐵) → 𝑇 ∈ LNoeM)
Theorem	lmhmfgsplit 43783	If the kernel and range of a homomorphism of left modules are finitely generated, then so is the domain. (Contributed by Stefan O'Rear, 1-Jan-2015.) (Revised by Stefan O'Rear, 6-May-2015.)
⊢ 0 = (0g‘𝑇)    &   ⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 𝑈 = (𝑆 ↾s 𝐾)    &   ⊢ 𝑉 = (𝑇 ↾s ran 𝐹)    ⇒   ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LFinGen ∧ 𝑉 ∈ LFinGen) → 𝑆 ∈ LFinGen)
Theorem	lmhmlnmsplit 43784	If the kernel and range of a homomorphism of left modules are Noetherian, then so is the domain. (Contributed by Stefan O'Rear, 1-Jan-2015.) (Revised by Stefan O'Rear, 12-Jun-2015.)
⊢ 0 = (0g‘𝑇)    &   ⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 𝑈 = (𝑆 ↾s 𝐾)    &   ⊢ 𝑉 = (𝑇 ↾s ran 𝐹)    ⇒   ⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) → 𝑆 ∈ LNoeM)
Theorem	lnmlmic 43785	Noetherian is an invariant property of modules. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ (𝑅 ≃𝑚 𝑆 → (𝑅 ∈ LNoeM ↔ 𝑆 ∈ LNoeM))
21.34.39  Addenda for structure powers
Theorem	pwssplit4 43786*	Splitting for structure powers 4: maps isomorphically onto the other half. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ 𝐸 = (𝑅 ↑s (𝐴 ∪ 𝐵))    &   ⊢ 𝐺 = (Base‘𝐸)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐾 = {𝑦 ∈ 𝐺 ∣ (𝑦 ↾ 𝐴) = (𝐴 × { 0 })}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ (𝑥 ↾ 𝐵))    &   ⊢ 𝐶 = (𝑅 ↑s 𝐴)    &   ⊢ 𝐷 = (𝑅 ↑s 𝐵)    &   ⊢ 𝐿 = (𝐸 ↾s 𝐾)    ⇒   ⊢ ((𝑅 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ 𝑉 ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐹 ∈ (𝐿 LMIso 𝐷))
Theorem	filnm 43787	Finite left modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ ((𝑊 ∈ LMod ∧ 𝐵 ∈ Fin) → 𝑊 ∈ LNoeM)
Theorem	pwslnmlem0 43788	Zeroeth powers are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑊 ↑s ∅)    ⇒   ⊢ (𝑊 ∈ LMod → 𝑌 ∈ LNoeM)
Theorem	pwslnmlem1 43789*	First powers are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑊 ↑s {𝑖})    ⇒   ⊢ (𝑊 ∈ LNoeM → 𝑌 ∈ LNoeM)
Theorem	pwslnmlem2 43790	A sum of powers is Noetherian. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑋 = (𝑊 ↑s 𝐴)    &   ⊢ 𝑌 = (𝑊 ↑s 𝐵)    &   ⊢ 𝑍 = (𝑊 ↑s (𝐴 ∪ 𝐵))    &   ⊢ (𝜑 → 𝑊 ∈ LMod)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → 𝑋 ∈ LNoeM)    &   ⊢ (𝜑 → 𝑌 ∈ LNoeM)    ⇒   ⊢ (𝜑 → 𝑍 ∈ LNoeM)
Theorem	pwslnm 43791	Finite powers of Noetherian modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑊 ↑s 𝐼)    ⇒   ⊢ ((𝑊 ∈ LNoeM ∧ 𝐼 ∈ Fin) → 𝑌 ∈ LNoeM)
21.34.40  Every set admits a group structure iff choice
Theorem	unxpwdom3 43792*	Weaker version of unxpwdom 9550 where a function is required only to be cancellative, not an injection. 𝐷 and 𝐵 are to be thought of as "large" "horizonal" sets, the others as "small". Because the operator is row-wise injective, but the whole row cannot inject into 𝐴, each row must hit an element of 𝐵; by column injectivity, each row can be identified in at least one way by the 𝐵 element that it hits and the column in which it is hit. (Contributed by Stefan O'Rear, 8-Jul-2015.) MOVABLE
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐷) → (𝑎 + 𝑏) ∈ (𝐴 ∪ 𝐵))    &   ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑏 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) → ((𝑎 + 𝑏) = (𝑎 + 𝑐) ↔ 𝑏 = 𝑐))    &   ⊢ (((𝜑 ∧ 𝑑 ∈ 𝐷) ∧ (𝑎 ∈ 𝐶 ∧ 𝑐 ∈ 𝐶)) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎))    &   ⊢ (𝜑 → ¬ 𝐷 ≼ 𝐴)    ⇒   ⊢ (𝜑 → 𝐶 ≼* (𝐷 × 𝐵))
Theorem	pwfi2f1o 43793*	The pw2f1o 9069 bijection relates finitely supported indicator functions on a two-element set to finite subsets. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) (Revised by AV, 14-Jun-2020.)
⊢ 𝑆 = {𝑦 ∈ (2o ↑m 𝐴) ∣ 𝑦 finSupp ∅}    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ (◡𝑥 “ {1o}))    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐹:𝑆–1-1-onto→(𝒫 𝐴 ∩ Fin))
Theorem	pwfi2en 43794*	Finitely supported indicator functions are equinumerous to finite subsets. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) (Revised by AV, 14-Jun-2020.)
⊢ 𝑆 = {𝑦 ∈ (2o ↑m 𝐴) ∣ 𝑦 finSupp ∅}    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝑆 ≈ (𝒫 𝐴 ∩ Fin))
Theorem	frlmpwfi 43795	Formal linear combinations over Z/2Z are equivalent to finite subsets. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.) (Proof shortened by AV, 14-Jun-2020.)
⊢ 𝑅 = (ℤ/nℤ‘2)    &   ⊢ 𝑌 = (𝑅 freeLMod 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐵 ≈ (𝒫 𝐼 ∩ Fin))
Theorem	gicabl 43796	Being Abelian is a group invariant. MOVABLE (Contributed by Stefan O'Rear, 8-Jul-2015.)
⊢ (𝐺 ≃𝑔 𝐻 → (𝐺 ∈ Abel ↔ 𝐻 ∈ Abel))
Theorem	imasgim 43797	A relabeling of the elements of a group induces an isomorphism to the relabeled group. MOVABLE (Contributed by Stefan O'Rear, 8-Jul-2015.) (Revised by Mario Carneiro, 11-Aug-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpIso 𝑈))
Theorem	isnumbasgrplem1 43798	A set which is equipollent to the base set of a definable Abelian group is the base set of some (relabeled) Abelian group. (Contributed by Stefan O'Rear, 8-Jul-2015.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Abel ∧ 𝐶 ≈ 𝐵) → 𝐶 ∈ (Base “ Abel))
Theorem	harn0 43799	The Hartogs number of a set is never zero. MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015.)
⊢ (𝑆 ∈ 𝑉 → (har‘𝑆) ≠ ∅)
Theorem	numinfctb 43800	A numerable infinite set contains a countable subset. MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015.)
⊢ ((𝑆 ∈ dom card ∧ ¬ 𝑆 ∈ Fin) → ω ≼ 𝑆)