Metamath Proof Explorer

Theorem fnrelpredd

Description: A function that preserves a relation also preserves predecessors. (Contributed by BTernaryTau, 16-Jul-2024)

Ref Expression
Hypotheses fnrelpredd.1 
|- ( ph -> F Fn A )
fnrelpredd.2 
|- ( ph -> A. x e. A A. y e. A ( x R y <-> ( F ` x ) S ( F ` y ) ) )
fnrelpredd.3 
|- ( ph -> C C_ A )
fnrelpredd.4 
|- ( ph -> D e. A )
Assertion fnrelpredd 
|- ( ph -> Pred ( S , ( F " C ) , ( F ` D ) ) = ( F " Pred ( R , C , D ) ) )

Proof

Step Hyp Ref Expression
1 fnrelpredd.1 
 |-  ( ph -> F Fn A )
2 fnrelpredd.2 
 |-  ( ph -> A. x e. A A. y e. A ( x R y <-> ( F ` x ) S ( F ` y ) ) )
3 fnrelpredd.3 
 |-  ( ph -> C C_ A )
4 fnrelpredd.4 
 |-  ( ph -> D e. A )
5 fvex 
 |-  ( F ` D ) e. _V
6 5 dfpred3 
 |-  Pred ( S , ( F " C ) , ( F ` D ) ) = { v e. ( F " C ) | v S ( F ` D ) }
7 elrabi 
 |-  ( u e. { x e. C | ( F ` x ) S ( F ` D ) } -> u e. C )
8 7 anim1i 
 |-  ( ( u e. { x e. C | ( F ` x ) S ( F ` D ) } /\ ( F ` u ) = v ) -> ( u e. C /\ ( F ` u ) = v ) )
9 8 reximi2 
 |-  ( E. u e. { x e. C | ( F ` x ) S ( F ` D ) } ( F ` u ) = v -> E. u e. C ( F ` u ) = v )
10 1 3 fvelimabd 
 |-  ( ph -> ( v e. ( F " C ) <-> E. u e. C ( F ` u ) = v ) )
11 9 10 syl5ibr 
 |-  ( ph -> ( E. u e. { x e. C | ( F ` x ) S ( F ` D ) } ( F ` u ) = v -> v e. ( F " C ) ) )
12 fveq2 
 |-  ( x = u -> ( F ` x ) = ( F ` u ) )
13 12 breq1d 
 |-  ( x = u -> ( ( F ` x ) S ( F ` D ) <-> ( F ` u ) S ( F ` D ) ) )
14 13 elrab 
 |-  ( u e. { x e. C | ( F ` x ) S ( F ` D ) } <-> ( u e. C /\ ( F ` u ) S ( F ` D ) ) )
15 breq1 
 |-  ( ( F ` u ) = v -> ( ( F ` u ) S ( F ` D ) <-> v S ( F ` D ) ) )
16 15 biimpac 
 |-  ( ( ( F ` u ) S ( F ` D ) /\ ( F ` u ) = v ) -> v S ( F ` D ) )
17 16 adantll 
 |-  ( ( ( u e. C /\ ( F ` u ) S ( F ` D ) ) /\ ( F ` u ) = v ) -> v S ( F ` D ) )
18 14 17 sylanb 
 |-  ( ( u e. { x e. C | ( F ` x ) S ( F ` D ) } /\ ( F ` u ) = v ) -> v S ( F ` D ) )
19 18 rexlimiva 
 |-  ( E. u e. { x e. C | ( F ` x ) S ( F ` D ) } ( F ` u ) = v -> v S ( F ` D ) )
20 11 19 jca2 
 |-  ( ph -> ( E. u e. { x e. C | ( F ` x ) S ( F ` D ) } ( F ` u ) = v -> ( v e. ( F " C ) /\ v S ( F ` D ) ) ) )
21 10 biimpd 
 |-  ( ph -> ( v e. ( F " C ) -> E. u e. C ( F ` u ) = v ) )
22 21 adantrd 
 |-  ( ph -> ( ( v e. ( F " C ) /\ v S ( F ` D ) ) -> E. u e. C ( F ` u ) = v ) )
23 simpl 
 |-  ( ( u e. C /\ ( F ` u ) = v ) -> u e. C )
24 23 a1i 
 |-  ( v S ( F ` D ) -> ( ( u e. C /\ ( F ` u ) = v ) -> u e. C ) )
25 15 biimprcd 
 |-  ( v S ( F ` D ) -> ( ( F ` u ) = v -> ( F ` u ) S ( F ` D ) ) )
26 25 adantld 
 |-  ( v S ( F ` D ) -> ( ( u e. C /\ ( F ` u ) = v ) -> ( F ` u ) S ( F ` D ) ) )
27 simpr 
 |-  ( ( u e. C /\ ( F ` u ) = v ) -> ( F ` u ) = v )
28 27 a1i 
 |-  ( v S ( F ` D ) -> ( ( u e. C /\ ( F ` u ) = v ) -> ( F ` u ) = v ) )
29 24 26 28 3jcad 
 |-  ( v S ( F ` D ) -> ( ( u e. C /\ ( F ` u ) = v ) -> ( u e. C /\ ( F ` u ) S ( F ` D ) /\ ( F ` u ) = v ) ) )
30 14 biimpri 
 |-  ( ( u e. C /\ ( F ` u ) S ( F ` D ) ) -> u e. { x e. C | ( F ` x ) S ( F ` D ) } )
31 30 anim1i 
 |-  ( ( ( u e. C /\ ( F ` u ) S ( F ` D ) ) /\ ( F ` u ) = v ) -> ( u e. { x e. C | ( F ` x ) S ( F ` D ) } /\ ( F ` u ) = v ) )
32 31 3impa 
 |-  ( ( u e. C /\ ( F ` u ) S ( F ` D ) /\ ( F ` u ) = v ) -> ( u e. { x e. C | ( F ` x ) S ( F ` D ) } /\ ( F ` u ) = v ) )
33 29 32 syl6 
 |-  ( v S ( F ` D ) -> ( ( u e. C /\ ( F ` u ) = v ) -> ( u e. { x e. C | ( F ` x ) S ( F ` D ) } /\ ( F ` u ) = v ) ) )
34 33 reximdv2 
 |-  ( v S ( F ` D ) -> ( E. u e. C ( F ` u ) = v -> E. u e. { x e. C | ( F ` x ) S ( F ` D ) } ( F ` u ) = v ) )
35 34 adantl 
 |-  ( ( v e. ( F " C ) /\ v S ( F ` D ) ) -> ( E. u e. C ( F ` u ) = v -> E. u e. { x e. C | ( F ` x ) S ( F ` D ) } ( F ` u ) = v ) )
36 22 35 sylcom 
 |-  ( ph -> ( ( v e. ( F " C ) /\ v S ( F ` D ) ) -> E. u e. { x e. C | ( F ` x ) S ( F ` D ) } ( F ` u ) = v ) )
37 20 36 impbid 
 |-  ( ph -> ( E. u e. { x e. C | ( F ` x ) S ( F ` D ) } ( F ` u ) = v <-> ( v e. ( F " C ) /\ v S ( F ` D ) ) ) )
38 37 abbidv 
 |-  ( ph -> { v | E. u e. { x e. C | ( F ` x ) S ( F ` D ) } ( F ` u ) = v } = { v | ( v e. ( F " C ) /\ v S ( F ` D ) ) } )
39 df-rab 
 |-  { v e. ( F " C ) | v S ( F ` D ) } = { v | ( v e. ( F " C ) /\ v S ( F ` D ) ) }
40 38 39 eqtr4di 
 |-  ( ph -> { v | E. u e. { x e. C | ( F ` x ) S ( F ` D ) } ( F ` u ) = v } = { v e. ( F " C ) | v S ( F ` D ) } )
41 6 40 eqtr4id 
 |-  ( ph -> Pred ( S , ( F " C ) , ( F ` D ) ) = { v | E. u e. { x e. C | ( F ` x ) S ( F ` D ) } ( F ` u ) = v } )
42 fnfun 
 |-  ( F Fn A -> Fun F )
43 1 42 syl 
 |-  ( ph -> Fun F )
44 ssrab2 
 |-  { x e. C | ( F ` x ) S ( F ` D ) } C_ C
45 44 3 sstrid 
 |-  ( ph -> { x e. C | ( F ` x ) S ( F ` D ) } C_ A )
46 1 fndmd 
 |-  ( ph -> dom F = A )
47 45 46 sseqtrrd 
 |-  ( ph -> { x e. C | ( F ` x ) S ( F ` D ) } C_ dom F )
48 dfimafn 
 |-  ( ( Fun F /\ { x e. C | ( F ` x ) S ( F ` D ) } C_ dom F ) -> ( F " { x e. C | ( F ` x ) S ( F ` D ) } ) = { v | E. u e. { x e. C | ( F ` x ) S ( F ` D ) } ( F ` u ) = v } )
49 43 47 48 syl2anc 
 |-  ( ph -> ( F " { x e. C | ( F ` x ) S ( F ` D ) } ) = { v | E. u e. { x e. C | ( F ` x ) S ( F ` D ) } ( F ` u ) = v } )
50 41 49 eqtr4d 
 |-  ( ph -> Pred ( S , ( F " C ) , ( F ` D ) ) = ( F " { x e. C | ( F ` x ) S ( F ` D ) } ) )
51 dfpred3g 
 |-  ( D e. A -> Pred ( R , C , D ) = { x e. C | x R D } )
52 4 51 syl 
 |-  ( ph -> Pred ( R , C , D ) = { x e. C | x R D } )
53 3 sselda 
 |-  ( ( ph /\ x e. C ) -> x e. A )
54 2 r19.21bi 
 |-  ( ( ph /\ x e. A ) -> A. y e. A ( x R y <-> ( F ` x ) S ( F ` y ) ) )
55 breq2 
 |-  ( y = D -> ( x R y <-> x R D ) )
56 fveq2 
 |-  ( y = D -> ( F ` y ) = ( F ` D ) )
57 56 breq2d 
 |-  ( y = D -> ( ( F ` x ) S ( F ` y ) <-> ( F ` x ) S ( F ` D ) ) )
58 55 57 bibi12d 
 |-  ( y = D -> ( ( x R y <-> ( F ` x ) S ( F ` y ) ) <-> ( x R D <-> ( F ` x ) S ( F ` D ) ) ) )
59 58 rspcv 
 |-  ( D e. A -> ( A. y e. A ( x R y <-> ( F ` x ) S ( F ` y ) ) -> ( x R D <-> ( F ` x ) S ( F ` D ) ) ) )
60 4 59 syl 
 |-  ( ph -> ( A. y e. A ( x R y <-> ( F ` x ) S ( F ` y ) ) -> ( x R D <-> ( F ` x ) S ( F ` D ) ) ) )
61 60 adantr 
 |-  ( ( ph /\ x e. A ) -> ( A. y e. A ( x R y <-> ( F ` x ) S ( F ` y ) ) -> ( x R D <-> ( F ` x ) S ( F ` D ) ) ) )
62 54 61 mpd 
 |-  ( ( ph /\ x e. A ) -> ( x R D <-> ( F ` x ) S ( F ` D ) ) )
63 53 62 syldan 
 |-  ( ( ph /\ x e. C ) -> ( x R D <-> ( F ` x ) S ( F ` D ) ) )
64 63 rabbidva 
 |-  ( ph -> { x e. C | x R D } = { x e. C | ( F ` x ) S ( F ` D ) } )
65 52 64 eqtrd 
 |-  ( ph -> Pred ( R , C , D ) = { x e. C | ( F ` x ) S ( F ` D ) } )
66 65 imaeq2d 
 |-  ( ph -> ( F " Pred ( R , C , D ) ) = ( F " { x e. C | ( F ` x ) S ( F ` D ) } ) )
67 50 66 eqtr4d 
 |-  ( ph -> Pred ( S , ( F " C ) , ( F ` D ) ) = ( F " Pred ( R , C , D ) ) )