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 = seqom ( ( i e. _om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t )

Assertion

|- ( A e. _om -> ( ( U ` suc A ) C_ ( t ` A ) \/ ( ( U ` suc A ) i^i ( t ` A ) ) = (/) ) )

Proof

Step	Hyp	Ref	Expression
1		fin23lem.a	\|- U = seqom ( ( i e. _om , u e. _V \|-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t )
2	1	fin23lem12	\|- ( A e. _om -> ( U ` suc A ) = if ( ( ( t ` A ) i^i ( U ` A ) ) = (/) , ( U ` A ) , ( ( t ` A ) i^i ( U ` A ) ) ) )
3		eqif	\|- ( ( U ` suc A ) = if ( ( ( t ` A ) i^i ( U ` A ) ) = (/) , ( U ` A ) , ( ( t ` A ) i^i ( U ` A ) ) ) <-> ( ( ( ( t ` A ) i^i ( U ` A ) ) = (/) /\ ( U ` suc A ) = ( U ` A ) ) \/ ( -. ( ( t ` A ) i^i ( U ` A ) ) = (/) /\ ( U ` suc A ) = ( ( t ` A ) i^i ( U ` A ) ) ) ) )
4	2 3	sylib	\|- ( A e. _om -> ( ( ( ( t ` A ) i^i ( U ` A ) ) = (/) /\ ( U ` suc A ) = ( U ` A ) ) \/ ( -. ( ( t ` A ) i^i ( U ` A ) ) = (/) /\ ( U ` suc A ) = ( ( t ` A ) i^i ( U ` A ) ) ) ) )
5		incom	\|- ( ( U ` suc A ) i^i ( t ` A ) ) = ( ( t ` A ) i^i ( U ` suc A ) )
6		ineq2	\|- ( ( U ` suc A ) = ( U ` A ) -> ( ( t ` A ) i^i ( U ` suc A ) ) = ( ( t ` A ) i^i ( U ` A ) ) )
7	6	eqeq1d	\|- ( ( U ` suc A ) = ( U ` A ) -> ( ( ( t ` A ) i^i ( U ` suc A ) ) = (/) <-> ( ( t ` A ) i^i ( U ` A ) ) = (/) ) )
8	7	biimparc	\|- ( ( ( ( t ` A ) i^i ( U ` A ) ) = (/) /\ ( U ` suc A ) = ( U ` A ) ) -> ( ( t ` A ) i^i ( U ` suc A ) ) = (/) )
9	5 8	eqtrid	\|- ( ( ( ( t ` A ) i^i ( U ` A ) ) = (/) /\ ( U ` suc A ) = ( U ` A ) ) -> ( ( U ` suc A ) i^i ( t ` A ) ) = (/) )
10		inss1	\|- ( ( t ` A ) i^i ( U ` A ) ) C_ ( t ` A )
11		sseq1	\|- ( ( U ` suc A ) = ( ( t ` A ) i^i ( U ` A ) ) -> ( ( U ` suc A ) C_ ( t ` A ) <-> ( ( t ` A ) i^i ( U ` A ) ) C_ ( t ` A ) ) )
12	10 11	mpbiri	\|- ( ( U ` suc A ) = ( ( t ` A ) i^i ( U ` A ) ) -> ( U ` suc A ) C_ ( t ` A ) )
13	12	adantl	\|- ( ( -. ( ( t ` A ) i^i ( U ` A ) ) = (/) /\ ( U ` suc A ) = ( ( t ` A ) i^i ( U ` A ) ) ) -> ( U ` suc A ) C_ ( t ` A ) )
14	9 13	orim12i	\|- ( ( ( ( ( t ` A ) i^i ( U ` A ) ) = (/) /\ ( U ` suc A ) = ( U ` A ) ) \/ ( -. ( ( t ` A ) i^i ( U ` A ) ) = (/) /\ ( U ` suc A ) = ( ( t ` A ) i^i ( U ` A ) ) ) ) -> ( ( ( U ` suc A ) i^i ( t ` A ) ) = (/) \/ ( U ` suc A ) C_ ( t ` A ) ) )
15	4 14	syl	\|- ( A e. _om -> ( ( ( U ` suc A ) i^i ( t ` A ) ) = (/) \/ ( U ` suc A ) C_ ( t ` A ) ) )
16	15	orcomd	\|- ( A e. _om -> ( ( U ` suc A ) C_ ( t ` A ) \/ ( ( U ` suc A ) i^i ( t ` A ) ) = (/) ) )