fv1stcnv

Description: The value of the converse of 1st restricted to a singleton. (Contributed by Scott Fenton, 2-Jul-2020)

		Ref	Expression
	Assertion	fv1stcnv	$⊢ (X \in A \land Y \in V) \to {({1^{st} ↾}_{(A \times \{Y\})})}^{-1} (X) = ⟨X, Y⟩$

Proof

Step	Hyp	Ref	Expression
1		snidg	$⊢ Y \in V \to Y \in \{Y\}$
2	1	anim2i	$⊢ (X \in A \land Y \in V) \to (X \in A \land Y \in \{Y\})$
3		eqid	$⊢ X = X$
4	2 3	jctir	$⊢ (X \in A \land Y \in V) \to ((X \in A \land Y \in \{Y\}) \land X = X)$
5		opex	$⊢ ⟨X, Y⟩ \in V$
6		brcnvg	$⊢ (X \in A \land ⟨X, Y⟩ \in V) \to (X {({1^{st} ↾}_{(A \times \{Y\})})}^{-1} ⟨X, Y⟩ \leftrightarrow ⟨X, Y⟩ ({1^{st} ↾}_{(A \times \{Y\})}) X)$
7	5 6	mpan2	$⊢ X \in A \to (X {({1^{st} ↾}_{(A \times \{Y\})})}^{-1} ⟨X, Y⟩ \leftrightarrow ⟨X, Y⟩ ({1^{st} ↾}_{(A \times \{Y\})}) X)$
8		brres	$⊢ X \in A \to (⟨X, Y⟩ ({1^{st} ↾}_{(A \times \{Y\})}) X \leftrightarrow (⟨X, Y⟩ \in (A \times \{Y\}) \land ⟨X, Y⟩ 1^{st} X))$
9	7 8	bitrd	$⊢ X \in A \to (X {({1^{st} ↾}_{(A \times \{Y\})})}^{-1} ⟨X, Y⟩ \leftrightarrow (⟨X, Y⟩ \in (A \times \{Y\}) \land ⟨X, Y⟩ 1^{st} X))$
10	9	adantr	$⊢ (X \in A \land Y \in V) \to (X {({1^{st} ↾}_{(A \times \{Y\})})}^{-1} ⟨X, Y⟩ \leftrightarrow (⟨X, Y⟩ \in (A \times \{Y\}) \land ⟨X, Y⟩ 1^{st} X))$
11		opelxp	$⊢ ⟨X, Y⟩ \in (A \times \{Y\}) \leftrightarrow (X \in A \land Y \in \{Y\})$
12	11	anbi1i	$⊢ (⟨X, Y⟩ \in (A \times \{Y\}) \land ⟨X, Y⟩ 1^{st} X) \leftrightarrow ((X \in A \land Y \in \{Y\}) \land ⟨X, Y⟩ 1^{st} X)$
13		br1steqg	$⊢ (X \in A \land Y \in V) \to (⟨X, Y⟩ 1^{st} X \leftrightarrow X = X)$
14	13	anbi2d	$⊢ (X \in A \land Y \in V) \to (((X \in A \land Y \in \{Y\}) \land ⟨X, Y⟩ 1^{st} X) \leftrightarrow ((X \in A \land Y \in \{Y\}) \land X = X))$
15	12 14	bitrid	$⊢ (X \in A \land Y \in V) \to ((⟨X, Y⟩ \in (A \times \{Y\}) \land ⟨X, Y⟩ 1^{st} X) \leftrightarrow ((X \in A \land Y \in \{Y\}) \land X = X))$
16	10 15	bitrd	$⊢ (X \in A \land Y \in V) \to (X {({1^{st} ↾}_{(A \times \{Y\})})}^{-1} ⟨X, Y⟩ \leftrightarrow ((X \in A \land Y \in \{Y\}) \land X = X))$
17	4 16	mpbird	$⊢ (X \in A \land Y \in V) \to X {({1^{st} ↾}_{(A \times \{Y\})})}^{-1} ⟨X, Y⟩$
18		1stconst	$⊢ Y \in V \to ({1^{st} ↾}_{(A \times \{Y\})}) : A \times \{Y\} \underset{1-1 onto}{⟶} A$
19		f1ocnv	$⊢ ({1^{st} ↾}_{(A \times \{Y\})}) : A \times \{Y\} \underset{1-1 onto}{⟶} A \to {({1^{st} ↾}_{(A \times \{Y\})})}^{-1} : A \underset{1-1 onto}{⟶} A \times \{Y\}$
20		f1ofn	$⊢ {({1^{st} ↾}_{(A \times \{Y\})})}^{-1} : A \underset{1-1 onto}{⟶} A \times \{Y\} \to {({1^{st} ↾}_{(A \times \{Y\})})}^{-1} Fn A$
21	18 19 20	3syl	$⊢ Y \in V \to {({1^{st} ↾}_{(A \times \{Y\})})}^{-1} Fn A$
22		simpl	$⊢ (X \in A \land Y \in V) \to X \in A$
23		fnbrfvb	$⊢ ({({1^{st} ↾}_{(A \times \{Y\})})}^{-1} Fn A \land X \in A) \to ({({1^{st} ↾}_{(A \times \{Y\})})}^{-1} (X) = ⟨X, Y⟩ \leftrightarrow X {({1^{st} ↾}_{(A \times \{Y\})})}^{-1} ⟨X, Y⟩)$
24	21 22 23	syl2an2	$⊢ (X \in A \land Y \in V) \to ({({1^{st} ↾}_{(A \times \{Y\})})}^{-1} (X) = ⟨X, Y⟩ \leftrightarrow X {({1^{st} ↾}_{(A \times \{Y\})})}^{-1} ⟨X, Y⟩)$
25	17 24	mpbird	$⊢ (X \in A \land Y \in V) \to {({1^{st} ↾}_{(A \times \{Y\})})}^{-1} (X) = ⟨X, Y⟩$

Metamath Proof Explorer

Theorem fv1stcnv

Proof