1st2val

Description: Value of an alternate definition of the 1st function. (Contributed by NM, 14-Oct-2004) (Revised by Mario Carneiro, 30-Dec-2014)

		Ref	Expression
	Assertion	1st2val	$⊢ \{⟨⟨x, y⟩, z⟩ \| z = x\} (A) = 1^{st} (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 = x\} (A) = \{⟨⟨x, y⟩, z⟩ \| z = x\} (⟨w, v⟩)$
3		df-ov	$⊢ w \{⟨⟨x, y⟩, z⟩ \| z = x\} v = \{⟨⟨x, y⟩, z⟩ \| z = x\} (⟨w, v⟩)$
4		simpl	$⊢ (x = w \land y = v) \to x = w$
5		mpov	$⊢ (x \in V, y \in V ⟼ x) = \{⟨⟨x, y⟩, z⟩ \| z = x\}$
6	5	eqcomi	$⊢ \{⟨⟨x, y⟩, z⟩ \| z = x\} = (x \in V, y \in V ⟼ x)$
7		vex	$⊢ w \in V$
8	4 6 7	ovmpoa	$⊢ (w \in V \land v \in V) \to w \{⟨⟨x, y⟩, z⟩ \| z = x\} v = w$
9	8	el2v	$⊢ w \{⟨⟨x, y⟩, z⟩ \| z = x\} v = w$
10	3 9	eqtr3i	$⊢ \{⟨⟨x, y⟩, z⟩ \| z = x\} (⟨w, v⟩) = w$
11	2 10	eqtrdi	$⊢ A = ⟨w, v⟩ \to \{⟨⟨x, y⟩, z⟩ \| z = x\} (A) = w$
12		vex	$⊢ v \in V$
13	7 12	op1std	$⊢ A = ⟨w, v⟩ \to 1^{st} (A) = w$
14	11 13	eqtr4d	$⊢ A = ⟨w, v⟩ \to \{⟨⟨x, y⟩, z⟩ \| z = x\} (A) = 1^{st} (A)$
15	14	exlimivv	$⊢ \exists w \exists v A = ⟨w, v⟩ \to \{⟨⟨x, y⟩, z⟩ \| z = x\} (A) = 1^{st} (A)$
16	1 15	sylbi	$⊢ A \in (V \times V) \to \{⟨⟨x, y⟩, z⟩ \| z = x\} (A) = 1^{st} (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 = x$
21	19 20	2th	$⊢ (x \in V \land y \in V) \leftrightarrow \exists z z = x$
22	21	opabbii	$⊢ \{⟨x, y⟩ \| (x \in V \land y \in V)\} = \{⟨x, y⟩ \| \exists z z = x\}$
23		df-xp	$⊢ V \times V = \{⟨x, y⟩ \| (x \in V \land y \in V)\}$
24		dmoprab	$⊢ dom \{⟨⟨x, y⟩, z⟩ \| z = x\} = \{⟨x, y⟩ \| \exists z z = x\}$
25	22 23 24	3eqtr4ri	$⊢ dom \{⟨⟨x, y⟩, z⟩ \| z = x\} = V \times V$
26	25	eleq2i	$⊢ A \in dom \{⟨⟨x, y⟩, z⟩ \| z = x\} \leftrightarrow A \in (V \times V)$
27		ndmfv	$⊢ \neg A \in dom \{⟨⟨x, y⟩, z⟩ \| z = x\} \to \{⟨⟨x, y⟩, z⟩ \| z = x\} (A) = \emptyset$
28	26 27	sylnbir	$⊢ \neg A \in (V \times V) \to \{⟨⟨x, y⟩, z⟩ \| z = x\} (A) = \emptyset$
29		dmsnn0	$⊢ A \in (V \times V) \leftrightarrow dom \{A\} \neq \emptyset$
30	29	biimpri	$⊢ dom \{A\} \neq \emptyset \to A \in (V \times V)$
31	30	necon1bi	$⊢ \neg A \in (V \times V) \to dom \{A\} = \emptyset$
32	31	unieqd	$⊢ \neg A \in (V \times V) \to ⋃ dom \{A\} = ⋃ \emptyset$
33		uni0	$⊢ ⋃ \emptyset = \emptyset$
34	32 33	eqtrdi	$⊢ \neg A \in (V \times V) \to ⋃ dom \{A\} = \emptyset$
35	28 34	eqtr4d	$⊢ \neg A \in (V \times V) \to \{⟨⟨x, y⟩, z⟩ \| z = x\} (A) = ⋃ dom \{A\}$
36		1stval	$⊢ 1^{st} (A) = ⋃ dom \{A\}$
37	35 36	eqtr4di	$⊢ \neg A \in (V \times V) \to \{⟨⟨x, y⟩, z⟩ \| z = x\} (A) = 1^{st} (A)$
38	16 37	pm2.61i	$⊢ \{⟨⟨x, y⟩, z⟩ \| z = x\} (A) = 1^{st} (A)$

Metamath Proof Explorer

Theorem 1st2val

Proof