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 ) )