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

Metamath Proof Explorer

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→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) )