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 𝑈 ∩ ( 𝑡 ‘ 𝐴 ) ) = ∅ ) )