Metamath Proof Explorer

Theorem dmrelrnrel

Description: A relation preserving function. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses dmrelrnrel.x 
|- F/ x ph
dmrelrnrel.y 
|- F/ y ph
dmrelrnrel.i 
|- ( ph -> A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) )
dmrelrnrel.b 
|- ( ph -> B e. A )
dmrelrnrel.c 
|- ( ph -> C e. A )
dmrelrnrel.r 
|- ( ph -> B R C )
Assertion dmrelrnrel 
|- ( ph -> ( F ` B ) S ( F ` C ) )

Proof

Step Hyp Ref Expression
1 dmrelrnrel.x 
 |-  F/ x ph
2 dmrelrnrel.y 
 |-  F/ y ph
3 dmrelrnrel.i 
 |-  ( ph -> A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) )
4 dmrelrnrel.b 
 |-  ( ph -> B e. A )
5 dmrelrnrel.c 
 |-  ( ph -> C e. A )
6 dmrelrnrel.r 
 |-  ( ph -> B R C )
7 id 
 |-  ( ph -> ph )
8 7 4 5 jca31 
 |-  ( ph -> ( ( ph /\ B e. A ) /\ C e. A ) )
9 nfv 
 |-  F/ y B e. A
10 2 9 nfan 
 |-  F/ y ( ph /\ B e. A )
11 nfv 
 |-  F/ y C e. A
12 10 11 nfan 
 |-  F/ y ( ( ph /\ B e. A ) /\ C e. A )
13 nfv 
 |-  F/ y ( B R C -> ( F ` B ) S ( F ` C ) )
14 12 13 nfim 
 |-  F/ y ( ( ( ph /\ B e. A ) /\ C e. A ) -> ( B R C -> ( F ` B ) S ( F ` C ) ) )
15 9 14 nfim 
 |-  F/ y ( B e. A -> ( ( ( ph /\ B e. A ) /\ C e. A ) -> ( B R C -> ( F ` B ) S ( F ` C ) ) ) )
16 eleq1 
 |-  ( y = C -> ( y e. A <-> C e. A ) )
17 16 anbi2d 
 |-  ( y = C -> ( ( ( ph /\ B e. A ) /\ y e. A ) <-> ( ( ph /\ B e. A ) /\ C e. A ) ) )
18 breq2 
 |-  ( y = C -> ( B R y <-> B R C ) )
19 fveq2 
 |-  ( y = C -> ( F ` y ) = ( F ` C ) )
20 19 breq2d 
 |-  ( y = C -> ( ( F ` B ) S ( F ` y ) <-> ( F ` B ) S ( F ` C ) ) )
21 18 20 imbi12d 
 |-  ( y = C -> ( ( B R y -> ( F ` B ) S ( F ` y ) ) <-> ( B R C -> ( F ` B ) S ( F ` C ) ) ) )
22 17 21 imbi12d 
 |-  ( y = C -> ( ( ( ( ph /\ B e. A ) /\ y e. A ) -> ( B R y -> ( F ` B ) S ( F ` y ) ) ) <-> ( ( ( ph /\ B e. A ) /\ C e. A ) -> ( B R C -> ( F ` B ) S ( F ` C ) ) ) ) )
23 22 imbi2d 
 |-  ( y = C -> ( ( B e. A -> ( ( ( ph /\ B e. A ) /\ y e. A ) -> ( B R y -> ( F ` B ) S ( F ` y ) ) ) ) <-> ( B e. A -> ( ( ( ph /\ B e. A ) /\ C e. A ) -> ( B R C -> ( F ` B ) S ( F ` C ) ) ) ) ) )
24 nfv 
 |-  F/ x B e. A
25 1 24 nfan 
 |-  F/ x ( ph /\ B e. A )
26 nfv 
 |-  F/ x y e. A
27 25 26 nfan 
 |-  F/ x ( ( ph /\ B e. A ) /\ y e. A )
28 nfv 
 |-  F/ x ( B R y -> ( F ` B ) S ( F ` y ) )
29 27 28 nfim 
 |-  F/ x ( ( ( ph /\ B e. A ) /\ y e. A ) -> ( B R y -> ( F ` B ) S ( F ` y ) ) )
30 eleq1 
 |-  ( x = B -> ( x e. A <-> B e. A ) )
31 30 anbi2d 
 |-  ( x = B -> ( ( ph /\ x e. A ) <-> ( ph /\ B e. A ) ) )
32 31 anbi1d 
 |-  ( x = B -> ( ( ( ph /\ x e. A ) /\ y e. A ) <-> ( ( ph /\ B e. A ) /\ y e. A ) ) )
33 breq1 
 |-  ( x = B -> ( x R y <-> B R y ) )
34 fveq2 
 |-  ( x = B -> ( F ` x ) = ( F ` B ) )
35 34 breq1d 
 |-  ( x = B -> ( ( F ` x ) S ( F ` y ) <-> ( F ` B ) S ( F ` y ) ) )
36 33 35 imbi12d 
 |-  ( x = B -> ( ( x R y -> ( F ` x ) S ( F ` y ) ) <-> ( B R y -> ( F ` B ) S ( F ` y ) ) ) )
37 32 36 imbi12d 
 |-  ( x = B -> ( ( ( ( ph /\ x e. A ) /\ y e. A ) -> ( x R y -> ( F ` x ) S ( F ` y ) ) ) <-> ( ( ( ph /\ B e. A ) /\ y e. A ) -> ( B R y -> ( F ` B ) S ( F ` y ) ) ) ) )
38 3 r19.21bi 
 |-  ( ( ph /\ x e. A ) -> A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) )
39 38 r19.21bi 
 |-  ( ( ( ph /\ x e. A ) /\ y e. A ) -> ( x R y -> ( F ` x ) S ( F ` y ) ) )
40 29 37 39 vtoclg1f 
 |-  ( B e. A -> ( ( ( ph /\ B e. A ) /\ y e. A ) -> ( B R y -> ( F ` B ) S ( F ` y ) ) ) )
41 15 23 40 vtoclg1f 
 |-  ( C e. A -> ( B e. A -> ( ( ( ph /\ B e. A ) /\ C e. A ) -> ( B R C -> ( F ` B ) S ( F ` C ) ) ) ) )
42 5 4 41 sylc 
 |-  ( ph -> ( ( ( ph /\ B e. A ) /\ C e. A ) -> ( B R C -> ( F ` B ) S ( F ` C ) ) ) )
43 8 6 42 mp2d 
 |-  ( ph -> ( F ` B ) S ( F ` C ) )