2ndconst

Description: The mapping of a restriction of the 2nd function to a converse constant function. (Contributed by NM, 27-Mar-2008) (Proof shortened by Peter Mazsa, 2-Oct-2022)

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

Proof

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

Metamath Proof Explorer

Theorem 2ndconst

Proof