Home | Metamath
Proof Explorer Theorem List (p. 91 of 424) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | isfin3 9001 | Definition of a III-finite set. (Contributed by Stefan O'Rear, 16-May-2015.) |
⊢ (𝐴 ∈ FinIII ↔ 𝒫 𝐴 ∈ FinIV) | ||
Theorem | isfin4 9002* | Definition of a IV-finite set. (Contributed by Stefan O'Rear, 16-May-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinIV ↔ ¬ ∃𝑦(𝑦 ⊊ 𝐴 ∧ 𝑦 ≈ 𝐴))) | ||
Theorem | fin4i 9003 | Infer that a set is IV-infinite. (Contributed by Stefan O'Rear, 16-May-2015.) |
⊢ ((𝑋 ⊊ 𝐴 ∧ 𝑋 ≈ 𝐴) → ¬ 𝐴 ∈ FinIV) | ||
Theorem | isfin5 9004 | Definition of a V-finite set. (Contributed by Stefan O'Rear, 16-May-2015.) |
⊢ (𝐴 ∈ FinV ↔ (𝐴 = ∅ ∨ 𝐴 ≺ (𝐴 +𝑐 𝐴))) | ||
Theorem | isfin6 9005 | Definition of a VI-finite set. (Contributed by Stefan O'Rear, 16-May-2015.) |
⊢ (𝐴 ∈ FinVI ↔ (𝐴 ≺ 2𝑜 ∨ 𝐴 ≺ (𝐴 × 𝐴))) | ||
Theorem | isfin7 9006* | Definition of a VII-finite set. (Contributed by Stefan O'Rear, 16-May-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinVII ↔ ¬ ∃𝑦 ∈ (On ∖ ω)𝐴 ≈ 𝑦)) | ||
Theorem | sdom2en01 9007 | A set with less than two elements has 0 or 1. (Contributed by Stefan O'Rear, 30-Oct-2014.) |
⊢ (𝐴 ≺ 2𝑜 ↔ (𝐴 = ∅ ∨ 𝐴 ≈ 1𝑜)) | ||
Theorem | infpssrlem1 9008 | Lemma for infpssr 9013. (Contributed by Stefan O'Rear, 30-Oct-2014.) |
⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝐴) & ⊢ (𝜑 → 𝐶 ∈ (𝐴 ∖ 𝐵)) & ⊢ 𝐺 = (rec(◡𝐹, 𝐶) ↾ ω) ⇒ ⊢ (𝜑 → (𝐺‘∅) = 𝐶) | ||
Theorem | infpssrlem2 9009 | Lemma for infpssr 9013. (Contributed by Stefan O'Rear, 30-Oct-2014.) |
⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝐴) & ⊢ (𝜑 → 𝐶 ∈ (𝐴 ∖ 𝐵)) & ⊢ 𝐺 = (rec(◡𝐹, 𝐶) ↾ ω) ⇒ ⊢ (𝑀 ∈ ω → (𝐺‘suc 𝑀) = (◡𝐹‘(𝐺‘𝑀))) | ||
Theorem | infpssrlem3 9010 | Lemma for infpssr 9013. (Contributed by Stefan O'Rear, 30-Oct-2014.) |
⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝐴) & ⊢ (𝜑 → 𝐶 ∈ (𝐴 ∖ 𝐵)) & ⊢ 𝐺 = (rec(◡𝐹, 𝐶) ↾ ω) ⇒ ⊢ (𝜑 → 𝐺:ω⟶𝐴) | ||
Theorem | infpssrlem4 9011 | Lemma for infpssr 9013. (Contributed by Stefan O'Rear, 30-Oct-2014.) |
⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝐴) & ⊢ (𝜑 → 𝐶 ∈ (𝐴 ∖ 𝐵)) & ⊢ 𝐺 = (rec(◡𝐹, 𝐶) ↾ ω) ⇒ ⊢ ((𝜑 ∧ 𝑀 ∈ ω ∧ 𝑁 ∈ 𝑀) → (𝐺‘𝑀) ≠ (𝐺‘𝑁)) | ||
Theorem | infpssrlem5 9012 | Lemma for infpssr 9013. (Contributed by Stefan O'Rear, 30-Oct-2014.) |
⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝐴) & ⊢ (𝜑 → 𝐶 ∈ (𝐴 ∖ 𝐵)) & ⊢ 𝐺 = (rec(◡𝐹, 𝐶) ↾ ω) ⇒ ⊢ (𝜑 → (𝐴 ∈ 𝑉 → ω ≼ 𝐴)) | ||
Theorem | infpssr 9013 | 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 9014 | 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 9015 | Dedekind finite sets have Dedekind finite subsets. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 16-May-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ ((𝐴 ∈ FinIV ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ FinIV) | ||
Theorem | domfin4 9016 | A set dominated by a Dedekind finite set is Dedekind finite. (Contributed by Mario Carneiro, 16-May-2015.) |
⊢ ((𝐴 ∈ FinIV ∧ 𝐵 ≼ 𝐴) → 𝐵 ∈ FinIV) | ||
Theorem | ominf4 9017 | ω is Dedekind infinite. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Proof shortened by Mario Carneiro, 16-May-2015.) |
⊢ ¬ ω ∈ FinIV | ||
Theorem | infpssALT 9018* | Alternate proof of infpss 8922, shorter but requiring Replacement (ax-rep 4699). (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 9019 | 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 | isfin4-3 9020 | Alternate definition of IV-finite sets: they are strictly dominated by their successors. (Thus, the proper subset referred to in isfin4 9002 can be assumed to be only a singleton smaller than the original.) (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ (𝐴 ∈ FinIV ↔ 𝐴 ≺ (𝐴 +𝑐 1𝑜)) | ||
Theorem | fin23lem7 9021* | Lemma for isfin2-2 9024. 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 9022* | Lemma for isfin2-2 9024. (Contributed by Stefan O'Rear, 31-Oct-2014.) (Revised by Mario Carneiro, 16-May-2015.) |
⊢ (𝑧 = (𝐴 ∖ 𝑥) → (𝜓 ↔ 𝜒)) & ⊢ (𝑤 = (𝐴 ∖ 𝑣) → (𝜑 ↔ 𝜃)) & ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑣 ⊆ 𝐴) → (𝜒 ↔ 𝜃)) ⇒ ⊢ (𝐵 ⊆ 𝒫 𝐴 → (∃𝑥 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵}∀𝑤 ∈ {𝑐 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑐) ∈ 𝐵} ¬ 𝜑 → ∃𝑧 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ¬ 𝜓)) | ||
Theorem | fin2i2 9023 | A II-finite set contains minimal elements for every nonempty chain. (Contributed by Mario Carneiro, 16-May-2015.) |
⊢ (((𝐴 ∈ FinII ∧ 𝐵 ⊆ 𝒫 𝐴) ∧ (𝐵 ≠ ∅ ∧ [⊊] Or 𝐵)) → ∩ 𝐵 ∈ 𝐵) | ||
Theorem | isfin2-2 9024* | 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 9025 | 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 9026 | II-finiteness is a cardinal property. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ FinII → 𝐵 ∈ FinII)) | ||
Theorem | fin23lem24 9027 | Lemma for fin23 9094. 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 9028 | In a chain of finite sets, dominance and subset coincide. (Contributed by Stefan O'Rear, 8-Nov-2014.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴)) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | fin23lem25 9029 | Lemma for fin23 9094. In a chain of finite sets, equinumerosity is equivalent to equality. (Contributed by Stefan O'Rear, 1-Nov-2014.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴)) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | fin23lem26 9030* | Lemma for fin23lem22 9032. (Contributed by Stefan O'Rear, 1-Nov-2014.) |
⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑖 ∈ ω) → ∃𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖) | ||
Theorem | fin23lem23 9031* | Lemma for fin23lem22 9032. (Contributed by Stefan O'Rear, 1-Nov-2014.) |
⊢ (((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) ∧ 𝑖 ∈ ω) → ∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖) | ||
Theorem | fin23lem22 9032* | Lemma for fin23 9094 but could be used elsewhere if we find a good name for it. Explicit construction of a bijection (actually an isomorphism, see fin23lem27 9033) between an infinite subset of ω and ω itself. (Contributed by Stefan O'Rear, 1-Nov-2014.) |
⊢ 𝐶 = (𝑖 ∈ ω ↦ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖)) ⇒ ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶:ω–1-1-onto→𝑆) | ||
Theorem | fin23lem27 9033* | The mapping constructed in fin23lem22 9032 is in fact an isomorphism. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ 𝐶 = (𝑖 ∈ ω ↦ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖)) ⇒ ⊢ ((𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin) → 𝐶 Isom E , E (ω, 𝑆)) | ||
Theorem | isfin3ds 9034* | Property of a III-finite set (descending sequence version). (Contributed by Mario Carneiro, 16-May-2015.) |
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑𝑚 ω)(∀𝑏 ∈ ω (𝑎‘suc 𝑏) ⊆ (𝑎‘𝑏) → ∩ ran 𝑎 ∈ ran 𝑎)} ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐹 ↔ ∀𝑓 ∈ (𝒫 𝐴 ↑𝑚 ω)(∀𝑥 ∈ ω (𝑓‘suc 𝑥) ⊆ (𝑓‘𝑥) → ∩ ran 𝑓 ∈ ran 𝑓))) | ||
Theorem | ssfin3ds 9035* | A subset of a III-finite set is III-finite. (Contributed by Stefan O'Rear, 4-Nov-2014.) |
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑𝑚 ω)(∀𝑏 ∈ ω (𝑎‘suc 𝑏) ⊆ (𝑎‘𝑏) → ∩ ran 𝑎 ∈ ran 𝑎)} ⇒ ⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ 𝐹) | ||
Theorem | fin23lem12 9036* |
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 9037* | Lemma for fin23 9094. Each step of 𝑈 is a decrease. (Contributed by Stefan O'Rear, 1-Nov-2014.) |
⊢ 𝑈 = seq𝜔((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡‘𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡‘𝑖) ∩ 𝑢))), ∪ ran 𝑡) ⇒ ⊢ (𝐴 ∈ ω → (𝑈‘suc 𝐴) ⊆ (𝑈‘𝐴)) | ||
Theorem | fin23lem14 9038* | Lemma for fin23 9094. 𝑈 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 9039* | Lemma for fin23 9094. 𝑈 is a monotone function. (Contributed by Stefan O'Rear, 1-Nov-2014.) |
⊢ 𝑈 = seq𝜔((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡‘𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡‘𝑖) ∩ 𝑢))), ∪ ran 𝑡) ⇒ ⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵 ⊆ 𝐴) → (𝑈‘𝐴) ⊆ (𝑈‘𝐵)) | ||
Theorem | fin23lem16 9040* | Lemma for fin23 9094. 𝑈 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 9041* | Lemma for fin23 9094. 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 9042* | Lemma for fin23 9094. 𝑋 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 9043* | Lemma for fin23 9094. 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 𝑡) & ⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)} ⇒ ⊢ ((∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡:ω–1-1→𝑉) → ∩ ran 𝑈 ∈ ran 𝑈) | ||
Theorem | fin23lem21 9044* | Lemma for fin23 9094. 𝑋 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 𝑡) & ⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)} ⇒ ⊢ ((∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡:ω–1-1→𝑉) → ∩ ran 𝑈 ≠ ∅) | ||
Theorem | fin23lem28 9045* | Lemma for fin23 9094. The residual is also one-to-one. This preserves the induction invariant. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ 𝑈 = seq𝜔((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡‘𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡‘𝑖) ∩ 𝑢))), ∪ ran 𝑡) & ⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)} & ⊢ 𝑃 = {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)} & ⊢ 𝑄 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ 𝑃 (𝑥 ∩ 𝑃) ≈ 𝑤)) & ⊢ 𝑅 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ (ω ∖ 𝑃)(𝑥 ∩ (ω ∖ 𝑃)) ≈ 𝑤)) & ⊢ 𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄)) ⇒ ⊢ (𝑡:ω–1-1→V → 𝑍:ω–1-1→V) | ||
Theorem | fin23lem29 9046* | Lemma for fin23 9094. The residual is built from the same elements as the previous sequence. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ 𝑈 = seq𝜔((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡‘𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡‘𝑖) ∩ 𝑢))), ∪ ran 𝑡) & ⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)} & ⊢ 𝑃 = {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)} & ⊢ 𝑄 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ 𝑃 (𝑥 ∩ 𝑃) ≈ 𝑤)) & ⊢ 𝑅 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ (ω ∖ 𝑃)(𝑥 ∩ (ω ∖ 𝑃)) ≈ 𝑤)) & ⊢ 𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄)) ⇒ ⊢ ∪ ran 𝑍 ⊆ ∪ ran 𝑡 | ||
Theorem | fin23lem30 9047* | Lemma for fin23 9094. The residual is disjoint from the common set. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ 𝑈 = seq𝜔((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡‘𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡‘𝑖) ∩ 𝑢))), ∪ ran 𝑡) & ⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)} & ⊢ 𝑃 = {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)} & ⊢ 𝑄 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ 𝑃 (𝑥 ∩ 𝑃) ≈ 𝑤)) & ⊢ 𝑅 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ (ω ∖ 𝑃)(𝑥 ∩ (ω ∖ 𝑃)) ≈ 𝑤)) & ⊢ 𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄)) ⇒ ⊢ (Fun 𝑡 → (∪ ran 𝑍 ∩ ∩ ran 𝑈) = ∅) | ||
Theorem | fin23lem31 9048* | Lemma for fin23 9094. 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 𝑡) & ⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)} & ⊢ 𝑃 = {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)} & ⊢ 𝑄 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ 𝑃 (𝑥 ∩ 𝑃) ≈ 𝑤)) & ⊢ 𝑅 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ (ω ∖ 𝑃)(𝑥 ∩ (ω ∖ 𝑃)) ≈ 𝑤)) & ⊢ 𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄)) ⇒ ⊢ ((𝑡:ω–1-1→𝑉 ∧ 𝐺 ∈ 𝐹 ∧ ∪ ran 𝑡 ⊆ 𝐺) → ∪ ran 𝑍 ⊊ ∪ ran 𝑡) | ||
Theorem | fin23lem32 9049* | Lemma for fin23 9094. Wrap the previous construction into a function to hide the hypotheses. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ 𝑈 = seq𝜔((𝑖 ∈ ω, 𝑢 ∈ V ↦ if(((𝑡‘𝑖) ∩ 𝑢) = ∅, 𝑢, ((𝑡‘𝑖) ∩ 𝑢))), ∪ ran 𝑡) & ⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)} & ⊢ 𝑃 = {𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ (𝑡‘𝑣)} & ⊢ 𝑄 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ 𝑃 (𝑥 ∩ 𝑃) ≈ 𝑤)) & ⊢ 𝑅 = (𝑤 ∈ ω ↦ (℩𝑥 ∈ (ω ∖ 𝑃)(𝑥 ∩ (ω ∖ 𝑃)) ≈ 𝑤)) & ⊢ 𝑍 = if(𝑃 ∈ Fin, (𝑡 ∘ 𝑅), ((𝑧 ∈ 𝑃 ↦ ((𝑡‘𝑧) ∖ ∩ ran 𝑈)) ∘ 𝑄)) ⇒ ⊢ (𝐺 ∈ 𝐹 → ∃𝑓∀𝑏((𝑏:ω–1-1→V ∧ ∪ ran 𝑏 ⊆ 𝐺) → ((𝑓‘𝑏):ω–1-1→V ∧ ∪ ran (𝑓‘𝑏) ⊊ ∪ ran 𝑏))) | ||
Theorem | fin23lem33 9050* | Lemma for fin23 9094. Discharge hypotheses. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)} ⇒ ⊢ (𝐺 ∈ 𝐹 → ∃𝑓∀𝑏((𝑏:ω–1-1→V ∧ ∪ ran 𝑏 ⊆ 𝐺) → ((𝑓‘𝑏):ω–1-1→V ∧ ∪ ran (𝑓‘𝑏) ⊊ ∪ ran 𝑏))) | ||
Theorem | fin23lem34 9051* | Lemma for fin23 9094. 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.) |
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)} & ⊢ (𝜑 → ℎ:ω–1-1→V) & ⊢ (𝜑 → ∪ ran ℎ ⊆ 𝐺) & ⊢ (𝜑 → ∀𝑗((𝑗:ω–1-1→V ∧ ∪ ran 𝑗 ⊆ 𝐺) → ((𝑖‘𝑗):ω–1-1→V ∧ ∪ ran (𝑖‘𝑗) ⊊ ∪ ran 𝑗))) & ⊢ 𝑌 = (rec(𝑖, ℎ) ↾ ω) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ((𝑌‘𝐴):ω–1-1→V ∧ ∪ ran (𝑌‘𝐴) ⊆ 𝐺)) | ||
Theorem | fin23lem35 9052* | Lemma for fin23 9094. Strict order property of 𝑌. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)} & ⊢ (𝜑 → ℎ:ω–1-1→V) & ⊢ (𝜑 → ∪ ran ℎ ⊆ 𝐺) & ⊢ (𝜑 → ∀𝑗((𝑗:ω–1-1→V ∧ ∪ ran 𝑗 ⊆ 𝐺) → ((𝑖‘𝑗):ω–1-1→V ∧ ∪ ran (𝑖‘𝑗) ⊊ ∪ ran 𝑗))) & ⊢ 𝑌 = (rec(𝑖, ℎ) ↾ ω) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ∪ ran (𝑌‘suc 𝐴) ⊊ ∪ ran (𝑌‘𝐴)) | ||
Theorem | fin23lem36 9053* | Lemma for fin23 9094. Weak order property of 𝑌. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)} & ⊢ (𝜑 → ℎ:ω–1-1→V) & ⊢ (𝜑 → ∪ ran ℎ ⊆ 𝐺) & ⊢ (𝜑 → ∀𝑗((𝑗:ω–1-1→V ∧ ∪ ran 𝑗 ⊆ 𝐺) → ((𝑖‘𝑗):ω–1-1→V ∧ ∪ ran (𝑖‘𝑗) ⊊ ∪ ran 𝑗))) & ⊢ 𝑌 = (rec(𝑖, ℎ) ↾ ω) ⇒ ⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝐵 ⊆ 𝐴 ∧ 𝜑)) → ∪ ran (𝑌‘𝐴) ⊆ ∪ ran (𝑌‘𝐵)) | ||
Theorem | fin23lem38 9054* | Lemma for fin23 9094. The contradictory chain has no minimum. (Contributed by Stefan O'Rear, 2-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.) |
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)} & ⊢ (𝜑 → ℎ:ω–1-1→V) & ⊢ (𝜑 → ∪ ran ℎ ⊆ 𝐺) & ⊢ (𝜑 → ∀𝑗((𝑗:ω–1-1→V ∧ ∪ ran 𝑗 ⊆ 𝐺) → ((𝑖‘𝑗):ω–1-1→V ∧ ∪ ran (𝑖‘𝑗) ⊊ ∪ ran 𝑗))) & ⊢ 𝑌 = (rec(𝑖, ℎ) ↾ ω) ⇒ ⊢ (𝜑 → ¬ ∩ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏)) ∈ ran (𝑏 ∈ ω ↦ ∪ ran (𝑌‘𝑏))) | ||
Theorem | fin23lem39 9055* | Lemma for fin23 9094. Thus, we have that 𝑔 could not have been in 𝐹 after all. (Contributed by Stefan O'Rear, 4-Nov-2014.) |
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)} & ⊢ (𝜑 → ℎ:ω–1-1→V) & ⊢ (𝜑 → ∪ ran ℎ ⊆ 𝐺) & ⊢ (𝜑 → ∀𝑗((𝑗:ω–1-1→V ∧ ∪ ran 𝑗 ⊆ 𝐺) → ((𝑖‘𝑗):ω–1-1→V ∧ ∪ ran (𝑖‘𝑗) ⊊ ∪ ran 𝑗))) & ⊢ 𝑌 = (rec(𝑖, ℎ) ↾ ω) ⇒ ⊢ (𝜑 → ¬ 𝐺 ∈ 𝐹) | ||
Theorem | fin23lem40 9056* | Lemma for fin23 9094. FinII sets satisfy the descending chain condition. (Contributed by Stefan O'Rear, 3-Nov-2014.) |
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)} ⇒ ⊢ (𝐴 ∈ FinII → 𝐴 ∈ 𝐹) | ||
Theorem | fin23lem41 9057* | Lemma for fin23 9094. A set which satisfies the descending sequence condition must be III-finite. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)} ⇒ ⊢ (𝐴 ∈ 𝐹 → 𝐴 ∈ FinIII) | ||
Theorem | isf32lem1 9058* | Lemma for isfin3-2 9072. Derive weak ordering property. (Contributed by Stefan O'Rear, 5-Nov-2014.) |
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺) & ⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥)) & ⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹) ⇒ ⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝐵 ⊆ 𝐴 ∧ 𝜑)) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵)) | ||
Theorem | isf32lem2 9059* | Lemma for isfin3-2 9072. Non-minimum implies that there is always another decrease. (Contributed by Stefan O'Rear, 5-Nov-2014.) |
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺) & ⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥)) & ⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ∃𝑎 ∈ ω (𝐴 ∈ 𝑎 ∧ (𝐹‘suc 𝑎) ⊊ (𝐹‘𝑎))) | ||
Theorem | isf32lem3 9060* | Lemma for isfin3-2 9072. Being a chain, difference sets are disjoint (one case). (Contributed by Stefan O'Rear, 5-Nov-2014.) |
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺) & ⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥)) & ⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹) ⇒ ⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝐵 ∈ 𝐴 ∧ 𝜑)) → (((𝐹‘𝐴) ∖ (𝐹‘suc 𝐴)) ∩ ((𝐹‘𝐵) ∖ (𝐹‘suc 𝐵))) = ∅) | ||
Theorem | isf32lem4 9061* | Lemma for isfin3-2 9072. Being a chain, difference sets are disjoint. (Contributed by Stefan O'Rear, 5-Nov-2014.) |
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺) & ⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥)) & ⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹) ⇒ ⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (((𝐹‘𝐴) ∖ (𝐹‘suc 𝐴)) ∩ ((𝐹‘𝐵) ∖ (𝐹‘suc 𝐵))) = ∅) | ||
Theorem | isf32lem5 9062* | Lemma for isfin3-2 9072. There are infinite decrease points. (Contributed by Stefan O'Rear, 5-Nov-2014.) |
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺) & ⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥)) & ⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹) & ⊢ 𝑆 = {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)} ⇒ ⊢ (𝜑 → ¬ 𝑆 ∈ Fin) | ||
Theorem | isf32lem6 9063* | Lemma for isfin3-2 9072. Each K value is nonempty. (Contributed by Stefan O'Rear, 5-Nov-2014.) |
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺) & ⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥)) & ⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹) & ⊢ 𝑆 = {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)} & ⊢ 𝐽 = (𝑢 ∈ ω ↦ (℩𝑣 ∈ 𝑆 (𝑣 ∩ 𝑆) ≈ 𝑢)) & ⊢ 𝐾 = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ ω) → (𝐾‘𝐴) ≠ ∅) | ||
Theorem | isf32lem7 9064* | Lemma for isfin3-2 9072. Different K values are disjoint. (Contributed by Stefan O'Rear, 5-Nov-2014.) |
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺) & ⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥)) & ⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹) & ⊢ 𝑆 = {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)} & ⊢ 𝐽 = (𝑢 ∈ ω ↦ (℩𝑣 ∈ 𝑆 (𝑣 ∩ 𝑆) ≈ 𝑢)) & ⊢ 𝐾 = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽) ⇒ ⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → ((𝐾‘𝐴) ∩ (𝐾‘𝐵)) = ∅) | ||
Theorem | isf32lem8 9065* | Lemma for isfin3-2 9072. K sets are subsets of the base. (Contributed by Stefan O'Rear, 6-Nov-2014.) |
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺) & ⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥)) & ⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹) & ⊢ 𝑆 = {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)} & ⊢ 𝐽 = (𝑢 ∈ ω ↦ (℩𝑣 ∈ 𝑆 (𝑣 ∩ 𝑆) ≈ 𝑢)) & ⊢ 𝐾 = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ ω) → (𝐾‘𝐴) ⊆ 𝐺) | ||
Theorem | isf32lem9 9066* | Lemma for isfin3-2 9072. 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 9067* | 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 9068* | Lemma for isfin3-2 9072. Remove hypotheses from isf32lem10 9067. (Contributed by Stefan O'Rear, 17-May-2015.) |
⊢ ((𝐺 ∈ 𝑉 ∧ (𝐹:ω⟶𝒫 𝐺 ∧ ∀𝑏 ∈ ω (𝐹‘suc 𝑏) ⊆ (𝐹‘𝑏) ∧ ¬ ∩ ran 𝐹 ∈ ran 𝐹)) → ω ≼* 𝐺) | ||
Theorem | isf32lem12 9069* | Lemma for isfin3-2 9072. (Contributed by Stefan O'Rear, 6-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.) |
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)} ⇒ ⊢ (𝐺 ∈ 𝑉 → (¬ ω ≼* 𝐺 → 𝐺 ∈ 𝐹)) | ||
Theorem | isfin32i 9070 | One half of isfin3-2 9072. (Contributed by Mario Carneiro, 3-Jun-2015.) |
⊢ (𝐴 ∈ FinIII → ¬ ω ≼* 𝐴) | ||
Theorem | isf33lem 9071* | Lemma for isfin3-3 9073. (Contributed by Stefan O'Rear, 17-May-2015.) |
⊢ FinIII = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)} | ||
Theorem | isfin3-2 9072 | 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 9073* | Weakly Dedekind-infinite sets are exactly those with an ω-indexed descending chain of subsets. (Contributed by Stefan O'Rear, 7-Nov-2014.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinIII ↔ ∀𝑓 ∈ (𝒫 𝐴 ↑𝑚 ω)(∀𝑥 ∈ ω (𝑓‘suc 𝑥) ⊆ (𝑓‘𝑥) → ∩ ran 𝑓 ∈ ran 𝑓))) | ||
Theorem | fin33i 9074* | Inference from isfin3-3 9073. (This is actually a bit stronger than isfin3-3 9073 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 9075* | Lemma for compsscnv 9076. (Contributed by Mario Carneiro, 17-May-2015.) |
⊢ ((𝑥 ∈ 𝒫 𝐴 ∧ 𝑦 = (𝐴 ∖ 𝑥)) → (𝑦 ∈ 𝒫 𝐴 ∧ 𝑥 = (𝐴 ∖ 𝑦))) | ||
Theorem | compsscnv 9076* | Complementation on a power set lattice is an involution. (Contributed by Mario Carneiro, 17-May-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥)) ⇒ ⊢ ◡𝐹 = 𝐹 | ||
Theorem | isf34lem1 9077* | Lemma for isfin3-4 9087. (Contributed by Stefan O'Rear, 7-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴) → (𝐹‘𝑋) = (𝐴 ∖ 𝑋)) | ||
Theorem | isf34lem2 9078* | Lemma for isfin3-4 9087. (Contributed by Stefan O'Rear, 7-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥)) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐹:𝒫 𝐴⟶𝒫 𝐴) | ||
Theorem | compssiso 9079* | 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 9080* | Lemma for isfin3-4 9087. (Contributed by Stefan O'Rear, 7-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) → (𝐹 “ (𝐹 “ 𝑋)) = 𝑋) | ||
Theorem | compss 9081* | 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 9082* | Lemma for isfin3-4 9087. (Contributed by Stefan O'Rear, 7-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (𝐹‘∪ 𝑋) = ∩ (𝐹 “ 𝑋)) | ||
Theorem | isf34lem5 9083* | Lemma for isfin3-4 9087. (Contributed by Stefan O'Rear, 7-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (𝐹‘∩ 𝑋) = ∪ (𝐹 “ 𝑋)) | ||
Theorem | isf34lem7 9084* | Lemma for isfin3-4 9087. (Contributed by Stefan O'Rear, 7-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥)) ⇒ ⊢ ((𝐴 ∈ FinIII ∧ 𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦)) → ∪ ran 𝐺 ∈ ran 𝐺) | ||
Theorem | isf34lem6 9085* | Lemma for isfin3-4 9087. (Contributed by Stefan O'Rear, 7-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinIII ↔ ∀𝑓 ∈ (𝒫 𝐴 ↑𝑚 ω)(∀𝑦 ∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran 𝑓 ∈ ran 𝑓))) | ||
Theorem | fin34i 9086* | Inference from isfin3-4 9087. (Contributed by Mario Carneiro, 17-May-2015.) |
⊢ ((𝐴 ∈ FinIII ∧ 𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑥 ∈ ω (𝐺‘𝑥) ⊆ (𝐺‘suc 𝑥)) → ∪ ran 𝐺 ∈ ran 𝐺) | ||
Theorem | isfin3-4 9087* | 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 ↔ ∀𝑓 ∈ (𝒫 𝐴 ↑𝑚 ω)(∀𝑥 ∈ ω (𝑓‘𝑥) ⊆ (𝑓‘suc 𝑥) → ∪ ran 𝑓 ∈ ran 𝑓))) | ||
Theorem | fin11a 9088 | 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 9089 | Ia-finiteness is a cardinal property. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ FinIa → 𝐵 ∈ FinIa)) | ||
Theorem | isfin1-2 9090 | 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) | ||
Theorem | isfin1-3 9091 | A set is I-finite iff every system of subsets contains a maximal subset. Definition I of [Levy58] p. 2. (Contributed by Stefan O'Rear, 4-Nov-2014.) (Proof shortened by Mario Carneiro, 17-May-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Fin ↔ ◡ [⊊] Fr 𝒫 𝐴)) | ||
Theorem | isfin1-4 9092 | A set is I-finite iff every system of subsets contains a minimal subset. (Contributed by Stefan O'Rear, 4-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Fin ↔ [⊊] Fr 𝒫 𝐴)) | ||
Theorem | dffin1-5 9093 | Compact quantifier-free version of the standard definition df-fin 7845. (Contributed by Stefan O'Rear, 6-Jan-2015.) |
⊢ Fin = ( ≈ “ ω) | ||
Theorem | fin23 9094 |
Every II-finite set (every chain of subsets has a maximal element) is
III-finite (has no denumerable collection of subsets). The proof here
is the only one I could find, from
http://matwbn.icm.edu.pl/ksiazki/fm/fm6/fm619.pdf
p.94 (writeup by
Tarski, credited to Kuratowski). Translated into English and modern
notation, the proof proceeds as follows (variables renamed for
uniqueness):
Suppose for a contradiction that 𝐴 is a set which is II-finite but not III-finite. For any countable sequence of distinct subsets 𝑇 of 𝐴, we can form a decreasing sequence of nonempty subsets (𝑈‘𝑇) by taking finite intersections of initial segments of 𝑇 while skipping over any element of 𝑇 which would cause the intersection to be empty. By II-finiteness (as fin2i2 9023) this sequence contains its intersection, call it 𝑌; since by induction every subset in the sequence 𝑈 is nonempty, the intersection must be nonempty. Suppose that an element 𝑋 of 𝑇 has nonempty intersection with 𝑌. Thus, said element has a nonempty intersection with the corresponding element of 𝑈, therefore it was used in the construction of 𝑈 and all further elements of 𝑈 are subsets of 𝑋, thus 𝑋 contains the 𝑌. That is, all elements of 𝑋 either contain 𝑌 or are disjoint from it. Since there are only two cases, there must exist an infinite subset of 𝑇 which uniformly either contain 𝑌 or are disjoint from it. In the former case we can create an infinite set by subtracting 𝑌 from each element. In either case, call the result 𝑍; this is an infinite set of subsets of 𝐴, each of which is disjoint from 𝑌 and contained in the union of 𝑇; the union of 𝑍 is strictly contained in the union of 𝑇, because only the latter is a superset of the nonempty set 𝑌. The preceding four steps may be iterated a countable number of times starting from the assumed denumerable set of subsets to produce a denumerable sequence 𝐵 of the 𝑇 sets from each stage. Great caution is required to avoid ax-dc 9151 here; in particular an effective version of the pigeonhole principle (for aleph-null pigeons and 2 holes) is required. Since a denumerable set of subsets is assumed to exist, we can conclude ω ∈ V without the axiom. This 𝐵 sequence is strictly decreasing, thus it has no minimum, contradicting the first assumption. (Contributed by Stefan O'Rear, 2-Nov-2014.) (Proof shortened by Mario Carneiro, 17-May-2015.) |
⊢ (𝐴 ∈ FinII → 𝐴 ∈ FinIII) | ||
Theorem | fin34 9095 | Every III-finite set is IV-finite. (Contributed by Stefan O'Rear, 30-Oct-2014.) |
⊢ (𝐴 ∈ FinIII → 𝐴 ∈ FinIV) | ||
Theorem | isfin5-2 9096 | Alternate definition of V-finite which emphasizes the idempotent behavior of V-infinite sets. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 17-May-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinV ↔ ¬ (𝐴 ≠ ∅ ∧ 𝐴 ≈ (𝐴 +𝑐 𝐴)))) | ||
Theorem | fin45 9097 | Every IV-finite set is V-finite: if we can pack two copies of the set into itself, we can certainly leave space. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Proof shortened by Mario Carneiro, 18-May-2015.) |
⊢ (𝐴 ∈ FinIV → 𝐴 ∈ FinV) | ||
Theorem | fin56 9098 | Every V-finite set is VI-finite because multiplication dominates addition for cardinals. (Contributed by Stefan O'Rear, 29-Oct-2014.) (Revised by Mario Carneiro, 17-May-2015.) |
⊢ (𝐴 ∈ FinV → 𝐴 ∈ FinVI) | ||
Theorem | fin17 9099 | Every I-finite set is VII-finite. (Contributed by Mario Carneiro, 17-May-2015.) |
⊢ (𝐴 ∈ Fin → 𝐴 ∈ FinVII) | ||
Theorem | fin67 9100 | Every VI-finite set is VII-finite. (Contributed by Stefan O'Rear, 29-Oct-2014.) (Revised by Mario Carneiro, 17-May-2015.) |
⊢ (𝐴 ∈ FinVI → 𝐴 ∈ FinVII) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |