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	⊢ ( 𝐵 ∈ 𝐶 → ( 𝐹 : 𝐴 ⟶ { 𝐵 } ↔ 𝐹 = ( 𝐴 × { 𝐵 } ) ) )