Metamath Proof Explorer


Theorem dmrelrnrel

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

Ref Expression
Hypotheses dmrelrnrel.x 𝑥 𝜑
dmrelrnrel.y 𝑦 𝜑
dmrelrnrel.i ( 𝜑 → ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹𝑥 ) 𝑆 ( 𝐹𝑦 ) ) )
dmrelrnrel.b ( 𝜑𝐵𝐴 )
dmrelrnrel.c ( 𝜑𝐶𝐴 )
dmrelrnrel.r ( 𝜑𝐵 𝑅 𝐶 )
Assertion dmrelrnrel ( 𝜑 → ( 𝐹𝐵 ) 𝑆 ( 𝐹𝐶 ) )

Proof

Step Hyp Ref Expression
1 dmrelrnrel.x 𝑥 𝜑
2 dmrelrnrel.y 𝑦 𝜑
3 dmrelrnrel.i ( 𝜑 → ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹𝑥 ) 𝑆 ( 𝐹𝑦 ) ) )
4 dmrelrnrel.b ( 𝜑𝐵𝐴 )
5 dmrelrnrel.c ( 𝜑𝐶𝐴 )
6 dmrelrnrel.r ( 𝜑𝐵 𝑅 𝐶 )
7 id ( 𝜑𝜑 )
8 7 4 5 jca31 ( 𝜑 → ( ( 𝜑𝐵𝐴 ) ∧ 𝐶𝐴 ) )
9 nfv 𝑦 𝐵𝐴
10 2 9 nfan 𝑦 ( 𝜑𝐵𝐴 )
11 nfv 𝑦 𝐶𝐴
12 10 11 nfan 𝑦 ( ( 𝜑𝐵𝐴 ) ∧ 𝐶𝐴 )
13 nfv 𝑦 ( 𝐵 𝑅 𝐶 → ( 𝐹𝐵 ) 𝑆 ( 𝐹𝐶 ) )
14 12 13 nfim 𝑦 ( ( ( 𝜑𝐵𝐴 ) ∧ 𝐶𝐴 ) → ( 𝐵 𝑅 𝐶 → ( 𝐹𝐵 ) 𝑆 ( 𝐹𝐶 ) ) )
15 9 14 nfim 𝑦 ( 𝐵𝐴 → ( ( ( 𝜑𝐵𝐴 ) ∧ 𝐶𝐴 ) → ( 𝐵 𝑅 𝐶 → ( 𝐹𝐵 ) 𝑆 ( 𝐹𝐶 ) ) ) )
16 eleq1 ( 𝑦 = 𝐶 → ( 𝑦𝐴𝐶𝐴 ) )
17 16 anbi2d ( 𝑦 = 𝐶 → ( ( ( 𝜑𝐵𝐴 ) ∧ 𝑦𝐴 ) ↔ ( ( 𝜑𝐵𝐴 ) ∧ 𝐶𝐴 ) ) )
18 breq2 ( 𝑦 = 𝐶 → ( 𝐵 𝑅 𝑦𝐵 𝑅 𝐶 ) )
19 fveq2 ( 𝑦 = 𝐶 → ( 𝐹𝑦 ) = ( 𝐹𝐶 ) )
20 19 breq2d ( 𝑦 = 𝐶 → ( ( 𝐹𝐵 ) 𝑆 ( 𝐹𝑦 ) ↔ ( 𝐹𝐵 ) 𝑆 ( 𝐹𝐶 ) ) )
21 18 20 imbi12d ( 𝑦 = 𝐶 → ( ( 𝐵 𝑅 𝑦 → ( 𝐹𝐵 ) 𝑆 ( 𝐹𝑦 ) ) ↔ ( 𝐵 𝑅 𝐶 → ( 𝐹𝐵 ) 𝑆 ( 𝐹𝐶 ) ) ) )
22 17 21 imbi12d ( 𝑦 = 𝐶 → ( ( ( ( 𝜑𝐵𝐴 ) ∧ 𝑦𝐴 ) → ( 𝐵 𝑅 𝑦 → ( 𝐹𝐵 ) 𝑆 ( 𝐹𝑦 ) ) ) ↔ ( ( ( 𝜑𝐵𝐴 ) ∧ 𝐶𝐴 ) → ( 𝐵 𝑅 𝐶 → ( 𝐹𝐵 ) 𝑆 ( 𝐹𝐶 ) ) ) ) )
23 22 imbi2d ( 𝑦 = 𝐶 → ( ( 𝐵𝐴 → ( ( ( 𝜑𝐵𝐴 ) ∧ 𝑦𝐴 ) → ( 𝐵 𝑅 𝑦 → ( 𝐹𝐵 ) 𝑆 ( 𝐹𝑦 ) ) ) ) ↔ ( 𝐵𝐴 → ( ( ( 𝜑𝐵𝐴 ) ∧ 𝐶𝐴 ) → ( 𝐵 𝑅 𝐶 → ( 𝐹𝐵 ) 𝑆 ( 𝐹𝐶 ) ) ) ) ) )
24 nfv 𝑥 𝐵𝐴
25 1 24 nfan 𝑥 ( 𝜑𝐵𝐴 )
26 nfv 𝑥 𝑦𝐴
27 25 26 nfan 𝑥 ( ( 𝜑𝐵𝐴 ) ∧ 𝑦𝐴 )
28 nfv 𝑥 ( 𝐵 𝑅 𝑦 → ( 𝐹𝐵 ) 𝑆 ( 𝐹𝑦 ) )
29 27 28 nfim 𝑥 ( ( ( 𝜑𝐵𝐴 ) ∧ 𝑦𝐴 ) → ( 𝐵 𝑅 𝑦 → ( 𝐹𝐵 ) 𝑆 ( 𝐹𝑦 ) ) )
30 eleq1 ( 𝑥 = 𝐵 → ( 𝑥𝐴𝐵𝐴 ) )
31 30 anbi2d ( 𝑥 = 𝐵 → ( ( 𝜑𝑥𝐴 ) ↔ ( 𝜑𝐵𝐴 ) ) )
32 31 anbi1d ( 𝑥 = 𝐵 → ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑦𝐴 ) ↔ ( ( 𝜑𝐵𝐴 ) ∧ 𝑦𝐴 ) ) )
33 breq1 ( 𝑥 = 𝐵 → ( 𝑥 𝑅 𝑦𝐵 𝑅 𝑦 ) )
34 fveq2 ( 𝑥 = 𝐵 → ( 𝐹𝑥 ) = ( 𝐹𝐵 ) )
35 34 breq1d ( 𝑥 = 𝐵 → ( ( 𝐹𝑥 ) 𝑆 ( 𝐹𝑦 ) ↔ ( 𝐹𝐵 ) 𝑆 ( 𝐹𝑦 ) ) )
36 33 35 imbi12d ( 𝑥 = 𝐵 → ( ( 𝑥 𝑅 𝑦 → ( 𝐹𝑥 ) 𝑆 ( 𝐹𝑦 ) ) ↔ ( 𝐵 𝑅 𝑦 → ( 𝐹𝐵 ) 𝑆 ( 𝐹𝑦 ) ) ) )
37 32 36 imbi12d ( 𝑥 = 𝐵 → ( ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑦𝐴 ) → ( 𝑥 𝑅 𝑦 → ( 𝐹𝑥 ) 𝑆 ( 𝐹𝑦 ) ) ) ↔ ( ( ( 𝜑𝐵𝐴 ) ∧ 𝑦𝐴 ) → ( 𝐵 𝑅 𝑦 → ( 𝐹𝐵 ) 𝑆 ( 𝐹𝑦 ) ) ) ) )
38 3 r19.21bi ( ( 𝜑𝑥𝐴 ) → ∀ 𝑦𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹𝑥 ) 𝑆 ( 𝐹𝑦 ) ) )
39 38 r19.21bi ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑦𝐴 ) → ( 𝑥 𝑅 𝑦 → ( 𝐹𝑥 ) 𝑆 ( 𝐹𝑦 ) ) )
40 29 37 39 vtoclg1f ( 𝐵𝐴 → ( ( ( 𝜑𝐵𝐴 ) ∧ 𝑦𝐴 ) → ( 𝐵 𝑅 𝑦 → ( 𝐹𝐵 ) 𝑆 ( 𝐹𝑦 ) ) ) )
41 15 23 40 vtoclg1f ( 𝐶𝐴 → ( 𝐵𝐴 → ( ( ( 𝜑𝐵𝐴 ) ∧ 𝐶𝐴 ) → ( 𝐵 𝑅 𝐶 → ( 𝐹𝐵 ) 𝑆 ( 𝐹𝐶 ) ) ) ) )
42 5 4 41 sylc ( 𝜑 → ( ( ( 𝜑𝐵𝐴 ) ∧ 𝐶𝐴 ) → ( 𝐵 𝑅 𝐶 → ( 𝐹𝐵 ) 𝑆 ( 𝐹𝐶 ) ) ) )
43 8 6 42 mp2d ( 𝜑 → ( 𝐹𝐵 ) 𝑆 ( 𝐹𝐶 ) )