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 nfmpt1 ⊢ Ⅎ _ x x ∈ A ⟼ C
3 1 2 nfcxfr ⊢ Ⅎ _ x F
4 3 dffo3f ⊢ F : A ⟶ onto B ↔ F : A ⟶ B ∧ ∀ y ∈ B ∃ x ∈ A y = F ⁡ x
5 4 simplbi ⊢ F : A ⟶ onto B → F : A ⟶ B
6 1 fmpt ⊢ ∀ x ∈ A C ∈ B ↔ F : A ⟶ B
7 6 bicomi ⊢ F : A ⟶ B ↔ ∀ x ∈ A C ∈ B
8 7 biimpi ⊢ F : A ⟶ B → ∀ x ∈ A C ∈ B
9 5 8 syl ⊢ F : A ⟶ onto B → ∀ x ∈ A C ∈ B
10 3 foelrnf ⊢ F : A ⟶ onto B ∧ y ∈ B → ∃ x ∈ A y = F ⁡ x
11 nfcv ⊢ Ⅎ _ x A
12 nfcv ⊢ Ⅎ _ x B
13 3 11 12 nffo ⊢ Ⅎ x F : A ⟶ onto B
14 simpr ⊢ F : A ⟶ onto B ∧ x ∈ A ∧ y = F ⁡ x → y = F ⁡ x
15 simpr ⊢ F : A ⟶ onto B ∧ x ∈ A → x ∈ A
16 9 r19.21bi ⊢ F : A ⟶ onto B ∧ x ∈ A → C ∈ B
17 1 fvmpt2 ⊢ x ∈ A ∧ C ∈ B → F ⁡ x = C
18 15 16 17 syl2anc ⊢ F : A ⟶ onto B ∧ x ∈ A → F ⁡ x = C
19 18 adantr ⊢ F : A ⟶ onto B ∧ x ∈ A ∧ y = F ⁡ x → F ⁡ x = C
20 14 19 eqtrd ⊢ F : A ⟶ onto B ∧ x ∈ A ∧ y = F ⁡ x → y = C
21 20 ex ⊢ F : A ⟶ onto B ∧ x ∈ A → y = F ⁡ x → y = C
22 21 ex ⊢ F : A ⟶ onto B → x ∈ A → y = F ⁡ x → y = C
23 13 22 reximdai ⊢ F : A ⟶ onto B → ∃ x ∈ A y = F ⁡ x → ∃ x ∈ A y = C
24 23 adantr ⊢ F : A ⟶ onto B ∧ y ∈ B → ∃ x ∈ A y = F ⁡ x → ∃ x ∈ A y = C
25 10 24 mpd ⊢ F : A ⟶ onto B ∧ y ∈ B → ∃ x ∈ A y = C
26 25 ralrimiva ⊢ F : A ⟶ onto B → ∀ y ∈ B ∃ x ∈ A y = C
27 9 26 jca ⊢ F : A ⟶ onto B → ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C
28 6 biimpi ⊢ ∀ x ∈ A C ∈ B → F : A ⟶ B
29 28 adantr ⊢ ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C → F : A ⟶ B
30 nfv ⊢ Ⅎ y ∀ x ∈ A C ∈ B
31 nfra1 ⊢ Ⅎ y ∀ y ∈ B ∃ x ∈ A y = C
32 30 31 nfan ⊢ Ⅎ y ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C
33 simpll ⊢ ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C ∧ y ∈ B → ∀ x ∈ A C ∈ B
34 rspa ⊢ ∀ y ∈ B ∃ x ∈ A y = C ∧ y ∈ B → ∃ x ∈ A y = C
35 34 adantll ⊢ ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C ∧ y ∈ B → ∃ x ∈ A y = C
36 nfra1 ⊢ Ⅎ x ∀ x ∈ A C ∈ B
37 simp3 ⊢ ∀ x ∈ A C ∈ B ∧ x ∈ A ∧ y = C → y = C
38 simpr ⊢ ∀ x ∈ A C ∈ B ∧ x ∈ A → x ∈ A
39 rspa ⊢ ∀ x ∈ A C ∈ B ∧ x ∈ A → C ∈ B
40 38 39 17 syl2anc ⊢ ∀ x ∈ A C ∈ B ∧ x ∈ A → F ⁡ x = C
41 40 eqcomd ⊢ ∀ x ∈ A C ∈ B ∧ x ∈ A → C = F ⁡ x
42 41 3adant3 ⊢ ∀ x ∈ A C ∈ B ∧ x ∈ A ∧ y = C → C = F ⁡ x
43 37 42 eqtrd ⊢ ∀ x ∈ A C ∈ B ∧ x ∈ A ∧ y = C → y = F ⁡ x
44 43 3exp ⊢ ∀ x ∈ A C ∈ B → x ∈ A → y = C → y = F ⁡ x
45 36 44 reximdai ⊢ ∀ x ∈ A C ∈ B → ∃ x ∈ A y = C → ∃ x ∈ A y = F ⁡ x
46 45 imp ⊢ ∀ x ∈ A C ∈ B ∧ ∃ x ∈ A y = C → ∃ x ∈ A y = F ⁡ x
47 33 35 46 syl2anc ⊢ ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C ∧ y ∈ B → ∃ x ∈ A y = F ⁡ x
48 47 ex ⊢ ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C → y ∈ B → ∃ x ∈ A y = F ⁡ x
49 32 48 ralrimi ⊢ ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C → ∀ y ∈ B ∃ x ∈ A y = F ⁡ x
50 29 49 jca ⊢ ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C → F : A ⟶ B ∧ ∀ y ∈ B ∃ x ∈ A y = F ⁡ x
51 50 4 sylibr ⊢ ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C → F : A ⟶ onto B
52 27 51 impbii ⊢ F : A ⟶ onto B ↔ ∀ x ∈ A C ∈ B ∧ ∀ y ∈ B ∃ x ∈ A y = C