Metamath Proof Explorer


Theorem dffo4

Description: Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007)

Ref Expression
Assertion dffo4 ( 𝐹 : 𝐴onto𝐵 ↔ ( 𝐹 : 𝐴𝐵 ∧ ∀ 𝑦𝐵𝑥𝐴 𝑥 𝐹 𝑦 ) )

Proof

Step Hyp Ref Expression
1 dffo2 ( 𝐹 : 𝐴onto𝐵 ↔ ( 𝐹 : 𝐴𝐵 ∧ ran 𝐹 = 𝐵 ) )
2 simpl ( ( 𝐹 : 𝐴𝐵 ∧ ran 𝐹 = 𝐵 ) → 𝐹 : 𝐴𝐵 )
3 vex 𝑦 ∈ V
4 3 elrn ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑥 𝑥 𝐹 𝑦 )
5 eleq2 ( ran 𝐹 = 𝐵 → ( 𝑦 ∈ ran 𝐹𝑦𝐵 ) )
6 4 5 bitr3id ( ran 𝐹 = 𝐵 → ( ∃ 𝑥 𝑥 𝐹 𝑦𝑦𝐵 ) )
7 6 biimpar ( ( ran 𝐹 = 𝐵𝑦𝐵 ) → ∃ 𝑥 𝑥 𝐹 𝑦 )
8 7 adantll ( ( ( 𝐹 : 𝐴𝐵 ∧ ran 𝐹 = 𝐵 ) ∧ 𝑦𝐵 ) → ∃ 𝑥 𝑥 𝐹 𝑦 )
9 ffn ( 𝐹 : 𝐴𝐵𝐹 Fn 𝐴 )
10 fnbr ( ( 𝐹 Fn 𝐴𝑥 𝐹 𝑦 ) → 𝑥𝐴 )
11 10 ex ( 𝐹 Fn 𝐴 → ( 𝑥 𝐹 𝑦𝑥𝐴 ) )
12 9 11 syl ( 𝐹 : 𝐴𝐵 → ( 𝑥 𝐹 𝑦𝑥𝐴 ) )
13 12 ancrd ( 𝐹 : 𝐴𝐵 → ( 𝑥 𝐹 𝑦 → ( 𝑥𝐴𝑥 𝐹 𝑦 ) ) )
14 13 eximdv ( 𝐹 : 𝐴𝐵 → ( ∃ 𝑥 𝑥 𝐹 𝑦 → ∃ 𝑥 ( 𝑥𝐴𝑥 𝐹 𝑦 ) ) )
15 df-rex ( ∃ 𝑥𝐴 𝑥 𝐹 𝑦 ↔ ∃ 𝑥 ( 𝑥𝐴𝑥 𝐹 𝑦 ) )
16 14 15 syl6ibr ( 𝐹 : 𝐴𝐵 → ( ∃ 𝑥 𝑥 𝐹 𝑦 → ∃ 𝑥𝐴 𝑥 𝐹 𝑦 ) )
17 16 ad2antrr ( ( ( 𝐹 : 𝐴𝐵 ∧ ran 𝐹 = 𝐵 ) ∧ 𝑦𝐵 ) → ( ∃ 𝑥 𝑥 𝐹 𝑦 → ∃ 𝑥𝐴 𝑥 𝐹 𝑦 ) )
18 8 17 mpd ( ( ( 𝐹 : 𝐴𝐵 ∧ ran 𝐹 = 𝐵 ) ∧ 𝑦𝐵 ) → ∃ 𝑥𝐴 𝑥 𝐹 𝑦 )
19 18 ralrimiva ( ( 𝐹 : 𝐴𝐵 ∧ ran 𝐹 = 𝐵 ) → ∀ 𝑦𝐵𝑥𝐴 𝑥 𝐹 𝑦 )
20 2 19 jca ( ( 𝐹 : 𝐴𝐵 ∧ ran 𝐹 = 𝐵 ) → ( 𝐹 : 𝐴𝐵 ∧ ∀ 𝑦𝐵𝑥𝐴 𝑥 𝐹 𝑦 ) )
21 1 20 sylbi ( 𝐹 : 𝐴onto𝐵 → ( 𝐹 : 𝐴𝐵 ∧ ∀ 𝑦𝐵𝑥𝐴 𝑥 𝐹 𝑦 ) )
22 fnbrfvb ( ( 𝐹 Fn 𝐴𝑥𝐴 ) → ( ( 𝐹𝑥 ) = 𝑦𝑥 𝐹 𝑦 ) )
23 22 biimprd ( ( 𝐹 Fn 𝐴𝑥𝐴 ) → ( 𝑥 𝐹 𝑦 → ( 𝐹𝑥 ) = 𝑦 ) )
24 eqcom ( ( 𝐹𝑥 ) = 𝑦𝑦 = ( 𝐹𝑥 ) )
25 23 24 syl6ib ( ( 𝐹 Fn 𝐴𝑥𝐴 ) → ( 𝑥 𝐹 𝑦𝑦 = ( 𝐹𝑥 ) ) )
26 9 25 sylan ( ( 𝐹 : 𝐴𝐵𝑥𝐴 ) → ( 𝑥 𝐹 𝑦𝑦 = ( 𝐹𝑥 ) ) )
27 26 reximdva ( 𝐹 : 𝐴𝐵 → ( ∃ 𝑥𝐴 𝑥 𝐹 𝑦 → ∃ 𝑥𝐴 𝑦 = ( 𝐹𝑥 ) ) )
28 27 ralimdv ( 𝐹 : 𝐴𝐵 → ( ∀ 𝑦𝐵𝑥𝐴 𝑥 𝐹 𝑦 → ∀ 𝑦𝐵𝑥𝐴 𝑦 = ( 𝐹𝑥 ) ) )
29 28 imdistani ( ( 𝐹 : 𝐴𝐵 ∧ ∀ 𝑦𝐵𝑥𝐴 𝑥 𝐹 𝑦 ) → ( 𝐹 : 𝐴𝐵 ∧ ∀ 𝑦𝐵𝑥𝐴 𝑦 = ( 𝐹𝑥 ) ) )
30 dffo3 ( 𝐹 : 𝐴onto𝐵 ↔ ( 𝐹 : 𝐴𝐵 ∧ ∀ 𝑦𝐵𝑥𝐴 𝑦 = ( 𝐹𝑥 ) ) )
31 29 30 sylibr ( ( 𝐹 : 𝐴𝐵 ∧ ∀ 𝑦𝐵𝑥𝐴 𝑥 𝐹 𝑦 ) → 𝐹 : 𝐴onto𝐵 )
32 21 31 impbii ( 𝐹 : 𝐴onto𝐵 ↔ ( 𝐹 : 𝐴𝐵 ∧ ∀ 𝑦𝐵𝑥𝐴 𝑥 𝐹 𝑦 ) )