This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dffo5

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

Ref Expression
Assertion dffo5 ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 𝑥 𝐹 𝑦 ) )

Proof

Step Hyp Ref Expression
1 dffo4 ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑥 𝐹 𝑦 ) )
2 rexex ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑥 𝐹 𝑦 → ∃ 𝑥 𝑥 𝐹 𝑦 )
3 2 ralimi ⊢ ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑥 𝐹 𝑦 → ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 𝑥 𝐹 𝑦 )
4 3 anim2i ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑥 𝐹 𝑦 ) → ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 𝑥 𝐹 𝑦 ) )
5 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
6 fnbr ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 𝐹 𝑦 ) → 𝑥 ∈ 𝐴 )
7 6 ex ⊢ ( 𝐹 Fn 𝐴 → ( 𝑥 𝐹 𝑦 → 𝑥 ∈ 𝐴 ) )
8 5 7 syl ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝑥 𝐹 𝑦 → 𝑥 ∈ 𝐴 ) )
9 8 ancrd ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝑥 𝐹 𝑦 → ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ) )
10 9 eximdv ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ∃ 𝑥 𝑥 𝐹 𝑦 → ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ) )
11 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑥 𝐹 𝑦 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) )
12 10 11 imbitrrdi ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ∃ 𝑥 𝑥 𝐹 𝑦 → ∃ 𝑥 ∈ 𝐴 𝑥 𝐹 𝑦 ) )
13 12 ralimdv ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 𝑥 𝐹 𝑦 → ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑥 𝐹 𝑦 ) )
14 13 imdistani ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 𝑥 𝐹 𝑦 ) → ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑥 𝐹 𝑦 ) )
15 4 14 impbii ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑥 𝐹 𝑦 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 𝑥 𝐹 𝑦 ) )
16 1 15 bitri ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 𝑥 𝐹 𝑦 ) )