1stconst

Description: The mapping of a restriction of the 1st function to a constant function. (Contributed by NM, 14-Dec-2008) (Proof shortened by Peter Mazsa, 2-Oct-2022)

		Ref	Expression
	Assertion	1stconst	$⊢ B \in V \to ({1^{st} ↾}_{(A \times \{B\})}) : A \times \{B\} \underset{1-1 onto}{⟶} A$

Proof

Step	Hyp	Ref	Expression
1		snnzg	$⊢ B \in V \to \{B\} \neq \emptyset$
2		fo1stres	$⊢ \{B\} \neq \emptyset \to ({1^{st} ↾}_{(A \times \{B\})}) : A \times \{B\} \underset{onto}{⟶} A$
3	1 2	syl	$⊢ B \in V \to ({1^{st} ↾}_{(A \times \{B\})}) : A \times \{B\} \underset{onto}{⟶} A$
4		moeq	$⊢ \exists^{*} x x = ⟨y, B⟩$
5	4	moani	$⊢ \exists^{*} x (y \in A \land x = ⟨y, B⟩)$
6		vex	$⊢ y \in V$
7	6	brresi	$⊢ x ({1^{st} ↾}_{(A \times \{B\})}) y \leftrightarrow (x \in (A \times \{B\}) \land x 1^{st} y)$
8		fo1st	$⊢ 1^{st} : V \underset{onto}{⟶} V$
9		fofn	$⊢ 1^{st} : V \underset{onto}{⟶} V \to 1^{st} Fn V$
10	8 9	ax-mp	$⊢ 1^{st} Fn V$
11		vex	$⊢ x \in V$
12		fnbrfvb	$⊢ (1^{st} Fn V \land x \in V) \to (1^{st} (x) = y \leftrightarrow x 1^{st} y)$
13	10 11 12	mp2an	$⊢ 1^{st} (x) = y \leftrightarrow x 1^{st} y$
14	13	anbi2i	$⊢ (x \in (A \times \{B\}) \land 1^{st} (x) = y) \leftrightarrow (x \in (A \times \{B\}) \land x 1^{st} y)$
15		elxp7	$⊢ x \in (A \times \{B\}) \leftrightarrow (x \in (V \times V) \land (1^{st} (x) \in A \land 2^{nd} (x) \in \{B\}))$
16		eleq1	$⊢ 1^{st} (x) = y \to (1^{st} (x) \in A \leftrightarrow y \in A)$
17	16	biimpac	$⊢ (1^{st} (x) \in A \land 1^{st} (x) = y) \to y \in A$
18	17	adantlr	$⊢ ((1^{st} (x) \in A \land 2^{nd} (x) \in \{B\}) \land 1^{st} (x) = y) \to y \in A$
19	18	adantll	$⊢ ((x \in (V \times V) \land (1^{st} (x) \in A \land 2^{nd} (x) \in \{B\})) \land 1^{st} (x) = y) \to y \in A$
20		elsni	$⊢ 2^{nd} (x) \in \{B\} \to 2^{nd} (x) = B$
21		eqopi	$⊢ (x \in (V \times V) \land (1^{st} (x) = y \land 2^{nd} (x) = B)) \to x = ⟨y, B⟩$
22	21	anass1rs	$⊢ ((x \in (V \times V) \land 2^{nd} (x) = B) \land 1^{st} (x) = y) \to x = ⟨y, B⟩$
23	20 22	sylanl2	$⊢ ((x \in (V \times V) \land 2^{nd} (x) \in \{B\}) \land 1^{st} (x) = y) \to x = ⟨y, B⟩$
24	23	adantlrl	$⊢ ((x \in (V \times V) \land (1^{st} (x) \in A \land 2^{nd} (x) \in \{B\})) \land 1^{st} (x) = y) \to x = ⟨y, B⟩$
25	19 24	jca	$⊢ ((x \in (V \times V) \land (1^{st} (x) \in A \land 2^{nd} (x) \in \{B\})) \land 1^{st} (x) = y) \to (y \in A \land x = ⟨y, B⟩)$
26	15 25	sylanb	$⊢ (x \in (A \times \{B\}) \land 1^{st} (x) = y) \to (y \in A \land x = ⟨y, B⟩)$
27	26	adantl	$⊢ (B \in V \land (x \in (A \times \{B\}) \land 1^{st} (x) = y)) \to (y \in A \land x = ⟨y, B⟩)$
28		simprr	$⊢ (B \in V \land (y \in A \land x = ⟨y, B⟩)) \to x = ⟨y, B⟩$
29		simprl	$⊢ (B \in V \land (y \in A \land x = ⟨y, B⟩)) \to y \in A$
30		snidg	$⊢ B \in V \to B \in \{B\}$
31	30	adantr	$⊢ (B \in V \land (y \in A \land x = ⟨y, B⟩)) \to B \in \{B\}$
32	29 31	opelxpd	$⊢ (B \in V \land (y \in A \land x = ⟨y, B⟩)) \to ⟨y, B⟩ \in (A \times \{B\})$
33	28 32	eqeltrd	$⊢ (B \in V \land (y \in A \land x = ⟨y, B⟩)) \to x \in (A \times \{B\})$
34	28	fveq2d	$⊢ (B \in V \land (y \in A \land x = ⟨y, B⟩)) \to 1^{st} (x) = 1^{st} (⟨y, B⟩)$
35		simpl	$⊢ (B \in V \land (y \in A \land x = ⟨y, B⟩)) \to B \in V$
36		op1stg	$⊢ (y \in A \land B \in V) \to 1^{st} (⟨y, B⟩) = y$
37	29 35 36	syl2anc	$⊢ (B \in V \land (y \in A \land x = ⟨y, B⟩)) \to 1^{st} (⟨y, B⟩) = y$
38	34 37	eqtrd	$⊢ (B \in V \land (y \in A \land x = ⟨y, B⟩)) \to 1^{st} (x) = y$
39	33 38	jca	$⊢ (B \in V \land (y \in A \land x = ⟨y, B⟩)) \to (x \in (A \times \{B\}) \land 1^{st} (x) = y)$
40	27 39	impbida	$⊢ B \in V \to ((x \in (A \times \{B\}) \land 1^{st} (x) = y) \leftrightarrow (y \in A \land x = ⟨y, B⟩))$
41	14 40	bitr3id	$⊢ B \in V \to ((x \in (A \times \{B\}) \land x 1^{st} y) \leftrightarrow (y \in A \land x = ⟨y, B⟩))$
42	7 41	bitrid	$⊢ B \in V \to (x ({1^{st} ↾}_{(A \times \{B\})}) y \leftrightarrow (y \in A \land x = ⟨y, B⟩))$
43	42	mobidv	$⊢ B \in V \to (\exists^{} x x ({1^{st} ↾}_{(A \times \{B\})}) y \leftrightarrow \exists^{} x (y \in A \land x = ⟨y, B⟩))$
44	5 43	mpbiri	$⊢ B \in V \to \exists^{*} x x ({1^{st} ↾}_{(A \times \{B\})}) y$
45	44	alrimiv	$⊢ B \in V \to \forall y \exists^{*} x x ({1^{st} ↾}_{(A \times \{B\})}) y$
46		funcnv2	$⊢ Fun {({1^{st} ↾}_{(A \times \{B\})})}^{-1} \leftrightarrow \forall y \exists^{*} x x ({1^{st} ↾}_{(A \times \{B\})}) y$
47	45 46	sylibr	$⊢ B \in V \to Fun {({1^{st} ↾}_{(A \times \{B\})})}^{-1}$
48		dff1o3	$⊢ ({1^{st} ↾}_{(A \times \{B\})}) : A \times \{B\} \underset{1-1 onto}{⟶} A \leftrightarrow (({1^{st} ↾}_{(A \times \{B\})}) : A \times \{B\} \underset{onto}{⟶} A \land Fun {({1^{st} ↾}_{(A \times \{B\})})}^{-1})$
49	3 47 48	sylanbrc	$⊢ B \in V \to ({1^{st} ↾}_{(A \times \{B\})}) : A \times \{B\} \underset{1-1 onto}{⟶} A$

Metamath Proof Explorer

Theorem 1stconst

Proof