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	biimpi	$⊢ Rel A \to A \subseteq V \times V$
23	22	adantr	$⊢ (Rel A \land X \in V) \to A \subseteq V \times V$
24	23	sselda	$⊢ ((Rel A \land X \in V) \land z \in A) \to z \in (V \times V)$
25	24	adantrr	$⊢ ((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \to z \in (V \times V)$
26	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)$
27		simprr	$⊢ ((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \to ({1^{st} ↾}_{A}) (z) = X$
28	26 27	eqtr3d	$⊢ ((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \to 1^{st} (z) = X$
29	28 5	sylibr	$⊢ ((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \to 1^{st} (z) \in \{X\}$
30	28 29	eqeltrrd	$⊢ ((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \to X \in \{X\}$
31		simpr	$⊢ (((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \land x = X) \to x = X$
32	31	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)⟩$
33	32	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)$
34		1st2nd	$⊢ (Rel A \land z \in A) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
35	34	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)⟩$
36	28	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)⟩$
37	35 36	eqtrd	$⊢ ((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \to z = ⟨X, 2^{nd} (z)⟩$
38		simprl	$⊢ ((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \to z \in A$
39	37 38	eqeltrrd	$⊢ ((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \to ⟨X, 2^{nd} (z)⟩ \in A$
40	30 33 39	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$
41		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)$
42	40 41	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)$
43		fvex	$⊢ 2^{nd} (z) \in V$
44	43	elima3	$⊢ 2^{nd} (z) \in A [\{X\}] \leftrightarrow \exists x (x \in \{X\} \land ⟨x, 2^{nd} (z)⟩ \in A)$
45	42 44	sylibr	$⊢ ((Rel A \land X \in V) \land (z \in A \land ({1^{st} ↾}_{A}) (z) = X)) \to 2^{nd} (z) \in A [\{X\}]$
46	29 45	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\}])$
47	25 46	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\}]))$
48	20 47	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))$
49		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\}]))$
50	49	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\}])))$
51		fo1st	$⊢ 1^{st} : V \underset{onto}{⟶} V$
52		fofn	$⊢ 1^{st} : V \underset{onto}{⟶} V \to 1^{st} Fn V$
53	51 52	ax-mp	$⊢ 1^{st} Fn V$
54		ssv	$⊢ A \subseteq V$
55		fnssres	$⊢ (1^{st} Fn V \land A \subseteq V) \to ({1^{st} ↾}_{A}) Fn A$
56	53 54 55	mp2an	$⊢ ({1^{st} ↾}_{A}) Fn A$
57		fniniseg	$⊢ ({1^{st} ↾}_{A}) Fn A \to (z \in {({1^{st} ↾}_{A})}^{-1} [\{X\}] \leftrightarrow (z \in A \land ({1^{st} ↾}_{A}) (z) = X))$
58	56 57	ax-mp	$⊢ z \in {({1^{st} ↾}_{A})}^{-1} [\{X\}] \leftrightarrow (z \in A \land ({1^{st} ↾}_{A}) (z) = X)$
59	58	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))$
60	48 50 59	3bitr4rd	$⊢ (Rel A \land X \in V) \to (z \in {({1^{st} ↾}_{A})}^{-1} [\{X\}] \leftrightarrow z \in (\{X\} \times A [\{X\}]))$
61	60	eqrdv	$⊢ (Rel A \land X \in V) \to {({1^{st} ↾}_{A})}^{-1} [\{X\}] = \{X\} \times A [\{X\}]$

Metamath Proof Explorer

Theorem 1stpreimas

Proof