Metamath Proof Explorer


Theorem caofid2

Description: Transfer a right absorption law to the function operation. (Contributed by Mario Carneiro, 28-Jul-2014)

Ref Expression
Hypotheses caofref.1 ( 𝜑𝐴𝑉 )
caofref.2 ( 𝜑𝐹 : 𝐴𝑆 )
caofid0.3 ( 𝜑𝐵𝑊 )
caofid1.4 ( 𝜑𝐶𝑋 )
caofid2.5 ( ( 𝜑𝑥𝑆 ) → ( 𝐵 𝑅 𝑥 ) = 𝐶 )
Assertion caofid2 ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f 𝑅 𝐹 ) = ( 𝐴 × { 𝐶 } ) )

Proof

Step Hyp Ref Expression
1 caofref.1 ( 𝜑𝐴𝑉 )
2 caofref.2 ( 𝜑𝐹 : 𝐴𝑆 )
3 caofid0.3 ( 𝜑𝐵𝑊 )
4 caofid1.4 ( 𝜑𝐶𝑋 )
5 caofid2.5 ( ( 𝜑𝑥𝑆 ) → ( 𝐵 𝑅 𝑥 ) = 𝐶 )
6 fnconstg ( 𝐵𝑊 → ( 𝐴 × { 𝐵 } ) Fn 𝐴 )
7 3 6 syl ( 𝜑 → ( 𝐴 × { 𝐵 } ) Fn 𝐴 )
8 2 ffnd ( 𝜑𝐹 Fn 𝐴 )
9 fnconstg ( 𝐶𝑋 → ( 𝐴 × { 𝐶 } ) Fn 𝐴 )
10 4 9 syl ( 𝜑 → ( 𝐴 × { 𝐶 } ) Fn 𝐴 )
11 fvconst2g ( ( 𝐵𝑊𝑤𝐴 ) → ( ( 𝐴 × { 𝐵 } ) ‘ 𝑤 ) = 𝐵 )
12 3 11 sylan ( ( 𝜑𝑤𝐴 ) → ( ( 𝐴 × { 𝐵 } ) ‘ 𝑤 ) = 𝐵 )
13 eqidd ( ( 𝜑𝑤𝐴 ) → ( 𝐹𝑤 ) = ( 𝐹𝑤 ) )
14 5 ralrimiva ( 𝜑 → ∀ 𝑥𝑆 ( 𝐵 𝑅 𝑥 ) = 𝐶 )
15 2 ffvelrnda ( ( 𝜑𝑤𝐴 ) → ( 𝐹𝑤 ) ∈ 𝑆 )
16 oveq2 ( 𝑥 = ( 𝐹𝑤 ) → ( 𝐵 𝑅 𝑥 ) = ( 𝐵 𝑅 ( 𝐹𝑤 ) ) )
17 16 eqeq1d ( 𝑥 = ( 𝐹𝑤 ) → ( ( 𝐵 𝑅 𝑥 ) = 𝐶 ↔ ( 𝐵 𝑅 ( 𝐹𝑤 ) ) = 𝐶 ) )
18 17 rspccva ( ( ∀ 𝑥𝑆 ( 𝐵 𝑅 𝑥 ) = 𝐶 ∧ ( 𝐹𝑤 ) ∈ 𝑆 ) → ( 𝐵 𝑅 ( 𝐹𝑤 ) ) = 𝐶 )
19 14 15 18 syl2an2r ( ( 𝜑𝑤𝐴 ) → ( 𝐵 𝑅 ( 𝐹𝑤 ) ) = 𝐶 )
20 fvconst2g ( ( 𝐶𝑋𝑤𝐴 ) → ( ( 𝐴 × { 𝐶 } ) ‘ 𝑤 ) = 𝐶 )
21 4 20 sylan ( ( 𝜑𝑤𝐴 ) → ( ( 𝐴 × { 𝐶 } ) ‘ 𝑤 ) = 𝐶 )
22 19 21 eqtr4d ( ( 𝜑𝑤𝐴 ) → ( 𝐵 𝑅 ( 𝐹𝑤 ) ) = ( ( 𝐴 × { 𝐶 } ) ‘ 𝑤 ) )
23 1 7 8 10 12 13 22 offveq ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f 𝑅 𝐹 ) = ( 𝐴 × { 𝐶 } ) )