Metamath Proof Explorer

Theorem fparlem1

Description: Lemma for fpar . (Contributed by NM, 22-Dec-2008) (Revised by Mario Carneiro, 28-Apr-2015)

		Ref	Expression
	Assertion	fparlem1	$⊢ {({1^{st} ↾}_{(V \times V)})}^{-1} [\{x\}] = \{x\} \times V$

Proof

Step	Hyp	Ref	Expression
1		fvres	$⊢ y \in (V \times V) \to ({1^{st} ↾}_{(V \times V)}) (y) = 1^{st} (y)$
2	1	eqeq1d	$⊢ y \in (V \times V) \to (({1^{st} ↾}_{(V \times V)}) (y) = x \leftrightarrow 1^{st} (y) = x)$
3		vex	$⊢ x \in V$
4	3	elsn2	$⊢ 1^{st} (y) \in \{x\} \leftrightarrow 1^{st} (y) = x$
5		fvex	$⊢ 2^{nd} (y) \in V$
6	5	biantru	$⊢ 1^{st} (y) \in \{x\} \leftrightarrow (1^{st} (y) \in \{x\} \land 2^{nd} (y) \in V)$
7	4 6	bitr3i	$⊢ 1^{st} (y) = x \leftrightarrow (1^{st} (y) \in \{x\} \land 2^{nd} (y) \in V)$
8	2 7	bitrdi	$⊢ y \in (V \times V) \to (({1^{st} ↾}_{(V \times V)}) (y) = x \leftrightarrow (1^{st} (y) \in \{x\} \land 2^{nd} (y) \in V))$
9	8	pm5.32i	$⊢ (y \in (V \times V) \land ({1^{st} ↾}_{(V \times V)}) (y) = x) \leftrightarrow (y \in (V \times V) \land (1^{st} (y) \in \{x\} \land 2^{nd} (y) \in V))$
10		f1stres	$⊢ ({1^{st} ↾}_{(V \times V)}) : V \times V ⟶ V$
11		ffn	$⊢ ({1^{st} ↾}_{(V \times V)}) : V \times V ⟶ V \to ({1^{st} ↾}_{(V \times V)}) Fn (V \times V)$
12		fniniseg	$⊢ ({1^{st} ↾}_{(V \times V)}) Fn (V \times V) \to (y \in {({1^{st} ↾}_{(V \times V)})}^{-1} [\{x\}] \leftrightarrow (y \in (V \times V) \land ({1^{st} ↾}_{(V \times V)}) (y) = x))$
13	10 11 12	mp2b	$⊢ y \in {({1^{st} ↾}_{(V \times V)})}^{-1} [\{x\}] \leftrightarrow (y \in (V \times V) \land ({1^{st} ↾}_{(V \times V)}) (y) = x)$
14		elxp7	$⊢ y \in (\{x\} \times V) \leftrightarrow (y \in (V \times V) \land (1^{st} (y) \in \{x\} \land 2^{nd} (y) \in V))$
15	9 13 14	3bitr4i	$⊢ y \in {({1^{st} ↾}_{(V \times V)})}^{-1} [\{x\}] \leftrightarrow y \in (\{x\} \times V)$
16	15	eqriv	$⊢ {({1^{st} ↾}_{(V \times V)})}^{-1} [\{x\}] = \{x\} \times V$