Metamath Proof Explorer

Theorem fin23lem20

Description: Lemma for fin23 . X is either contained in or disjoint from all input sets. (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 fin23lem20 
|- ( A e. _om -> ( |^| ran U C_ ( t ` A ) \/ ( |^| ran U 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 fnseqom 
 |-  U Fn _om
3 peano2 
 |-  ( A e. _om -> suc A e. _om )
4 fnfvelrn 
 |-  ( ( U Fn _om /\ suc A e. _om ) -> ( U ` suc A ) e. ran U )
5 2 3 4 sylancr 
 |-  ( A e. _om -> ( U ` suc A ) e. ran U )
6 intss1 
 |-  ( ( U ` suc A ) e. ran U -> |^| ran U C_ ( U ` suc A ) )
7 5 6 syl 
 |-  ( A e. _om -> |^| ran U C_ ( U ` suc A ) )
8 1 fin23lem19 
 |-  ( A e. _om -> ( ( U ` suc A ) C_ ( t ` A ) \/ ( ( U ` suc A ) i^i ( t ` A ) ) = (/) ) )
9 sstr2 
 |-  ( |^| ran U C_ ( U ` suc A ) -> ( ( U ` suc A ) C_ ( t ` A ) -> |^| ran U C_ ( t ` A ) ) )
10 ssdisj 
 |-  ( ( |^| ran U C_ ( U ` suc A ) /\ ( ( U ` suc A ) i^i ( t ` A ) ) = (/) ) -> ( |^| ran U i^i ( t ` A ) ) = (/) )
11 10 ex 
 |-  ( |^| ran U C_ ( U ` suc A ) -> ( ( ( U ` suc A ) i^i ( t ` A ) ) = (/) -> ( |^| ran U i^i ( t ` A ) ) = (/) ) )
12 9 11 orim12d 
 |-  ( |^| ran U C_ ( U ` suc A ) -> ( ( ( U ` suc A ) C_ ( t ` A ) \/ ( ( U ` suc A ) i^i ( t ` A ) ) = (/) ) -> ( |^| ran U C_ ( t ` A ) \/ ( |^| ran U i^i ( t ` A ) ) = (/) ) ) )
13 7 8 12 sylc 
 |-  ( A e. _om -> ( |^| ran U C_ ( t ` A ) \/ ( |^| ran U i^i ( t ` A ) ) = (/) ) )