Theorem 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	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
	bj-imdirco.exb	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	bj-imdirco.exc	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
	bj-imdirco.arg1	⊢ ( 𝜑 → 𝑅 ⊆ ( 𝐴 × 𝐵 ) )
	bj-imdirco.arg2	⊢ ( 𝜑 → 𝑆 ⊆ ( 𝐵 × 𝐶 ) )
Assertion	bj-imdirco	⊢ ( 𝜑 → ( ( 𝐴 𝒫* 𝐶 ) ‘ ( 𝑆 ∘ 𝑅 ) ) = ( ( ( 𝐵 𝒫* 𝐶 ) ‘ 𝑆 ) ∘ ( ( 𝐴 𝒫* 𝐵 ) ‘ 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		bj-imdirco.exa	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
2		bj-imdirco.exb	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
3		bj-imdirco.exc	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
4		bj-imdirco.arg1	⊢ ( 𝜑 → 𝑅 ⊆ ( 𝐴 × 𝐵 ) )
5		bj-imdirco.arg2	⊢ ( 𝜑 → 𝑆 ⊆ ( 𝐵 × 𝐶 ) )
6		imaco	⊢ ( ( 𝑆 ∘ 𝑅 ) “ 𝑥 ) = ( 𝑆 “ ( 𝑅 “ 𝑥 ) )
7	6	eqeq1i	⊢ ( ( ( 𝑆 ∘ 𝑅 ) “ 𝑥 ) = 𝑧 ↔ ( 𝑆 “ ( 𝑅 “ 𝑥 ) ) = 𝑧 )
8	7	anbi2i	⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( ( 𝑆 ∘ 𝑅 ) “ 𝑥 ) = 𝑧 ) ↔ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ ( 𝑅 “ 𝑥 ) ) = 𝑧 ) )
9	8	a1i	⊢ ( 𝜑 → ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( ( 𝑆 ∘ 𝑅 ) “ 𝑥 ) = 𝑧 ) ↔ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ ( 𝑅 “ 𝑥 ) ) = 𝑧 ) ) )
10	1 2	xpexd	⊢ ( 𝜑 → ( 𝐴 × 𝐵 ) ∈ V )
11	10 4	ssexd	⊢ ( 𝜑 → 𝑅 ∈ V )
12		imaexg	⊢ ( 𝑅 ∈ V → ( 𝑅 “ 𝑥 ) ∈ V )
13	11 12	syl	⊢ ( 𝜑 → ( 𝑅 “ 𝑥 ) ∈ V )
14		imass1	⊢ ( 𝑅 ⊆ ( 𝐴 × 𝐵 ) → ( 𝑅 “ 𝑥 ) ⊆ ( ( 𝐴 × 𝐵 ) “ 𝑥 ) )
15		xpima	⊢ ( ( 𝐴 × 𝐵 ) “ 𝑥 ) = if ( ( 𝐴 ∩ 𝑥 ) = ∅ , ∅ , 𝐵 )
16		simpr	⊢ ( ( ( 𝐴 ∩ 𝑥 ) = ∅ ∧ 𝑢 ∈ ∅ ) → 𝑢 ∈ ∅ )
17		simpr	⊢ ( ( ¬ ( 𝐴 ∩ 𝑥 ) = ∅ ∧ 𝑢 ∈ 𝐵 ) → 𝑢 ∈ 𝐵 )
18	16 17	orim12i	⊢ ( ( ( ( 𝐴 ∩ 𝑥 ) = ∅ ∧ 𝑢 ∈ ∅ ) ∨ ( ¬ ( 𝐴 ∩ 𝑥 ) = ∅ ∧ 𝑢 ∈ 𝐵 ) ) → ( 𝑢 ∈ ∅ ∨ 𝑢 ∈ 𝐵 ) )
19		elif	⊢ ( 𝑢 ∈ if ( ( 𝐴 ∩ 𝑥 ) = ∅ , ∅ , 𝐵 ) ↔ ( ( ( 𝐴 ∩ 𝑥 ) = ∅ ∧ 𝑢 ∈ ∅ ) ∨ ( ¬ ( 𝐴 ∩ 𝑥 ) = ∅ ∧ 𝑢 ∈ 𝐵 ) ) )
20		elun	⊢ ( 𝑢 ∈ ( ∅ ∪ 𝐵 ) ↔ ( 𝑢 ∈ ∅ ∨ 𝑢 ∈ 𝐵 ) )
21	18 19 20	3imtr4i	⊢ ( 𝑢 ∈ if ( ( 𝐴 ∩ 𝑥 ) = ∅ , ∅ , 𝐵 ) → 𝑢 ∈ ( ∅ ∪ 𝐵 ) )
22	21	ssriv	⊢ if ( ( 𝐴 ∩ 𝑥 ) = ∅ , ∅ , 𝐵 ) ⊆ ( ∅ ∪ 𝐵 )
23		0ss	⊢ ∅ ⊆ 𝐵
24		ssid	⊢ 𝐵 ⊆ 𝐵
25	23 24	unssi	⊢ ( ∅ ∪ 𝐵 ) ⊆ 𝐵
26	22 25	sstri	⊢ if ( ( 𝐴 ∩ 𝑥 ) = ∅ , ∅ , 𝐵 ) ⊆ 𝐵
27	15 26	eqsstri	⊢ ( ( 𝐴 × 𝐵 ) “ 𝑥 ) ⊆ 𝐵
28	14 27	sstrdi	⊢ ( 𝑅 ⊆ ( 𝐴 × 𝐵 ) → ( 𝑅 “ 𝑥 ) ⊆ 𝐵 )
29	4 28	syl	⊢ ( 𝜑 → ( 𝑅 “ 𝑥 ) ⊆ 𝐵 )
30		eqidd	⊢ ( 𝜑 → ( 𝑅 “ 𝑥 ) = ( 𝑅 “ 𝑥 ) )
31	29 30	jca	⊢ ( 𝜑 → ( ( 𝑅 “ 𝑥 ) ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = ( 𝑅 “ 𝑥 ) ) )
32		sseq1	⊢ ( 𝑦 = ( 𝑅 “ 𝑥 ) → ( 𝑦 ⊆ 𝐵 ↔ ( 𝑅 “ 𝑥 ) ⊆ 𝐵 ) )
33		eqeq2	⊢ ( 𝑦 = ( 𝑅 “ 𝑥 ) → ( ( 𝑅 “ 𝑥 ) = 𝑦 ↔ ( 𝑅 “ 𝑥 ) = ( 𝑅 “ 𝑥 ) ) )
34	32 33	anbi12d	⊢ ( 𝑦 = ( 𝑅 “ 𝑥 ) → ( ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ↔ ( ( 𝑅 “ 𝑥 ) ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = ( 𝑅 “ 𝑥 ) ) ) )
35	13 31 34	spcedv	⊢ ( 𝜑 → ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) )
36	35	biantrurd	⊢ ( 𝜑 → ( ( 𝑆 “ ( 𝑅 “ 𝑥 ) ) = 𝑧 ↔ ( ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ∧ ( 𝑆 “ ( 𝑅 “ 𝑥 ) ) = 𝑧 ) ) )
37		19.41v	⊢ ( ∃ 𝑦 ( ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ∧ ( 𝑆 “ ( 𝑅 “ 𝑥 ) ) = 𝑧 ) ↔ ( ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ∧ ( 𝑆 “ ( 𝑅 “ 𝑥 ) ) = 𝑧 ) )
38		anass	⊢ ( ( ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ∧ ( 𝑆 “ ( 𝑅 “ 𝑥 ) ) = 𝑧 ) ↔ ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑅 “ 𝑥 ) = 𝑦 ∧ ( 𝑆 “ ( 𝑅 “ 𝑥 ) ) = 𝑧 ) ) )
39	38	exbii	⊢ ( ∃ 𝑦 ( ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ∧ ( 𝑆 “ ( 𝑅 “ 𝑥 ) ) = 𝑧 ) ↔ ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑅 “ 𝑥 ) = 𝑦 ∧ ( 𝑆 “ ( 𝑅 “ 𝑥 ) ) = 𝑧 ) ) )
40	37 39	bitr3i	⊢ ( ( ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ∧ ( 𝑆 “ ( 𝑅 “ 𝑥 ) ) = 𝑧 ) ↔ ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑅 “ 𝑥 ) = 𝑦 ∧ ( 𝑆 “ ( 𝑅 “ 𝑥 ) ) = 𝑧 ) ) )
41	36 40	bitrdi	⊢ ( 𝜑 → ( ( 𝑆 “ ( 𝑅 “ 𝑥 ) ) = 𝑧 ↔ ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑅 “ 𝑥 ) = 𝑦 ∧ ( 𝑆 “ ( 𝑅 “ 𝑥 ) ) = 𝑧 ) ) ) )
42		imaeq2	⊢ ( ( 𝑅 “ 𝑥 ) = 𝑦 → ( 𝑆 “ ( 𝑅 “ 𝑥 ) ) = ( 𝑆 “ 𝑦 ) )
43	42	eqeq1d	⊢ ( ( 𝑅 “ 𝑥 ) = 𝑦 → ( ( 𝑆 “ ( 𝑅 “ 𝑥 ) ) = 𝑧 ↔ ( 𝑆 “ 𝑦 ) = 𝑧 ) )
44	43	pm5.32i	⊢ ( ( ( 𝑅 “ 𝑥 ) = 𝑦 ∧ ( 𝑆 “ ( 𝑅 “ 𝑥 ) ) = 𝑧 ) ↔ ( ( 𝑅 “ 𝑥 ) = 𝑦 ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) )
45	44	bianass	⊢ ( ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑅 “ 𝑥 ) = 𝑦 ∧ ( 𝑆 “ ( 𝑅 “ 𝑥 ) ) = 𝑧 ) ) ↔ ( ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) )
46	45	biancomi	⊢ ( ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑅 “ 𝑥 ) = 𝑦 ∧ ( 𝑆 “ ( 𝑅 “ 𝑥 ) ) = 𝑧 ) ) ↔ ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) )
47	46	exbii	⊢ ( ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑅 “ 𝑥 ) = 𝑦 ∧ ( 𝑆 “ ( 𝑅 “ 𝑥 ) ) = 𝑧 ) ) ↔ ∃ 𝑦 ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) )
48	47	a1i	⊢ ( 𝜑 → ( ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑅 “ 𝑥 ) = 𝑦 ∧ ( 𝑆 “ ( 𝑅 “ 𝑥 ) ) = 𝑧 ) ) ↔ ∃ 𝑦 ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ) )
49		pm4.24	⊢ ( 𝑦 ⊆ 𝐵 ↔ ( 𝑦 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝐵 ) )
50	49	anbi1i	⊢ ( ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ↔ ( ( 𝑦 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) )
51		anass	⊢ ( ( ( 𝑦 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ↔ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) )
52	50 51	bitri	⊢ ( ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ↔ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) )
53	52	anbi2i	⊢ ( ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ↔ ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ) )
54		an12	⊢ ( ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ) ↔ ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ) )
55	53 54	bitri	⊢ ( ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ↔ ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ) )
56	55	exbii	⊢ ( ∃ 𝑦 ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ↔ ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ) )
57	56	a1i	⊢ ( 𝜑 → ( ∃ 𝑦 ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ↔ ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ) ) )
58	41 48 57	3bitrd	⊢ ( 𝜑 → ( ( 𝑆 “ ( 𝑅 “ 𝑥 ) ) = 𝑧 ↔ ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ) ) )
59	58	anbi2d	⊢ ( 𝜑 → ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ ( 𝑅 “ 𝑥 ) ) = 𝑧 ) ↔ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝐶 ) ∧ ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ) ) ) )
60		19.42v	⊢ ( ∃ 𝑦 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ) ) ↔ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝐶 ) ∧ ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ) ) )
61		anass	⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ) ) ↔ ( 𝑥 ⊆ 𝐴 ∧ ( 𝑧 ⊆ 𝐶 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ) ) ) )
62		ancom	⊢ ( ( ( ( 𝑅 “ 𝑥 ) = 𝑦 ∧ ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) ) ∧ 𝑦 ⊆ 𝐵 ) ↔ ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑅 “ 𝑥 ) = 𝑦 ∧ ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) ) ) )
63	62	bianass	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ ( ( ( 𝑅 “ 𝑥 ) = 𝑦 ∧ ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) ) ∧ 𝑦 ⊆ 𝐵 ) ) ↔ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( ( 𝑅 “ 𝑥 ) = 𝑦 ∧ ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) ) ) )
64		ancom	⊢ ( ( ( ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ↔ ( ( 𝑅 “ 𝑥 ) = 𝑦 ∧ ( ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) ∧ 𝑦 ⊆ 𝐵 ) ) )
65		ancom	⊢ ( ( 𝑧 ⊆ 𝐶 ∧ 𝑦 ⊆ 𝐵 ) ↔ ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) )
66	65	anbi1i	⊢ ( ( ( 𝑧 ⊆ 𝐶 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) ↔ ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) )
67	66	anbi1i	⊢ ( ( ( ( 𝑧 ⊆ 𝐶 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ↔ ( ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) )
68		biid	⊢ ( ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ) ↔ ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ) )
69	68	bianass	⊢ ( ( 𝑧 ⊆ 𝐶 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ) ) ↔ ( ( 𝑧 ⊆ 𝐶 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ) )
70		anass	⊢ ( ( ( ( 𝑧 ⊆ 𝐶 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ↔ ( ( 𝑧 ⊆ 𝐶 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ) )
71	69 70	bitr4i	⊢ ( ( 𝑧 ⊆ 𝐶 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ) ) ↔ ( ( ( 𝑧 ⊆ 𝐶 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) )
72		anass	⊢ ( ( ( ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ↔ ( ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) )
73	67 71 72	3bitr4i	⊢ ( ( 𝑧 ⊆ 𝐶 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ) ) ↔ ( ( ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) )
74		anass	⊢ ( ( ( ( 𝑅 “ 𝑥 ) = 𝑦 ∧ ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) ) ∧ 𝑦 ⊆ 𝐵 ) ↔ ( ( 𝑅 “ 𝑥 ) = 𝑦 ∧ ( ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) ∧ 𝑦 ⊆ 𝐵 ) ) )
75	64 73 74	3bitr4i	⊢ ( ( 𝑧 ⊆ 𝐶 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ) ) ↔ ( ( ( 𝑅 “ 𝑥 ) = 𝑦 ∧ ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) ) ∧ 𝑦 ⊆ 𝐵 ) )
76	75	anbi2i	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ ( 𝑧 ⊆ 𝐶 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ) ) ) ↔ ( 𝑥 ⊆ 𝐴 ∧ ( ( ( 𝑅 “ 𝑥 ) = 𝑦 ∧ ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) ) ∧ 𝑦 ⊆ 𝐵 ) ) )
77		anass	⊢ ( ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ∧ ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) ) ↔ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( ( 𝑅 “ 𝑥 ) = 𝑦 ∧ ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) ) ) )
78	63 76 77	3bitr4i	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ ( 𝑧 ⊆ 𝐶 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ) ) ) ↔ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ∧ ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) ) )
79	61 78	bitri	⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ) ) ↔ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ∧ ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) ) )
80	79	exbii	⊢ ( ∃ 𝑦 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ) ) ↔ ∃ 𝑦 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ∧ ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) ) )
81	60 80	bitr3i	⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝐶 ) ∧ ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ) ) ↔ ∃ 𝑦 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ∧ ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) ) )
82	81	a1i	⊢ ( 𝜑 → ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝐶 ) ∧ ∃ 𝑦 ( 𝑦 ⊆ 𝐵 ∧ ( ( 𝑆 “ 𝑦 ) = 𝑧 ∧ ( 𝑦 ⊆ 𝐵 ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ) ) ) ↔ ∃ 𝑦 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ∧ ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) ) ) )
83	9 59 82	3bitrd	⊢ ( 𝜑 → ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( ( 𝑆 ∘ 𝑅 ) “ 𝑥 ) = 𝑧 ) ↔ ∃ 𝑦 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ∧ ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) ) ) )
84	83	opabbidv	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( ( 𝑆 ∘ 𝑅 ) “ 𝑥 ) = 𝑧 ) } = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ∧ ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) ) } )
85		bj-opabco	⊢ ( { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) } ∘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) } ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) ∧ ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) ) }
86	84 85	eqtr4di	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( ( 𝑆 ∘ 𝑅 ) “ 𝑥 ) = 𝑧 ) } = ( { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) } ∘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) } ) )
87	5 4	coss12d	⊢ ( 𝜑 → ( 𝑆 ∘ 𝑅 ) ⊆ ( ( 𝐵 × 𝐶 ) ∘ ( 𝐴 × 𝐵 ) ) )
88		bj-xpcossxp	⊢ ( ( 𝐵 × 𝐶 ) ∘ ( 𝐴 × 𝐵 ) ) ⊆ ( 𝐴 × 𝐶 )
89	87 88	sstrdi	⊢ ( 𝜑 → ( 𝑆 ∘ 𝑅 ) ⊆ ( 𝐴 × 𝐶 ) )
90	1 3 89	bj-imdirval2	⊢ ( 𝜑 → ( ( 𝐴 𝒫* 𝐶 ) ‘ ( 𝑆 ∘ 𝑅 ) ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( ( 𝑆 ∘ 𝑅 ) “ 𝑥 ) = 𝑧 ) } )
91	2 3 5	bj-imdirval2	⊢ ( 𝜑 → ( ( 𝐵 𝒫* 𝐶 ) ‘ 𝑆 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) } )
92	1 2 4	bj-imdirval2	⊢ ( 𝜑 → ( ( 𝐴 𝒫* 𝐵 ) ‘ 𝑅 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) } )
93	91 92	coeq12d	⊢ ( 𝜑 → ( ( ( 𝐵 𝒫* 𝐶 ) ‘ 𝑆 ) ∘ ( ( 𝐴 𝒫* 𝐵 ) ‘ 𝑅 ) ) = ( { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ⊆ 𝐵 ∧ 𝑧 ⊆ 𝐶 ) ∧ ( 𝑆 “ 𝑦 ) = 𝑧 ) } ∘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑦 ⊆ 𝐵 ) ∧ ( 𝑅 “ 𝑥 ) = 𝑦 ) } ) )
94	86 90 93	3eqtr4d	⊢ ( 𝜑 → ( ( 𝐴 𝒫* 𝐶 ) ‘ ( 𝑆 ∘ 𝑅 ) ) = ( ( ( 𝐵 𝒫* 𝐶 ) ‘ 𝑆 ) ∘ ( ( 𝐴 𝒫* 𝐵 ) ‘ 𝑅 ) ) )