This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑈 = seqω ( ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) , ∪ ran 𝑡 )
Assertion fin23lem20 ( 𝐴 ∈ ω → ( ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝐴 ) ∨ ( ∩ ran 𝑈 ∩ ( 𝑡 ‘ 𝐴 ) ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 fin23lem.a ⊢ 𝑈 = seqω ( ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) , ∪ ran 𝑡 )
2 1 fnseqom ⊢ 𝑈 Fn ω
3 peano2 ⊢ ( 𝐴 ∈ ω → suc 𝐴 ∈ ω )
4 fnfvelrn ⊢ ( ( 𝑈 Fn ω ∧ suc 𝐴 ∈ ω ) → ( 𝑈 ‘ suc 𝐴 ) ∈ ran 𝑈 )
5 2 3 4 sylancr ⊢ ( 𝐴 ∈ ω → ( 𝑈 ‘ suc 𝐴 ) ∈ ran 𝑈 )
6 intss1 ⊢ ( ( 𝑈 ‘ suc 𝐴 ) ∈ ran 𝑈 → ∩ ran 𝑈 ⊆ ( 𝑈 ‘ suc 𝐴 ) )
7 5 6 syl ⊢ ( 𝐴 ∈ ω → ∩ ran 𝑈 ⊆ ( 𝑈 ‘ suc 𝐴 ) )
8 1 fin23lem19 ⊢ ( 𝐴 ∈ ω → ( ( 𝑈 ‘ suc 𝐴 ) ⊆ ( 𝑡 ‘ 𝐴 ) ∨ ( ( 𝑈 ‘ suc 𝐴 ) ∩ ( 𝑡 ‘ 𝐴 ) ) = ∅ ) )
9 sstr2 ⊢ ( ∩ ran 𝑈 ⊆ ( 𝑈 ‘ suc 𝐴 ) → ( ( 𝑈 ‘ suc 𝐴 ) ⊆ ( 𝑡 ‘ 𝐴 ) → ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝐴 ) ) )
10 ssdisj ⊢ ( ( ∩ ran 𝑈 ⊆ ( 𝑈 ‘ suc 𝐴 ) ∧ ( ( 𝑈 ‘ suc 𝐴 ) ∩ ( 𝑡 ‘ 𝐴 ) ) = ∅ ) → ( ∩ ran 𝑈 ∩ ( 𝑡 ‘ 𝐴 ) ) = ∅ )
11 10 ex ⊢ ( ∩ ran 𝑈 ⊆ ( 𝑈 ‘ suc 𝐴 ) → ( ( ( 𝑈 ‘ suc 𝐴 ) ∩ ( 𝑡 ‘ 𝐴 ) ) = ∅ → ( ∩ ran 𝑈 ∩ ( 𝑡 ‘ 𝐴 ) ) = ∅ ) )
12 9 11 orim12d ⊢ ( ∩ ran 𝑈 ⊆ ( 𝑈 ‘ suc 𝐴 ) → ( ( ( 𝑈 ‘ suc 𝐴 ) ⊆ ( 𝑡 ‘ 𝐴 ) ∨ ( ( 𝑈 ‘ suc 𝐴 ) ∩ ( 𝑡 ‘ 𝐴 ) ) = ∅ ) → ( ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝐴 ) ∨ ( ∩ ran 𝑈 ∩ ( 𝑡 ‘ 𝐴 ) ) = ∅ ) ) )
13 7 8 12 sylc ⊢ ( 𝐴 ∈ ω → ( ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝐴 ) ∨ ( ∩ ran 𝑈 ∩ ( 𝑡 ‘ 𝐴 ) ) = ∅ ) )