Theorem ffoss

Description: Relationship between a mapping and an onto mapping. Figure 38 of Enderton p. 145. (Contributed by NM, 10-May-1998)

	Ref	Expression
Hypothesis	f11o.1	⊢ 𝐹 ∈ V
Assertion	ffoss	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ∃ 𝑥 ( 𝐹 : 𝐴 –onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		f11o.1	⊢ 𝐹 ∈ V
2		df-f	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) )
3		dffn4	⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 : 𝐴 –onto→ ran 𝐹 )
4	3	anbi1i	⊢ ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) ↔ ( 𝐹 : 𝐴 –onto→ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) )
5	2 4	bitri	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 : 𝐴 –onto→ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) )
6	1	rnex	⊢ ran 𝐹 ∈ V
7		foeq3	⊢ ( 𝑥 = ran 𝐹 → ( 𝐹 : 𝐴 –onto→ 𝑥 ↔ 𝐹 : 𝐴 –onto→ ran 𝐹 ) )
8		sseq1	⊢ ( 𝑥 = ran 𝐹 → ( 𝑥 ⊆ 𝐵 ↔ ran 𝐹 ⊆ 𝐵 ) )
9	7 8	anbi12d	⊢ ( 𝑥 = ran 𝐹 → ( ( 𝐹 : 𝐴 –onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ↔ ( 𝐹 : 𝐴 –onto→ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) ) )
10	6 9	spcev	⊢ ( ( 𝐹 : 𝐴 –onto→ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) → ∃ 𝑥 ( 𝐹 : 𝐴 –onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) )
11	5 10	sylbi	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ∃ 𝑥 ( 𝐹 : 𝐴 –onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) )
12		fof	⊢ ( 𝐹 : 𝐴 –onto→ 𝑥 → 𝐹 : 𝐴 ⟶ 𝑥 )
13		fss	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
14	12 13	sylan	⊢ ( ( 𝐹 : 𝐴 –onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
15	14	exlimiv	⊢ ( ∃ 𝑥 ( 𝐹 : 𝐴 –onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
16	11 15	impbii	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ∃ 𝑥 ( 𝐹 : 𝐴 –onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) )