Theorem fconst3

Description: Two ways to express a constant function. (Contributed by NM, 15-Mar-2007)

	Ref	Expression
Assertion	fconst3	⊢ ( 𝐹 : 𝐴 ⟶ { 𝐵 } ↔ ( 𝐹 Fn 𝐴 ∧ 𝐴 ⊆ ( ◡ 𝐹 “ { 𝐵 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		fconstfv	⊢ ( 𝐹 : 𝐴 ⟶ { 𝐵 } ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐵 ) )
2		fnfun	⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
3		fndm	⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
4		eqimss2	⊢ ( dom 𝐹 = 𝐴 → 𝐴 ⊆ dom 𝐹 )
5	3 4	syl	⊢ ( 𝐹 Fn 𝐴 → 𝐴 ⊆ dom 𝐹 )
6		funconstss	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐵 ↔ 𝐴 ⊆ ( ◡ 𝐹 “ { 𝐵 } ) ) )
7	2 5 6	syl2anc	⊢ ( 𝐹 Fn 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐵 ↔ 𝐴 ⊆ ( ◡ 𝐹 “ { 𝐵 } ) ) )
8	7	pm5.32i	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐵 ) ↔ ( 𝐹 Fn 𝐴 ∧ 𝐴 ⊆ ( ◡ 𝐹 “ { 𝐵 } ) ) )
9	1 8	bitri	⊢ ( 𝐹 : 𝐴 ⟶ { 𝐵 } ↔ ( 𝐹 Fn 𝐴 ∧ 𝐴 ⊆ ( ◡ 𝐹 “ { 𝐵 } ) ) )