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 ) ) = (/) ) )