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 )