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

Metamath Proof Explorer

Theorem 2ndimaxp

Description: Image of a cartesian product by 2nd . (Contributed by Thierry Arnoux, 23-Jun-2024)

Ref Expression
Assertion 2ndimaxp ( 𝐴 ≠ ∅ → ( 2nd “ ( 𝐴 × 𝐵 ) ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 ima0 ⊢ ( 2nd “ ∅ ) = ∅
2 xpeq2 ⊢ ( 𝐵 = ∅ → ( 𝐴 × 𝐵 ) = ( 𝐴 × ∅ ) )
3 xp0 ⊢ ( 𝐴 × ∅ ) = ∅
4 2 3 eqtrdi ⊢ ( 𝐵 = ∅ → ( 𝐴 × 𝐵 ) = ∅ )
5 4 imaeq2d ⊢ ( 𝐵 = ∅ → ( 2nd “ ( 𝐴 × 𝐵 ) ) = ( 2nd “ ∅ ) )
6 id ⊢ ( 𝐵 = ∅ → 𝐵 = ∅ )
7 1 5 6 3eqtr4a ⊢ ( 𝐵 = ∅ → ( 2nd “ ( 𝐴 × 𝐵 ) ) = 𝐵 )
8 7 adantl ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 = ∅ ) → ( 2nd “ ( 𝐴 × 𝐵 ) ) = 𝐵 )
9 xpnz ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ↔ ( 𝐴 × 𝐵 ) ≠ ∅ )
10 fo2nd ⊢ 2nd : V –onto→ V
11 fofn ⊢ ( 2nd : V –onto→ V → 2nd Fn V )
12 10 11 mp1i ⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ → 2nd Fn V )
13 ssv ⊢ ( 𝐴 × 𝐵 ) ⊆ V
14 13 a1i ⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ → ( 𝐴 × 𝐵 ) ⊆ V )
15 12 14 fvelimabd ⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ → ( 𝑦 ∈ ( 2nd “ ( 𝐴 × 𝐵 ) ) ↔ ∃ 𝑝 ∈ ( 𝐴 × 𝐵 ) ( 2nd ‘ 𝑝 ) = 𝑦 ) )
16 9 15 sylbi ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → ( 𝑦 ∈ ( 2nd “ ( 𝐴 × 𝐵 ) ) ↔ ∃ 𝑝 ∈ ( 𝐴 × 𝐵 ) ( 2nd ‘ 𝑝 ) = 𝑦 ) )
17 simpr ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝐴 × 𝐵 ) ) ∧ ( 2nd ‘ 𝑝 ) = 𝑦 ) → ( 2nd ‘ 𝑝 ) = 𝑦 )
18 xp2nd ⊢ ( 𝑝 ∈ ( 𝐴 × 𝐵 ) → ( 2nd ‘ 𝑝 ) ∈ 𝐵 )
19 18 ad2antlr ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝐴 × 𝐵 ) ) ∧ ( 2nd ‘ 𝑝 ) = 𝑦 ) → ( 2nd ‘ 𝑝 ) ∈ 𝐵 )
20 17 19 eqeltrrd ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝐴 × 𝐵 ) ) ∧ ( 2nd ‘ 𝑝 ) = 𝑦 ) → 𝑦 ∈ 𝐵 )
21 20 r19.29an ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ∃ 𝑝 ∈ ( 𝐴 × 𝐵 ) ( 2nd ‘ 𝑝 ) = 𝑦 ) → 𝑦 ∈ 𝐵 )
22 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
23 22 biimpi ⊢ ( 𝐴 ≠ ∅ → ∃ 𝑥 𝑥 ∈ 𝐴 )
24 23 ad2antrr ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 𝑥 ∈ 𝐴 )
25 opelxpi ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) )
26 25 ancoms ⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) )
27 26 adantll ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) )
28 fveqeq2 ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 2nd ‘ 𝑝 ) = 𝑦 ↔ ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑦 ) )
29 28 adantl ⊢ ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 2nd ‘ 𝑝 ) = 𝑦 ↔ ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑦 ) )
30 vex ⊢ 𝑥 ∈ V
31 vex ⊢ 𝑦 ∈ V
32 30 31 op2nd ⊢ ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑦
33 32 a1i ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑦 )
34 27 29 33 rspcedvd ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑝 ∈ ( 𝐴 × 𝐵 ) ( 2nd ‘ 𝑝 ) = 𝑦 )
35 24 34 exlimddv ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑝 ∈ ( 𝐴 × 𝐵 ) ( 2nd ‘ 𝑝 ) = 𝑦 )
36 21 35 impbida ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → ( ∃ 𝑝 ∈ ( 𝐴 × 𝐵 ) ( 2nd ‘ 𝑝 ) = 𝑦 ↔ 𝑦 ∈ 𝐵 ) )
37 16 36 bitrd ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → ( 𝑦 ∈ ( 2nd “ ( 𝐴 × 𝐵 ) ) ↔ 𝑦 ∈ 𝐵 ) )
38 37 eqrdv ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → ( 2nd “ ( 𝐴 × 𝐵 ) ) = 𝐵 )
39 8 38 pm2.61dane ⊢ ( 𝐴 ≠ ∅ → ( 2nd “ ( 𝐴 × 𝐵 ) ) = 𝐵 )