Theorem fconst4

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

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

Proof

Step	Hyp	Ref	Expression
1		fconst3	⊢ ( 𝐹 : 𝐴 ⟶ { 𝐵 } ↔ ( 𝐹 Fn 𝐴 ∧ 𝐴 ⊆ ( ◡ 𝐹 “ { 𝐵 } ) ) )
2		cnvimass	⊢ ( ◡ 𝐹 “ { 𝐵 } ) ⊆ dom 𝐹
3		fndm	⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
4	2 3	sseqtrid	⊢ ( 𝐹 Fn 𝐴 → ( ◡ 𝐹 “ { 𝐵 } ) ⊆ 𝐴 )
5	4	biantrurd	⊢ ( 𝐹 Fn 𝐴 → ( 𝐴 ⊆ ( ◡ 𝐹 “ { 𝐵 } ) ↔ ( ( ◡ 𝐹 “ { 𝐵 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ◡ 𝐹 “ { 𝐵 } ) ) ) )
6		eqss	⊢ ( ( ◡ 𝐹 “ { 𝐵 } ) = 𝐴 ↔ ( ( ◡ 𝐹 “ { 𝐵 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ◡ 𝐹 “ { 𝐵 } ) ) )
7	5 6	bitr4di	⊢ ( 𝐹 Fn 𝐴 → ( 𝐴 ⊆ ( ◡ 𝐹 “ { 𝐵 } ) ↔ ( ◡ 𝐹 “ { 𝐵 } ) = 𝐴 ) )
8	7	pm5.32i	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ⊆ ( ◡ 𝐹 “ { 𝐵 } ) ) ↔ ( 𝐹 Fn 𝐴 ∧ ( ◡ 𝐹 “ { 𝐵 } ) = 𝐴 ) )
9	1 8	bitri	⊢ ( 𝐹 : 𝐴 ⟶ { 𝐵 } ↔ ( 𝐹 Fn 𝐴 ∧ ( ◡ 𝐹 “ { 𝐵 } ) = 𝐴 ) )