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

Metamath Proof Explorer

Theorem offveqb

Description: Equivalent expressions for equality with a function operation. (Contributed by NM, 9-Oct-2014) (Proof shortened by Mario Carneiro, 5-Dec-2016)

Ref Expression
Hypotheses offveq.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
offveq.2 ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
offveq.3 ⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
offveq.4 ⊢ ( 𝜑 → 𝐻 Fn 𝐴 )
offveq.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
offveq.6 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = 𝐶 )
Assertion offveqb ( 𝜑 → ( 𝐻 = ( 𝐹 ∘f 𝑅 𝐺 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = ( 𝐵 𝑅 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 offveq.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 offveq.2 ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
3 offveq.3 ⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
4 offveq.4 ⊢ ( 𝜑 → 𝐻 Fn 𝐴 )
5 offveq.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
6 offveq.6 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = 𝐶 )
7 dffn5 ⊢ ( 𝐻 Fn 𝐴 ↔ 𝐻 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐻 ‘ 𝑥 ) ) )
8 4 7 sylib ⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐻 ‘ 𝑥 ) ) )
9 inidm ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
10 2 3 1 1 9 5 6 offval ⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )
11 8 10 eqeq12d ⊢ ( 𝜑 → ( 𝐻 = ( 𝐹 ∘f 𝑅 𝐺 ) ↔ ( 𝑥 ∈ 𝐴 ↦ ( 𝐻 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) ) )
12 fvexd ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑥 ) ∈ V )
13 12 ralrimivw ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) ∈ V )
14 mpteqb ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) ∈ V → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐻 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = ( 𝐵 𝑅 𝐶 ) ) )
15 13 14 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐻 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = ( 𝐵 𝑅 𝐶 ) ) )
16 11 15 bitrd ⊢ ( 𝜑 → ( 𝐻 = ( 𝐹 ∘f 𝑅 𝐺 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = ( 𝐵 𝑅 𝐶 ) ) )