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

Metamath Proof Explorer

Theorem f2ndres

Description: Mapping of a restriction of the 2nd (second member of an ordered pair) function. (Contributed by NM, 7-Aug-2006) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion f2ndres ( 2nd ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) ⟶ 𝐵

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑦 ∈ V
2 vex ⊢ 𝑧 ∈ V
3 1 2 op2nda ⊢ ∪ ran { ⟨ 𝑦 , 𝑧 ⟩ } = 𝑧
4 3 eleq1i ⊢ ( ∪ ran { ⟨ 𝑦 , 𝑧 ⟩ } ∈ 𝐵 ↔ 𝑧 ∈ 𝐵 )
5 4 biimpri ⊢ ( 𝑧 ∈ 𝐵 → ∪ ran { ⟨ 𝑦 , 𝑧 ⟩ } ∈ 𝐵 )
6 5 adantl ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → ∪ ran { ⟨ 𝑦 , 𝑧 ⟩ } ∈ 𝐵 )
7 6 rgen2 ⊢ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∪ ran { ⟨ 𝑦 , 𝑧 ⟩ } ∈ 𝐵
8 sneq ⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → { 𝑥 } = { ⟨ 𝑦 , 𝑧 ⟩ } )
9 8 rneqd ⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ran { 𝑥 } = ran { ⟨ 𝑦 , 𝑧 ⟩ } )
10 9 unieqd ⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ∪ ran { 𝑥 } = ∪ ran { ⟨ 𝑦 , 𝑧 ⟩ } )
11 10 eleq1d ⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( ∪ ran { 𝑥 } ∈ 𝐵 ↔ ∪ ran { ⟨ 𝑦 , 𝑧 ⟩ } ∈ 𝐵 ) )
12 11 ralxp ⊢ ( ∀ 𝑥 ∈ ( 𝐴 × 𝐵 ) ∪ ran { 𝑥 } ∈ 𝐵 ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∪ ran { ⟨ 𝑦 , 𝑧 ⟩ } ∈ 𝐵 )
13 7 12 mpbir ⊢ ∀ 𝑥 ∈ ( 𝐴 × 𝐵 ) ∪ ran { 𝑥 } ∈ 𝐵
14 df-2nd ⊢ 2nd = ( 𝑥 ∈ V ↦ ∪ ran { 𝑥 } )
15 14 reseq1i ⊢ ( 2nd ↾ ( 𝐴 × 𝐵 ) ) = ( ( 𝑥 ∈ V ↦ ∪ ran { 𝑥 } ) ↾ ( 𝐴 × 𝐵 ) )
16 ssv ⊢ ( 𝐴 × 𝐵 ) ⊆ V
17 resmpt ⊢ ( ( 𝐴 × 𝐵 ) ⊆ V → ( ( 𝑥 ∈ V ↦ ∪ ran { 𝑥 } ) ↾ ( 𝐴 × 𝐵 ) ) = ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↦ ∪ ran { 𝑥 } ) )
18 16 17 ax-mp ⊢ ( ( 𝑥 ∈ V ↦ ∪ ran { 𝑥 } ) ↾ ( 𝐴 × 𝐵 ) ) = ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↦ ∪ ran { 𝑥 } )
19 15 18 eqtri ⊢ ( 2nd ↾ ( 𝐴 × 𝐵 ) ) = ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↦ ∪ ran { 𝑥 } )
20 19 fmpt ⊢ ( ∀ 𝑥 ∈ ( 𝐴 × 𝐵 ) ∪ ran { 𝑥 } ∈ 𝐵 ↔ ( 2nd ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) ⟶ 𝐵 )
21 13 20 mpbi ⊢ ( 2nd ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) ⟶ 𝐵