2nd2val

Description: Value of an alternate definition of the 2nd function. (Contributed by NM, 10-Aug-2006) (Revised by Mario Carneiro, 30-Dec-2014)

		Ref	Expression
	Assertion	2nd2val	$⊢ \{⟨⟨x, y⟩, z⟩ \| z = y\} (A) = 2^{nd} (A)$

Proof

Step	Hyp	Ref	Expression
1		elvv	$⊢ A \in (V \times V) \leftrightarrow \exists w \exists v A = ⟨w, v⟩$
2		fveq2	$⊢ A = ⟨w, v⟩ \to \{⟨⟨x, y⟩, z⟩ \| z = y\} (A) = \{⟨⟨x, y⟩, z⟩ \| z = y\} (⟨w, v⟩)$
3		df-ov	$⊢ w \{⟨⟨x, y⟩, z⟩ \| z = y\} v = \{⟨⟨x, y⟩, z⟩ \| z = y\} (⟨w, v⟩)$
4		simpr	$⊢ (x = w \land y = v) \to y = v$
5		mpov	$⊢ (x \in V, y \in V ⟼ y) = \{⟨⟨x, y⟩, z⟩ \| z = y\}$
6	5	eqcomi	$⊢ \{⟨⟨x, y⟩, z⟩ \| z = y\} = (x \in V, y \in V ⟼ y)$
7		vex	$⊢ v \in V$
8	4 6 7	ovmpoa	$⊢ (w \in V \land v \in V) \to w \{⟨⟨x, y⟩, z⟩ \| z = y\} v = v$
9	8	el2v	$⊢ w \{⟨⟨x, y⟩, z⟩ \| z = y\} v = v$
10	3 9	eqtr3i	$⊢ \{⟨⟨x, y⟩, z⟩ \| z = y\} (⟨w, v⟩) = v$
11	2 10	eqtrdi	$⊢ A = ⟨w, v⟩ \to \{⟨⟨x, y⟩, z⟩ \| z = y\} (A) = v$
12		vex	$⊢ w \in V$
13	12 7	op2ndd	$⊢ A = ⟨w, v⟩ \to 2^{nd} (A) = v$
14	11 13	eqtr4d	$⊢ A = ⟨w, v⟩ \to \{⟨⟨x, y⟩, z⟩ \| z = y\} (A) = 2^{nd} (A)$
15	14	exlimivv	$⊢ \exists w \exists v A = ⟨w, v⟩ \to \{⟨⟨x, y⟩, z⟩ \| z = y\} (A) = 2^{nd} (A)$
16	1 15	sylbi	$⊢ A \in (V \times V) \to \{⟨⟨x, y⟩, z⟩ \| z = y\} (A) = 2^{nd} (A)$
17		vex	$⊢ x \in V$
18		vex	$⊢ y \in V$
19	17 18	pm3.2i	$⊢ (x \in V \land y \in V)$
20		ax6ev	$⊢ \exists z z = y$
21	19 20	2th	$⊢ (x \in V \land y \in V) \leftrightarrow \exists z z = y$
22	21	opabbii	$⊢ \{⟨x, y⟩ \| (x \in V \land y \in V)\} = \{⟨x, y⟩ \| \exists z z = y\}$
23		df-xp	$⊢ V \times V = \{⟨x, y⟩ \| (x \in V \land y \in V)\}$
24		dmoprab	$⊢ dom \{⟨⟨x, y⟩, z⟩ \| z = y\} = \{⟨x, y⟩ \| \exists z z = y\}$
25	22 23 24	3eqtr4ri	$⊢ dom \{⟨⟨x, y⟩, z⟩ \| z = y\} = V \times V$
26	25	eleq2i	$⊢ A \in dom \{⟨⟨x, y⟩, z⟩ \| z = y\} \leftrightarrow A \in (V \times V)$
27		ndmfv	$⊢ \neg A \in dom \{⟨⟨x, y⟩, z⟩ \| z = y\} \to \{⟨⟨x, y⟩, z⟩ \| z = y\} (A) = \emptyset$
28	26 27	sylnbir	$⊢ \neg A \in (V \times V) \to \{⟨⟨x, y⟩, z⟩ \| z = y\} (A) = \emptyset$
29		rnsnn0	$⊢ A \in (V \times V) \leftrightarrow ran \{A\} \neq \emptyset$
30	29	biimpri	$⊢ ran \{A\} \neq \emptyset \to A \in (V \times V)$
31	30	necon1bi	$⊢ \neg A \in (V \times V) \to ran \{A\} = \emptyset$
32	31	unieqd	$⊢ \neg A \in (V \times V) \to ⋃ ran \{A\} = ⋃ \emptyset$
33		uni0	$⊢ ⋃ \emptyset = \emptyset$
34	32 33	eqtrdi	$⊢ \neg A \in (V \times V) \to ⋃ ran \{A\} = \emptyset$
35	28 34	eqtr4d	$⊢ \neg A \in (V \times V) \to \{⟨⟨x, y⟩, z⟩ \| z = y\} (A) = ⋃ ran \{A\}$
36		2ndval	$⊢ 2^{nd} (A) = ⋃ ran \{A\}$
37	35 36	eqtr4di	$⊢ \neg A \in (V \times V) \to \{⟨⟨x, y⟩, z⟩ \| z = y\} (A) = 2^{nd} (A)$
38	16 37	pm2.61i	$⊢ \{⟨⟨x, y⟩, z⟩ \| z = y\} (A) = 2^{nd} (A)$

Metamath Proof Explorer

Theorem 2nd2val

Proof