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

Metamath Proof Explorer

Theorem fo2ndres

Description: Onto mapping of a restriction of the 2nd (second member of an ordered pair) function. (Contributed by NM, 14-Dec-2008)

Ref Expression
Assertion fo2ndres ( 𝐴 ≠ ∅ → ( 2nd ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) –onto→ 𝐵 )

Proof

Step Hyp Ref Expression
1 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
2 opelxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
3 fvres ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) → ( ( 2nd ↾ ( 𝐴 × 𝐵 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
4 vex ⊢ 𝑥 ∈ V
5 vex ⊢ 𝑦 ∈ V
6 4 5 op2nd ⊢ ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑦
7 3 6 eqtr2di ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) → 𝑦 = ( ( 2nd ↾ ( 𝐴 × 𝐵 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
8 f2ndres ⊢ ( 2nd ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) ⟶ 𝐵
9 ffn ⊢ ( ( 2nd ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) ⟶ 𝐵 → ( 2nd ↾ ( 𝐴 × 𝐵 ) ) Fn ( 𝐴 × 𝐵 ) )
10 8 9 ax-mp ⊢ ( 2nd ↾ ( 𝐴 × 𝐵 ) ) Fn ( 𝐴 × 𝐵 )
11 fnfvelrn ⊢ ( ( ( 2nd ↾ ( 𝐴 × 𝐵 ) ) Fn ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ) → ( ( 2nd ↾ ( 𝐴 × 𝐵 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ ran ( 2nd ↾ ( 𝐴 × 𝐵 ) ) )
12 10 11 mpan ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) → ( ( 2nd ↾ ( 𝐴 × 𝐵 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ ran ( 2nd ↾ ( 𝐴 × 𝐵 ) ) )
13 7 12 eqeltrd ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) → 𝑦 ∈ ran ( 2nd ↾ ( 𝐴 × 𝐵 ) ) )
14 2 13 sylbir ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ran ( 2nd ↾ ( 𝐴 × 𝐵 ) ) )
15 14 ex ⊢ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ran ( 2nd ↾ ( 𝐴 × 𝐵 ) ) ) )
16 15 exlimiv ⊢ ( ∃ 𝑥 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ran ( 2nd ↾ ( 𝐴 × 𝐵 ) ) ) )
17 1 16 sylbi ⊢ ( 𝐴 ≠ ∅ → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ran ( 2nd ↾ ( 𝐴 × 𝐵 ) ) ) )
18 17 ssrdv ⊢ ( 𝐴 ≠ ∅ → 𝐵 ⊆ ran ( 2nd ↾ ( 𝐴 × 𝐵 ) ) )
19 frn ⊢ ( ( 2nd ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) ⟶ 𝐵 → ran ( 2nd ↾ ( 𝐴 × 𝐵 ) ) ⊆ 𝐵 )
20 8 19 ax-mp ⊢ ran ( 2nd ↾ ( 𝐴 × 𝐵 ) ) ⊆ 𝐵
21 18 20 jctil ⊢ ( 𝐴 ≠ ∅ → ( ran ( 2nd ↾ ( 𝐴 × 𝐵 ) ) ⊆ 𝐵 ∧ 𝐵 ⊆ ran ( 2nd ↾ ( 𝐴 × 𝐵 ) ) ) )
22 eqss ⊢ ( ran ( 2nd ↾ ( 𝐴 × 𝐵 ) ) = 𝐵 ↔ ( ran ( 2nd ↾ ( 𝐴 × 𝐵 ) ) ⊆ 𝐵 ∧ 𝐵 ⊆ ran ( 2nd ↾ ( 𝐴 × 𝐵 ) ) ) )
23 21 22 sylibr ⊢ ( 𝐴 ≠ ∅ → ran ( 2nd ↾ ( 𝐴 × 𝐵 ) ) = 𝐵 )
24 23 8 jctil ⊢ ( 𝐴 ≠ ∅ → ( ( 2nd ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) ⟶ 𝐵 ∧ ran ( 2nd ↾ ( 𝐴 × 𝐵 ) ) = 𝐵 ) )
25 dffo2 ⊢ ( ( 2nd ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) –onto→ 𝐵 ↔ ( ( 2nd ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) ⟶ 𝐵 ∧ ran ( 2nd ↾ ( 𝐴 × 𝐵 ) ) = 𝐵 ) )
26 24 25 sylibr ⊢ ( 𝐴 ≠ ∅ → ( 2nd ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) –onto→ 𝐵 )