ofpreima

Description: Express the preimage of a function operation as a union of preimages. (Contributed by Thierry Arnoux, 8-Mar-2018)

	Ref	Expression
Hypotheses	ofpreima.1	$⊢ φ \to F : A ⟶ B$
	ofpreima.2	$⊢ φ \to G : A ⟶ C$
	ofpreima.3	$⊢ φ \to A \in V$
	ofpreima.4	$⊢ φ \to R Fn (B \times C)$
Assertion	ofpreima	$⊢ φ \to {(F R_{f} G)}^{-1} [D] = ⋃_{p \in R^{-1} [D]} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}])$

Proof

Step	Hyp	Ref	Expression
1		ofpreima.1	$⊢ φ \to F : A ⟶ B$
2		ofpreima.2	$⊢ φ \to G : A ⟶ C$
3		ofpreima.3	$⊢ φ \to A \in V$
4		ofpreima.4	$⊢ φ \to R Fn (B \times C)$
5		nfmpt1	$⊢ \underline{Ⅎ} s (s \in A ⟼ ⟨F (s), G (s)⟩)$
6		eqidd	$⊢ φ \to (s \in A ⟼ ⟨F (s), G (s)⟩) = (s \in A ⟼ ⟨F (s), G (s)⟩)$
7		fnov	$⊢ R Fn (B \times C) \leftrightarrow R = (x \in B, y \in C ⟼ x R y)$
8	4 7	sylib	$⊢ φ \to R = (x \in B, y \in C ⟼ x R y)$
9	5 1 2 3 6 8	ofoprabco	$⊢ φ \to F R_{f} G = R \circ (s \in A ⟼ ⟨F (s), G (s)⟩)$
10	9	cnveqd	$⊢ φ \to {(F R_{f} G)}^{-1} = {(R \circ (s \in A ⟼ ⟨F (s), G (s)⟩))}^{-1}$
11		cnvco	$⊢ {(R \circ (s \in A ⟼ ⟨F (s), G (s)⟩))}^{-1} = {(s \in A ⟼ ⟨F (s), G (s)⟩)}^{-1} \circ R^{-1}$
12	10 11	eqtrdi	$⊢ φ \to {(F R_{f} G)}^{-1} = {(s \in A ⟼ ⟨F (s), G (s)⟩)}^{-1} \circ R^{-1}$
13	12	imaeq1d	$⊢ φ \to {(F R_{f} G)}^{-1} [D] = ({(s \in A ⟼ ⟨F (s), G (s)⟩)}^{-1} \circ R^{-1}) [D]$
14		imaco	$⊢ ({(s \in A ⟼ ⟨F (s), G (s)⟩)}^{-1} \circ R^{-1}) [D] = {(s \in A ⟼ ⟨F (s), G (s)⟩)}^{-1} [R^{-1} [D]]$
15	13 14	eqtrdi	$⊢ φ \to {(F R_{f} G)}^{-1} [D] = {(s \in A ⟼ ⟨F (s), G (s)⟩)}^{-1} [R^{-1} [D]]$
16		dfima2	$⊢ {(s \in A ⟼ ⟨F (s), G (s)⟩)}^{-1} [R^{-1} [D]] = \{q \| \exists p \in R^{-1} [D] p {(s \in A ⟼ ⟨F (s), G (s)⟩)}^{-1} q\}$
17		vex	$⊢ p \in V$
18		vex	$⊢ q \in V$
19	17 18	brcnv	$⊢ p {(s \in A ⟼ ⟨F (s), G (s)⟩)}^{-1} q \leftrightarrow q (s \in A ⟼ ⟨F (s), G (s)⟩) p$
20		funmpt	$⊢ Fun (s \in A ⟼ ⟨F (s), G (s)⟩)$
21		funbrfv2b	$⊢ Fun (s \in A ⟼ ⟨F (s), G (s)⟩) \to (q (s \in A ⟼ ⟨F (s), G (s)⟩) p \leftrightarrow (q \in dom (s \in A ⟼ ⟨F (s), G (s)⟩) \land (s \in A ⟼ ⟨F (s), G (s)⟩) (q) = p))$
22	20 21	ax-mp	$⊢ q (s \in A ⟼ ⟨F (s), G (s)⟩) p \leftrightarrow (q \in dom (s \in A ⟼ ⟨F (s), G (s)⟩) \land (s \in A ⟼ ⟨F (s), G (s)⟩) (q) = p)$
23		opex	$⊢ ⟨F (s), G (s)⟩ \in V$
24		eqid	$⊢ (s \in A ⟼ ⟨F (s), G (s)⟩) = (s \in A ⟼ ⟨F (s), G (s)⟩)$
25	23 24	dmmpti	$⊢ dom (s \in A ⟼ ⟨F (s), G (s)⟩) = A$
26	25	eleq2i	$⊢ q \in dom (s \in A ⟼ ⟨F (s), G (s)⟩) \leftrightarrow q \in A$
27	26	anbi1i	$⊢ (q \in dom (s \in A ⟼ ⟨F (s), G (s)⟩) \land (s \in A ⟼ ⟨F (s), G (s)⟩) (q) = p) \leftrightarrow (q \in A \land (s \in A ⟼ ⟨F (s), G (s)⟩) (q) = p)$
28	22 27	bitri	$⊢ q (s \in A ⟼ ⟨F (s), G (s)⟩) p \leftrightarrow (q \in A \land (s \in A ⟼ ⟨F (s), G (s)⟩) (q) = p)$
29		fveq2	$⊢ s = q \to F (s) = F (q)$
30		fveq2	$⊢ s = q \to G (s) = G (q)$
31	29 30	opeq12d	$⊢ s = q \to ⟨F (s), G (s)⟩ = ⟨F (q), G (q)⟩$
32		opex	$⊢ ⟨F (q), G (q)⟩ \in V$
33	31 24 32	fvmpt	$⊢ q \in A \to (s \in A ⟼ ⟨F (s), G (s)⟩) (q) = ⟨F (q), G (q)⟩$
34	33	eqeq1d	$⊢ q \in A \to ((s \in A ⟼ ⟨F (s), G (s)⟩) (q) = p \leftrightarrow ⟨F (q), G (q)⟩ = p)$
35	34	pm5.32i	$⊢ (q \in A \land (s \in A ⟼ ⟨F (s), G (s)⟩) (q) = p) \leftrightarrow (q \in A \land ⟨F (q), G (q)⟩ = p)$
36	19 28 35	3bitri	$⊢ p {(s \in A ⟼ ⟨F (s), G (s)⟩)}^{-1} q \leftrightarrow (q \in A \land ⟨F (q), G (q)⟩ = p)$
37	36	rexbii	$⊢ \exists p \in R^{-1} [D] p {(s \in A ⟼ ⟨F (s), G (s)⟩)}^{-1} q \leftrightarrow \exists p \in R^{-1} [D] (q \in A \land ⟨F (q), G (q)⟩ = p)$
38	37	abbii	$⊢ \{q \| \exists p \in R^{-1} [D] p {(s \in A ⟼ ⟨F (s), G (s)⟩)}^{-1} q\} = \{q \| \exists p \in R^{-1} [D] (q \in A \land ⟨F (q), G (q)⟩ = p)\}$
39		nfv	$⊢ Ⅎ q φ$
40		nfab1	$⊢ \underline{Ⅎ} q \{q \| \exists p \in R^{-1} [D] (q \in A \land ⟨F (q), G (q)⟩ = p)\}$
41		nfcv	$⊢ \underline{Ⅎ} q ⋃_{p \in R^{-1} [D]} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}])$
42		eliun	$⊢ q \in ⋃_{p \in R^{-1} [D]} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}]) \leftrightarrow \exists p \in R^{-1} [D] q \in (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}])$
43		ffn	$⊢ F : A ⟶ B \to F Fn A$
44		fniniseg	$⊢ F Fn A \to (q \in F^{-1} [\{1^{st} (p)\}] \leftrightarrow (q \in A \land F (q) = 1^{st} (p)))$
45	1 43 44	3syl	$⊢ φ \to (q \in F^{-1} [\{1^{st} (p)\}] \leftrightarrow (q \in A \land F (q) = 1^{st} (p)))$
46		ffn	$⊢ G : A ⟶ C \to G Fn A$
47		fniniseg	$⊢ G Fn A \to (q \in G^{-1} [\{2^{nd} (p)\}] \leftrightarrow (q \in A \land G (q) = 2^{nd} (p)))$
48	2 46 47	3syl	$⊢ φ \to (q \in G^{-1} [\{2^{nd} (p)\}] \leftrightarrow (q \in A \land G (q) = 2^{nd} (p)))$
49	45 48	anbi12d	$⊢ φ \to ((q \in F^{-1} [\{1^{st} (p)\}] \land q \in G^{-1} [\{2^{nd} (p)\}]) \leftrightarrow ((q \in A \land F (q) = 1^{st} (p)) \land (q \in A \land G (q) = 2^{nd} (p))))$
50		elin	$⊢ q \in (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}]) \leftrightarrow (q \in F^{-1} [\{1^{st} (p)\}] \land q \in G^{-1} [\{2^{nd} (p)\}])$
51		anandi	$⊢ (q \in A \land (F (q) = 1^{st} (p) \land G (q) = 2^{nd} (p))) \leftrightarrow ((q \in A \land F (q) = 1^{st} (p)) \land (q \in A \land G (q) = 2^{nd} (p)))$
52	49 50 51	3bitr4g	$⊢ φ \to (q \in (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}]) \leftrightarrow (q \in A \land (F (q) = 1^{st} (p) \land G (q) = 2^{nd} (p))))$
53	52	adantr	$⊢ (φ \land p \in R^{-1} [D]) \to (q \in (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}]) \leftrightarrow (q \in A \land (F (q) = 1^{st} (p) \land G (q) = 2^{nd} (p))))$
54		cnvimass	$⊢ R^{-1} [D] \subseteq dom R$
55	4	fndmd	$⊢ φ \to dom R = B \times C$
56	54 55	sseqtrid	$⊢ φ \to R^{-1} [D] \subseteq B \times C$
57	56	sselda	$⊢ (φ \land p \in R^{-1} [D]) \to p \in (B \times C)$
58		1st2nd2	$⊢ p \in (B \times C) \to p = ⟨1^{st} (p), 2^{nd} (p)⟩$
59		eqeq2	$⊢ p = ⟨1^{st} (p), 2^{nd} (p)⟩ \to (⟨F (q), G (q)⟩ = p \leftrightarrow ⟨F (q), G (q)⟩ = ⟨1^{st} (p), 2^{nd} (p)⟩)$
60	57 58 59	3syl	$⊢ (φ \land p \in R^{-1} [D]) \to (⟨F (q), G (q)⟩ = p \leftrightarrow ⟨F (q), G (q)⟩ = ⟨1^{st} (p), 2^{nd} (p)⟩)$
61		fvex	$⊢ F (q) \in V$
62		fvex	$⊢ G (q) \in V$
63	61 62	opth	$⊢ ⟨F (q), G (q)⟩ = ⟨1^{st} (p), 2^{nd} (p)⟩ \leftrightarrow (F (q) = 1^{st} (p) \land G (q) = 2^{nd} (p))$
64	60 63	bitrdi	$⊢ (φ \land p \in R^{-1} [D]) \to (⟨F (q), G (q)⟩ = p \leftrightarrow (F (q) = 1^{st} (p) \land G (q) = 2^{nd} (p)))$
65	64	anbi2d	$⊢ (φ \land p \in R^{-1} [D]) \to ((q \in A \land ⟨F (q), G (q)⟩ = p) \leftrightarrow (q \in A \land (F (q) = 1^{st} (p) \land G (q) = 2^{nd} (p))))$
66	53 65	bitr4d	$⊢ (φ \land p \in R^{-1} [D]) \to (q \in (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}]) \leftrightarrow (q \in A \land ⟨F (q), G (q)⟩ = p))$
67	66	rexbidva	$⊢ φ \to (\exists p \in R^{-1} [D] q \in (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}]) \leftrightarrow \exists p \in R^{-1} [D] (q \in A \land ⟨F (q), G (q)⟩ = p))$
68		abid	$⊢ q \in \{q \| \exists p \in R^{-1} [D] (q \in A \land ⟨F (q), G (q)⟩ = p)\} \leftrightarrow \exists p \in R^{-1} [D] (q \in A \land ⟨F (q), G (q)⟩ = p)$
69	67 68	bitr4di	$⊢ φ \to (\exists p \in R^{-1} [D] q \in (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}]) \leftrightarrow q \in \{q \| \exists p \in R^{-1} [D] (q \in A \land ⟨F (q), G (q)⟩ = p)\})$
70	42 69	bitr2id	$⊢ φ \to (q \in \{q \| \exists p \in R^{-1} [D] (q \in A \land ⟨F (q), G (q)⟩ = p)\} \leftrightarrow q \in ⋃_{p \in R^{-1} [D]} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}]))$
71	39 40 41 70	eqrd	$⊢ φ \to \{q \| \exists p \in R^{-1} [D] (q \in A \land ⟨F (q), G (q)⟩ = p)\} = ⋃_{p \in R^{-1} [D]} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}])$
72	38 71	syl5eq	$⊢ φ \to \{q \| \exists p \in R^{-1} [D] p {(s \in A ⟼ ⟨F (s), G (s)⟩)}^{-1} q\} = ⋃_{p \in R^{-1} [D]} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}])$
73	16 72	syl5eq	$⊢ φ \to {(s \in A ⟼ ⟨F (s), G (s)⟩)}^{-1} [R^{-1} [D]] = ⋃_{p \in R^{-1} [D]} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}])$
74	15 73	eqtrd	$⊢ φ \to {(F R_{f} G)}^{-1} [D] = ⋃_{p \in R^{-1} [D]} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}])$

Metamath Proof Explorer

Theorem ofpreima

Proof