1stpreimas

Description: The preimage of a singleton. (Contributed by Thierry Arnoux, 27-Apr-2020)

		Ref	Expression
	Assertion	1stpreimas	$⊢ (Rel A \land X \in V) \to {({1^{st} ↾}_{A})}^{-1} [\{X\}] = \{X\} \times A [\{X\}]$

Proof

Step	Hyp	Ref	Expression
1		1st2ndb	$⊢ z \in (V \times V) \leftrightarrow z = ⟨1^{st} (z), 2^{nd} (z)⟩$
2	1	biimpi	$⊢ z \in (V \times V) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
3	2	ad2antrl	$⊢ ((Rel A \land X \in V) \land (z \in (V \times V) \land (1^{st} (z) \in \{X\} \land 2^{nd} (z) \in A [\{X\}]))) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
4		fvex	$⊢ 1^{st} (z) \in V$
5	4	elsn	$⊢ 1^{st} (z) \in \{X\} \leftrightarrow 1^{st} (z) = X$
6	5	biimpi	$⊢ 1^{st} (z) \in \{X\} \to 1^{st} (z) = X$
7	6	ad2antrl	$⊢ (z \in (V \times V) \land (1^{st} (z) \in \{X\} \land 2^{nd} (z) \in A [\{X\}])) \to 1^{st} (z) = X$
8	7	adantl	$⊢ ((Rel A \land X \in V) \land (z \in (V \times V) \land (1^{st} (z) \in \{X\} \land 2^{nd} (z) \in A [\{X\}]))) \to 1^{st} (z) = X$
9	8	opeq1d	$⊢ ((Rel A \land X \in V) \land (z \in (V \times V) \land (1^{st} (z) \in \{X\} \land 2^{nd} (z) \in A [\{X\}]))) \to ⟨1^{st} (z), 2^{nd} (z)⟩ = ⟨X, 2^{nd} (z)⟩$
10	3 9	eqtrd	$⊢ ((Rel A \land X \in V) \land (z \in (V \times V) \land (1^{st} (z) \in \{X\} \land 2^{nd} (z) \in A [\{X\}]))) \to z = ⟨X, 2^{nd} (z)⟩$
11		simplr	$⊢ ((Rel A \land X \in V) \land (z \in (V \times V) \land (1^{st} (z) \in \{X\} \land 2^{nd} (z) \in A [\{X\}]))) \to X \in V$
12		simprrr	$⊢ ((Rel A \land X \in V) \land (z \in (V \times V) \land (1^{st} (z) \in \{X\} \land 2^{nd} (z) \in A [\{X\}]))) \to 2^{nd} (z) \in A [\{X\}]$
13		elimasng	$⊢ (X \in V \land 2^{nd} (z) \in A [\{X\}]) \to (2^{nd} (z) \in A [\{X\}] \leftrightarrow ⟨X, 2^{nd} (z)⟩ \in A)$
14	13	biimpa	$⊢ ((X \in V \land 2^{nd} (z) \in A [\{X\}]) \land 2^{nd} (z) \in A [\{X\}]) \to ⟨X, 2^{nd} (z)⟩ \in A$
15	11 12 12 14	syl21anc	$⊢ ((Rel A \land X \in V) \land (z \in (V \times V) \land (1^{st} (z) \in \{X\} \land 2^{nd} (z) \in A [\{X\}]))) \to ⟨X, 2^{nd} (z)⟩ \in A$
16	10 15	eqeltrd	$⊢ ((Rel A \land X \in V) \land (z \in (V \times V) \land (1^{st} (z) \in \{X\} \land 2^{nd} (z) \in A [\{X\}]))) \to z \in A$
17		fvres	$⊢ z \in A \to ({1^{st} ↾}_{A}) (z) = 1^{st} (z)$
18	16 17	syl	$⊢ ((Rel A \land X \in V) \land (z \in (V \times V) \land (1^{st} (z) \in \{X\} \land 2^{nd} (z) \in A [\{X\}]))) \to ({1^{st} ↾}_{A}) (z) = 1^{st} (z)$
19	18 8	eqtrd	$⊢ ((Rel A \land X \in V) \land (z \in (V \times V) \land (1^{st} (z) \in \{X\} \land 2^{nd} (z) \in A [\{X\}]))) \to ({1^{st} ↾}_{A}) (z) = X$
20	16 19	jca	$⊢ ((Rel A \land X \in V) \land (z \in (V \times V) \land (1^{st} (z) \in \{X\} \land 2^{nd} (z) \in A [\{X\}]))) \to (z \in A \land ({1^{st} ↾}_{A}) (z) = X)$
21		df-rel	$⊢ Rel A \leftrightarrow A \subseteq V \times V$
22	21	birani	$⊢ (Rel A \land X \in V) \to A \subseteq V \times V$
23	22	sselda	$⊢ ((Rel A \land X \in V) \land z \in A) \to z \in (V \times V)$
24	23	adantrr	$⊢ ((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \to z \in (V \times V)$
25	17	ad2antrl	$⊢ ((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \to ({1^{st} ↾}_{A}) (z) = 1^{st} (z)$
26		simprr	$⊢ ((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \to ({1^{st} ↾}_{A}) (z) = X$
27	25 26	eqtr3d	$⊢ ((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \to 1^{st} (z) = X$
28	27 5	sylibr	$⊢ ((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \to 1^{st} (z) \in \{X\}$
29	27 28	eqeltrrd	$⊢ ((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \to X \in \{X\}$
30		simpr	$⊢ (((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \land x = X) \to x = X$
31	30	opeq1d	$⊢ (((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \land x = X) \to ⟨x, 2^{nd} (z)⟩ = ⟨X, 2^{nd} (z)⟩$
32	31	eleq1d	$⊢ (((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \land x = X) \to (⟨x, 2^{nd} (z)⟩ \in A \leftrightarrow ⟨X, 2^{nd} (z)⟩ \in A)$
33		1st2nd	$⊢ (Rel A \land z \in A) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
34	33	ad2ant2r	$⊢ ((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
35	27	opeq1d	$⊢ ((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \to ⟨1^{st} (z), 2^{nd} (z)⟩ = ⟨X, 2^{nd} (z)⟩$
36	34 35	eqtrd	$⊢ ((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \to z = ⟨X, 2^{nd} (z)⟩$
37		simprl	$⊢ ((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \to z \in A$
38	36 37	eqeltrrd	$⊢ ((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \to ⟨X, 2^{nd} (z)⟩ \in A$
39	29 32 38	rspcedvd	$⊢ ((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \to \exists x \in \{X\} ⟨x, 2^{nd} (z)⟩ \in A$
40		df-rex	$⊢ \exists x \in \{X\} ⟨x, 2^{nd} (z)⟩ \in A \leftrightarrow \exists x (x \in \{X\} \land ⟨x, 2^{nd} (z)⟩ \in A)$
41	39 40	sylib	$⊢ ((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \to \exists x (x \in \{X\} \land ⟨x, 2^{nd} (z)⟩ \in A)$
42		fvex	$⊢ 2^{nd} (z) \in V$
43	42	elima3	$⊢ 2^{nd} (z) \in A [\{X\}] \leftrightarrow \exists x (x \in \{X\} \land ⟨x, 2^{nd} (z)⟩ \in A)$
44	41 43	sylibr	$⊢ ((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \to 2^{nd} (z) \in A [\{X\}]$
45	28 44	jca	$⊢ ((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \to (1^{st} (z) \in \{X\} \land 2^{nd} (z) \in A [\{X\}])$
46	24 45	jca	$⊢ ((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \to (z \in (V \times V) \land (1^{st} (z) \in \{X\} \land 2^{nd} (z) \in A [\{X\}]))$
47	20 46	impbida	$⊢ (Rel A \land X \in V) \to ((z \in (V \times V) \land (1^{st} (z) \in \{X\} \land 2^{nd} (z) \in A [\{X\}])) \leftrightarrow (z \in A \land ({1^{st} ↾}_{A}) (z) = X))$
48		elxp7	$⊢ z \in (\{X\} \times A [\{X\}]) \leftrightarrow (z \in (V \times V) \land (1^{st} (z) \in \{X\} \land 2^{nd} (z) \in A [\{X\}]))$
49	48	a1i	$⊢ (Rel A \land X \in V) \to (z \in (\{X\} \times A [\{X\}]) \leftrightarrow (z \in (V \times V) \land (1^{st} (z) \in \{X\} \land 2^{nd} (z) \in A [\{X\}])))$
50		fo1st	$⊢ 1^{st} : V \underset{onto}{⟶} V$
51		fofn	$⊢ 1^{st} : V \underset{onto}{⟶} V \to 1^{st} Fn V$
52	50 51	ax-mp	$⊢ 1^{st} Fn V$
53		ssv	$⊢ A \subseteq V$
54		fnssres	$⊢ (1^{st} Fn V \land A \subseteq V) \to ({1^{st} ↾}_{A}) Fn A$
55	52 53 54	mp2an	$⊢ ({1^{st} ↾}_{A}) Fn A$
56		fniniseg	$⊢ ({1^{st} ↾}_{A}) Fn A \to (z \in {({1^{st} ↾}_{A})}^{-1} [\{X\}] \leftrightarrow (z \in A \land ({1^{st} ↾}_{A}) (z) = X))$
57	55 56	ax-mp	$⊢ z \in {({1^{st} ↾}_{A})}^{-1} [\{X\}] \leftrightarrow (z \in A \land ({1^{st} ↾}_{A}) (z) = X)$
58	57	a1i	$⊢ (Rel A \land X \in V) \to (z \in {({1^{st} ↾}_{A})}^{-1} [\{X\}] \leftrightarrow (z \in A \land ({1^{st} ↾}_{A}) (z) = X))$
59	47 49 58	3bitr4rd	$⊢ (Rel A \land X \in V) \to (z \in {({1^{st} ↾}_{A})}^{-1} [\{X\}] \leftrightarrow z \in (\{X\} \times A [\{X\}]))$
60	59	eqrdv	$⊢ (Rel A \land X \in V) \to {({1^{st} ↾}_{A})}^{-1} [\{X\}] = \{X\} \times A [\{X\}]$

Metamath Proof Explorer

Theorem 1stpreimas

Proof