This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem caofid0r

Description: Transfer a right identity law to the function operation. (Contributed by NM, 21-Oct-2014)

Ref Expression
Hypotheses caofref.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
caofref.2 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
caofid0.3 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
caofid0r.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 𝑅 𝐵 ) = 𝑥 )
Assertion caofid0r ( 𝜑 → ( 𝐹 ∘f 𝑅 ( 𝐴 × { 𝐵 } ) ) = 𝐹 )

Proof

Step Hyp Ref Expression
1 caofref.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 caofref.2 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
3 caofid0.3 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
4 caofid0r.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 𝑅 𝐵 ) = 𝑥 )
5 2 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
6 fnconstg ⊢ ( 𝐵 ∈ 𝑊 → ( 𝐴 × { 𝐵 } ) Fn 𝐴 )
7 3 6 syl ⊢ ( 𝜑 → ( 𝐴 × { 𝐵 } ) Fn 𝐴 )
8 eqidd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) )
9 fvconst2g ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐴 × { 𝐵 } ) ‘ 𝑤 ) = 𝐵 )
10 3 9 sylan ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐴 × { 𝐵 } ) ‘ 𝑤 ) = 𝐵 )
11 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ( 𝑥 𝑅 𝐵 ) = 𝑥 )
12 2 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 )
13 oveq1 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → ( 𝑥 𝑅 𝐵 ) = ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝐵 ) )
14 id ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → 𝑥 = ( 𝐹 ‘ 𝑤 ) )
15 13 14 eqeq12d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → ( ( 𝑥 𝑅 𝐵 ) = 𝑥 ↔ ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝐵 ) = ( 𝐹 ‘ 𝑤 ) ) )
16 15 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝑆 ( 𝑥 𝑅 𝐵 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝐵 ) = ( 𝐹 ‘ 𝑤 ) )
17 11 12 16 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝐵 ) = ( 𝐹 ‘ 𝑤 ) )
18 1 5 7 5 8 10 17 offveq ⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 ( 𝐴 × { 𝐵 } ) ) = 𝐹 )