ofpreima2

Description: Express the preimage of a function operation as a union of preimages. This version of ofpreima iterates the union over a smaller set. (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	ofpreima2	$⊢ φ \to {(F R_{f} G)}^{-1} [D] = ⋃_{p \in R^{-1} [D] \cap (ran F \times ran G)} (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	1 2 3 4	ofpreima	$⊢ φ \to {(F R_{f} G)}^{-1} [D] = ⋃_{p \in R^{-1} [D]} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}])$
6		inundif	$⊢ (R^{-1} [D] \cap (ran F \times ran G)) \cup (R^{-1} [D] ∖ (ran F \times ran G)) = R^{-1} [D]$
7		iuneq1	$⊢ (R^{-1} [D] \cap (ran F \times ran G)) \cup (R^{-1} [D] ∖ (ran F \times ran G)) = R^{-1} [D] \to ⋃_{p \in (R^{-1} [D] \cap (ran F \times ran G)) \cup (R^{-1} [D] ∖ (ran F \times ran G))} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}]) = ⋃_{p \in R^{-1} [D]} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}])$
8	6 7	ax-mp	$⊢ ⋃_{p \in (R^{-1} [D] \cap (ran F \times ran G)) \cup (R^{-1} [D] ∖ (ran F \times ran G))} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}]) = ⋃_{p \in R^{-1} [D]} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}])$
9		iunxun	$⊢ ⋃_{p \in (R^{-1} [D] \cap (ran F \times ran G)) \cup (R^{-1} [D] ∖ (ran F \times ran G))} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}]) = ⋃_{p \in R^{-1} [D] \cap (ran F \times ran G)} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}]) \cup ⋃_{p \in R^{-1} [D] ∖ (ran F \times ran G)} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}])$
10	8 9	eqtr3i	$⊢ ⋃_{p \in R^{-1} [D]} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}]) = ⋃_{p \in R^{-1} [D] \cap (ran F \times ran G)} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}]) \cup ⋃_{p \in R^{-1} [D] ∖ (ran F \times ran G)} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}])$
11	5 10	eqtrdi	$⊢ φ \to {(F R_{f} G)}^{-1} [D] = ⋃_{p \in R^{-1} [D] \cap (ran F \times ran G)} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}]) \cup ⋃_{p \in R^{-1} [D] ∖ (ran F \times ran G)} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}])$
12		simpr	$⊢ (φ \land p \in (R^{-1} [D] ∖ (ran F \times ran G))) \to p \in (R^{-1} [D] ∖ (ran F \times ran G))$
13	12	eldifbd	$⊢ (φ \land p \in (R^{-1} [D] ∖ (ran F \times ran G))) \to \neg p \in (ran F \times ran G)$
14		cnvimass	$⊢ R^{-1} [D] \subseteq dom R$
15	4	fndmd	$⊢ φ \to dom R = B \times C$
16	14 15	sseqtrid	$⊢ φ \to R^{-1} [D] \subseteq B \times C$
17	16	ssdifssd	$⊢ φ \to R^{-1} [D] ∖ (ran F \times ran G) \subseteq B \times C$
18	17	sselda	$⊢ (φ \land p \in (R^{-1} [D] ∖ (ran F \times ran G))) \to p \in (B \times C)$
19		1st2nd2	$⊢ p \in (B \times C) \to p = ⟨1^{st} (p), 2^{nd} (p)⟩$
20		elxp6	$⊢ p \in (ran F \times ran G) \leftrightarrow (p = ⟨1^{st} (p), 2^{nd} (p)⟩ \land (1^{st} (p) \in ran F \land 2^{nd} (p) \in ran G))$
21	20	simplbi2	$⊢ p = ⟨1^{st} (p), 2^{nd} (p)⟩ \to ((1^{st} (p) \in ran F \land 2^{nd} (p) \in ran G) \to p \in (ran F \times ran G))$
22	18 19 21	3syl	$⊢ (φ \land p \in (R^{-1} [D] ∖ (ran F \times ran G))) \to ((1^{st} (p) \in ran F \land 2^{nd} (p) \in ran G) \to p \in (ran F \times ran G))$
23	13 22	mtod	$⊢ (φ \land p \in (R^{-1} [D] ∖ (ran F \times ran G))) \to \neg (1^{st} (p) \in ran F \land 2^{nd} (p) \in ran G)$
24		ianor	$⊢ \neg (1^{st} (p) \in ran F \land 2^{nd} (p) \in ran G) \leftrightarrow (\neg 1^{st} (p) \in ran F \lor \neg 2^{nd} (p) \in ran G)$
25	23 24	sylib	$⊢ (φ \land p \in (R^{-1} [D] ∖ (ran F \times ran G))) \to (\neg 1^{st} (p) \in ran F \lor \neg 2^{nd} (p) \in ran G)$
26		disjsn	$⊢ ran F \cap \{1^{st} (p)\} = \emptyset \leftrightarrow \neg 1^{st} (p) \in ran F$
27		disjsn	$⊢ ran G \cap \{2^{nd} (p)\} = \emptyset \leftrightarrow \neg 2^{nd} (p) \in ran G$
28	26 27	orbi12i	$⊢ (ran F \cap \{1^{st} (p)\} = \emptyset \lor ran G \cap \{2^{nd} (p)\} = \emptyset) \leftrightarrow (\neg 1^{st} (p) \in ran F \lor \neg 2^{nd} (p) \in ran G)$
29	25 28	sylibr	$⊢ (φ \land p \in (R^{-1} [D] ∖ (ran F \times ran G))) \to (ran F \cap \{1^{st} (p)\} = \emptyset \lor ran G \cap \{2^{nd} (p)\} = \emptyset)$
30	1	ffnd	$⊢ φ \to F Fn A$
31		dffn3	$⊢ F Fn A \leftrightarrow F : A ⟶ ran F$
32	30 31	sylib	$⊢ φ \to F : A ⟶ ran F$
33	2	ffnd	$⊢ φ \to G Fn A$
34		dffn3	$⊢ G Fn A \leftrightarrow G : A ⟶ ran G$
35	33 34	sylib	$⊢ φ \to G : A ⟶ ran G$
36	35	adantr	$⊢ (φ \land p \in (R^{-1} [D] ∖ (ran F \times ran G))) \to G : A ⟶ ran G$
37		fimacnvdisj	$⊢ (F : A ⟶ ran F \land ran F \cap \{1^{st} (p)\} = \emptyset) \to F^{-1} [\{1^{st} (p)\}] = \emptyset$
38		ineq1	$⊢ F^{-1} [\{1^{st} (p)\}] = \emptyset \to F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}] = \emptyset \cap G^{-1} [\{2^{nd} (p)\}]$
39		0in	$⊢ \emptyset \cap G^{-1} [\{2^{nd} (p)\}] = \emptyset$
40	38 39	eqtrdi	$⊢ F^{-1} [\{1^{st} (p)\}] = \emptyset \to F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}] = \emptyset$
41	37 40	syl	$⊢ (F : A ⟶ ran F \land ran F \cap \{1^{st} (p)\} = \emptyset) \to F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}] = \emptyset$
42	41	ex	$⊢ F : A ⟶ ran F \to (ran F \cap \{1^{st} (p)\} = \emptyset \to F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}] = \emptyset)$
43		fimacnvdisj	$⊢ (G : A ⟶ ran G \land ran G \cap \{2^{nd} (p)\} = \emptyset) \to G^{-1} [\{2^{nd} (p)\}] = \emptyset$
44		ineq2	$⊢ G^{-1} [\{2^{nd} (p)\}] = \emptyset \to F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}] = F^{-1} [\{1^{st} (p)\}] \cap \emptyset$
45		in0	$⊢ F^{-1} [\{1^{st} (p)\}] \cap \emptyset = \emptyset$
46	44 45	eqtrdi	$⊢ G^{-1} [\{2^{nd} (p)\}] = \emptyset \to F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}] = \emptyset$
47	43 46	syl	$⊢ (G : A ⟶ ran G \land ran G \cap \{2^{nd} (p)\} = \emptyset) \to F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}] = \emptyset$
48	47	ex	$⊢ G : A ⟶ ran G \to (ran G \cap \{2^{nd} (p)\} = \emptyset \to F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}] = \emptyset)$
49	42 48	jaao	$⊢ (F : A ⟶ ran F \land G : A ⟶ ran G) \to ((ran F \cap \{1^{st} (p)\} = \emptyset \lor ran G \cap \{2^{nd} (p)\} = \emptyset) \to F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}] = \emptyset)$
50	32 36 49	syl2an2r	$⊢ (φ \land p \in (R^{-1} [D] ∖ (ran F \times ran G))) \to ((ran F \cap \{1^{st} (p)\} = \emptyset \lor ran G \cap \{2^{nd} (p)\} = \emptyset) \to F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}] = \emptyset)$
51	29 50	mpd	$⊢ (φ \land p \in (R^{-1} [D] ∖ (ran F \times ran G))) \to F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}] = \emptyset$
52	51	iuneq2dv	$⊢ φ \to ⋃_{p \in R^{-1} [D] ∖ (ran F \times ran G)} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}]) = ⋃_{p \in R^{-1} [D] ∖ (ran F \times ran G)} \emptyset$
53		iun0	$⊢ ⋃_{p \in R^{-1} [D] ∖ (ran F \times ran G)} \emptyset = \emptyset$
54	52 53	eqtrdi	$⊢ φ \to ⋃_{p \in R^{-1} [D] ∖ (ran F \times ran G)} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}]) = \emptyset$
55	54	uneq2d	$⊢ φ \to ⋃_{p \in R^{-1} [D] \cap (ran F \times ran G)} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}]) \cup ⋃_{p \in R^{-1} [D] ∖ (ran F \times ran G)} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}]) = ⋃_{p \in R^{-1} [D] \cap (ran F \times ran G)} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}]) \cup \emptyset$
56		un0	$⊢ ⋃_{p \in R^{-1} [D] \cap (ran F \times ran G)} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}]) \cup \emptyset = ⋃_{p \in R^{-1} [D] \cap (ran F \times ran G)} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}])$
57	55 56	eqtrdi	$⊢ φ \to ⋃_{p \in R^{-1} [D] \cap (ran F \times ran G)} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}]) \cup ⋃_{p \in R^{-1} [D] ∖ (ran F \times ran G)} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}]) = ⋃_{p \in R^{-1} [D] \cap (ran F \times ran G)} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}])$
58	11 57	eqtrd	$⊢ φ \to {(F R_{f} G)}^{-1} [D] = ⋃_{p \in R^{-1} [D] \cap (ran F \times ran G)} (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}])$

Metamath Proof Explorer

Theorem ofpreima2

Proof