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