Metamath Proof Explorer

Theorem dffo3

Description: An onto mapping expressed in terms of function values. (Contributed by NM, 29-Oct-2006)

Ref Expression
Assertion dffo3 ⊢F:A⟶ontoB↔F:A⟶B∧∀y∈B∃x∈Ay=F⁡x

Proof

Step Hyp Ref Expression
1 dffo2 ⊢F:A⟶ontoB↔F:A⟶B∧ran⁡F=B
2 ffn ⊢F:A⟶B→FFnA
3 fnrnfv ⊢FFnA→ran⁡F=y|∃x∈Ay=F⁡x
4 3 eqeq1d ⊢FFnA→ran⁡F=B↔y|∃x∈Ay=F⁡x=B
5 2 4 syl ⊢F:A⟶B→ran⁡F=B↔y|∃x∈Ay=F⁡x=B
6 dfbi2 ⊢∃x∈Ay=F⁡x↔y∈B↔∃x∈Ay=F⁡x→y∈B∧y∈B→∃x∈Ay=F⁡x
7 simpr ⊢F:A⟶B∧x∈A∧y=F⁡x→y=F⁡x
8 ffvelcdm ⊢F:A⟶B∧x∈A→F⁡x∈B
9 8 adantr ⊢F:A⟶B∧x∈A∧y=F⁡x→F⁡x∈B
10 7 9 eqeltrd ⊢F:A⟶B∧x∈A∧y=F⁡x→y∈B
11 10 rexlimdva2 ⊢F:A⟶B→∃x∈Ay=F⁡x→y∈B
12 11 biantrurd ⊢F:A⟶B→y∈B→∃x∈Ay=F⁡x↔∃x∈Ay=F⁡x→y∈B∧y∈B→∃x∈Ay=F⁡x
13 6 12 bitr4id ⊢F:A⟶B→∃x∈Ay=F⁡x↔y∈B↔y∈B→∃x∈Ay=F⁡x
14 13 albidv ⊢F:A⟶B→∀y∃x∈Ay=F⁡x↔y∈B↔∀yy∈B→∃x∈Ay=F⁡x
15 eqabcb ⊢y|∃x∈Ay=F⁡x=B↔∀y∃x∈Ay=F⁡x↔y∈B
16 df-ral ⊢∀y∈B∃x∈Ay=F⁡x↔∀yy∈B→∃x∈Ay=F⁡x
17 14 15 16 3bitr4g ⊢F:A⟶B→y|∃x∈Ay=F⁡x=B↔∀y∈B∃x∈Ay=F⁡x
18 5 17 bitrd ⊢F:A⟶B→ran⁡F=B↔∀y∈B∃x∈Ay=F⁡x
19 18 pm5.32i ⊢F:A⟶B∧ran⁡F=B↔F:A⟶B∧∀y∈B∃x∈Ay=F⁡x
20 1 19 bitri ⊢F:A⟶ontoB↔F:A⟶B∧∀y∈B∃x∈Ay=F⁡x