Metamath Proof Explorer

Theorem fin23lem20

Description: Lemma for fin23 . X is either contained in or disjoint from all input sets. (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 fin23lem20 ⊢ A ∈ ω → ⋂ ran ⁡ U ⊆ t ⁡ A ∨ ⋂ ran ⁡ U ∩ t ⁡ 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 fnseqom ⊢ U Fn ω
3 peano2 ⊢ A ∈ ω → suc ⁡ A ∈ ω
4 fnfvelrn ⊢ U Fn ω ∧ suc ⁡ A ∈ ω → U ⁡ suc ⁡ A ∈ ran ⁡ U
5 2 3 4 sylancr ⊢ A ∈ ω → U ⁡ suc ⁡ A ∈ ran ⁡ U
6 intss1 ⊢ U ⁡ suc ⁡ A ∈ ran ⁡ U → ⋂ ran ⁡ U ⊆ U ⁡ suc ⁡ A
7 5 6 syl ⊢ A ∈ ω → ⋂ ran ⁡ U ⊆ U ⁡ suc ⁡ A
8 1 fin23lem19 ⊢ A ∈ ω → U ⁡ suc ⁡ A ⊆ t ⁡ A ∨ U ⁡ suc ⁡ A ∩ t ⁡ A = ∅
9 sstr2 ⊢ ⋂ ran ⁡ U ⊆ U ⁡ suc ⁡ A → U ⁡ suc ⁡ A ⊆ t ⁡ A → ⋂ ran ⁡ U ⊆ t ⁡ A
10 ssdisj ⊢ ⋂ ran ⁡ U ⊆ U ⁡ suc ⁡ A ∧ U ⁡ suc ⁡ A ∩ t ⁡ A = ∅ → ⋂ ran ⁡ U ∩ t ⁡ A = ∅
11 10 ex ⊢ ⋂ ran ⁡ U ⊆ U ⁡ suc ⁡ A → U ⁡ suc ⁡ A ∩ t ⁡ A = ∅ → ⋂ ran ⁡ U ∩ t ⁡ A = ∅
12 9 11 orim12d ⊢ ⋂ ran ⁡ U ⊆ U ⁡ suc ⁡ A → U ⁡ suc ⁡ A ⊆ t ⁡ A ∨ U ⁡ suc ⁡ A ∩ t ⁡ A = ∅ → ⋂ ran ⁡ U ⊆ t ⁡ A ∨ ⋂ ran ⁡ U ∩ t ⁡ A = ∅
13 7 8 12 sylc ⊢ A ∈ ω → ⋂ ran ⁡ U ⊆ t ⁡ A ∨ ⋂ ran ⁡ U ∩ t ⁡ A = ∅