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

Metamath Proof Explorer

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 𝐴 ∧ ( ◡ 𝐹 “ { 𝐵 } ) = 𝐴 ) )