Theorem fin23lem19

Description: Lemma for fin23 . The first set in U to see an input set is either contained in it or disjoint from it. (Contributed by Stefan O'Rear, 1-Nov-2014)

	Ref	Expression
Hypothesis	fin23lem.a	⊢ 𝑈 = seqω ( ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) , ∪ ran 𝑡 )
Assertion	fin23lem19	⊢ ( 𝐴 ∈ ω → ( ( 𝑈 ‘ suc 𝐴 ) ⊆ ( 𝑡 ‘ 𝐴 ) ∨ ( ( 𝑈 ‘ suc 𝐴 ) ∩ ( 𝑡 ‘ 𝐴 ) ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		fin23lem.a	⊢ 𝑈 = seqω ( ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) , ∪ ran 𝑡 )
2	1	fin23lem12	⊢ ( 𝐴 ∈ ω → ( 𝑈 ‘ suc 𝐴 ) = if ( ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) = ∅ , ( 𝑈 ‘ 𝐴 ) , ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) ) )
3		eqif	⊢ ( ( 𝑈 ‘ suc 𝐴 ) = if ( ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) = ∅ , ( 𝑈 ‘ 𝐴 ) , ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) ) ↔ ( ( ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) = ∅ ∧ ( 𝑈 ‘ suc 𝐴 ) = ( 𝑈 ‘ 𝐴 ) ) ∨ ( ¬ ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) = ∅ ∧ ( 𝑈 ‘ suc 𝐴 ) = ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) ) ) )
4	2 3	sylib	⊢ ( 𝐴 ∈ ω → ( ( ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) = ∅ ∧ ( 𝑈 ‘ suc 𝐴 ) = ( 𝑈 ‘ 𝐴 ) ) ∨ ( ¬ ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) = ∅ ∧ ( 𝑈 ‘ suc 𝐴 ) = ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) ) ) )
5		incom	⊢ ( ( 𝑈 ‘ suc 𝐴 ) ∩ ( 𝑡 ‘ 𝐴 ) ) = ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ suc 𝐴 ) )
6		ineq2	⊢ ( ( 𝑈 ‘ suc 𝐴 ) = ( 𝑈 ‘ 𝐴 ) → ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ suc 𝐴 ) ) = ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) )
7	6	eqeq1d	⊢ ( ( 𝑈 ‘ suc 𝐴 ) = ( 𝑈 ‘ 𝐴 ) → ( ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ suc 𝐴 ) ) = ∅ ↔ ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) = ∅ ) )
8	7	biimparc	⊢ ( ( ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) = ∅ ∧ ( 𝑈 ‘ suc 𝐴 ) = ( 𝑈 ‘ 𝐴 ) ) → ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ suc 𝐴 ) ) = ∅ )
9	5 8	eqtrid	⊢ ( ( ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) = ∅ ∧ ( 𝑈 ‘ suc 𝐴 ) = ( 𝑈 ‘ 𝐴 ) ) → ( ( 𝑈 ‘ suc 𝐴 ) ∩ ( 𝑡 ‘ 𝐴 ) ) = ∅ )
10		inss1	⊢ ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) ⊆ ( 𝑡 ‘ 𝐴 )
11		sseq1	⊢ ( ( 𝑈 ‘ suc 𝐴 ) = ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) → ( ( 𝑈 ‘ suc 𝐴 ) ⊆ ( 𝑡 ‘ 𝐴 ) ↔ ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) ⊆ ( 𝑡 ‘ 𝐴 ) ) )
12	10 11	mpbiri	⊢ ( ( 𝑈 ‘ suc 𝐴 ) = ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) → ( 𝑈 ‘ suc 𝐴 ) ⊆ ( 𝑡 ‘ 𝐴 ) )
13	12	adantl	⊢ ( ( ¬ ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) = ∅ ∧ ( 𝑈 ‘ suc 𝐴 ) = ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) ) → ( 𝑈 ‘ suc 𝐴 ) ⊆ ( 𝑡 ‘ 𝐴 ) )
14	9 13	orim12i	⊢ ( ( ( ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) = ∅ ∧ ( 𝑈 ‘ suc 𝐴 ) = ( 𝑈 ‘ 𝐴 ) ) ∨ ( ¬ ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) = ∅ ∧ ( 𝑈 ‘ suc 𝐴 ) = ( ( 𝑡 ‘ 𝐴 ) ∩ ( 𝑈 ‘ 𝐴 ) ) ) ) → ( ( ( 𝑈 ‘ suc 𝐴 ) ∩ ( 𝑡 ‘ 𝐴 ) ) = ∅ ∨ ( 𝑈 ‘ suc 𝐴 ) ⊆ ( 𝑡 ‘ 𝐴 ) ) )
15	4 14	syl	⊢ ( 𝐴 ∈ ω → ( ( ( 𝑈 ‘ suc 𝐴 ) ∩ ( 𝑡 ‘ 𝐴 ) ) = ∅ ∨ ( 𝑈 ‘ suc 𝐴 ) ⊆ ( 𝑡 ‘ 𝐴 ) ) )
16	15	orcomd	⊢ ( 𝐴 ∈ ω → ( ( 𝑈 ‘ suc 𝐴 ) ⊆ ( 𝑡 ‘ 𝐴 ) ∨ ( ( 𝑈 ‘ suc 𝐴 ) ∩ ( 𝑡 ‘ 𝐴 ) ) = ∅ ) )