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 “ ( 𝐴 × 𝐵 ) ) = 𝐵 )