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