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	Could not format assertion : No typesetting found for \|- ( ph -> ( ( A ~P_* C ) ` ( S o. R ) ) = ( ( ( B ~P_* C ) ` S ) o. ( ( A ~P_* B ) ` R ) ) ) with typecode \|-

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	syl6bb	$⊢ φ \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	Could not format ( ph -> ( ( A ~P_* C ) ` ( S o. R ) ) = { <. x , z >. \| ( ( x C_ A /\ z C_ C ) /\ ( ( S o. R ) " x ) = z ) } ) : No typesetting found for \|- ( ph -> ( ( A ~P_* C ) ` ( S o. R ) ) = { <. x , z >. \| ( ( x C_ A /\ z C_ C ) /\ ( ( S o. R ) " x ) = z ) } ) with typecode \|-
91	2 3 5	bj-imdirval2	Could not format ( ph -> ( ( B ~P_* C ) ` S ) = { <. y , z >. \| ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) } ) : No typesetting found for \|- ( ph -> ( ( B ~P_* C ) ` S ) = { <. y , z >. \| ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) } ) with typecode \|-
92	1 2 4	bj-imdirval2	Could not format ( ph -> ( ( A ~P_* B ) ` R ) = { <. x , y >. \| ( ( x C_ A /\ y C_ B ) /\ ( R " x ) = y ) } ) : No typesetting found for \|- ( ph -> ( ( A ~P_* B ) ` R ) = { <. x , y >. \| ( ( x C_ A /\ y C_ B ) /\ ( R " x ) = y ) } ) with typecode \|-
93	91 92	coeq12d	Could not format ( ph -> ( ( ( B ~P_* C ) ` S ) o. ( ( A ~P_* B ) ` R ) ) = ( { <. y , z >. \| ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) } o. { <. x , y >. \| ( ( x C_ A /\ y C_ B ) /\ ( R " x ) = y ) } ) ) : No typesetting found for \|- ( ph -> ( ( ( B ~P_* C ) ` S ) o. ( ( A ~P_* B ) ` R ) ) = ( { <. y , z >. \| ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) } o. { <. x , y >. \| ( ( x C_ A /\ y C_ B ) /\ ( R " x ) = y ) } ) ) with typecode \|-
94	86 90 93	3eqtr4d	Could not format ( ph -> ( ( A ~P_* C ) ` ( S o. R ) ) = ( ( ( B ~P_* C ) ` S ) o. ( ( A ~P_* B ) ` R ) ) ) : No typesetting found for \|- ( ph -> ( ( A ~P_* C ) ` ( S o. R ) ) = ( ( ( B ~P_* C ) ` S ) o. ( ( A ~P_* B ) ` R ) ) ) with typecode \|-

Metamath Proof Explorer

Theorem bj-imdirco

Proof