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 biimpi ⊢ ∀ x ∈ A C ∈ B → F : A ⟶ B
25 24 adantr ⊢ ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C → F : A ⟶ B
26 nfv ⊢ Ⅎ y ∀ x ∈ A C ∈ B
27 nfra1 ⊢ Ⅎ y ∀ y ∈ B ∃ x ∈ A y = C
28 26 27 nfan ⊢ Ⅎ y ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C
29 simpll ⊢ ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C ∧ y ∈ B → ∀ x ∈ A C ∈ B
30 rspa ⊢ ∀ y ∈ B ∃ x ∈ A y = C ∧ y ∈ B → ∃ x ∈ A y = C
31 30 adantll ⊢ ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C ∧ y ∈ B → ∃ x ∈ A y = C
32 nfra1 ⊢ Ⅎ x ∀ x ∈ A C ∈ B
33 simp3 ⊢ ∀ x ∈ A C ∈ B ∧ x ∈ A ∧ y = C → y = C
34 simpr ⊢ ∀ x ∈ A C ∈ B ∧ x ∈ A → x ∈ A
35 rspa ⊢ ∀ x ∈ A C ∈ B ∧ x ∈ A → C ∈ B
36 34 35 14 syl2anc ⊢ ∀ x ∈ A C ∈ B ∧ x ∈ A → F ⁡ x = C
37 36 eqcomd ⊢ ∀ x ∈ A C ∈ B ∧ x ∈ A → C = F ⁡ x
38 37 3adant3 ⊢ ∀ x ∈ A C ∈ B ∧ x ∈ A ∧ y = C → C = F ⁡ x
39 33 38 eqtrd ⊢ ∀ x ∈ A C ∈ B ∧ x ∈ A ∧ y = C → y = F ⁡ x
40 39 3exp ⊢ ∀ x ∈ A C ∈ B → x ∈ A → y = C → y = F ⁡ x
41 32 40 reximdai ⊢ ∀ x ∈ A C ∈ B → ∃ x ∈ A y = C → ∃ x ∈ A y = F ⁡ x
42 29 31 41 sylc ⊢ ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C ∧ y ∈ B → ∃ x ∈ A y = F ⁡ x
43 28 42 ralrimia ⊢ ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C → ∀ y ∈ B ∃ x ∈ A y = F ⁡ x
44 6 dffo3f ⊢ F : A ⟶ onto B ↔ F : A ⟶ B ∧ ∀ y ∈ B ∃ x ∈ A y = F ⁡ x
45 25 43 44 sylanbrc ⊢ ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C → F : A ⟶ onto B
46 23 45 impbii ⊢ F : A ⟶ onto B ↔ ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C