Metamath Proof Explorer

Theorem fin23lem12

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 ⊢ U = seq ω i ∈ ω , u ∈ V ⟼ if t ⁡ i ∩ u = ∅ u t ⁡ i ∩ u ⋃ ran ⁡ t
Assertion fin23lem12 ⊢ A ∈ ω → U ⁡ suc ⁡ A = if t ⁡ A ∩ U ⁡ A = ∅ U ⁡ A t ⁡ A ∩ U ⁡ A

Proof

Step Hyp Ref Expression
1 fin23lem.a ⊢ U = seq ω i ∈ ω , u ∈ V ⟼ if t ⁡ i ∩ u = ∅ u t ⁡ i ∩ u ⋃ ran ⁡ t
2 1 seqomsuc ⊢ A ∈ ω → U ⁡ suc ⁡ A = A i ∈ ω , u ∈ V ⟼ if t ⁡ i ∩ u = ∅ u t ⁡ i ∩ u U ⁡ A
3 fvex ⊢ U ⁡ A ∈ V
4 fveq2 ⊢ i = A → t ⁡ i = t ⁡ A
5 4 ineq1d ⊢ i = A → t ⁡ i ∩ u = t ⁡ A ∩ u
6 5 eqeq1d ⊢ i = A → t ⁡ i ∩ u = ∅ ↔ t ⁡ A ∩ u = ∅
7 6 5 ifbieq2d ⊢ i = A → if t ⁡ i ∩ u = ∅ u t ⁡ i ∩ u = if t ⁡ A ∩ u = ∅ u t ⁡ A ∩ u
8 ineq2 ⊢ u = U ⁡ A → t ⁡ A ∩ u = t ⁡ A ∩ U ⁡ A
9 8 eqeq1d ⊢ u = U ⁡ A → t ⁡ A ∩ u = ∅ ↔ t ⁡ A ∩ U ⁡ A = ∅
10 id ⊢ u = U ⁡ A → u = U ⁡ A
11 9 10 8 ifbieq12d ⊢ u = U ⁡ A → if t ⁡ A ∩ u = ∅ u t ⁡ A ∩ u = if t ⁡ A ∩ U ⁡ A = ∅ U ⁡ A t ⁡ A ∩ U ⁡ A
12 eqid ⊢ i ∈ ω , u ∈ V ⟼ if t ⁡ i ∩ u = ∅ u t ⁡ i ∩ u = i ∈ ω , u ∈ V ⟼ if t ⁡ i ∩ u = ∅ u t ⁡ i ∩ u
13 3 inex2 ⊢ t ⁡ A ∩ U ⁡ A ∈ V
14 3 13 ifex ⊢ if t ⁡ A ∩ U ⁡ A = ∅ U ⁡ A t ⁡ A ∩ U ⁡ A ∈ V
15 7 11 12 14 ovmpo ⊢ A ∈ ω ∧ U ⁡ A ∈ V → A i ∈ ω , u ∈ V ⟼ if t ⁡ i ∩ u = ∅ u t ⁡ i ∩ u U ⁡ A = if t ⁡ A ∩ U ⁡ A = ∅ U ⁡ A t ⁡ A ∩ U ⁡ A
16 3 15 mpan2 ⊢ A ∈ ω → A i ∈ ω , u ∈ V ⟼ if t ⁡ i ∩ u = ∅ u t ⁡ i ∩ u U ⁡ A = if t ⁡ A ∩ U ⁡ A = ∅ U ⁡ A t ⁡ A ∩ U ⁡ A
17 2 16 eqtrd ⊢ A ∈ ω → U ⁡ suc ⁡ A = if t ⁡ A ∩ U ⁡ A = ∅ U ⁡ A t ⁡ A ∩ U ⁡ A