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	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	ofpreima.2	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐶 )
	ofpreima.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	ofpreima.4	⊢ ( 𝜑 → 𝑅 Fn ( 𝐵 × 𝐶 ) )
Assertion	ofpreima2	⊢ ( 𝜑 → ( ^◡ ( 𝐹 ∘_f 𝑅 𝐺 ) “ 𝐷 ) = ∪ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		ofpreima.1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		ofpreima.2	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐶 )
3		ofpreima.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		ofpreima.4	⊢ ( 𝜑 → 𝑅 Fn ( 𝐵 × 𝐶 ) )
5	1 2 3 4	ofpreima	⊢ ( 𝜑 → ( ^◡ ( 𝐹 ∘_f 𝑅 𝐺 ) “ 𝐷 ) = ∪ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) )
6		inundif	⊢ ( ( ( ^◡ 𝑅 “ 𝐷 ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ∪ ( ( ^◡ 𝑅 “ 𝐷 ) ∖ ( ran 𝐹 × ran 𝐺 ) ) ) = ( ^◡ 𝑅 “ 𝐷 )
7		iuneq1	⊢ ( ( ( ( ^◡ 𝑅 “ 𝐷 ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ∪ ( ( ^◡ 𝑅 “ 𝐷 ) ∖ ( ran 𝐹 × ran 𝐺 ) ) ) = ( ^◡ 𝑅 “ 𝐷 ) → ∪ 𝑝 ∈ ( ( ( ^◡ 𝑅 “ 𝐷 ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ∪ ( ( ^◡ 𝑅 “ 𝐷 ) ∖ ( ran 𝐹 × ran 𝐺 ) ) ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) = ∪ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) )
8	6 7	ax-mp	⊢ ∪ 𝑝 ∈ ( ( ( ^◡ 𝑅 “ 𝐷 ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ∪ ( ( ^◡ 𝑅 “ 𝐷 ) ∖ ( ran 𝐹 × ran 𝐺 ) ) ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) = ∪ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) )
9		iunxun	⊢ ∪ 𝑝 ∈ ( ( ( ^◡ 𝑅 “ 𝐷 ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ∪ ( ( ^◡ 𝑅 “ 𝐷 ) ∖ ( ran 𝐹 × ran 𝐺 ) ) ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) = ( ∪ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) ∪ ∪ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∖ ( ran 𝐹 × ran 𝐺 ) ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) )
10	8 9	eqtr3i	⊢ ∪ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) = ( ∪ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) ∪ ∪ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∖ ( ran 𝐹 × ran 𝐺 ) ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) )
11	5 10	eqtrdi	⊢ ( 𝜑 → ( ^◡ ( 𝐹 ∘_f 𝑅 𝐺 ) “ 𝐷 ) = ( ∪ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) ∪ ∪ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∖ ( ran 𝐹 × ran 𝐺 ) ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) ) )
12		simpr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∖ ( ran 𝐹 × ran 𝐺 ) ) ) → 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∖ ( ran 𝐹 × ran 𝐺 ) ) )
13	12	eldifbd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∖ ( ran 𝐹 × ran 𝐺 ) ) ) → ¬ 𝑝 ∈ ( ran 𝐹 × ran 𝐺 ) )
14		cnvimass	⊢ ( ^◡ 𝑅 “ 𝐷 ) ⊆ dom 𝑅
15	4	fndmd	⊢ ( 𝜑 → dom 𝑅 = ( 𝐵 × 𝐶 ) )
16	14 15	sseqtrid	⊢ ( 𝜑 → ( ^◡ 𝑅 “ 𝐷 ) ⊆ ( 𝐵 × 𝐶 ) )
17	16	ssdifssd	⊢ ( 𝜑 → ( ( ^◡ 𝑅 “ 𝐷 ) ∖ ( ran 𝐹 × ran 𝐺 ) ) ⊆ ( 𝐵 × 𝐶 ) )
18	17	sselda	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∖ ( ran 𝐹 × ran 𝐺 ) ) ) → 𝑝 ∈ ( 𝐵 × 𝐶 ) )
19		1st2nd2	⊢ ( 𝑝 ∈ ( 𝐵 × 𝐶 ) → 𝑝 = ⟨ ( 1^st ‘ 𝑝 ) , ( 2^nd ‘ 𝑝 ) ⟩ )
20		elxp6	⊢ ( 𝑝 ∈ ( ran 𝐹 × ran 𝐺 ) ↔ ( 𝑝 = ⟨ ( 1^st ‘ 𝑝 ) , ( 2^nd ‘ 𝑝 ) ⟩ ∧ ( ( 1^st ‘ 𝑝 ) ∈ ran 𝐹 ∧ ( 2^nd ‘ 𝑝 ) ∈ ran 𝐺 ) ) )
21	20	simplbi2	⊢ ( 𝑝 = ⟨ ( 1^st ‘ 𝑝 ) , ( 2^nd ‘ 𝑝 ) ⟩ → ( ( ( 1^st ‘ 𝑝 ) ∈ ran 𝐹 ∧ ( 2^nd ‘ 𝑝 ) ∈ ran 𝐺 ) → 𝑝 ∈ ( ran 𝐹 × ran 𝐺 ) ) )
22	18 19 21	3syl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∖ ( ran 𝐹 × ran 𝐺 ) ) ) → ( ( ( 1^st ‘ 𝑝 ) ∈ ran 𝐹 ∧ ( 2^nd ‘ 𝑝 ) ∈ ran 𝐺 ) → 𝑝 ∈ ( ran 𝐹 × ran 𝐺 ) ) )
23	13 22	mtod	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∖ ( ran 𝐹 × ran 𝐺 ) ) ) → ¬ ( ( 1^st ‘ 𝑝 ) ∈ ran 𝐹 ∧ ( 2^nd ‘ 𝑝 ) ∈ ran 𝐺 ) )
24		ianor	⊢ ( ¬ ( ( 1^st ‘ 𝑝 ) ∈ ran 𝐹 ∧ ( 2^nd ‘ 𝑝 ) ∈ ran 𝐺 ) ↔ ( ¬ ( 1^st ‘ 𝑝 ) ∈ ran 𝐹 ∨ ¬ ( 2^nd ‘ 𝑝 ) ∈ ran 𝐺 ) )
25	23 24	sylib	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∖ ( ran 𝐹 × ran 𝐺 ) ) ) → ( ¬ ( 1^st ‘ 𝑝 ) ∈ ran 𝐹 ∨ ¬ ( 2^nd ‘ 𝑝 ) ∈ ran 𝐺 ) )
26		disjsn	⊢ ( ( ran 𝐹 ∩ { ( 1^st ‘ 𝑝 ) } ) = ∅ ↔ ¬ ( 1^st ‘ 𝑝 ) ∈ ran 𝐹 )
27		disjsn	⊢ ( ( ran 𝐺 ∩ { ( 2^nd ‘ 𝑝 ) } ) = ∅ ↔ ¬ ( 2^nd ‘ 𝑝 ) ∈ ran 𝐺 )
28	26 27	orbi12i	⊢ ( ( ( ran 𝐹 ∩ { ( 1^st ‘ 𝑝 ) } ) = ∅ ∨ ( ran 𝐺 ∩ { ( 2^nd ‘ 𝑝 ) } ) = ∅ ) ↔ ( ¬ ( 1^st ‘ 𝑝 ) ∈ ran 𝐹 ∨ ¬ ( 2^nd ‘ 𝑝 ) ∈ ran 𝐺 ) )
29	25 28	sylibr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∖ ( ran 𝐹 × ran 𝐺 ) ) ) → ( ( ran 𝐹 ∩ { ( 1^st ‘ 𝑝 ) } ) = ∅ ∨ ( ran 𝐺 ∩ { ( 2^nd ‘ 𝑝 ) } ) = ∅ ) )
30	1	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
31		dffn3	⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 : 𝐴 ⟶ ran 𝐹 )
32	30 31	sylib	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ran 𝐹 )
33	2	ffnd	⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
34		dffn3	⊢ ( 𝐺 Fn 𝐴 ↔ 𝐺 : 𝐴 ⟶ ran 𝐺 )
35	33 34	sylib	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ ran 𝐺 )
36	35	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∖ ( ran 𝐹 × ran 𝐺 ) ) ) → 𝐺 : 𝐴 ⟶ ran 𝐺 )
37		fimacnvdisj	⊢ ( ( 𝐹 : 𝐴 ⟶ ran 𝐹 ∧ ( ran 𝐹 ∩ { ( 1^st ‘ 𝑝 ) } ) = ∅ ) → ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) = ∅ )
38		ineq1	⊢ ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) = ∅ → ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) = ( ∅ ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) )
39		0in	⊢ ( ∅ ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) = ∅
40	38 39	eqtrdi	⊢ ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) = ∅ → ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) = ∅ )
41	37 40	syl	⊢ ( ( 𝐹 : 𝐴 ⟶ ran 𝐹 ∧ ( ran 𝐹 ∩ { ( 1^st ‘ 𝑝 ) } ) = ∅ ) → ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) = ∅ )
42	41	ex	⊢ ( 𝐹 : 𝐴 ⟶ ran 𝐹 → ( ( ran 𝐹 ∩ { ( 1^st ‘ 𝑝 ) } ) = ∅ → ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) = ∅ ) )
43		fimacnvdisj	⊢ ( ( 𝐺 : 𝐴 ⟶ ran 𝐺 ∧ ( ran 𝐺 ∩ { ( 2^nd ‘ 𝑝 ) } ) = ∅ ) → ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) = ∅ )
44		ineq2	⊢ ( ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) = ∅ → ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) = ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ∅ ) )
45		in0	⊢ ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ∅ ) = ∅
46	44 45	eqtrdi	⊢ ( ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) = ∅ → ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) = ∅ )
47	43 46	syl	⊢ ( ( 𝐺 : 𝐴 ⟶ ran 𝐺 ∧ ( ran 𝐺 ∩ { ( 2^nd ‘ 𝑝 ) } ) = ∅ ) → ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) = ∅ )
48	47	ex	⊢ ( 𝐺 : 𝐴 ⟶ ran 𝐺 → ( ( ran 𝐺 ∩ { ( 2^nd ‘ 𝑝 ) } ) = ∅ → ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) = ∅ ) )
49	42 48	jaao	⊢ ( ( 𝐹 : 𝐴 ⟶ ran 𝐹 ∧ 𝐺 : 𝐴 ⟶ ran 𝐺 ) → ( ( ( ran 𝐹 ∩ { ( 1^st ‘ 𝑝 ) } ) = ∅ ∨ ( ran 𝐺 ∩ { ( 2^nd ‘ 𝑝 ) } ) = ∅ ) → ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) = ∅ ) )
50	32 36 49	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∖ ( ran 𝐹 × ran 𝐺 ) ) ) → ( ( ( ran 𝐹 ∩ { ( 1^st ‘ 𝑝 ) } ) = ∅ ∨ ( ran 𝐺 ∩ { ( 2^nd ‘ 𝑝 ) } ) = ∅ ) → ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) = ∅ ) )
51	29 50	mpd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∖ ( ran 𝐹 × ran 𝐺 ) ) ) → ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) = ∅ )
52	51	iuneq2dv	⊢ ( 𝜑 → ∪ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∖ ( ran 𝐹 × ran 𝐺 ) ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) = ∪ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∖ ( ran 𝐹 × ran 𝐺 ) ) ∅ )
53		iun0	⊢ ∪ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∖ ( ran 𝐹 × ran 𝐺 ) ) ∅ = ∅
54	52 53	eqtrdi	⊢ ( 𝜑 → ∪ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∖ ( ran 𝐹 × ran 𝐺 ) ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) = ∅ )
55	54	uneq2d	⊢ ( 𝜑 → ( ∪ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) ∪ ∪ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∖ ( ran 𝐹 × ran 𝐺 ) ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) ) = ( ∪ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) ∪ ∅ ) )
56		un0	⊢ ( ∪ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) ∪ ∅ ) = ∪ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) )
57	55 56	eqtrdi	⊢ ( 𝜑 → ( ∪ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) ∪ ∪ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∖ ( ran 𝐹 × ran 𝐺 ) ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) ) = ∪ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) )
58	11 57	eqtrd	⊢ ( 𝜑 → ( ^◡ ( 𝐹 ∘_f 𝑅 𝐺 ) “ 𝐷 ) = ∪ 𝑝 ∈ ( ( ^◡ 𝑅 “ 𝐷 ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) )

Metamath Proof Explorer

Theorem ofpreima2

Proof