![]() |
Metamath
Proof Explorer Theorem List (p. 96 of 437) | < 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: | ![]() (1-28347) |
![]() (28348-29872) |
![]() (29873-43657) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fin23lem32 9501* | Lemma for fin23 9546. 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 9502* | Lemma for fin23 9546. Discharge hypotheses. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)} ⇒ ⊢ (𝐺 ∈ 𝐹 → ∃𝑓∀𝑏((𝑏:ω–1-1→V ∧ ∪ ran 𝑏 ⊆ 𝐺) → ((𝑓‘𝑏):ω–1-1→V ∧ ∪ ran (𝑓‘𝑏) ⊊ ∪ ran 𝑏))) | ||
Theorem | fin23lem34 9503* | Lemma for fin23 9546. 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 9504* | Lemma for fin23 9546. 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 9505* | Lemma for fin23 9546. 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 9506* | Lemma for fin23 9546. 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 9507* | Lemma for fin23 9546. 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 9508* | Lemma for fin23 9546. FinII sets satisfy the descending chain condition. (Contributed by Stefan O'Rear, 3-Nov-2014.) |
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)} ⇒ ⊢ (𝐴 ∈ FinII → 𝐴 ∈ 𝐹) | ||
Theorem | fin23lem41 9509* | Lemma for fin23 9546. 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 9510* | Lemma for isfin3-2 9524. Derive weak ordering property. (Contributed by Stefan O'Rear, 5-Nov-2014.) |
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺) & ⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥)) & ⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹) ⇒ ⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝐵 ⊆ 𝐴 ∧ 𝜑)) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵)) | ||
Theorem | isf32lem2 9511* | Lemma for isfin3-2 9524. Non-minimum implies that there is always another decrease. (Contributed by Stefan O'Rear, 5-Nov-2014.) |
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺) & ⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥)) & ⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ∃𝑎 ∈ ω (𝐴 ∈ 𝑎 ∧ (𝐹‘suc 𝑎) ⊊ (𝐹‘𝑎))) | ||
Theorem | isf32lem3 9512* | Lemma for isfin3-2 9524. Being a chain, difference sets are disjoint (one case). (Contributed by Stefan O'Rear, 5-Nov-2014.) |
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺) & ⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥)) & ⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹) ⇒ ⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝐵 ∈ 𝐴 ∧ 𝜑)) → (((𝐹‘𝐴) ∖ (𝐹‘suc 𝐴)) ∩ ((𝐹‘𝐵) ∖ (𝐹‘suc 𝐵))) = ∅) | ||
Theorem | isf32lem4 9513* | Lemma for isfin3-2 9524. Being a chain, difference sets are disjoint. (Contributed by Stefan O'Rear, 5-Nov-2014.) |
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺) & ⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥)) & ⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹) ⇒ ⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (((𝐹‘𝐴) ∖ (𝐹‘suc 𝐴)) ∩ ((𝐹‘𝐵) ∖ (𝐹‘suc 𝐵))) = ∅) | ||
Theorem | isf32lem5 9514* | Lemma for isfin3-2 9524. There are infinite decrease points. (Contributed by Stefan O'Rear, 5-Nov-2014.) |
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺) & ⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥)) & ⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹) & ⊢ 𝑆 = {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)} ⇒ ⊢ (𝜑 → ¬ 𝑆 ∈ Fin) | ||
Theorem | isf32lem6 9515* | Lemma for isfin3-2 9524. Each K value is nonempty. (Contributed by Stefan O'Rear, 5-Nov-2014.) |
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺) & ⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥)) & ⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹) & ⊢ 𝑆 = {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)} & ⊢ 𝐽 = (𝑢 ∈ ω ↦ (℩𝑣 ∈ 𝑆 (𝑣 ∩ 𝑆) ≈ 𝑢)) & ⊢ 𝐾 = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ ω) → (𝐾‘𝐴) ≠ ∅) | ||
Theorem | isf32lem7 9516* | Lemma for isfin3-2 9524. Different K values are disjoint. (Contributed by Stefan O'Rear, 5-Nov-2014.) |
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺) & ⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥)) & ⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹) & ⊢ 𝑆 = {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)} & ⊢ 𝐽 = (𝑢 ∈ ω ↦ (℩𝑣 ∈ 𝑆 (𝑣 ∩ 𝑆) ≈ 𝑢)) & ⊢ 𝐾 = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽) ⇒ ⊢ (((𝜑 ∧ 𝐴 ≠ 𝐵) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → ((𝐾‘𝐴) ∩ (𝐾‘𝐵)) = ∅) | ||
Theorem | isf32lem8 9517* | Lemma for isfin3-2 9524. K sets are subsets of the base. (Contributed by Stefan O'Rear, 6-Nov-2014.) |
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺) & ⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥)) & ⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹) & ⊢ 𝑆 = {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)} & ⊢ 𝐽 = (𝑢 ∈ ω ↦ (℩𝑣 ∈ 𝑆 (𝑣 ∩ 𝑆) ≈ 𝑢)) & ⊢ 𝐾 = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ ω) → (𝐾‘𝐴) ⊆ 𝐺) | ||
Theorem | isf32lem9 9518* | Lemma for isfin3-2 9524. 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 9519* | 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 9520* | Lemma for isfin3-2 9524. Remove hypotheses from isf32lem10 9519. (Contributed by Stefan O'Rear, 17-May-2015.) |
⊢ ((𝐺 ∈ 𝑉 ∧ (𝐹:ω⟶𝒫 𝐺 ∧ ∀𝑏 ∈ ω (𝐹‘suc 𝑏) ⊆ (𝐹‘𝑏) ∧ ¬ ∩ ran 𝐹 ∈ ran 𝐹)) → ω ≼* 𝐺) | ||
Theorem | isf32lem12 9521* | Lemma for isfin3-2 9524. (Contributed by Stefan O'Rear, 6-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.) |
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)} ⇒ ⊢ (𝐺 ∈ 𝑉 → (¬ ω ≼* 𝐺 → 𝐺 ∈ 𝐹)) | ||
Theorem | isfin32i 9522 | One half of isfin3-2 9524. (Contributed by Mario Carneiro, 3-Jun-2015.) |
⊢ (𝐴 ∈ FinIII → ¬ ω ≼* 𝐴) | ||
Theorem | isf33lem 9523* | Lemma for isfin3-3 9525. (Contributed by Stefan O'Rear, 17-May-2015.) |
⊢ FinIII = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑𝑚 ω)(∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) → ∩ ran 𝑎 ∈ ran 𝑎)} | ||
Theorem | isfin3-2 9524 | 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 9525* | 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 9526* | Inference from isfin3-3 9525. (This is actually a bit stronger than isfin3-3 9525 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 9527* | Lemma for compsscnv 9528. (Contributed by Mario Carneiro, 17-May-2015.) |
⊢ ((𝑥 ∈ 𝒫 𝐴 ∧ 𝑦 = (𝐴 ∖ 𝑥)) → (𝑦 ∈ 𝒫 𝐴 ∧ 𝑥 = (𝐴 ∖ 𝑦))) | ||
Theorem | compsscnv 9528* | Complementation on a power set lattice is an involution. (Contributed by Mario Carneiro, 17-May-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥)) ⇒ ⊢ ◡𝐹 = 𝐹 | ||
Theorem | isf34lem1 9529* | Lemma for isfin3-4 9539. (Contributed by Stefan O'Rear, 7-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴) → (𝐹‘𝑋) = (𝐴 ∖ 𝑋)) | ||
Theorem | isf34lem2 9530* | Lemma for isfin3-4 9539. (Contributed by Stefan O'Rear, 7-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥)) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐹:𝒫 𝐴⟶𝒫 𝐴) | ||
Theorem | compssiso 9531* | 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 9532* | Lemma for isfin3-4 9539. (Contributed by Stefan O'Rear, 7-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) → (𝐹 “ (𝐹 “ 𝑋)) = 𝑋) | ||
Theorem | compss 9533* | 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 9534* | Lemma for isfin3-4 9539. (Contributed by Stefan O'Rear, 7-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (𝐹‘∪ 𝑋) = ∩ (𝐹 “ 𝑋)) | ||
Theorem | isf34lem5 9535* | Lemma for isfin3-4 9539. (Contributed by Stefan O'Rear, 7-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (𝐹‘∩ 𝑋) = ∪ (𝐹 “ 𝑋)) | ||
Theorem | isf34lem7 9536* | Lemma for isfin3-4 9539. (Contributed by Stefan O'Rear, 7-Nov-2014.) |
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥)) ⇒ ⊢ ((𝐴 ∈ FinIII ∧ 𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦)) → ∪ ran 𝐺 ∈ ran 𝐺) | ||
Theorem | isf34lem6 9537* | Lemma for isfin3-4 9539. (Contributed by Stefan O'Rear, 7-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinIII ↔ ∀𝑓 ∈ (𝒫 𝐴 ↑𝑚 ω)(∀𝑦 ∈ ω (𝑓‘𝑦) ⊆ (𝑓‘suc 𝑦) → ∪ ran 𝑓 ∈ ran 𝑓))) | ||
Theorem | fin34i 9538* | Inference from isfin3-4 9539. (Contributed by Mario Carneiro, 17-May-2015.) |
⊢ ((𝐴 ∈ FinIII ∧ 𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑥 ∈ ω (𝐺‘𝑥) ⊆ (𝐺‘suc 𝑥)) → ∪ ran 𝐺 ∈ ran 𝐺) | ||
Theorem | isfin3-4 9539* | 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 9540 | 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 9541 | Ia-finiteness is a cardinal property. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ FinIa → 𝐵 ∈ FinIa)) | ||
Theorem | isfin1-2 9542 | 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 9543 | 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 9544 | 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 9545 | Compact quantifier-free version of the standard definition df-fin 8245. (Contributed by Stefan O'Rear, 6-Jan-2015.) |
⊢ Fin = ( ≈ “ ω) | ||
Theorem | fin23 9546 |
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 9475) 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 9603 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 9547 | Every III-finite set is IV-finite. (Contributed by Stefan O'Rear, 30-Oct-2014.) |
⊢ (𝐴 ∈ FinIII → 𝐴 ∈ FinIV) | ||
Theorem | isfin5-2 9548 | 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 9549 | 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 9550 | 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 9551 | Every I-finite set is VII-finite. (Contributed by Mario Carneiro, 17-May-2015.) |
⊢ (𝐴 ∈ Fin → 𝐴 ∈ FinVII) | ||
Theorem | fin67 9552 | Every VI-finite set is VII-finite. (Contributed by Stefan O'Rear, 29-Oct-2014.) (Revised by Mario Carneiro, 17-May-2015.) |
⊢ (𝐴 ∈ FinVI → 𝐴 ∈ FinVII) | ||
Theorem | isfin7-2 9553 | A set is VII-finite iff it is non-well-orderable or finite. (Contributed by Mario Carneiro, 17-May-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinVII ↔ (𝐴 ∈ dom card → 𝐴 ∈ Fin))) | ||
Theorem | fin71num 9554 | A well-orderable set is VII-finite iff it is I-finite. Thus, even without choice, on the class of well-orderable sets all eight definitions of finite set coincide. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ (𝐴 ∈ dom card → (𝐴 ∈ FinVII ↔ 𝐴 ∈ Fin)) | ||
Theorem | dffin7-2 9555 | Class form of isfin7-2 9553. (Contributed by Mario Carneiro, 17-May-2015.) |
⊢ FinVII = (Fin ∪ (V ∖ dom card)) | ||
Theorem | dfacfin7 9556 | Axiom of Choice equivalent: the VII-finite sets are the same as I-finite sets. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ (CHOICE ↔ FinVII = Fin) | ||
Theorem | fin1a2lem1 9557 | Lemma for fin1a2 9572. (Contributed by Stefan O'Rear, 7-Nov-2014.) |
⊢ 𝑆 = (𝑥 ∈ On ↦ suc 𝑥) ⇒ ⊢ (𝐴 ∈ On → (𝑆‘𝐴) = suc 𝐴) | ||
Theorem | fin1a2lem2 9558 | Lemma for fin1a2 9572. (Contributed by Stefan O'Rear, 7-Nov-2014.) |
⊢ 𝑆 = (𝑥 ∈ On ↦ suc 𝑥) ⇒ ⊢ 𝑆:On–1-1→On | ||
Theorem | fin1a2lem3 9559 | Lemma for fin1a2 9572. (Contributed by Stefan O'Rear, 7-Nov-2014.) |
⊢ 𝐸 = (𝑥 ∈ ω ↦ (2o ·o 𝑥)) ⇒ ⊢ (𝐴 ∈ ω → (𝐸‘𝐴) = (2o ·o 𝐴)) | ||
Theorem | fin1a2lem4 9560 | Lemma for fin1a2 9572. (Contributed by Stefan O'Rear, 7-Nov-2014.) |
⊢ 𝐸 = (𝑥 ∈ ω ↦ (2o ·o 𝑥)) ⇒ ⊢ 𝐸:ω–1-1→ω | ||
Theorem | fin1a2lem5 9561 | Lemma for fin1a2 9572. (Contributed by Stefan O'Rear, 7-Nov-2014.) |
⊢ 𝐸 = (𝑥 ∈ ω ↦ (2o ·o 𝑥)) ⇒ ⊢ (𝐴 ∈ ω → (𝐴 ∈ ran 𝐸 ↔ ¬ suc 𝐴 ∈ ran 𝐸)) | ||
Theorem | fin1a2lem6 9562 | Lemma for fin1a2 9572. Establish that ω can be broken into two equipollent pieces. (Contributed by Stefan O'Rear, 7-Nov-2014.) |
⊢ 𝐸 = (𝑥 ∈ ω ↦ (2o ·o 𝑥)) & ⊢ 𝑆 = (𝑥 ∈ On ↦ suc 𝑥) ⇒ ⊢ (𝑆 ↾ ran 𝐸):ran 𝐸–1-1-onto→(ω ∖ ran 𝐸) | ||
Theorem | fin1a2lem7 9563* | Lemma for fin1a2 9572. Split a III-infinite set in two pieces. (Contributed by Stefan O'Rear, 7-Nov-2014.) |
⊢ 𝐸 = (𝑥 ∈ ω ↦ (2o ·o 𝑥)) & ⊢ 𝑆 = (𝑥 ∈ On ↦ suc 𝑥) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴 ∖ 𝑦) ∈ FinIII)) → 𝐴 ∈ FinIII) | ||
Theorem | fin1a2lem8 9564* | Lemma for fin1a2 9572. Split a III-infinite set in two pieces. (Contributed by Stefan O'Rear, 7-Nov-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝒫 𝐴(𝑥 ∈ FinIII ∨ (𝐴 ∖ 𝑥) ∈ FinIII)) → 𝐴 ∈ FinIII) | ||
Theorem | fin1a2lem9 9565* | Lemma for fin1a2 9572. In a chain of finite sets, initial segments are finite. (Contributed by Stefan O'Rear, 8-Nov-2014.) |
⊢ (( [⊊] Or 𝑋 ∧ 𝑋 ⊆ Fin ∧ 𝐴 ∈ ω) → {𝑏 ∈ 𝑋 ∣ 𝑏 ≼ 𝐴} ∈ Fin) | ||
Theorem | fin1a2lem10 9566 | Lemma for fin1a2 9572. A nonempty finite union of members of a chain is a member of the chain. (Contributed by Stefan O'Rear, 8-Nov-2014.) |
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ∧ [⊊] Or 𝐴) → ∪ 𝐴 ∈ 𝐴) | ||
Theorem | fin1a2lem11 9567* | Lemma for fin1a2 9572. (Contributed by Stefan O'Rear, 8-Nov-2014.) |
⊢ (( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin) → ran (𝑏 ∈ ω ↦ ∪ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏}) = (𝐴 ∪ {∅})) | ||
Theorem | fin1a2lem12 9568 | Lemma for fin1a2 9572. (Contributed by Stefan O'Rear, 8-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.) |
⊢ (((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) → ¬ 𝐵 ∈ FinIII) | ||
Theorem | fin1a2lem13 9569 | Lemma for fin1a2 9572. (Contributed by Stefan O'Rear, 8-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.) |
⊢ (((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵 ∖ 𝐶) ∈ FinII) | ||
Theorem | fin12 9570 | Weak theorem which skips Ia but has a trivial proof, needed to prove fin1a2 9572. (Contributed by Stefan O'Rear, 8-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.) |
⊢ (𝐴 ∈ Fin → 𝐴 ∈ FinII) | ||
Theorem | fin1a2s 9571* | An II-infinite set can have an I-infinite part broken off and remain II-infinite. (Contributed by Stefan O'Rear, 8-Nov-2014.) (Proof shortened by Mario Carneiro, 17-May-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝒫 𝐴(𝑥 ∈ Fin ∨ (𝐴 ∖ 𝑥) ∈ FinII)) → 𝐴 ∈ FinII) | ||
Theorem | fin1a2 9572 | Every Ia-finite set is II-finite. Theorem 1 of [Levy58], p. 3. (Contributed by Stefan O'Rear, 8-Nov-2014.) (Proof shortened by Mario Carneiro, 17-May-2015.) |
⊢ (𝐴 ∈ FinIa → 𝐴 ∈ FinII) | ||
Theorem | itunifval 9573* | Function value of iterated unions. EDITORIAL: The iterated unions and order types of ordered sets are split out here because they could conceivably be independently useful. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦), 𝑥) ↾ ω)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝑈‘𝐴) = (rec((𝑦 ∈ V ↦ ∪ 𝑦), 𝐴) ↾ ω)) | ||
Theorem | itunifn 9574* | Functionality of the iterated union. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦), 𝑥) ↾ ω)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝑈‘𝐴) Fn ω) | ||
Theorem | ituni0 9575* | A zero-fold iterated union. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦), 𝑥) ↾ ω)) ⇒ ⊢ (𝐴 ∈ 𝑉 → ((𝑈‘𝐴)‘∅) = 𝐴) | ||
Theorem | itunisuc 9576* | Successor iterated union. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦), 𝑥) ↾ ω)) ⇒ ⊢ ((𝑈‘𝐴)‘suc 𝐵) = ∪ ((𝑈‘𝐴)‘𝐵) | ||
Theorem | itunitc1 9577* | Each union iterate is a member of the transitive closure. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦), 𝑥) ↾ ω)) ⇒ ⊢ ((𝑈‘𝐴)‘𝐵) ⊆ (TC‘𝐴) | ||
Theorem | itunitc 9578* | The union of all union iterates creates the transitive closure; compare trcl 8901. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦), 𝑥) ↾ ω)) ⇒ ⊢ (TC‘𝐴) = ∪ ran (𝑈‘𝐴) | ||
Theorem | ituniiun 9579* | Unwrap an iterated union from the "other end". (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦), 𝑥) ↾ ω)) ⇒ ⊢ (𝐴 ∈ 𝑉 → ((𝑈‘𝐴)‘suc 𝐵) = ∪ 𝑎 ∈ 𝐴 ((𝑈‘𝑎)‘𝐵)) | ||
Theorem | hsmexlem7 9580* | Lemma for hsmex 9589. Properties of the recurrent sequence of ordinals. (Contributed by Stefan O'Rear, 14-Feb-2015.) |
⊢ 𝐻 = (rec((𝑧 ∈ V ↦ (har‘𝒫 (𝑋 × 𝑧))), (har‘𝒫 𝑋)) ↾ ω) ⇒ ⊢ (𝐻‘∅) = (har‘𝒫 𝑋) | ||
Theorem | hsmexlem8 9581* | Lemma for hsmex 9589. Properties of the recurrent sequence of ordinals. (Contributed by Stefan O'Rear, 14-Feb-2015.) |
⊢ 𝐻 = (rec((𝑧 ∈ V ↦ (har‘𝒫 (𝑋 × 𝑧))), (har‘𝒫 𝑋)) ↾ ω) ⇒ ⊢ (𝑎 ∈ ω → (𝐻‘suc 𝑎) = (har‘𝒫 (𝑋 × (𝐻‘𝑎)))) | ||
Theorem | hsmexlem9 9582* | Lemma for hsmex 9589. Properties of the recurrent sequence of ordinals. (Contributed by Stefan O'Rear, 14-Feb-2015.) |
⊢ 𝐻 = (rec((𝑧 ∈ V ↦ (har‘𝒫 (𝑋 × 𝑧))), (har‘𝒫 𝑋)) ↾ ω) ⇒ ⊢ (𝑎 ∈ ω → (𝐻‘𝑎) ∈ On) | ||
Theorem | hsmexlem1 9583 | Lemma for hsmex 9589. Bound the order type of a limited-cardinality set of ordinals. (Contributed by Stefan O'Rear, 14-Feb-2015.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ 𝑂 = OrdIso( E , 𝐴) ⇒ ⊢ ((𝐴 ⊆ On ∧ 𝐴 ≼* 𝐵) → dom 𝑂 ∈ (har‘𝒫 𝐵)) | ||
Theorem | hsmexlem2 9584* | Lemma for hsmex 9589. Bound the order type of a union of sets of ordinals, each of limited order type. Vaguely reminiscent of unictb 9732 but use of order types allows to canonically choose the sub-bijections, removing the choice requirement. (Contributed by Stefan O'Rear, 14-Feb-2015.) (Revised by Mario Carneiro, 26-Jun-2015.) (Revised by AV, 18-Sep-2021.) |
⊢ 𝐹 = OrdIso( E , 𝐵) & ⊢ 𝐺 = OrdIso( E , ∪ 𝑎 ∈ 𝐴 𝐵) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ On ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → dom 𝐺 ∈ (har‘𝒫 (𝐴 × 𝐶))) | ||
Theorem | hsmexlem3 9585* | Lemma for hsmex 9589. Clear 𝐼 hypothesis and extend previous result by dominance. Note that this could be substantially strengthened, e.g., using the weak Hartogs function, but all we need here is that there be *some* dominating ordinal. (Contributed by Stefan O'Rear, 14-Feb-2015.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ 𝐹 = OrdIso( E , 𝐵) & ⊢ 𝐺 = OrdIso( E , ∪ 𝑎 ∈ 𝐴 𝐵) ⇒ ⊢ (((𝐴 ≼* 𝐷 ∧ 𝐶 ∈ On) ∧ ∀𝑎 ∈ 𝐴 (𝐵 ∈ 𝒫 On ∧ dom 𝐹 ∈ 𝐶)) → dom 𝐺 ∈ (har‘𝒫 (𝐷 × 𝐶))) | ||
Theorem | hsmexlem4 9586* | Lemma for hsmex 9589. The core induction, establishing bounds on the order types of iterated unions of the initial set. (Contributed by Stefan O'Rear, 14-Feb-2015.) |
⊢ 𝑋 ∈ V & ⊢ 𝐻 = (rec((𝑧 ∈ V ↦ (har‘𝒫 (𝑋 × 𝑧))), (har‘𝒫 𝑋)) ↾ ω) & ⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦), 𝑥) ↾ ω)) & ⊢ 𝑆 = {𝑎 ∈ ∪ (𝑅1 “ On) ∣ ∀𝑏 ∈ (TC‘{𝑎})𝑏 ≼ 𝑋} & ⊢ 𝑂 = OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑐))) ⇒ ⊢ ((𝑐 ∈ ω ∧ 𝑑 ∈ 𝑆) → dom 𝑂 ∈ (𝐻‘𝑐)) | ||
Theorem | hsmexlem5 9587* | Lemma for hsmex 9589. Combining the above constraints, along with itunitc 9578 and tcrank 9044, gives an effective constraint on the rank of 𝑆. (Contributed by Stefan O'Rear, 14-Feb-2015.) |
⊢ 𝑋 ∈ V & ⊢ 𝐻 = (rec((𝑧 ∈ V ↦ (har‘𝒫 (𝑋 × 𝑧))), (har‘𝒫 𝑋)) ↾ ω) & ⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦), 𝑥) ↾ ω)) & ⊢ 𝑆 = {𝑎 ∈ ∪ (𝑅1 “ On) ∣ ∀𝑏 ∈ (TC‘{𝑎})𝑏 ≼ 𝑋} & ⊢ 𝑂 = OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑐))) ⇒ ⊢ (𝑑 ∈ 𝑆 → (rank‘𝑑) ∈ (har‘𝒫 (ω × ∪ ran 𝐻))) | ||
Theorem | hsmexlem6 9588* | Lemma for hsmex 9589. (Contributed by Stefan O'Rear, 14-Feb-2015.) |
⊢ 𝑋 ∈ V & ⊢ 𝐻 = (rec((𝑧 ∈ V ↦ (har‘𝒫 (𝑋 × 𝑧))), (har‘𝒫 𝑋)) ↾ ω) & ⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦), 𝑥) ↾ ω)) & ⊢ 𝑆 = {𝑎 ∈ ∪ (𝑅1 “ On) ∣ ∀𝑏 ∈ (TC‘{𝑎})𝑏 ≼ 𝑋} & ⊢ 𝑂 = OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑐))) ⇒ ⊢ 𝑆 ∈ V | ||
Theorem | hsmex 9589* | The collection of hereditarily size-limited well-founded sets comprise a set. The proof is that of Randall Holmes at http://math.boisestate.edu/~holmes/holmes/hereditary.pdf, with modifications to use Hartogs' theorem instead of the weak variant (inconsequentially weakening some intermediate results), and making the well-foundedness condition explicit to avoid a direct dependence on ax-reg 8786. (Contributed by Stefan O'Rear, 14-Feb-2015.) |
⊢ (𝑋 ∈ 𝑉 → {𝑠 ∈ ∪ (𝑅1 “ On) ∣ ∀𝑥 ∈ (TC‘{𝑠})𝑥 ≼ 𝑋} ∈ V) | ||
Theorem | hsmex2 9590* | The set of hereditary size-limited sets, assuming ax-reg 8786. (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ (𝑋 ∈ 𝑉 → {𝑠 ∣ ∀𝑥 ∈ (TC‘{𝑠})𝑥 ≼ 𝑋} ∈ V) | ||
Theorem | hsmex3 9591* | The set of hereditary size-limited sets, assuming ax-reg 8786, using strict comparison (an easy corollary by separation). (Contributed by Stefan O'Rear, 11-Feb-2015.) |
⊢ (𝑋 ∈ 𝑉 → {𝑠 ∣ ∀𝑥 ∈ (TC‘{𝑠})𝑥 ≺ 𝑋} ∈ V) | ||
In this section we add the Axiom of Choice ax-ac 9616, as well as weaker forms such as the axiom of countable choice ax-cc 9592 and dependent choice ax-dc 9603. We introduce these weaker forms so that theorems that do not need the full power of the axiom of choice, but need more than simple ZF, can use these intermediate axioms instead. The combination of the Zermelo-Fraenkel axioms and the axiom of choice is often abbreviated as ZFC. The axiom of choice is widely accepted, and ZFC is the most commonly-accepted fundamental set of axioms for mathematics. However, there have been and still are some lingering controversies about the Axiom of Choice. The axiom of choice does not satisfy those who wish to have a constructive proof (e.g., it will not satisfy intuitionistic logic). Thus, we make it easy to identify which proofs depend on the axiom of choice or its weaker forms. | ||
Axiom | ax-cc 9592* | The axiom of countable choice (CC), also known as the axiom of denumerable choice. It is clearly a special case of ac5 9634, but is weak enough that it can be proven using DC (see axcc 9615). It is, however, strictly stronger than ZF and cannot be proven in ZF. It states that any countable collection of nonempty sets must have a choice function. (Contributed by Mario Carneiro, 9-Feb-2013.) |
⊢ (𝑥 ≈ ω → ∃𝑓∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)) | ||
Theorem | axcc2lem 9593* | Lemma for axcc2 9594. (Contributed by Mario Carneiro, 8-Feb-2013.) |
⊢ 𝐾 = (𝑛 ∈ ω ↦ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛))) & ⊢ 𝐴 = (𝑛 ∈ ω ↦ ({𝑛} × (𝐾‘𝑛))) & ⊢ 𝐺 = (𝑛 ∈ ω ↦ (2nd ‘(𝑓‘(𝐴‘𝑛)))) ⇒ ⊢ ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛))) | ||
Theorem | axcc2 9594* | A possibly more useful version of ax-cc using sequences instead of countable sets. The Axiom of Infinity is needed to prove this, and indeed this implies the Axiom of Infinity. (Contributed by Mario Carneiro, 8-Feb-2013.) |
⊢ ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛))) | ||
Theorem | axcc3 9595* | A possibly more useful version of ax-cc 9592 using sequences 𝐹(𝑛) instead of countable sets. The Axiom of Infinity is needed to prove this, and indeed this implies the Axiom of Infinity. (Contributed by Mario Carneiro, 8-Feb-2013.) (Revised by Mario Carneiro, 26-Dec-2014.) |
⊢ 𝐹 ∈ V & ⊢ 𝑁 ≈ ω ⇒ ⊢ ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝐹 ≠ ∅ → (𝑓‘𝑛) ∈ 𝐹)) | ||
Theorem | axcc4 9596* | A version of axcc3 9595 that uses wffs instead of classes. (Contributed by Mario Carneiro, 7-Apr-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝑁 ≈ ω & ⊢ (𝑥 = (𝑓‘𝑛) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑛 ∈ 𝑁 ∃𝑥 ∈ 𝐴 𝜑 → ∃𝑓(𝑓:𝑁⟶𝐴 ∧ ∀𝑛 ∈ 𝑁 𝜓)) | ||
Theorem | acncc 9597 | An ax-cc 9592 equivalent: every set has choice sets of length ω. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ AC ω = V | ||
Theorem | axcc4dom 9598* | Relax the constraint on axcc4 9596 to dominance instead of equinumerosity. (Contributed by Mario Carneiro, 18-Jan-2014.) |
⊢ 𝐴 ∈ V & ⊢ (𝑥 = (𝑓‘𝑛) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝑁 ≼ ω ∧ ∀𝑛 ∈ 𝑁 ∃𝑥 ∈ 𝐴 𝜑) → ∃𝑓(𝑓:𝑁⟶𝐴 ∧ ∀𝑛 ∈ 𝑁 𝜓)) | ||
Theorem | domtriomlem 9599* | Lemma for domtriom 9600. (Contributed by Mario Carneiro, 9-Feb-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 = {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} & ⊢ 𝐶 = (𝑛 ∈ ω ↦ ((𝑏‘𝑛) ∖ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘))) ⇒ ⊢ (¬ 𝐴 ∈ Fin → ω ≼ 𝐴) | ||
Theorem | domtriom 9600 | Trichotomy of equinumerosity for ω, proven using countable choice. Equivalently, all Dedekind-finite sets (as in isfin4-2 9471) are finite in the usual sense and conversely. (Contributed by Mario Carneiro, 9-Feb-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (ω ≼ 𝐴 ↔ ¬ 𝐴 ≺ ω) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |