bj-imdirco

Description: Functorial property of the direct image: the direct image by a composition is the composition of the direct images. (Contributed by BJ, 23-May-2024)

	Ref	Expression
Hypotheses	bj-imdirco.exa	$⊢ φ \to A \in U$
	bj-imdirco.exb	$⊢ φ \to B \in V$
	bj-imdirco.exc	$⊢ φ \to C \in W$
	bj-imdirco.arg1	$⊢ φ \to R \subseteq A \times B$
	bj-imdirco.arg2	$⊢ φ \to S \subseteq B \times C$
Assertion	bj-imdirco	$⊢ φ \to (A 𝒫_{} C) (S \circ R) = (B 𝒫_{} C) (S) \circ (A 𝒫_{*} B) (R)$

Proof

Step	Hyp	Ref	Expression
1		bj-imdirco.exa	$⊢ φ \to A \in U$
2		bj-imdirco.exb	$⊢ φ \to B \in V$
3		bj-imdirco.exc	$⊢ φ \to C \in W$
4		bj-imdirco.arg1	$⊢ φ \to R \subseteq A \times B$
5		bj-imdirco.arg2	$⊢ φ \to S \subseteq B \times C$
6		imaco	$⊢ (S \circ R) [x] = S [R [x]]$
7	6	eqeq1i	$⊢ (S \circ R) [x] = z \leftrightarrow S [R [x]] = z$
8	7	anbi2i	$⊢ ((x \subseteq A \land z \subseteq C) \land (S \circ R) [x] = z) \leftrightarrow ((x \subseteq A \land z \subseteq C) \land S [R [x]] = z)$
9	8	a1i	$⊢ φ \to (((x \subseteq A \land z \subseteq C) \land (S \circ R) [x] = z) \leftrightarrow ((x \subseteq A \land z \subseteq C) \land S [R [x]] = z))$
10	1 2	xpexd	$⊢ φ \to A \times B \in V$
11	10 4	ssexd	$⊢ φ \to R \in V$
12		imaexg	$⊢ R \in V \to R [x] \in V$
13	11 12	syl	$⊢ φ \to R [x] \in V$
14		imass1	$⊢ R \subseteq A \times B \to R [x] \subseteq (A \times B) [x]$
15		xpima	$⊢ (A \times B) [x] = if (A \cap x = \emptyset, \emptyset, B)$
16		simpr	$⊢ (A \cap x = \emptyset \land u \in \emptyset) \to u \in \emptyset$
17		simpr	$⊢ (\neg A \cap x = \emptyset \land u \in B) \to u \in B$
18	16 17	orim12i	$⊢ ((A \cap x = \emptyset \land u \in \emptyset) \lor (\neg A \cap x = \emptyset \land u \in B)) \to (u \in \emptyset \lor u \in B)$
19		elif	$⊢ u \in if (A \cap x = \emptyset, \emptyset, B) \leftrightarrow ((A \cap x = \emptyset \land u \in \emptyset) \lor (\neg A \cap x = \emptyset \land u \in B))$
20		elun	$⊢ u \in (\emptyset \cup B) \leftrightarrow (u \in \emptyset \lor u \in B)$
21	18 19 20	3imtr4i	$⊢ u \in if (A \cap x = \emptyset, \emptyset, B) \to u \in (\emptyset \cup B)$
22	21	ssriv	$⊢ if (A \cap x = \emptyset, \emptyset, B) \subseteq \emptyset \cup B$
23		0ss	$⊢ \emptyset \subseteq B$
24		ssid	$⊢ B \subseteq B$
25	23 24	unssi	$⊢ \emptyset \cup B \subseteq B$
26	22 25	sstri	$⊢ if (A \cap x = \emptyset, \emptyset, B) \subseteq B$
27	15 26	eqsstri	$⊢ (A \times B) [x] \subseteq B$
28	14 27	sstrdi	$⊢ R \subseteq A \times B \to R [x] \subseteq B$
29	4 28	syl	$⊢ φ \to R [x] \subseteq B$
30		eqidd	$⊢ φ \to R [x] = R [x]$
31	29 30	jca	$⊢ φ \to (R [x] \subseteq B \land R [x] = R [x])$
32		sseq1	$⊢ y = R [x] \to (y \subseteq B \leftrightarrow R [x] \subseteq B)$
33		eqeq2	$⊢ y = R [x] \to (R [x] = y \leftrightarrow R [x] = R [x])$
34	32 33	anbi12d	$⊢ y = R [x] \to ((y \subseteq B \land R [x] = y) \leftrightarrow (R [x] \subseteq B \land R [x] = R [x]))$
35	13 31 34	spcedv	$⊢ φ \to \exists y (y \subseteq B \land R [x] = y)$
36	35	biantrurd	$⊢ φ \to (S [R [x]] = z \leftrightarrow (\exists y (y \subseteq B \land R [x] = y) \land S [R [x]] = z))$
37		19.41v	$⊢ \exists y ((y \subseteq B \land R [x] = y) \land S [R [x]] = z) \leftrightarrow (\exists y (y \subseteq B \land R [x] = y) \land S [R [x]] = z)$
38		anass	$⊢ ((y \subseteq B \land R [x] = y) \land S [R [x]] = z) \leftrightarrow (y \subseteq B \land (R [x] = y \land S [R [x]] = z))$
39	38	exbii	$⊢ \exists y ((y \subseteq B \land R [x] = y) \land S [R [x]] = z) \leftrightarrow \exists y (y \subseteq B \land (R [x] = y \land S [R [x]] = z))$
40	37 39	bitr3i	$⊢ (\exists y (y \subseteq B \land R [x] = y) \land S [R [x]] = z) \leftrightarrow \exists y (y \subseteq B \land (R [x] = y \land S [R [x]] = z))$
41	36 40	bitrdi	$⊢ φ \to (S [R [x]] = z \leftrightarrow \exists y (y \subseteq B \land (R [x] = y \land S [R [x]] = z)))$
42		imaeq2	$⊢ R [x] = y \to S [R [x]] = S [y]$
43	42	eqeq1d	$⊢ R [x] = y \to (S [R [x]] = z \leftrightarrow S [y] = z)$
44	43	pm5.32i	$⊢ (R [x] = y \land S [R [x]] = z) \leftrightarrow (R [x] = y \land S [y] = z)$
45	44	bianass	$⊢ (y \subseteq B \land (R [x] = y \land S [R [x]] = z)) \leftrightarrow ((y \subseteq B \land R [x] = y) \land S [y] = z)$
46	45	biancomi	$⊢ (y \subseteq B \land (R [x] = y \land S [R [x]] = z)) \leftrightarrow (S [y] = z \land (y \subseteq B \land R [x] = y))$
47	46	exbii	$⊢ \exists y (y \subseteq B \land (R [x] = y \land S [R [x]] = z)) \leftrightarrow \exists y (S [y] = z \land (y \subseteq B \land R [x] = y))$
48	47	a1i	$⊢ φ \to (\exists y (y \subseteq B \land (R [x] = y \land S [R [x]] = z)) \leftrightarrow \exists y (S [y] = z \land (y \subseteq B \land R [x] = y)))$
49		pm4.24	$⊢ y \subseteq B \leftrightarrow (y \subseteq B \land y \subseteq B)$
50	49	anbi1i	$⊢ (y \subseteq B \land R [x] = y) \leftrightarrow ((y \subseteq B \land y \subseteq B) \land R [x] = y)$
51		anass	$⊢ ((y \subseteq B \land y \subseteq B) \land R [x] = y) \leftrightarrow (y \subseteq B \land (y \subseteq B \land R [x] = y))$
52	50 51	bitri	$⊢ (y \subseteq B \land R [x] = y) \leftrightarrow (y \subseteq B \land (y \subseteq B \land R [x] = y))$
53	52	anbi2i	$⊢ (S [y] = z \land (y \subseteq B \land R [x] = y)) \leftrightarrow (S [y] = z \land (y \subseteq B \land (y \subseteq B \land R [x] = y)))$
54		an12	$⊢ (S [y] = z \land (y \subseteq B \land (y \subseteq B \land R [x] = y))) \leftrightarrow (y \subseteq B \land (S [y] = z \land (y \subseteq B \land R [x] = y)))$
55	53 54	bitri	$⊢ (S [y] = z \land (y \subseteq B \land R [x] = y)) \leftrightarrow (y \subseteq B \land (S [y] = z \land (y \subseteq B \land R [x] = y)))$
56	55	exbii	$⊢ \exists y (S [y] = z \land (y \subseteq B \land R [x] = y)) \leftrightarrow \exists y (y \subseteq B \land (S [y] = z \land (y \subseteq B \land R [x] = y)))$
57	56	a1i	$⊢ φ \to (\exists y (S [y] = z \land (y \subseteq B \land R [x] = y)) \leftrightarrow \exists y (y \subseteq B \land (S [y] = z \land (y \subseteq B \land R [x] = y))))$
58	41 48 57	3bitrd	$⊢ φ \to (S [R [x]] = z \leftrightarrow \exists y (y \subseteq B \land (S [y] = z \land (y \subseteq B \land R [x] = y))))$
59	58	anbi2d	$⊢ φ \to (((x \subseteq A \land z \subseteq C) \land S [R [x]] = z) \leftrightarrow ((x \subseteq A \land z \subseteq C) \land \exists y (y \subseteq B \land (S [y] = z \land (y \subseteq B \land R [x] = y)))))$
60		19.42v	$⊢ \exists y ((x \subseteq A \land z \subseteq C) \land (y \subseteq B \land (S [y] = z \land (y \subseteq B \land R [x] = y)))) \leftrightarrow ((x \subseteq A \land z \subseteq C) \land \exists y (y \subseteq B \land (S [y] = z \land (y \subseteq B \land R [x] = y))))$
61		anass	$⊢ ((x \subseteq A \land z \subseteq C) \land (y \subseteq B \land (S [y] = z \land (y \subseteq B \land R [x] = y)))) \leftrightarrow (x \subseteq A \land (z \subseteq C \land (y \subseteq B \land (S [y] = z \land (y \subseteq B \land R [x] = y)))))$
62		ancom	$⊢ ((R [x] = y \land ((y \subseteq B \land z \subseteq C) \land S [y] = z)) \land y \subseteq B) \leftrightarrow (y \subseteq B \land (R [x] = y \land ((y \subseteq B \land z \subseteq C) \land S [y] = z)))$
63	62	bianass	$⊢ (x \subseteq A \land ((R [x] = y \land ((y \subseteq B \land z \subseteq C) \land S [y] = z)) \land y \subseteq B)) \leftrightarrow ((x \subseteq A \land y \subseteq B) \land (R [x] = y \land ((y \subseteq B \land z \subseteq C) \land S [y] = z)))$
64		ancom	$⊢ ((((y \subseteq B \land z \subseteq C) \land S [y] = z) \land y \subseteq B) \land R [x] = y) \leftrightarrow (R [x] = y \land (((y \subseteq B \land z \subseteq C) \land S [y] = z) \land y \subseteq B))$
65		ancom	$⊢ (z \subseteq C \land y \subseteq B) \leftrightarrow (y \subseteq B \land z \subseteq C)$
66	65	anbi1i	$⊢ ((z \subseteq C \land y \subseteq B) \land S [y] = z) \leftrightarrow ((y \subseteq B \land z \subseteq C) \land S [y] = z)$
67	66	anbi1i	$⊢ (((z \subseteq C \land y \subseteq B) \land S [y] = z) \land (y \subseteq B \land R [x] = y)) \leftrightarrow (((y \subseteq B \land z \subseteq C) \land S [y] = z) \land (y \subseteq B \land R [x] = y))$
68		biid	$⊢ (y \subseteq B \land (S [y] = z \land (y \subseteq B \land R [x] = y))) \leftrightarrow (y \subseteq B \land (S [y] = z \land (y \subseteq B \land R [x] = y)))$
69	68	bianass	$⊢ (z \subseteq C \land (y \subseteq B \land (S [y] = z \land (y \subseteq B \land R [x] = y)))) \leftrightarrow ((z \subseteq C \land y \subseteq B) \land (S [y] = z \land (y \subseteq B \land R [x] = y)))$
70		anass	$⊢ (((z \subseteq C \land y \subseteq B) \land S [y] = z) \land (y \subseteq B \land R [x] = y)) \leftrightarrow ((z \subseteq C \land y \subseteq B) \land (S [y] = z \land (y \subseteq B \land R [x] = y)))$
71	69 70	bitr4i	$⊢ (z \subseteq C \land (y \subseteq B \land (S [y] = z \land (y \subseteq B \land R [x] = y)))) \leftrightarrow (((z \subseteq C \land y \subseteq B) \land S [y] = z) \land (y \subseteq B \land R [x] = y))$
72		anass	$⊢ ((((y \subseteq B \land z \subseteq C) \land S [y] = z) \land y \subseteq B) \land R [x] = y) \leftrightarrow (((y \subseteq B \land z \subseteq C) \land S [y] = z) \land (y \subseteq B \land R [x] = y))$
73	67 71 72	3bitr4i	$⊢ (z \subseteq C \land (y \subseteq B \land (S [y] = z \land (y \subseteq B \land R [x] = y)))) \leftrightarrow ((((y \subseteq B \land z \subseteq C) \land S [y] = z) \land y \subseteq B) \land R [x] = y)$
74		anass	$⊢ ((R [x] = y \land ((y \subseteq B \land z \subseteq C) \land S [y] = z)) \land y \subseteq B) \leftrightarrow (R [x] = y \land (((y \subseteq B \land z \subseteq C) \land S [y] = z) \land y \subseteq B))$
75	64 73 74	3bitr4i	$⊢ (z \subseteq C \land (y \subseteq B \land (S [y] = z \land (y \subseteq B \land R [x] = y)))) \leftrightarrow ((R [x] = y \land ((y \subseteq B \land z \subseteq C) \land S [y] = z)) \land y \subseteq B)$
76	75	anbi2i	$⊢ (x \subseteq A \land (z \subseteq C \land (y \subseteq B \land (S [y] = z \land (y \subseteq B \land R [x] = y))))) \leftrightarrow (x \subseteq A \land ((R [x] = y \land ((y \subseteq B \land z \subseteq C) \land S [y] = z)) \land y \subseteq B))$
77		anass	$⊢ (((x \subseteq A \land y \subseteq B) \land R [x] = y) \land ((y \subseteq B \land z \subseteq C) \land S [y] = z)) \leftrightarrow ((x \subseteq A \land y \subseteq B) \land (R [x] = y \land ((y \subseteq B \land z \subseteq C) \land S [y] = z)))$
78	63 76 77	3bitr4i	$⊢ (x \subseteq A \land (z \subseteq C \land (y \subseteq B \land (S [y] = z \land (y \subseteq B \land R [x] = y))))) \leftrightarrow (((x \subseteq A \land y \subseteq B) \land R [x] = y) \land ((y \subseteq B \land z \subseteq C) \land S [y] = z))$
79	61 78	bitri	$⊢ ((x \subseteq A \land z \subseteq C) \land (y \subseteq B \land (S [y] = z \land (y \subseteq B \land R [x] = y)))) \leftrightarrow (((x \subseteq A \land y \subseteq B) \land R [x] = y) \land ((y \subseteq B \land z \subseteq C) \land S [y] = z))$
80	79	exbii	$⊢ \exists y ((x \subseteq A \land z \subseteq C) \land (y \subseteq B \land (S [y] = z \land (y \subseteq B \land R [x] = y)))) \leftrightarrow \exists y (((x \subseteq A \land y \subseteq B) \land R [x] = y) \land ((y \subseteq B \land z \subseteq C) \land S [y] = z))$
81	60 80	bitr3i	$⊢ ((x \subseteq A \land z \subseteq C) \land \exists y (y \subseteq B \land (S [y] = z \land (y \subseteq B \land R [x] = y)))) \leftrightarrow \exists y (((x \subseteq A \land y \subseteq B) \land R [x] = y) \land ((y \subseteq B \land z \subseteq C) \land S [y] = z))$
82	81	a1i	$⊢ φ \to (((x \subseteq A \land z \subseteq C) \land \exists y (y \subseteq B \land (S [y] = z \land (y \subseteq B \land R [x] = y)))) \leftrightarrow \exists y (((x \subseteq A \land y \subseteq B) \land R [x] = y) \land ((y \subseteq B \land z \subseteq C) \land S [y] = z)))$
83	9 59 82	3bitrd	$⊢ φ \to (((x \subseteq A \land z \subseteq C) \land (S \circ R) [x] = z) \leftrightarrow \exists y (((x \subseteq A \land y \subseteq B) \land R [x] = y) \land ((y \subseteq B \land z \subseteq C) \land S [y] = z)))$
84	83	opabbidv	$⊢ φ \to \{⟨x, z⟩ \| ((x \subseteq A \land z \subseteq C) \land (S \circ R) [x] = z)\} = \{⟨x, z⟩ \| \exists y (((x \subseteq A \land y \subseteq B) \land R [x] = y) \land ((y \subseteq B \land z \subseteq C) \land S [y] = z))\}$
85		bj-opabco	$⊢ \{⟨y, z⟩ \| ((y \subseteq B \land z \subseteq C) \land S [y] = z)\} \circ \{⟨x, y⟩ \| ((x \subseteq A \land y \subseteq B) \land R [x] = y)\} = \{⟨x, z⟩ \| \exists y (((x \subseteq A \land y \subseteq B) \land R [x] = y) \land ((y \subseteq B \land z \subseteq C) \land S [y] = z))\}$
86	84 85	eqtr4di	$⊢ φ \to \{⟨x, z⟩ \| ((x \subseteq A \land z \subseteq C) \land (S \circ R) [x] = z)\} = \{⟨y, z⟩ \| ((y \subseteq B \land z \subseteq C) \land S [y] = z)\} \circ \{⟨x, y⟩ \| ((x \subseteq A \land y \subseteq B) \land R [x] = y)\}$
87	5 4	coss12d	$⊢ φ \to S \circ R \subseteq (B \times C) \circ (A \times B)$
88		bj-xpcossxp	$⊢ (B \times C) \circ (A \times B) \subseteq A \times C$
89	87 88	sstrdi	$⊢ φ \to S \circ R \subseteq A \times C$
90	1 3 89	bj-imdirval2	$⊢ φ \to (A 𝒫_{*} C) (S \circ R) = \{⟨x, z⟩ \| ((x \subseteq A \land z \subseteq C) \land (S \circ R) [x] = z)\}$
91	2 3 5	bj-imdirval2	$⊢ φ \to (B 𝒫_{*} C) (S) = \{⟨y, z⟩ \| ((y \subseteq B \land z \subseteq C) \land S [y] = z)\}$
92	1 2 4	bj-imdirval2	$⊢ φ \to (A 𝒫_{*} B) (R) = \{⟨x, y⟩ \| ((x \subseteq A \land y \subseteq B) \land R [x] = y)\}$
93	91 92	coeq12d	$⊢ φ \to (B 𝒫_{} C) (S) \circ (A 𝒫_{} B) (R) = \{⟨y, z⟩ \| ((y \subseteq B \land z \subseteq C) \land S [y] = z)\} \circ \{⟨x, y⟩ \| ((x \subseteq A \land y \subseteq B) \land R [x] = y)\}$
94	86 90 93	3eqtr4d	$⊢ φ \to (A 𝒫_{} C) (S \circ R) = (B 𝒫_{} C) (S) \circ (A 𝒫_{*} B) (R)$

Metamath Proof Explorer

Theorem bj-imdirco

Proof