Metamath Proof Explorer

Theorem fin23lem21

Description: Lemma for fin23 . X is not empty. We only need here that t has at least one set in its range besides (/) ; the much stronger hypothesis here will serve as our induction hypothesis though. (Contributed by Stefan O'Rear, 1-Nov-2014) (Revised by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses 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 )
fin23lem17.f 
|- F = { g | A. a e. ( ~P g ^m _om ) ( A. x e. _om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }
Assertion fin23lem21 
|- ( ( U. ran t e. F /\ t : _om -1-1-> V ) -> |^| ran U =/= (/) )

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 fin23lem17.f 
 |-  F = { g | A. a e. ( ~P g ^m _om ) ( A. x e. _om ( a ` suc x ) C_ ( a ` x ) -> |^| ran a e. ran a ) }
3 1 2 fin23lem17 
 |-  ( ( U. ran t e. F /\ t : _om -1-1-> V ) -> |^| ran U e. ran U )
4 1 fnseqom 
 |-  U Fn _om
5 fvelrnb 
 |-  ( U Fn _om -> ( |^| ran U e. ran U <-> E. a e. _om ( U ` a ) = |^| ran U ) )
6 4 5 ax-mp 
 |-  ( |^| ran U e. ran U <-> E. a e. _om ( U ` a ) = |^| ran U )
7 id 
 |-  ( a e. _om -> a e. _om )
8 vex 
 |-  t e. _V
9 f1f1orn 
 |-  ( t : _om -1-1-> V -> t : _om -1-1-onto-> ran t )
10 f1oen3g 
 |-  ( ( t e. _V /\ t : _om -1-1-onto-> ran t ) -> _om ~~ ran t )
11 8 9 10 sylancr 
 |-  ( t : _om -1-1-> V -> _om ~~ ran t )
12 ominf 
 |-  -. _om e. Fin
13 ssdif0 
 |-  ( ran t C_ { (/) } <-> ( ran t \ { (/) } ) = (/) )
14 snfi 
 |-  { (/) } e. Fin
15 ssfi 
 |-  ( ( { (/) } e. Fin /\ ran t C_ { (/) } ) -> ran t e. Fin )
16 14 15 mpan 
 |-  ( ran t C_ { (/) } -> ran t e. Fin )
17 enfi 
 |-  ( _om ~~ ran t -> ( _om e. Fin <-> ran t e. Fin ) )
18 16 17 syl5ibr 
 |-  ( _om ~~ ran t -> ( ran t C_ { (/) } -> _om e. Fin ) )
19 13 18 syl5bir 
 |-  ( _om ~~ ran t -> ( ( ran t \ { (/) } ) = (/) -> _om e. Fin ) )
20 19 necon3bd 
 |-  ( _om ~~ ran t -> ( -. _om e. Fin -> ( ran t \ { (/) } ) =/= (/) ) )
21 11 12 20 mpisyl 
 |-  ( t : _om -1-1-> V -> ( ran t \ { (/) } ) =/= (/) )
22 n0 
 |-  ( ( ran t \ { (/) } ) =/= (/) <-> E. a a e. ( ran t \ { (/) } ) )
23 eldifsn 
 |-  ( a e. ( ran t \ { (/) } ) <-> ( a e. ran t /\ a =/= (/) ) )
24 elssuni 
 |-  ( a e. ran t -> a C_ U. ran t )
25 ssn0 
 |-  ( ( a C_ U. ran t /\ a =/= (/) ) -> U. ran t =/= (/) )
26 24 25 sylan 
 |-  ( ( a e. ran t /\ a =/= (/) ) -> U. ran t =/= (/) )
27 23 26 sylbi 
 |-  ( a e. ( ran t \ { (/) } ) -> U. ran t =/= (/) )
28 27 exlimiv 
 |-  ( E. a a e. ( ran t \ { (/) } ) -> U. ran t =/= (/) )
29 22 28 sylbi 
 |-  ( ( ran t \ { (/) } ) =/= (/) -> U. ran t =/= (/) )
30 21 29 syl 
 |-  ( t : _om -1-1-> V -> U. ran t =/= (/) )
31 1 fin23lem14 
 |-  ( ( a e. _om /\ U. ran t =/= (/) ) -> ( U ` a ) =/= (/) )
32 7 30 31 syl2anr 
 |-  ( ( t : _om -1-1-> V /\ a e. _om ) -> ( U ` a ) =/= (/) )
33 neeq1 
 |-  ( ( U ` a ) = |^| ran U -> ( ( U ` a ) =/= (/) <-> |^| ran U =/= (/) ) )
34 32 33 syl5ibcom 
 |-  ( ( t : _om -1-1-> V /\ a e. _om ) -> ( ( U ` a ) = |^| ran U -> |^| ran U =/= (/) ) )
35 34 rexlimdva 
 |-  ( t : _om -1-1-> V -> ( E. a e. _om ( U ` a ) = |^| ran U -> |^| ran U =/= (/) ) )
36 6 35 syl5bi 
 |-  ( t : _om -1-1-> V -> ( |^| ran U e. ran U -> |^| ran U =/= (/) ) )
37 36 adantl 
 |-  ( ( U. ran t e. F /\ t : _om -1-1-> V ) -> ( |^| ran U e. ran U -> |^| ran U =/= (/) ) )
38 3 37 mpd 
 |-  ( ( U. ran t e. F /\ t : _om -1-1-> V ) -> |^| ran U =/= (/) )