2ndimaxp

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

		Ref	Expression
	Assertion	2ndimaxp	$⊢ A \neq \emptyset \to 2^{nd} [A \times B] = B$

Proof

Step	Hyp	Ref	Expression
1		ima0	$⊢ 2^{nd} [\emptyset] = \emptyset$
2		xpeq2	$⊢ B = \emptyset \to A \times B = A \times \emptyset$
3		xp0	$⊢ A \times \emptyset = \emptyset$
4	2 3	eqtrdi	$⊢ B = \emptyset \to A \times B = \emptyset$
5	4	imaeq2d	$⊢ B = \emptyset \to 2^{nd} [A \times B] = 2^{nd} [\emptyset]$
6		id	$⊢ B = \emptyset \to B = \emptyset$
7	1 5 6	3eqtr4a	$⊢ B = \emptyset \to 2^{nd} [A \times B] = B$
8	7	adantl	$⊢ (A \neq \emptyset \land B = \emptyset) \to 2^{nd} [A \times B] = B$
9		xpnz	$⊢ (A \neq \emptyset \land B \neq \emptyset) \leftrightarrow A \times B \neq \emptyset$
10		fo2nd	$⊢ 2^{nd} : V \underset{onto}{⟶} V$
11		fofn	$⊢ 2^{nd} : V \underset{onto}{⟶} V \to 2^{nd} Fn V$
12	10 11	mp1i	$⊢ A \times B \neq \emptyset \to 2^{nd} Fn V$
13		ssv	$⊢ A \times B \subseteq V$
14	13	a1i	$⊢ A \times B \neq \emptyset \to A \times B \subseteq V$
15	12 14	fvelimabd	$⊢ A \times B \neq \emptyset \to (y \in 2^{nd} [A \times B] \leftrightarrow \exists p \in (A \times B) 2^{nd} (p) = y)$
16	9 15	sylbi	$⊢ (A \neq \emptyset \land B \neq \emptyset) \to (y \in 2^{nd} [A \times B] \leftrightarrow \exists p \in (A \times B) 2^{nd} (p) = y)$
17		simpr	$⊢ (((A \neq \emptyset \land B \neq \emptyset) \land p \in (A \times B)) \land 2^{nd} (p) = y) \to 2^{nd} (p) = y$
18		xp2nd	$⊢ p \in (A \times B) \to 2^{nd} (p) \in B$
19	18	ad2antlr	$⊢ (((A \neq \emptyset \land B \neq \emptyset) \land p \in (A \times B)) \land 2^{nd} (p) = y) \to 2^{nd} (p) \in B$
20	17 19	eqeltrrd	$⊢ (((A \neq \emptyset \land B \neq \emptyset) \land p \in (A \times B)) \land 2^{nd} (p) = y) \to y \in B$
21	20	r19.29an	$⊢ ((A \neq \emptyset \land B \neq \emptyset) \land \exists p \in (A \times B) 2^{nd} (p) = y) \to y \in B$
22		n0	$⊢ A \neq \emptyset \leftrightarrow \exists x x \in A$
23	22	biimpi	$⊢ A \neq \emptyset \to \exists x x \in A$
24	23	ad2antrr	$⊢ ((A \neq \emptyset \land B \neq \emptyset) \land y \in B) \to \exists x x \in A$
25		opelxpi	$⊢ (x \in A \land y \in B) \to ⟨x, y⟩ \in (A \times B)$
26	25	ancoms	$⊢ (y \in B \land x \in A) \to ⟨x, y⟩ \in (A \times B)$
27	26	adantll	$⊢ (((A \neq \emptyset \land B \neq \emptyset) \land y \in B) \land x \in A) \to ⟨x, y⟩ \in (A \times B)$
28		fveqeq2	$⊢ p = ⟨x, y⟩ \to (2^{nd} (p) = y \leftrightarrow 2^{nd} (⟨x, y⟩) = y)$
29	28	adantl	$⊢ ((((A \neq \emptyset \land B \neq \emptyset) \land y \in B) \land x \in A) \land p = ⟨x, y⟩) \to (2^{nd} (p) = y \leftrightarrow 2^{nd} (⟨x, y⟩) = y)$
30		vex	$⊢ x \in V$
31		vex	$⊢ y \in V$
32	30 31	op2nd	$⊢ 2^{nd} (⟨x, y⟩) = y$
33	32	a1i	$⊢ (((A \neq \emptyset \land B \neq \emptyset) \land y \in B) \land x \in A) \to 2^{nd} (⟨x, y⟩) = y$
34	27 29 33	rspcedvd	$⊢ (((A \neq \emptyset \land B \neq \emptyset) \land y \in B) \land x \in A) \to \exists p \in (A \times B) 2^{nd} (p) = y$
35	24 34	exlimddv	$⊢ ((A \neq \emptyset \land B \neq \emptyset) \land y \in B) \to \exists p \in (A \times B) 2^{nd} (p) = y$
36	21 35	impbida	$⊢ (A \neq \emptyset \land B \neq \emptyset) \to (\exists p \in (A \times B) 2^{nd} (p) = y \leftrightarrow y \in B)$
37	16 36	bitrd	$⊢ (A \neq \emptyset \land B \neq \emptyset) \to (y \in 2^{nd} [A \times B] \leftrightarrow y \in B)$
38	37	eqrdv	$⊢ (A \neq \emptyset \land B \neq \emptyset) \to 2^{nd} [A \times B] = B$
39	8 38	pm2.61dane	$⊢ A \neq \emptyset \to 2^{nd} [A \times B] = B$

Metamath Proof Explorer

Theorem 2ndimaxp

Proof