Metamath Proof Explorer

Theorem fconst4

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

Ref Expression
Assertion fconst4 ⊢ F : A ⟶ B ↔ F Fn A ∧ F -1 B = A

Proof

Step Hyp Ref Expression
1 fconst3 ⊢ F : A ⟶ B ↔ F Fn A ∧ A ⊆ F -1 B
2 cnvimass ⊢ F -1 B ⊆ dom ⁡ F
3 fndm ⊢ F Fn A → dom ⁡ F = A
4 2 3 sseqtrid ⊢ F Fn A → F -1 B ⊆ A
5 4 biantrurd ⊢ F Fn A → A ⊆ F -1 B ↔ F -1 B ⊆ A ∧ A ⊆ F -1 B
6 eqss ⊢ F -1 B = A ↔ F -1 B ⊆ A ∧ A ⊆ F -1 B
7 5 6 bitr4di ⊢ F Fn A → A ⊆ F -1 B ↔ F -1 B = A
8 7 pm5.32i ⊢ F Fn A ∧ A ⊆ F -1 B ↔ F Fn A ∧ F -1 B = A
9 1 8 bitri ⊢ F : A ⟶ B ↔ F Fn A ∧ F -1 B = A