Description: 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 U and its intersection. First, the value of U at a successor. (Contributed by Stefan O'Rear, 1-Nov-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | fin23lem.a | ⊢ 𝑈 = seqω ( ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) , ∪ ran 𝑡 ) | |
| Assertion | fin23lem12 | ⊢ ( 𝐴 ∈ ω → ( 𝑈 ‘ suc 𝐴 ) = if ( ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) = ∅ , ( 𝑈 ‘ 𝐴 ) , ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fin23lem.a | ⊢ 𝑈 = seqω ( ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) , ∪ ran 𝑡 ) | |
| 2 | 1 | seqomsuc | ⊢ ( 𝐴 ∈ ω → ( 𝑈 ‘ suc 𝐴 ) = ( 𝐴 ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) ( 𝑈 ‘ 𝐴 ) ) ) |
| 3 | fvex | ⊢ ( 𝑈 ‘ 𝐴 ) ∈ V | |
| 4 | fveq2 | ⊢ ( 𝑖 = 𝐴 → ( 𝑡 ‘ 𝑖 ) = ( 𝑡 ‘ 𝐴 ) ) | |
| 5 | 4 | ineq1d | ⊢ ( 𝑖 = 𝐴 → ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ( ( 𝑡 ‘ 𝐴 ) ∩ 𝑢 ) ) |
| 6 | 5 | eqeq1d | ⊢ ( 𝑖 = 𝐴 → ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ ↔ ( ( 𝑡 ‘ 𝐴 ) ∩ 𝑢 ) = ∅ ) ) |
| 7 | 6 5 | ifbieq2d | ⊢ ( 𝑖 = 𝐴 → if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) = if ( ( ( 𝑡 ‘ 𝐴 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝐴 ) ∩ 𝑢 ) ) ) |
| 8 | ineq2 | ⊢ ( 𝑢 = ( 𝑈 ‘ 𝐴 ) → ( ( 𝑡 ‘ 𝐴 ) ∩ 𝑢 ) = ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) ) | |
| 9 | 8 | eqeq1d | ⊢ ( 𝑢 = ( 𝑈 ‘ 𝐴 ) → ( ( ( 𝑡 ‘ 𝐴 ) ∩ 𝑢 ) = ∅ ↔ ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) = ∅ ) ) |
| 10 | id | ⊢ ( 𝑢 = ( 𝑈 ‘ 𝐴 ) → 𝑢 = ( 𝑈 ‘ 𝐴 ) ) | |
| 11 | 9 10 8 | ifbieq12d | ⊢ ( 𝑢 = ( 𝑈 ‘ 𝐴 ) → if ( ( ( 𝑡 ‘ 𝐴 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝐴 ) ∩ 𝑢 ) ) = if ( ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) = ∅ , ( 𝑈 ‘ 𝐴 ) , ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) ) ) |
| 12 | eqid | ⊢ ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) = ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) | |
| 13 | 3 | inex2 | ⊢ ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) ∈ V |
| 14 | 3 13 | ifex | ⊢ if ( ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) = ∅ , ( 𝑈 ‘ 𝐴 ) , ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) ) ∈ V |
| 15 | 7 11 12 14 | ovmpo | ⊢ ( ( 𝐴 ∈ ω ∧ ( 𝑈 ‘ 𝐴 ) ∈ V ) → ( 𝐴 ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) ( 𝑈 ‘ 𝐴 ) ) = if ( ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) = ∅ , ( 𝑈 ‘ 𝐴 ) , ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) ) ) |
| 16 | 3 15 | mpan2 | ⊢ ( 𝐴 ∈ ω → ( 𝐴 ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) ( 𝑈 ‘ 𝐴 ) ) = if ( ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) = ∅ , ( 𝑈 ‘ 𝐴 ) , ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) ) ) |
| 17 | 2 16 | eqtrd | ⊢ ( 𝐴 ∈ ω → ( 𝑈 ‘ suc 𝐴 ) = if ( ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) = ∅ , ( 𝑈 ‘ 𝐴 ) , ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) ) ) |