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⟶ontoB↔∀x∈AC∈B∧∀y∈B∃x∈Ay=C

Proof

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