Metamath Proof Explorer

Theorem fparlem2

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

		Ref	Expression
	Assertion	fparlem2	$⊢ {({2^{nd} ↾}_{(V \times V)})}^{-1} [\{y\}] = V \times \{y\}$

Proof

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