fv2ndcnv

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

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

Proof

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

Metamath Proof Explorer

Theorem fv2ndcnv

Proof