P. 105 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 10401-10500   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-fin2 10401*	A set is II-finite (Tarski finite) iff every nonempty chain of subsets contains a maximum element. Definition II of [Levy58] p. 2. (Contributed by Stefan O'Rear, 12-Nov-2014.)
⊢ FinII = {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝒫 𝑥((𝑦 ≠ ∅ ∧ [⊊] Or 𝑦) → ∪ 𝑦 ∈ 𝑦)}
Definition	df-fin4 10402*	A set is IV-finite (Dedekind finite) iff it has no equinumerous proper subset. Definition IV of [Levy58] p. 3. (Contributed by Stefan O'Rear, 12-Nov-2014.)
⊢ FinIV = {𝑥 ∣ ¬ ∃𝑦(𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥)}
Definition	df-fin3 10403	A set is III-finite (weakly Dedekind finite) iff its power set is Dedekind finite. Definition III of [Levy58] p. 2. (Contributed by Stefan O'Rear, 12-Nov-2014.)
⊢ FinIII = {𝑥 ∣ 𝒫 𝑥 ∈ FinIV}
Definition	df-fin5 10404	A set is V-finite iff it behaves finitely under ⊔. Definition V of [Levy58] p. 3. (Contributed by Stefan O'Rear, 12-Nov-2014.)
⊢ FinV = {𝑥 ∣ (𝑥 = ∅ ∨ 𝑥 ≺ (𝑥 ⊔ 𝑥))}
Definition	df-fin6 10405	A set is VI-finite iff it behaves finitely under ×. Definition VI of [Levy58] p. 4. (Contributed by Stefan O'Rear, 12-Nov-2014.)
⊢ FinVI = {𝑥 ∣ (𝑥 ≺ 2o ∨ 𝑥 ≺ (𝑥 × 𝑥))}
Definition	df-fin7 10406*	A set is VII-finite iff it cannot be infinitely well-ordered. Equivalent to definition VII of [Levy58] p. 4. (Contributed by Stefan O'Rear, 12-Nov-2014.)
⊢ FinVII = {𝑥 ∣ ¬ ∃𝑦 ∈ (On ∖ ω)𝑥 ≈ 𝑦}
Theorem	isfin1a 10407*	Definition of a Ia-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinIa ↔ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ Fin ∨ (𝐴 ∖ 𝑦) ∈ Fin)))
Theorem	fin1ai 10408	Property of a Ia-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
⊢ ((𝐴 ∈ FinIa ∧ 𝑋 ⊆ 𝐴) → (𝑋 ∈ Fin ∨ (𝐴 ∖ 𝑋) ∈ Fin))
Theorem	isfin2 10409*	Definition of a II-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinII ↔ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or 𝑦) → ∪ 𝑦 ∈ 𝑦)))
Theorem	fin2i 10410	Property of a II-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
⊢ (((𝐴 ∈ FinII ∧ 𝐵 ⊆ 𝒫 𝐴) ∧ (𝐵 ≠ ∅ ∧ [⊊] Or 𝐵)) → ∪ 𝐵 ∈ 𝐵)
Theorem	isfin3 10411	Definition of a III-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
⊢ (𝐴 ∈ FinIII ↔ 𝒫 𝐴 ∈ FinIV)
Theorem	isfin4 10412*	Definition of a IV-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinIV ↔ ¬ ∃𝑦(𝑦 ⊊ 𝐴 ∧ 𝑦 ≈ 𝐴)))
Theorem	fin4i 10413	Infer that a set is IV-infinite. (Contributed by Stefan O'Rear, 16-May-2015.)
⊢ ((𝑋 ⊊ 𝐴 ∧ 𝑋 ≈ 𝐴) → ¬ 𝐴 ∈ FinIV)
Theorem	isfin5 10414	Definition of a V-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
⊢ (𝐴 ∈ FinV ↔ (𝐴 = ∅ ∨ 𝐴 ≺ (𝐴 ⊔ 𝐴)))
Theorem	isfin6 10415	Definition of a VI-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
⊢ (𝐴 ∈ FinVI ↔ (𝐴 ≺ 2o ∨ 𝐴 ≺ (𝐴 × 𝐴)))
Theorem	isfin7 10416*	Definition of a VII-finite set. (Contributed by Stefan O'Rear, 16-May-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinVII ↔ ¬ ∃𝑦 ∈ (On ∖ ω)𝐴 ≈ 𝑦))
Theorem	sdom2en01 10417	A set with less than two elements has 0 or 1. (Contributed by Stefan O'Rear, 30-Oct-2014.)
⊢ (𝐴 ≺ 2o ↔ (𝐴 = ∅ ∨ 𝐴 ≈ 1o))
Theorem	infpssrlem1 10418	Lemma for infpssr 10423. (Contributed by Stefan O'Rear, 30-Oct-2014.)
⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐵⟶1-1onto𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴 ∖ 𝐵))    &   ⊢ 𝐺 = (rec(◡𝐹, 𝐶) ↾ ω)    ⇒   ⊢ (𝜑 → (𝐺‘∅) = 𝐶)
Theorem	infpssrlem2 10419	Lemma for infpssr 10423. (Contributed by Stefan O'Rear, 30-Oct-2014.)
⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐵⟶1-1onto𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴 ∖ 𝐵))    &   ⊢ 𝐺 = (rec(◡𝐹, 𝐶) ↾ ω)    ⇒   ⊢ (𝑀 ∈ ω → (𝐺‘suc 𝑀) = (◡𝐹‘(𝐺‘𝑀)))
Theorem	infpssrlem3 10420	Lemma for infpssr 10423. (Contributed by Stefan O'Rear, 30-Oct-2014.)
⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐵⟶1-1onto𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴 ∖ 𝐵))    &   ⊢ 𝐺 = (rec(◡𝐹, 𝐶) ↾ ω)    ⇒   ⊢ (𝜑 → 𝐺:ω⟶𝐴)
Theorem	infpssrlem4 10421	Lemma for infpssr 10423. (Contributed by Stefan O'Rear, 30-Oct-2014.)
⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐵⟶1-1onto𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴 ∖ 𝐵))    &   ⊢ 𝐺 = (rec(◡𝐹, 𝐶) ↾ ω)    ⇒   ⊢ ((𝜑 ∧ 𝑀 ∈ ω ∧ 𝑁 ∈ 𝑀) → (𝐺‘𝑀) ≠ (𝐺‘𝑁))
Theorem	infpssrlem5 10422	Lemma for infpssr 10423. (Contributed by Stefan O'Rear, 30-Oct-2014.)
⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐵⟶1-1onto𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴 ∖ 𝐵))    &   ⊢ 𝐺 = (rec(◡𝐹, 𝐶) ↾ ω)    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝑉 → ω ≼ 𝐴))
Theorem	infpssr 10423	Dedekind infinity implies existence of a denumerable subset: take a single point witnessing the proper subset relation and iterate the embedding. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 16-May-2015.)
⊢ ((𝑋 ⊊ 𝐴 ∧ 𝑋 ≈ 𝐴) → ω ≼ 𝐴)
Theorem	fin4en1 10424	Dedekind finite is a cardinal property. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 16-May-2015.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ FinIV → 𝐵 ∈ FinIV))
Theorem	ssfin4 10425	Dedekind finite sets have Dedekind finite subsets. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 6-May-2015.) (Revised by Mario Carneiro, 16-May-2015.)
⊢ ((𝐴 ∈ FinIV ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ FinIV)
Theorem	domfin4 10426	A set dominated by a Dedekind finite set is Dedekind finite. (Contributed by Mario Carneiro, 16-May-2015.)
⊢ ((𝐴 ∈ FinIV ∧ 𝐵 ≼ 𝐴) → 𝐵 ∈ FinIV)
Theorem	ominf4 10427	ω is Dedekind infinite. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Proof shortened by Mario Carneiro, 16-May-2015.)
⊢ ¬ ω ∈ FinIV
Theorem	infpssALT 10428*	Alternate proof of infpss 10331, shorter but requiring Replacement (ax-rep 5236). (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 16-May-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (ω ≼ 𝐴 → ∃𝑥(𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴))
Theorem	isfin4-2 10429	Alternate definition of IV-finite sets: they lack a denumerable subset. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 17-May-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinIV ↔ ¬ ω ≼ 𝐴))
Theorem	isfin4p1 10430	Alternate definition of IV-finite sets: they are strictly dominated by their successors. (Thus, the proper subset referred to in isfin4 10412 can be assumed to be only a singleton smaller than the original.) (Contributed by Mario Carneiro, 18-May-2015.)
⊢ (𝐴 ∈ FinIV ↔ 𝐴 ≺ (𝐴 ⊔ 1o))
Theorem	fin23lem7 10431*	Lemma for isfin2-2 10434. The componentwise complement of a nonempty collection of sets is nonempty. (Contributed by Stefan O'Rear, 31-Oct-2014.) (Revised by Mario Carneiro, 16-May-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴 ∧ 𝐵 ≠ ∅) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑥) ∈ 𝐵} ≠ ∅)
Theorem	fin23lem11 10432*	Lemma for isfin2-2 10434. (Contributed by Stefan O'Rear, 31-Oct-2014.) (Revised by Mario Carneiro, 16-May-2015.)
⊢ (𝑧 = (𝐴 ∖ 𝑥) → (𝜓 ↔ 𝜒))    &   ⊢ (𝑤 = (𝐴 ∖ 𝑣) → (𝜑 ↔ 𝜃))    &   ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑣 ⊆ 𝐴) → (𝜒 ↔ 𝜃))    ⇒   ⊢ (𝐵 ⊆ 𝒫 𝐴 → (∃𝑥 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵}∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑 → ∃𝑧 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ¬ 𝜓))
Theorem	fin2i2 10433	A II-finite set contains minimal elements for every nonempty chain. (Contributed by Mario Carneiro, 16-May-2015.)
⊢ (((𝐴 ∈ FinII ∧ 𝐵 ⊆ 𝒫 𝐴) ∧ (𝐵 ≠ ∅ ∧ [⊊] Or 𝐵)) → ∩ 𝐵 ∈ 𝐵)
Theorem	isfin2-2 10434*	FinII expressed in terms of minimal elements. (Contributed by Stefan O'Rear, 2-Nov-2014.) (Proof shortened by Mario Carneiro, 16-May-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinII ↔ ∀𝑦 ∈ 𝒫 𝒫 𝐴((𝑦 ≠ ∅ ∧ [⊊] Or 𝑦) → ∩ 𝑦 ∈ 𝑦)))
Theorem	ssfin2 10435	A subset of a II-finite set is II-finite. (Contributed by Stefan O'Rear, 2-Nov-2014.) (Revised by Mario Carneiro, 16-May-2015.)
⊢ ((𝐴 ∈ FinII ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ FinII)
Theorem	enfin2i 10436	II-finiteness is a cardinal property. (Contributed by Mario Carneiro, 18-May-2015.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ FinII → 𝐵 ∈ FinII))
Theorem	fin23lem24 10437	Lemma for fin23 10504. In a class of ordinals, each element is fully identified by those of its predecessors which also belong to the class. (Contributed by Stefan O'Rear, 1-Nov-2014.)
⊢ (((Ord 𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) → ((𝐶 ∩ 𝐵) = (𝐷 ∩ 𝐵) ↔ 𝐶 = 𝐷))
Theorem	fincssdom 10438	In a chain of finite sets, dominance and subset coincide. (Contributed by Stefan O'Rear, 8-Nov-2014.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴)) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵))
Theorem	fin23lem25 10439	Lemma for fin23 10504. In a chain of finite sets, equinumerosity is equivalent to equality. (Contributed by Stefan O'Rear, 1-Nov-2014.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴)) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵))
Theorem	fin23lem26 10440*	Lemma for fin23lem22 10442. (Contributed by Stefan O'Rear, 1-Nov-2014.)
⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑖 ∈ ω) → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖)
Theorem	fin23lem23 10441*	Lemma for fin23lem22 10442. (Contributed by Stefan O'Rear, 1-Nov-2014.)
⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑖 ∈ ω) → ∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖)
Theorem	fin23lem22 10442*	Lemma for fin23 10504 but could be used elsewhere if we find a good name for it. Explicit construction of a bijection (actually an isomorphism, see fin23lem27 10443) between an infinite subset of ω and ω itself. (Contributed by Stefan O'Rear, 1-Nov-2014.)
⊢ 𝐶 = (𝑖 ∈ ω ↦ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖))    ⇒   ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶:ω⟶1-1onto𝑆)
Theorem	fin23lem27 10443*	The mapping constructed in fin23lem22 10442 is in fact an isomorphism. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ 𝐶 = (𝑖 ∈ ω ↦ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖))    ⇒   ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶 Isom E , E (ω, 𝑆))
Theorem	isfin3ds 10444*	Property of a III-finite set (descending sequence version). (Contributed by Mario Carneiro, 16-May-2015.)
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑏 ∈ ω (𝑎‘suc 𝑏) ⊆ (𝑎‘𝑏) → ∩ ran 𝑎 ∈ ran 𝑎)}    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐹 ↔ ∀𝑓 ∈ (𝒫 𝐴 ↑m ω)(∀𝑥 ∈ ω (𝑓‘suc 𝑥) ⊆ (𝑓‘𝑥) → ∩ ran 𝑓 ∈ ran 𝑓)))
Theorem	ssfin3ds 10445*	A subset of a III-finite set is III-finite. (Contributed by Stefan O'Rear, 4-Nov-2014.)
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑏 ∈ ω (𝑎‘suc 𝑏) ⊆ (𝑎‘𝑏) → ∩ ran 𝑎 ∈ ran 𝑎)}    ⇒   ⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ 𝐹)
Theorem	fin23lem12 10446*	The beginning of the proof that every II-finite set (every chain of subsets has a maximal element) is III-finite (has no denumerable collection of subsets). This first section is dedicated to the construction of 𝑈 and its intersection. First, the value of 𝑈 at a successor. (Contributed by Stefan O'Rear, 1-Nov-2014.)
⊢ 𝑈 = seqω((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡‘𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡‘𝑖) ∩ 𝑢))), ∪ ran 𝑡)    ⇒   ⊢ (𝐴 ∈ ω → (𝑈‘suc 𝐴) = if(((𝑡‘𝐴) ∩ (𝑈‘𝐴)) = ∅, (𝑈‘𝐴), ((𝑡‘𝐴) ∩ (𝑈‘𝐴))))
Theorem	fin23lem13 10447*	Lemma for fin23 10504. Each step of 𝑈 is a decrease. (Contributed by Stefan O'Rear, 1-Nov-2014.)
⊢ 𝑈 = seqω((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡‘𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡‘𝑖) ∩ 𝑢))), ∪ ran 𝑡)    ⇒   ⊢ (𝐴 ∈ ω → (𝑈‘suc 𝐴) ⊆ (𝑈‘𝐴))
Theorem	fin23lem14 10448*	Lemma for fin23 10504. 𝑈 will never evolve to an empty set if it did not start with one. (Contributed by Stefan O'Rear, 1-Nov-2014.)
⊢ 𝑈 = seqω((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡‘𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡‘𝑖) ∩ 𝑢))), ∪ ran 𝑡)    ⇒   ⊢ ((𝐴 ∈ ω ∧ ∪ ran 𝑡 ≠ ∅) → (𝑈‘𝐴) ≠ ∅)
Theorem	fin23lem15 10449*	Lemma for fin23 10504. 𝑈 is a monotone function. (Contributed by Stefan O'Rear, 1-Nov-2014.)
⊢ 𝑈 = seqω((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡‘𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡‘𝑖) ∩ 𝑢))), ∪ ran 𝑡)    ⇒   ⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵 ⊆ 𝐴) → (𝑈‘𝐴) ⊆ (𝑈‘𝐵))
Theorem	fin23lem16 10450*	Lemma for fin23 10504. 𝑈 ranges over the original set; in particular ran 𝑈 is a set, although we do not assume here that 𝑈 is. (Contributed by Stefan O'Rear, 1-Nov-2014.)
⊢ 𝑈 = seqω((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡‘𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡‘𝑖) ∩ 𝑢))), ∪ ran 𝑡)    ⇒   ⊢ ∪ ran 𝑈 = ∪ ran 𝑡
Theorem	fin23lem19 10451*	Lemma for fin23 10504. The first set in 𝑈 to see an input set is either contained in it or disjoint from it. (Contributed by Stefan O'Rear, 1-Nov-2014.)
⊢ 𝑈 = seqω((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡‘𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡‘𝑖) ∩ 𝑢))), ∪ ran 𝑡)    ⇒   ⊢ (𝐴 ∈ ω → ((𝑈‘suc 𝐴) ⊆ (𝑡‘𝐴) ∨ ((𝑈‘suc 𝐴) ∩ (𝑡‘𝐴)) = ∅))
Theorem	fin23lem20 10452*	Lemma for fin23 10504. 𝑋 is either contained in or disjoint from all input sets. (Contributed by Stefan O'Rear, 1-Nov-2014.)
⊢ 𝑈 = seqω((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡‘𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡‘𝑖) ∩ 𝑢))), ∪ ran 𝑡)    ⇒   ⊢ (𝐴 ∈ ω → (∩ ran 𝑈 ⊆ (𝑡‘𝐴) ∨ (∩ ran 𝑈 ∩ (𝑡‘𝐴)) = ∅))
Theorem	fin23lem17 10453*	Lemma for fin23 10504. By ? Fin3DS ? , 𝑈 achieves its minimum (𝑋 in the synopsis above, but we will not be assigning a symbol here). TODO: Fix comment; math symbol Fin3DS does not exist. (Contributed by Stefan O'Rear, 4-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
⊢ 𝑈 = seqω((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡‘𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡‘𝑖) ∩ 𝑢))), ∪ ran 𝑡)    &   ⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)}    ⇒   ⊢ ((∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡:ω⟶1-1𝑉) → ∩ ran 𝑈 ∈ ran 𝑈)
Theorem	fin23lem21 10454*	Lemma for fin23 10504. 𝑋 is not empty. We only need here that 𝑡 has at least one set in its range besides ∅; the much stronger hypothesis here will serve as our induction hypothesis though. (Contributed by Stefan O'Rear, 1-Nov-2014.) (Revised by Mario Carneiro, 6-May-2015.)
⊢ 𝑈 = seqω((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡‘𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡‘𝑖) ∩ 𝑢))), ∪ ran 𝑡)    &   ⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)}    ⇒   ⊢ ((∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡:ω⟶1-1𝑉) → ∩ ran 𝑈 ≠ ∅)
Theorem	fin23lem28 10455*	Lemma for fin23 10504. The residual is also one-to-one. This preserves the induction invariant. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ 𝑈 = seqω((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡‘𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡‘𝑖) ∩ 𝑢))), ∪ ran 𝑡)    &   ⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)}    &   ⊢ 𝑃 = {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)}    &   ⊢ 𝑄 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ 𝑃 (𝑥 ∩ 𝑃) ≈ 𝑤))    &   ⊢ 𝑅 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ (ω ∖ 𝑃)(𝑥 ∩ (ω ∖ 𝑃)) ≈ 𝑤))    &   ⊢ 𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄))    ⇒   ⊢ (𝑡:ω⟶1-1V → 𝑍:ω⟶1-1V)
Theorem	fin23lem29 10456*	Lemma for fin23 10504. The residual is built from the same elements as the previous sequence. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ 𝑈 = seqω((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡‘𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡‘𝑖) ∩ 𝑢))), ∪ ran 𝑡)    &   ⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)}    &   ⊢ 𝑃 = {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)}    &   ⊢ 𝑄 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ 𝑃 (𝑥 ∩ 𝑃) ≈ 𝑤))    &   ⊢ 𝑅 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ (ω ∖ 𝑃)(𝑥 ∩ (ω ∖ 𝑃)) ≈ 𝑤))    &   ⊢ 𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄))    ⇒   ⊢ ∪ ran 𝑍 ⊆ ∪ ran 𝑡
Theorem	fin23lem30 10457*	Lemma for fin23 10504. The residual is disjoint from the common set. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ 𝑈 = seqω((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡‘𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡‘𝑖) ∩ 𝑢))), ∪ ran 𝑡)    &   ⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)}    &   ⊢ 𝑃 = {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)}    &   ⊢ 𝑄 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ 𝑃 (𝑥 ∩ 𝑃) ≈ 𝑤))    &   ⊢ 𝑅 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ (ω ∖ 𝑃)(𝑥 ∩ (ω ∖ 𝑃)) ≈ 𝑤))    &   ⊢ 𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄))    ⇒   ⊢ (Fun 𝑡 → (∪ ran 𝑍 ∩ ∩ ran 𝑈) = ∅)
Theorem	fin23lem31 10458*	Lemma for fin23 10504. The residual is has a strictly smaller range than the previous sequence. This will be iterated to build an unbounded chain. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ 𝑈 = seqω((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡‘𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡‘𝑖) ∩ 𝑢))), ∪ ran 𝑡)    &   ⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)}    &   ⊢ 𝑃 = {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)}    &   ⊢ 𝑄 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ 𝑃 (𝑥 ∩ 𝑃) ≈ 𝑤))    &   ⊢ 𝑅 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ (ω ∖ 𝑃)(𝑥 ∩ (ω ∖ 𝑃)) ≈ 𝑤))    &   ⊢ 𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄))    ⇒   ⊢ ((𝑡:ω⟶1-1𝑉 ∧ 𝐺 ∈ 𝐹 ∧ ∪ ran 𝑡 ⊆ 𝐺) → ∪ ran 𝑍 ⊊ ∪ ran 𝑡)
Theorem	fin23lem32 10459*	Lemma for fin23 10504. Wrap the previous construction into a function to hide the hypotheses. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ 𝑈 = seqω((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡‘𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡‘𝑖) ∩ 𝑢))), ∪ ran 𝑡)    &   ⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)}    &   ⊢ 𝑃 = {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)}    &   ⊢ 𝑄 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ 𝑃 (𝑥 ∩ 𝑃) ≈ 𝑤))    &   ⊢ 𝑅 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ (ω ∖ 𝑃)(𝑥 ∩ (ω ∖ 𝑃)) ≈ 𝑤))    &   ⊢ 𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄))    ⇒   ⊢ (𝐺 ∈ 𝐹 → ∃𝑓∀𝑏((𝑏:ω⟶1-1V ∧ ∪ ran 𝑏 ⊆ 𝐺) → ((𝑓‘𝑏):ω⟶1-1V ∧ ∪ ran (𝑓‘𝑏) ⊊ ∪ ran 𝑏)))
Theorem	fin23lem33 10460*	Lemma for fin23 10504. Discharge hypotheses. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)}    ⇒   ⊢ (𝐺 ∈ 𝐹 → ∃𝑓∀𝑏((𝑏:ω⟶1-1V ∧ ∪ ran 𝑏 ⊆ 𝐺) → ((𝑓‘𝑏):ω⟶1-1V ∧ ∪ ran (𝑓‘𝑏) ⊊ ∪ ran 𝑏)))
Theorem	fin23lem34 10461*	Lemma for fin23 10504. Establish induction invariants on 𝑌 which parameterizes our contradictory chain of subsets. In this section, ℎ is the hypothetically assumed family of subsets, 𝑔 is the ground set, and 𝑖 is the induction function constructed in the previous section. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)}    &   ⊢ (𝜑 → ℎ:ω⟶1-1V)    &   ⊢ (𝜑 → ∪ ran ℎ ⊆ 𝐺)    &   ⊢ (𝜑 → ∀𝑗((𝑗:ω⟶1-1V ∧ ∪ ran 𝑗 ⊆ 𝐺) → ((𝑖‘𝑗):ω⟶1-1V ∧ ∪ ran (𝑖‘𝑗) ⊊ ∪ ran 𝑗)))    &   ⊢ 𝑌 = (rec(𝑖, ℎ) ↾ ω)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ((𝑌‘𝐴):ω⟶1-1V ∧ ∪ ran (𝑌‘𝐴) ⊆ 𝐺))
Theorem	fin23lem35 10462*	Lemma for fin23 10504. Strict order property of 𝑌. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)}    &   ⊢ (𝜑 → ℎ:ω⟶1-1V)    &   ⊢ (𝜑 → ∪ ran ℎ ⊆ 𝐺)    &   ⊢ (𝜑 → ∀𝑗((𝑗:ω⟶1-1V ∧ ∪ ran 𝑗 ⊆ 𝐺) → ((𝑖‘𝑗):ω⟶1-1V ∧ ∪ ran (𝑖‘𝑗) ⊊ ∪ ran 𝑗)))    &   ⊢ 𝑌 = (rec(𝑖, ℎ) ↾ ω)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ∪ ran (𝑌‘suc 𝐴) ⊊ ∪ ran (𝑌‘𝐴))
Theorem	fin23lem36 10463*	Lemma for fin23 10504. Weak order property of 𝑌. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)}    &   ⊢ (𝜑 → ℎ:ω⟶1-1V)    &   ⊢ (𝜑 → ∪ ran ℎ ⊆ 𝐺)    &   ⊢ (𝜑 → ∀𝑗((𝑗:ω⟶1-1V ∧ ∪ ran 𝑗 ⊆ 𝐺) → ((𝑖‘𝑗):ω⟶1-1V ∧ ∪ ran (𝑖‘𝑗) ⊊ ∪ ran 𝑗)))    &   ⊢ 𝑌 = (rec(𝑖, ℎ) ↾ ω)    ⇒   ⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝐵 ⊆ 𝐴 ∧ 𝜑)) → ∪ ran (𝑌‘𝐴) ⊆ ∪ ran (𝑌‘𝐵))
Theorem	fin23lem38 10464*	Lemma for fin23 10504. The contradictory chain has no minimum. (Contributed by Stefan O'Rear, 2-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)}    &   ⊢ (𝜑 → ℎ:ω⟶1-1V)    &   ⊢ (𝜑 → ∪ ran ℎ ⊆ 𝐺)    &   ⊢ (𝜑 → ∀𝑗((𝑗:ω⟶1-1V ∧ ∪ ran 𝑗 ⊆ 𝐺) → ((𝑖‘𝑗):ω⟶1-1V ∧ ∪ ran (𝑖‘𝑗) ⊊ ∪ ran 𝑗)))    &   ⊢ 𝑌 = (rec(𝑖, ℎ) ↾ ω)    ⇒   ⊢ (𝜑 → ¬ ∩ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) ∈ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)))
Theorem	fin23lem39 10465*	Lemma for fin23 10504. Thus, we have that 𝑔 could not have been in 𝐹 after all. (Contributed by Stefan O'Rear, 4-Nov-2014.)
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)}    &   ⊢ (𝜑 → ℎ:ω⟶1-1V)    &   ⊢ (𝜑 → ∪ ran ℎ ⊆ 𝐺)    &   ⊢ (𝜑 → ∀𝑗((𝑗:ω⟶1-1V ∧ ∪ ran 𝑗 ⊆ 𝐺) → ((𝑖‘𝑗):ω⟶1-1V ∧ ∪ ran (𝑖‘𝑗) ⊊ ∪ ran 𝑗)))    &   ⊢ 𝑌 = (rec(𝑖, ℎ) ↾ ω)    ⇒   ⊢ (𝜑 → ¬ 𝐺 ∈ 𝐹)
Theorem	fin23lem40 10466*	Lemma for fin23 10504. FinII sets satisfy the descending chain condition. (Contributed by Stefan O'Rear, 3-Nov-2014.)
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)}    ⇒   ⊢ (𝐴 ∈ FinII → 𝐴 ∈ 𝐹)
Theorem	fin23lem41 10467*	Lemma for fin23 10504. A set which satisfies the descending sequence condition must be III-finite. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)}    ⇒   ⊢ (𝐴 ∈ 𝐹 → 𝐴 ∈ FinIII)
Theorem	isf32lem1 10468*	Lemma for isfin3-2 10482. Derive weak ordering property. (Contributed by Stefan O'Rear, 5-Nov-2014.)
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺)    &   ⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥))    &   ⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹)    ⇒   ⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝐵 ⊆ 𝐴 ∧ 𝜑)) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵))
Theorem	isf32lem2 10469*	Lemma for isfin3-2 10482. Non-minimum implies that there is always another decrease. (Contributed by Stefan O'Rear, 5-Nov-2014.)
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺)    &   ⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥))    &   ⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ∃𝑎 ∈ ω (𝐴 ∈ 𝑎 ∧ (𝐹‘suc 𝑎) ⊊ (𝐹‘𝑎)))
Theorem	isf32lem3 10470*	Lemma for isfin3-2 10482. Being a chain, difference sets are disjoint (one case). (Contributed by Stefan O'Rear, 5-Nov-2014.)
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺)    &   ⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥))    &   ⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹)    ⇒   ⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝐵 ∈ 𝐴 ∧ 𝜑)) → (((𝐹‘𝐴) ∖ (𝐹‘suc 𝐴)) ∩ ((𝐹‘𝐵) ∖ (𝐹‘suc 𝐵))) = ∅)
Theorem	isf32lem4 10471*	Lemma for isfin3-2 10482. Being a chain, difference sets are disjoint. (Contributed by Stefan O'Rear, 5-Nov-2014.)
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺)    &   ⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥))    &   ⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹)    ⇒   ⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (((𝐹‘𝐴) ∖ (𝐹‘suc 𝐴)) ∩ ((𝐹‘𝐵) ∖ (𝐹‘suc 𝐵))) = ∅)
Theorem	isf32lem5 10472*	Lemma for isfin3-2 10482. There are infinite decrease points. (Contributed by Stefan O'Rear, 5-Nov-2014.)
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺)    &   ⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥))    &   ⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹)    &   ⊢ 𝑆 = {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)}    ⇒   ⊢ (𝜑 → ¬ 𝑆 ∈ Fin)
Theorem	isf32lem6 10473*	Lemma for isfin3-2 10482. Each K value is nonempty. (Contributed by Stefan O'Rear, 5-Nov-2014.)
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺)    &   ⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥))    &   ⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹)    &   ⊢ 𝑆 = {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)}    &   ⊢ 𝐽 = (𝑢 ∈ ω ↦ (℩𝑣 ∈ 𝑆 (𝑣 ∩ 𝑆) ≈ 𝑢))    &   ⊢ 𝐾 = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ ω) → (𝐾‘𝐴) ≠ ∅)
Theorem	isf32lem7 10474*	Lemma for isfin3-2 10482. Different K values are disjoint. (Contributed by Stefan O'Rear, 5-Nov-2014.)
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺)    &   ⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥))    &   ⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹)    &   ⊢ 𝑆 = {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)}    &   ⊢ 𝐽 = (𝑢 ∈ ω ↦ (℩𝑣 ∈ 𝑆 (𝑣 ∩ 𝑆) ≈ 𝑢))    &   ⊢ 𝐾 = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)    ⇒   ⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → ((𝐾‘𝐴) ∩ (𝐾‘𝐵)) = ∅)
Theorem	isf32lem8 10475*	Lemma for isfin3-2 10482. K sets are subsets of the base. (Contributed by Stefan O'Rear, 6-Nov-2014.)
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺)    &   ⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥))    &   ⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹)    &   ⊢ 𝑆 = {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)}    &   ⊢ 𝐽 = (𝑢 ∈ ω ↦ (℩𝑣 ∈ 𝑆 (𝑣 ∩ 𝑆) ≈ 𝑢))    &   ⊢ 𝐾 = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ ω) → (𝐾‘𝐴) ⊆ 𝐺)
Theorem	isf32lem9 10476*	Lemma for isfin3-2 10482. Construction of the onto function. (Contributed by Stefan O'Rear, 5-Nov-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺)    &   ⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥))    &   ⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹)    &   ⊢ 𝑆 = {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)}    &   ⊢ 𝐽 = (𝑢 ∈ ω ↦ (℩𝑣 ∈ 𝑆 (𝑣 ∩ 𝑆) ≈ 𝑢))    &   ⊢ 𝐾 = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)    &   ⊢ 𝐿 = (𝑡 ∈ 𝐺 ↦ (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))))    ⇒   ⊢ (𝜑 → 𝐿:𝐺⟶ontoω)
Theorem	isf32lem10 10477*	Lemma for isfin3-2 . Write in terms of weak dominance. (Contributed by Stefan O'Rear, 6-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺)    &   ⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥))    &   ⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹)    &   ⊢ 𝑆 = {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)}    &   ⊢ 𝐽 = (𝑢 ∈ ω ↦ (℩𝑣 ∈ 𝑆 (𝑣 ∩ 𝑆) ≈ 𝑢))    &   ⊢ 𝐾 = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)    &   ⊢ 𝐿 = (𝑡 ∈ 𝐺 ↦ (℩𝑠(𝑠 ∈ ω ∧ 𝑡 ∈ (𝐾‘𝑠))))    ⇒   ⊢ (𝜑 → (𝐺 ∈ 𝑉 → ω ≼* 𝐺))
Theorem	isf32lem11 10478*	Lemma for isfin3-2 10482. Remove hypotheses from isf32lem10 10477. (Contributed by Stefan O'Rear, 17-May-2015.)
⊢ ((𝐺 ∈ 𝑉 ∧ (𝐹:ω⟶𝒫 𝐺 ∧ ∀𝑏 ∈ ω (𝐹‘suc 𝑏) ⊆ (𝐹‘𝑏) ∧ ¬ ∩ ran 𝐹 ∈ ran 𝐹)) → ω ≼* 𝐺)
Theorem	isf32lem12 10479*	Lemma for isfin3-2 10482. (Contributed by Stefan O'Rear, 6-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)}    ⇒   ⊢ (𝐺 ∈ 𝑉 → (¬ ω ≼* 𝐺 → 𝐺 ∈ 𝐹))
Theorem	isfin32i 10480	One half of isfin3-2 10482. (Contributed by Mario Carneiro, 3-Jun-2015.)
⊢ (𝐴 ∈ FinIII → ¬ ω ≼* 𝐴)
Theorem	isf33lem 10481*	Lemma for isfin3-3 10483. (Contributed by Stefan O'Rear, 17-May-2015.)
⊢ FinIII = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)}
Theorem	isfin3-2 10482	Weakly Dedekind-infinite sets are exactly those which can be mapped onto ω. (Contributed by Stefan O'Rear, 6-Nov-2014.) (Proof shortened by Mario Carneiro, 17-May-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinIII ↔ ¬ ω ≼* 𝐴))
Theorem	isfin3-3 10483*	Weakly Dedekind-infinite sets are exactly those with an ω-indexed descending chain of subsets. (Contributed by Stefan O'Rear, 7-Nov-2014.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinIII ↔ ∀𝑓 ∈ (𝒫 𝐴 ↑m ω)(∀𝑥 ∈ ω (𝑓‘suc 𝑥) ⊆ (𝑓‘𝑥) → ∩ ran 𝑓 ∈ ran 𝑓)))
Theorem	fin33i 10484*	Inference from isfin3-3 10483. (This is actually a bit stronger than isfin3-3 10483 because it does not assume 𝐹 is a set and does not use the Axiom of Infinity either.) (Contributed by Mario Carneiro, 17-May-2015.)
⊢ ((𝐴 ∈ FinIII ∧ 𝐹:ω⟶𝒫 𝐴 ∧ ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥)) → ∩ ran 𝐹 ∈ ran 𝐹)
Theorem	compsscnvlem 10485*	Lemma for compsscnv 10486. (Contributed by Mario Carneiro, 17-May-2015.)
⊢ ((𝑥 ∈ 𝒫 𝐴 ∧ 𝑦 = (𝐴 ∖ 𝑥)) → (𝑦 ∈ 𝒫 𝐴 ∧ 𝑥 = (𝐴 ∖ 𝑦)))
Theorem	compsscnv 10486*	Complementation on a power set lattice is an involution. (Contributed by Mario Carneiro, 17-May-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥))    ⇒   ⊢ ◡𝐹 = 𝐹
Theorem	isf34lem1 10487*	Lemma for isfin3-4 10497. (Contributed by Stefan O'Rear, 7-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴) → (𝐹‘𝑋) = (𝐴 ∖ 𝑋))
Theorem	isf34lem2 10488*	Lemma for isfin3-4 10497. (Contributed by Stefan O'Rear, 7-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥))    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐹:𝒫 𝐴⟶𝒫 𝐴)
Theorem	compssiso 10489*	Complementation is an antiautomorphism on power set lattices. (Contributed by Stefan O'Rear, 4-Nov-2014.) (Proof shortened by Mario Carneiro, 17-May-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥))    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐹 Isom [⊊] , ◡ [⊊] (𝒫 𝐴, 𝒫 𝐴))
Theorem	isf34lem3 10490*	Lemma for isfin3-4 10497. (Contributed by Stefan O'Rear, 7-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) → (𝐹 “ (𝐹 “ 𝑋)) = 𝑋)
Theorem	compss 10491*	Express image under of the complementation isomorphism. (Contributed by Stefan O'Rear, 5-Nov-2014.) (Proof shortened by Mario Carneiro, 17-May-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥))    ⇒   ⊢ (𝐹 “ 𝐺) = {𝑦 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑦) ∈ 𝐺}
Theorem	isf34lem4 10492*	Lemma for isfin3-4 10497. (Contributed by Stefan O'Rear, 7-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (𝐹‘∪ 𝑋) = ∩ (𝐹 “ 𝑋))
Theorem	isf34lem5 10493*	Lemma for isfin3-4 10497. (Contributed by Stefan O'Rear, 7-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (𝐹‘∩ 𝑋) = ∪ (𝐹 “ 𝑋))
Theorem	isf34lem7 10494*	Lemma for isfin3-4 10497. (Contributed by Stefan O'Rear, 7-Nov-2014.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥))    ⇒   ⊢ ((𝐴 ∈ FinIII ∧ 𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦)) → ∪ ran 𝐺 ∈ ran 𝐺)
Theorem	isf34lem6 10495*	Lemma for isfin3-4 10497. (Contributed by Stefan O'Rear, 7-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinIII ↔ ∀𝑓 ∈ (𝒫 𝐴 ↑m ω)(∀𝑦 ∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran 𝑓 ∈ ran 𝑓)))
Theorem	fin34i 10496*	Inference from isfin3-4 10497. (Contributed by Mario Carneiro, 17-May-2015.)
⊢ ((𝐴 ∈ FinIII ∧ 𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑥 ∈ ω (𝐺‘𝑥) ⊆ (𝐺‘suc 𝑥)) → ∪ ran 𝐺 ∈ ran 𝐺)
Theorem	isfin3-4 10497*	Weakly Dedekind-infinite sets are exactly those with an ω-indexed ascending chain of subsets. (Contributed by Stefan O'Rear, 7-Nov-2014.) (Proof shortened by Mario Carneiro, 17-May-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinIII ↔ ∀𝑓 ∈ (𝒫 𝐴 ↑m ω)(∀𝑥 ∈ ω (𝑓‘𝑥) ⊆ (𝑓‘suc 𝑥) → ∪ ran 𝑓 ∈ ran 𝑓)))
Theorem	fin11a 10498	Every I-finite set is Ia-finite. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 17-May-2015.)
⊢ (𝐴 ∈ Fin → 𝐴 ∈ FinIa)
Theorem	enfin1ai 10499	Ia-finiteness is a cardinal property. (Contributed by Mario Carneiro, 18-May-2015.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ FinIa → 𝐵 ∈ FinIa))
Theorem	isfin1-2 10500	A set is finite in the usual sense iff the power set of its power set is Dedekind finite. (Contributed by Stefan O'Rear, 3-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
⊢ (𝐴 ∈ Fin ↔ 𝒫 𝒫 𝐴 ∈ FinIV)