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

Metamath Proof Explorer

Theorem fconst2g

Description: A constant function expressed as a Cartesian product. (Contributed by NM, 27-Nov-2007)

Ref Expression
Assertion fconst2g ( 𝐵 ∈ 𝐶 → ( 𝐹 : 𝐴 ⟶ { 𝐵 } ↔ 𝐹 = ( 𝐴 × { 𝐵 } ) ) )

Proof

Step Hyp Ref Expression
1 fvconst ⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
2 1 adantlr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ 𝐵 ∈ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
3 fvconst2g ⊢ ( ( 𝐵 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 × { 𝐵 } ) ‘ 𝑥 ) = 𝐵 )
4 3 adantll ⊢ ( ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ 𝐵 ∈ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 × { 𝐵 } ) ‘ 𝑥 ) = 𝐵 )
5 2 4 eqtr4d ⊢ ( ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ 𝐵 ∈ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( ( 𝐴 × { 𝐵 } ) ‘ 𝑥 ) )
6 5 ralrimiva ⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ 𝐵 ∈ 𝐶 ) → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( ( 𝐴 × { 𝐵 } ) ‘ 𝑥 ) )
7 ffn ⊢ ( 𝐹 : 𝐴 ⟶ { 𝐵 } → 𝐹 Fn 𝐴 )
8 fnconstg ⊢ ( 𝐵 ∈ 𝐶 → ( 𝐴 × { 𝐵 } ) Fn 𝐴 )
9 eqfnfv ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝐴 × { 𝐵 } ) Fn 𝐴 ) → ( 𝐹 = ( 𝐴 × { 𝐵 } ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( ( 𝐴 × { 𝐵 } ) ‘ 𝑥 ) ) )
10 7 8 9 syl2an ⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ 𝐵 ∈ 𝐶 ) → ( 𝐹 = ( 𝐴 × { 𝐵 } ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( ( 𝐴 × { 𝐵 } ) ‘ 𝑥 ) ) )
11 6 10 mpbird ⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ 𝐵 ∈ 𝐶 ) → 𝐹 = ( 𝐴 × { 𝐵 } ) )
12 11 expcom ⊢ ( 𝐵 ∈ 𝐶 → ( 𝐹 : 𝐴 ⟶ { 𝐵 } → 𝐹 = ( 𝐴 × { 𝐵 } ) ) )
13 fconstg ⊢ ( 𝐵 ∈ 𝐶 → ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ { 𝐵 } )
14 feq1 ⊢ ( 𝐹 = ( 𝐴 × { 𝐵 } ) → ( 𝐹 : 𝐴 ⟶ { 𝐵 } ↔ ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ { 𝐵 } ) )
15 13 14 syl5ibrcom ⊢ ( 𝐵 ∈ 𝐶 → ( 𝐹 = ( 𝐴 × { 𝐵 } ) → 𝐹 : 𝐴 ⟶ { 𝐵 } ) )
16 12 15 impbid ⊢ ( 𝐵 ∈ 𝐶 → ( 𝐹 : 𝐴 ⟶ { 𝐵 } ↔ 𝐹 = ( 𝐴 × { 𝐵 } ) ) )