Metamath Proof Explorer

Theorem fin23lem40

Description: Lemma for fin23 . Fin2 sets satisfy the descending chain condition. (Contributed by Stefan O'Rear, 3-Nov-2014)

Ref Expression
Hypothesis fin23lem40.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 fin23lem40 
|- ( A e. Fin2 -> A e. F )

Proof

Step Hyp Ref Expression
1 fin23lem40.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 ) }
2 elmapi 
 |-  ( f e. ( ~P A ^m _om ) -> f : _om --> ~P A )
3 simpl 
 |-  ( ( A e. Fin2 /\ ( f : _om --> ~P A /\ A. b e. _om ( f ` suc b ) C_ ( f ` b ) ) ) -> A e. Fin2 )
4 frn 
 |-  ( f : _om --> ~P A -> ran f C_ ~P A )
5 4 ad2antrl 
 |-  ( ( A e. Fin2 /\ ( f : _om --> ~P A /\ A. b e. _om ( f ` suc b ) C_ ( f ` b ) ) ) -> ran f C_ ~P A )
6 fdm 
 |-  ( f : _om --> ~P A -> dom f = _om )
7 peano1 
 |-  (/) e. _om
8 ne0i 
 |-  ( (/) e. _om -> _om =/= (/) )
9 7 8 mp1i 
 |-  ( f : _om --> ~P A -> _om =/= (/) )
10 6 9 eqnetrd 
 |-  ( f : _om --> ~P A -> dom f =/= (/) )
11 dm0rn0 
 |-  ( dom f = (/) <-> ran f = (/) )
12 11 necon3bii 
 |-  ( dom f =/= (/) <-> ran f =/= (/) )
13 10 12 sylib 
 |-  ( f : _om --> ~P A -> ran f =/= (/) )
14 13 ad2antrl 
 |-  ( ( A e. Fin2 /\ ( f : _om --> ~P A /\ A. b e. _om ( f ` suc b ) C_ ( f ` b ) ) ) -> ran f =/= (/) )
15 ffn 
 |-  ( f : _om --> ~P A -> f Fn _om )
16 15 ad2antrl 
 |-  ( ( A e. Fin2 /\ ( f : _om --> ~P A /\ A. b e. _om ( f ` suc b ) C_ ( f ` b ) ) ) -> f Fn _om )
17 sspss 
 |-  ( ( f ` suc b ) C_ ( f ` b ) <-> ( ( f ` suc b ) C. ( f ` b ) \/ ( f ` suc b ) = ( f ` b ) ) )
18 fvex 
 |-  ( f ` b ) e. _V
19 fvex 
 |-  ( f ` suc b ) e. _V
20 18 19 brcnv 
 |-  ( ( f ` b ) `' [C.] ( f ` suc b ) <-> ( f ` suc b ) [C.] ( f ` b ) )
21 18 brrpss 
 |-  ( ( f ` suc b ) [C.] ( f ` b ) <-> ( f ` suc b ) C. ( f ` b ) )
22 20 21 bitri 
 |-  ( ( f ` b ) `' [C.] ( f ` suc b ) <-> ( f ` suc b ) C. ( f ` b ) )
23 eqcom 
 |-  ( ( f ` b ) = ( f ` suc b ) <-> ( f ` suc b ) = ( f ` b ) )
24 22 23 orbi12i 
 |-  ( ( ( f ` b ) `' [C.] ( f ` suc b ) \/ ( f ` b ) = ( f ` suc b ) ) <-> ( ( f ` suc b ) C. ( f ` b ) \/ ( f ` suc b ) = ( f ` b ) ) )
25 17 24 sylbb2 
 |-  ( ( f ` suc b ) C_ ( f ` b ) -> ( ( f ` b ) `' [C.] ( f ` suc b ) \/ ( f ` b ) = ( f ` suc b ) ) )
26 25 ralimi 
 |-  ( A. b e. _om ( f ` suc b ) C_ ( f ` b ) -> A. b e. _om ( ( f ` b ) `' [C.] ( f ` suc b ) \/ ( f ` b ) = ( f ` suc b ) ) )
27 26 ad2antll 
 |-  ( ( A e. Fin2 /\ ( f : _om --> ~P A /\ A. b e. _om ( f ` suc b ) C_ ( f ` b ) ) ) -> A. b e. _om ( ( f ` b ) `' [C.] ( f ` suc b ) \/ ( f ` b ) = ( f ` suc b ) ) )
28 porpss 
 |-  [C.] Po ran f
29 cnvpo 
 |-  ( [C.] Po ran f <-> `' [C.] Po ran f )
30 28 29 mpbi 
 |-  `' [C.] Po ran f
31 30 a1i 
 |-  ( ( A e. Fin2 /\ ( f : _om --> ~P A /\ A. b e. _om ( f ` suc b ) C_ ( f ` b ) ) ) -> `' [C.] Po ran f )
32 sornom 
 |-  ( ( f Fn _om /\ A. b e. _om ( ( f ` b ) `' [C.] ( f ` suc b ) \/ ( f ` b ) = ( f ` suc b ) ) /\ `' [C.] Po ran f ) -> `' [C.] Or ran f )
33 16 27 31 32 syl3anc 
 |-  ( ( A e. Fin2 /\ ( f : _om --> ~P A /\ A. b e. _om ( f ` suc b ) C_ ( f ` b ) ) ) -> `' [C.] Or ran f )
34 cnvso 
 |-  ( [C.] Or ran f <-> `' [C.] Or ran f )
35 33 34 sylibr 
 |-  ( ( A e. Fin2 /\ ( f : _om --> ~P A /\ A. b e. _om ( f ` suc b ) C_ ( f ` b ) ) ) -> [C.] Or ran f )
36 fin2i2 
 |-  ( ( ( A e. Fin2 /\ ran f C_ ~P A ) /\ ( ran f =/= (/) /\ [C.] Or ran f ) ) -> |^| ran f e. ran f )
37 3 5 14 35 36 syl22anc 
 |-  ( ( A e. Fin2 /\ ( f : _om --> ~P A /\ A. b e. _om ( f ` suc b ) C_ ( f ` b ) ) ) -> |^| ran f e. ran f )
38 37 expr 
 |-  ( ( A e. Fin2 /\ f : _om --> ~P A ) -> ( A. b e. _om ( f ` suc b ) C_ ( f ` b ) -> |^| ran f e. ran f ) )
39 2 38 sylan2 
 |-  ( ( A e. Fin2 /\ f e. ( ~P A ^m _om ) ) -> ( A. b e. _om ( f ` suc b ) C_ ( f ` b ) -> |^| ran f e. ran f ) )
40 39 ralrimiva 
 |-  ( A e. Fin2 -> A. f e. ( ~P A ^m _om ) ( A. b e. _om ( f ` suc b ) C_ ( f ` b ) -> |^| ran f e. ran f ) )
41 1 isfin3ds 
 |-  ( A e. Fin2 -> ( A e. F <-> A. f e. ( ~P A ^m _om ) ( A. b e. _om ( f ` suc b ) C_ ( f ` b ) -> |^| ran f e. ran f ) ) )
42 40 41 mpbird 
 |-  ( A e. Fin2 -> A e. F )