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→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑥 𝐹 𝑦 ) )