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 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) 𝑆 ( 𝐹 ‘ 𝐶 ) )