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 U = seq ω i ω , u V if t i u = u t i u ran t
Assertion fin23lem19 A ω U suc A t A U suc A 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 fin23lem12 A ω U suc A = if t A U A = U A t A U A
3 eqif U suc A = if t A U A = U A t A U A t A U A = U suc A = U A ¬ t A U A = U suc A = t A U A
4 2 3 sylib A ω t A U A = U suc A = U A ¬ t A U A = U suc A = t A U A
5 incom U suc A t A = t A U suc A
6 ineq2 U suc A = U A t A U suc A = t A U A
7 6 eqeq1d U suc A = U A t A U suc A = t A U A =
8 7 biimparc t A U A = U suc A = U A t A U suc A =
9 5 8 syl5eq t A U A = U suc A = U A U suc A t A =
10 inss1 t A U A t A
11 sseq1 U suc A = t A U A U suc A t A t A U A t A
12 10 11 mpbiri U suc A = t A U A U suc A t A
13 12 adantl ¬ t A U A = U suc A = t A U A U suc A t A
14 9 13 orim12i t A U A = U suc A = U A ¬ t A U A = U suc A = t A U A U suc A t A = U suc A t A
15 4 14 syl A ω U suc A t A = U suc A t A
16 15 orcomd A ω U suc A t A U suc A t A =