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

Metamath Proof Explorer

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