Metamath Proof Explorer

Theorem fin23lem13

Description: Lemma for fin23 . Each step of U is a decrease. (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 fin23lem13 
|- ( A e. _om -> ( U ` suc A ) C_ ( U ` 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 sseq1 
 |-  ( ( U ` A ) = if ( ( ( t ` A ) i^i ( U ` A ) ) = (/) , ( U ` A ) , ( ( t ` A ) i^i ( U ` A ) ) ) -> ( ( U ` A ) C_ ( U ` A ) <-> if ( ( ( t ` A ) i^i ( U ` A ) ) = (/) , ( U ` A ) , ( ( t ` A ) i^i ( U ` A ) ) ) C_ ( U ` A ) ) )
4 sseq1 
 |-  ( ( ( t ` A ) i^i ( U ` A ) ) = if ( ( ( t ` A ) i^i ( U ` A ) ) = (/) , ( U ` A ) , ( ( t ` A ) i^i ( U ` A ) ) ) -> ( ( ( t ` A ) i^i ( U ` A ) ) C_ ( U ` A ) <-> if ( ( ( t ` A ) i^i ( U ` A ) ) = (/) , ( U ` A ) , ( ( t ` A ) i^i ( U ` A ) ) ) C_ ( U ` A ) ) )
5 ssid 
 |-  ( U ` A ) C_ ( U ` A )
6 inss2 
 |-  ( ( t ` A ) i^i ( U ` A ) ) C_ ( U ` A )
7 3 4 5 6 keephyp 
 |-  if ( ( ( t ` A ) i^i ( U ` A ) ) = (/) , ( U ` A ) , ( ( t ` A ) i^i ( U ` A ) ) ) C_ ( U ` A )
8 2 7 eqsstrdi 
 |-  ( A e. _om -> ( U ` suc A ) C_ ( U ` A ) )