Metamath Proof Explorer

Theorem fompt

Description: Express being onto for a mapping operation. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypothesis fompt.1 ⊢ F = x ∈ A ⟼ C
Assertion fompt ⊢ F : A ⟶ onto B ↔ ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C

Proof

Step Hyp Ref Expression
1 fompt.1 ⊢ F = x ∈ A ⟼ C
2 fof ⊢ F : A ⟶ onto B → F : A ⟶ B
3 1 fmpt ⊢ ∀ x ∈ A C ∈ B ↔ F : A ⟶ B
4 2 3 sylibr ⊢ F : A ⟶ onto B → ∀ x ∈ A C ∈ B
5 nfmpt1 ⊢ Ⅎ _ x x ∈ A ⟼ C
6 1 5 nfcxfr ⊢ Ⅎ _ x F
7 6 foelrnf ⊢ F : A ⟶ onto B ∧ y ∈ B → ∃ x ∈ A y = F ⁡ x
8 nfcv ⊢ Ⅎ _ x A
9 nfcv ⊢ Ⅎ _ x B
10 6 8 9 nffo ⊢ Ⅎ x F : A ⟶ onto B
11 simpr ⊢ F : A ⟶ onto B ∧ x ∈ A ∧ y = F ⁡ x → y = F ⁡ x
12 simpr ⊢ F : A ⟶ onto B ∧ x ∈ A → x ∈ A
13 4 r19.21bi ⊢ F : A ⟶ onto B ∧ x ∈ A → C ∈ B
14 1 fvmpt2 ⊢ x ∈ A ∧ C ∈ B → F ⁡ x = C
15 12 13 14 syl2anc ⊢ F : A ⟶ onto B ∧ x ∈ A → F ⁡ x = C
16 15 adantr ⊢ F : A ⟶ onto B ∧ x ∈ A ∧ y = F ⁡ x → F ⁡ x = C
17 11 16 eqtrd ⊢ F : A ⟶ onto B ∧ x ∈ A ∧ y = F ⁡ x → y = C
18 17 exp31 ⊢ F : A ⟶ onto B → x ∈ A → y = F ⁡ x → y = C
19 10 18 reximdai ⊢ F : A ⟶ onto B → ∃ x ∈ A y = F ⁡ x → ∃ x ∈ A y = C
20 19 adantr ⊢ F : A ⟶ onto B ∧ y ∈ B → ∃ x ∈ A y = F ⁡ x → ∃ x ∈ A y = C
21 7 20 mpd ⊢ F : A ⟶ onto B ∧ y ∈ B → ∃ x ∈ A y = C
22 21 ralrimiva ⊢ F : A ⟶ onto B → ∀ y ∈ B ∃ x ∈ A y = C
23 4 22 jca ⊢ F : A ⟶ onto B → ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C
24 3 birani ⊢ ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C → F : A ⟶ B
25 nfv ⊢ Ⅎ y ∀ x ∈ A C ∈ B
26 nfra1 ⊢ Ⅎ y ∀ y ∈ B ∃ x ∈ A y = C
27 25 26 nfan ⊢ Ⅎ y ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C
28 simpll ⊢ ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C ∧ y ∈ B → ∀ x ∈ A C ∈ B
29 rspa ⊢ ∀ y ∈ B ∃ x ∈ A y = C ∧ y ∈ B → ∃ x ∈ A y = C
30 29 adantll ⊢ ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C ∧ y ∈ B → ∃ x ∈ A y = C
31 nfra1 ⊢ Ⅎ x ∀ x ∈ A C ∈ B
32 simp3 ⊢ ∀ x ∈ A C ∈ B ∧ x ∈ A ∧ y = C → y = C
33 simpr ⊢ ∀ x ∈ A C ∈ B ∧ x ∈ A → x ∈ A
34 rspa ⊢ ∀ x ∈ A C ∈ B ∧ x ∈ A → C ∈ B
35 33 34 14 syl2anc ⊢ ∀ x ∈ A C ∈ B ∧ x ∈ A → F ⁡ x = C
36 35 eqcomd ⊢ ∀ x ∈ A C ∈ B ∧ x ∈ A → C = F ⁡ x
37 36 3adant3 ⊢ ∀ x ∈ A C ∈ B ∧ x ∈ A ∧ y = C → C = F ⁡ x
38 32 37 eqtrd ⊢ ∀ x ∈ A C ∈ B ∧ x ∈ A ∧ y = C → y = F ⁡ x
39 38 3exp ⊢ ∀ x ∈ A C ∈ B → x ∈ A → y = C → y = F ⁡ x
40 31 39 reximdai ⊢ ∀ x ∈ A C ∈ B → ∃ x ∈ A y = C → ∃ x ∈ A y = F ⁡ x
41 28 30 40 sylc ⊢ ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C ∧ y ∈ B → ∃ x ∈ A y = F ⁡ x
42 27 41 ralrimia ⊢ ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C → ∀ y ∈ B ∃ x ∈ A y = F ⁡ x
43 6 dffo3f ⊢ F : A ⟶ onto B ↔ F : A ⟶ B ∧ ∀ y ∈ B ∃ x ∈ A y = F ⁡ x
44 24 42 43 sylanbrc ⊢ ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C → F : A ⟶ onto B
45 23 44 impbii ⊢ F : A ⟶ onto B ↔ ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C