Metamath Proof Explorer

Theorem infpssrlem3

Description: Lemma for infpssr . (Contributed by Stefan O'Rear, 30-Oct-2014)

Ref Expression
Hypotheses infpssrlem.a 
|- ( ph -> B C_ A )
infpssrlem.c 
|- ( ph -> F : B -1-1-onto-> A )
infpssrlem.d 
|- ( ph -> C e. ( A \ B ) )
infpssrlem.e 
|- G = ( rec ( `' F , C ) |` _om )
Assertion infpssrlem3 
|- ( ph -> G : _om --> A )

Proof

Step Hyp Ref Expression
1 infpssrlem.a 
 |-  ( ph -> B C_ A )
2 infpssrlem.c 
 |-  ( ph -> F : B -1-1-onto-> A )
3 infpssrlem.d 
 |-  ( ph -> C e. ( A \ B ) )
4 infpssrlem.e 
 |-  G = ( rec ( `' F , C ) |` _om )
5 frfnom 
 |-  ( rec ( `' F , C ) |` _om ) Fn _om
6 4 fneq1i 
 |-  ( G Fn _om <-> ( rec ( `' F , C ) |` _om ) Fn _om )
7 5 6 mpbir 
 |-  G Fn _om
8 7 a1i 
 |-  ( ph -> G Fn _om )
9 fveq2 
 |-  ( c = (/) -> ( G ` c ) = ( G ` (/) ) )
10 9 eleq1d 
 |-  ( c = (/) -> ( ( G ` c ) e. A <-> ( G ` (/) ) e. A ) )
11 fveq2 
 |-  ( c = b -> ( G ` c ) = ( G ` b ) )
12 11 eleq1d 
 |-  ( c = b -> ( ( G ` c ) e. A <-> ( G ` b ) e. A ) )
13 fveq2 
 |-  ( c = suc b -> ( G ` c ) = ( G ` suc b ) )
14 13 eleq1d 
 |-  ( c = suc b -> ( ( G ` c ) e. A <-> ( G ` suc b ) e. A ) )
15 1 2 3 4 infpssrlem1 
 |-  ( ph -> ( G ` (/) ) = C )
16 3 eldifad 
 |-  ( ph -> C e. A )
17 15 16 eqeltrd 
 |-  ( ph -> ( G ` (/) ) e. A )
18 1 adantr 
 |-  ( ( ph /\ ( G ` b ) e. A ) -> B C_ A )
19 f1ocnv 
 |-  ( F : B -1-1-onto-> A -> `' F : A -1-1-onto-> B )
20 f1of 
 |-  ( `' F : A -1-1-onto-> B -> `' F : A --> B )
21 2 19 20 3syl 
 |-  ( ph -> `' F : A --> B )
22 21 ffvelrnda 
 |-  ( ( ph /\ ( G ` b ) e. A ) -> ( `' F ` ( G ` b ) ) e. B )
23 18 22 sseldd 
 |-  ( ( ph /\ ( G ` b ) e. A ) -> ( `' F ` ( G ` b ) ) e. A )
24 1 2 3 4 infpssrlem2 
 |-  ( b e. _om -> ( G ` suc b ) = ( `' F ` ( G ` b ) ) )
25 24 eleq1d 
 |-  ( b e. _om -> ( ( G ` suc b ) e. A <-> ( `' F ` ( G ` b ) ) e. A ) )
26 23 25 syl5ibr 
 |-  ( b e. _om -> ( ( ph /\ ( G ` b ) e. A ) -> ( G ` suc b ) e. A ) )
27 26 expd 
 |-  ( b e. _om -> ( ph -> ( ( G ` b ) e. A -> ( G ` suc b ) e. A ) ) )
28 10 12 14 17 27 finds2 
 |-  ( c e. _om -> ( ph -> ( G ` c ) e. A ) )
29 28 com12 
 |-  ( ph -> ( c e. _om -> ( G ` c ) e. A ) )
30 29 ralrimiv 
 |-  ( ph -> A. c e. _om ( G ` c ) e. A )
31 ffnfv 
 |-  ( G : _om --> A <-> ( G Fn _om /\ A. c e. _om ( G ` c ) e. A ) )
32 8 30 31 sylanbrc 
 |-  ( ph -> G : _om --> A )