Metamath Proof Explorer

Theorem fconst3

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

Ref Expression
Assertion fconst3 ⊢ F : A ⟶ B ↔ F Fn A ∧ A ⊆ F -1 B

Proof

Step Hyp Ref Expression
1 fconstfv ⊢ F : A ⟶ B ↔ F Fn A ∧ ∀ x ∈ A F ⁡ x = B
2 fnfun ⊢ F Fn A → Fun ⁡ F
3 fndm ⊢ F Fn A → dom ⁡ F = A
4 eqimss2 ⊢ dom ⁡ F = A → A ⊆ dom ⁡ F
5 3 4 syl ⊢ F Fn A → A ⊆ dom ⁡ F
6 funconstss ⊢ Fun ⁡ F ∧ A ⊆ dom ⁡ F → ∀ x ∈ A F ⁡ x = B ↔ A ⊆ F -1 B
7 2 5 6 syl2anc ⊢ F Fn A → ∀ x ∈ A F ⁡ x = B ↔ A ⊆ F -1 B
8 7 pm5.32i ⊢ F Fn A ∧ ∀ x ∈ A F ⁡ x = B ↔ F Fn A ∧ A ⊆ F -1 B
9 1 8 bitri ⊢ F : A ⟶ B ↔ F Fn A ∧ A ⊆ F -1 B