Metamath Proof Explorer

Theorem fmpt

Description: Functionality of the mapping operation. (Contributed by Mario Carneiro, 26-Jul-2013) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypothesis fmpt.1 ⊢ F = x ∈ A ⟼ C
Assertion fmpt ⊢ ∀ x ∈ A C ∈ B ↔ F : A ⟶ B

Proof

Step Hyp Ref Expression
1 fmpt.1 ⊢ F = x ∈ A ⟼ C
2 1 fnmpt ⊢ ∀ x ∈ A C ∈ B → F Fn A
3 1 rnmpt ⊢ ran ⁡ F = y | ∃ x ∈ A y = C
4 r19.29 ⊢ ∀ x ∈ A C ∈ B ∧ ∃ x ∈ A y = C → ∃ x ∈ A C ∈ B ∧ y = C
5 eleq1 ⊢ y = C → y ∈ B ↔ C ∈ B
6 5 biimparc ⊢ C ∈ B ∧ y = C → y ∈ B
7 6 rexlimivw ⊢ ∃ x ∈ A C ∈ B ∧ y = C → y ∈ B
8 4 7 syl ⊢ ∀ x ∈ A C ∈ B ∧ ∃ x ∈ A y = C → y ∈ B
9 8 ex ⊢ ∀ x ∈ A C ∈ B → ∃ x ∈ A y = C → y ∈ B
10 9 abssdv ⊢ ∀ x ∈ A C ∈ B → y | ∃ x ∈ A y = C ⊆ B
11 3 10 eqsstrid ⊢ ∀ x ∈ A C ∈ B → ran ⁡ F ⊆ B
12 df-f ⊢ F : A ⟶ B ↔ F Fn A ∧ ran ⁡ F ⊆ B
13 2 11 12 sylanbrc ⊢ ∀ x ∈ A C ∈ B → F : A ⟶ B
14 1 mptpreima ⊢ F -1 B = x ∈ A | C ∈ B
15 fimacnv ⊢ F : A ⟶ B → F -1 B = A
16 14 15 syl5reqr ⊢ F : A ⟶ B → A = x ∈ A | C ∈ B
17 rabid2 ⊢ A = x ∈ A | C ∈ B ↔ ∀ x ∈ A C ∈ B
18 16 17 sylib ⊢ F : A ⟶ B → ∀ x ∈ A C ∈ B
19 13 18 impbii ⊢ ∀ x ∈ A C ∈ B ↔ F : A ⟶ B