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

Metamath Proof Explorer

Theorem caofid0l

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

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

Proof

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