ofpreima

Description: Express the preimage of a function operation as a union of preimages. (Contributed by Thierry Arnoux, 8-Mar-2018)

	Ref	Expression
Hypotheses	ofpreima.1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	ofpreima.2	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐶 )
	ofpreima.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	ofpreima.4	⊢ ( 𝜑 → 𝑅 Fn ( 𝐵 × 𝐶 ) )
Assertion	ofpreima	⊢ ( 𝜑 → ( ^◡ ( 𝐹 ∘_f 𝑅 𝐺 ) “ 𝐷 ) = ∪ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		ofpreima.1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		ofpreima.2	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐶 )
3		ofpreima.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		ofpreima.4	⊢ ( 𝜑 → 𝑅 Fn ( 𝐵 × 𝐶 ) )
5		nfmpt1	⊢ Ⅎ 𝑠 ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ )
6		eqidd	⊢ ( 𝜑 → ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) = ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) )
7		fnov	⊢ ( 𝑅 Fn ( 𝐵 × 𝐶 ) ↔ 𝑅 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( 𝑥 𝑅 𝑦 ) ) )
8	4 7	sylib	⊢ ( 𝜑 → 𝑅 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐶 ↦ ( 𝑥 𝑅 𝑦 ) ) )
9	5 1 2 3 6 8	ofoprabco	⊢ ( 𝜑 → ( 𝐹 ∘_f 𝑅 𝐺 ) = ( 𝑅 ∘ ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) ) )
10	9	cnveqd	⊢ ( 𝜑 → ^◡ ( 𝐹 ∘_f 𝑅 𝐺 ) = ^◡ ( 𝑅 ∘ ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) ) )
11		cnvco	⊢ ^◡ ( 𝑅 ∘ ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) ) = ( ^◡ ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) ∘ ^◡ 𝑅 )
12	10 11	eqtrdi	⊢ ( 𝜑 → ^◡ ( 𝐹 ∘_f 𝑅 𝐺 ) = ( ^◡ ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) ∘ ^◡ 𝑅 ) )
13	12	imaeq1d	⊢ ( 𝜑 → ( ^◡ ( 𝐹 ∘_f 𝑅 𝐺 ) “ 𝐷 ) = ( ( ^◡ ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) ∘ ^◡ 𝑅 ) “ 𝐷 ) )
14		imaco	⊢ ( ( ^◡ ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) ∘ ^◡ 𝑅 ) “ 𝐷 ) = ( ^◡ ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) “ ( ^◡ 𝑅 “ 𝐷 ) )
15	13 14	eqtrdi	⊢ ( 𝜑 → ( ^◡ ( 𝐹 ∘_f 𝑅 𝐺 ) “ 𝐷 ) = ( ^◡ ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) “ ( ^◡ 𝑅 “ 𝐷 ) ) )
16		dfima2	⊢ ( ^◡ ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) “ ( ^◡ 𝑅 “ 𝐷 ) ) = { 𝑞 ∣ ∃ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) 𝑝 ^◡ ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) 𝑞 }
17		vex	⊢ 𝑝 ∈ V
18		vex	⊢ 𝑞 ∈ V
19	17 18	brcnv	⊢ ( 𝑝 ^◡ ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) 𝑞 ↔ 𝑞 ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) 𝑝 )
20		funmpt	⊢ Fun ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ )
21		funbrfv2b	⊢ ( Fun ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) → ( 𝑞 ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) 𝑝 ↔ ( 𝑞 ∈ dom ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) ∧ ( ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) ‘ 𝑞 ) = 𝑝 ) ) )
22	20 21	ax-mp	⊢ ( 𝑞 ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) 𝑝 ↔ ( 𝑞 ∈ dom ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) ∧ ( ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) ‘ 𝑞 ) = 𝑝 ) )
23		opex	⊢ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ∈ V
24		eqid	⊢ ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) = ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ )
25	23 24	dmmpti	⊢ dom ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) = 𝐴
26	25	eleq2i	⊢ ( 𝑞 ∈ dom ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) ↔ 𝑞 ∈ 𝐴 )
27	26	anbi1i	⊢ ( ( 𝑞 ∈ dom ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) ∧ ( ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) ‘ 𝑞 ) = 𝑝 ) ↔ ( 𝑞 ∈ 𝐴 ∧ ( ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) ‘ 𝑞 ) = 𝑝 ) )
28	22 27	bitri	⊢ ( 𝑞 ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) 𝑝 ↔ ( 𝑞 ∈ 𝐴 ∧ ( ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) ‘ 𝑞 ) = 𝑝 ) )
29		fveq2	⊢ ( 𝑠 = 𝑞 → ( 𝐹 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑞 ) )
30		fveq2	⊢ ( 𝑠 = 𝑞 → ( 𝐺 ‘ 𝑠 ) = ( 𝐺 ‘ 𝑞 ) )
31	29 30	opeq12d	⊢ ( 𝑠 = 𝑞 → ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑞 ) , ( 𝐺 ‘ 𝑞 ) ⟩ )
32		opex	⊢ ⟨ ( 𝐹 ‘ 𝑞 ) , ( 𝐺 ‘ 𝑞 ) ⟩ ∈ V
33	31 24 32	fvmpt	⊢ ( 𝑞 ∈ 𝐴 → ( ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) ‘ 𝑞 ) = ⟨ ( 𝐹 ‘ 𝑞 ) , ( 𝐺 ‘ 𝑞 ) ⟩ )
34	33	eqeq1d	⊢ ( 𝑞 ∈ 𝐴 → ( ( ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) ‘ 𝑞 ) = 𝑝 ↔ ⟨ ( 𝐹 ‘ 𝑞 ) , ( 𝐺 ‘ 𝑞 ) ⟩ = 𝑝 ) )
35	34	pm5.32i	⊢ ( ( 𝑞 ∈ 𝐴 ∧ ( ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) ‘ 𝑞 ) = 𝑝 ) ↔ ( 𝑞 ∈ 𝐴 ∧ ⟨ ( 𝐹 ‘ 𝑞 ) , ( 𝐺 ‘ 𝑞 ) ⟩ = 𝑝 ) )
36	19 28 35	3bitri	⊢ ( 𝑝 ^◡ ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) 𝑞 ↔ ( 𝑞 ∈ 𝐴 ∧ ⟨ ( 𝐹 ‘ 𝑞 ) , ( 𝐺 ‘ 𝑞 ) ⟩ = 𝑝 ) )
37	36	rexbii	⊢ ( ∃ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) 𝑝 ^◡ ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) 𝑞 ↔ ∃ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) ( 𝑞 ∈ 𝐴 ∧ ⟨ ( 𝐹 ‘ 𝑞 ) , ( 𝐺 ‘ 𝑞 ) ⟩ = 𝑝 ) )
38	37	abbii	⊢ { 𝑞 ∣ ∃ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) 𝑝 ^◡ ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) 𝑞 } = { 𝑞 ∣ ∃ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) ( 𝑞 ∈ 𝐴 ∧ ⟨ ( 𝐹 ‘ 𝑞 ) , ( 𝐺 ‘ 𝑞 ) ⟩ = 𝑝 ) }
39		nfv	⊢ Ⅎ 𝑞 𝜑
40		nfab1	⊢ Ⅎ 𝑞 { 𝑞 ∣ ∃ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) ( 𝑞 ∈ 𝐴 ∧ ⟨ ( 𝐹 ‘ 𝑞 ) , ( 𝐺 ‘ 𝑞 ) ⟩ = 𝑝 ) }
41		nfcv	⊢ Ⅎ 𝑞 ∪ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) )
42		eliun	⊢ ( 𝑞 ∈ ∪ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) ↔ ∃ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) 𝑞 ∈ ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) )
43		ffn	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
44		fniniseg	⊢ ( 𝐹 Fn 𝐴 → ( 𝑞 ∈ ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ↔ ( 𝑞 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑞 ) = ( 1^st ‘ 𝑝 ) ) ) )
45	1 43 44	3syl	⊢ ( 𝜑 → ( 𝑞 ∈ ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ↔ ( 𝑞 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑞 ) = ( 1^st ‘ 𝑝 ) ) ) )
46		ffn	⊢ ( 𝐺 : 𝐴 ⟶ 𝐶 → 𝐺 Fn 𝐴 )
47		fniniseg	⊢ ( 𝐺 Fn 𝐴 → ( 𝑞 ∈ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ↔ ( 𝑞 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑞 ) = ( 2^nd ‘ 𝑝 ) ) ) )
48	2 46 47	3syl	⊢ ( 𝜑 → ( 𝑞 ∈ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ↔ ( 𝑞 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑞 ) = ( 2^nd ‘ 𝑝 ) ) ) )
49	45 48	anbi12d	⊢ ( 𝜑 → ( ( 𝑞 ∈ ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∧ 𝑞 ∈ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) ↔ ( ( 𝑞 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑞 ) = ( 1^st ‘ 𝑝 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑞 ) = ( 2^nd ‘ 𝑝 ) ) ) ) )
50		elin	⊢ ( 𝑞 ∈ ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) ↔ ( 𝑞 ∈ ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∧ 𝑞 ∈ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) )
51		anandi	⊢ ( ( 𝑞 ∈ 𝐴 ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 1^st ‘ 𝑝 ) ∧ ( 𝐺 ‘ 𝑞 ) = ( 2^nd ‘ 𝑝 ) ) ) ↔ ( ( 𝑞 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑞 ) = ( 1^st ‘ 𝑝 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑞 ) = ( 2^nd ‘ 𝑝 ) ) ) )
52	49 50 51	3bitr4g	⊢ ( 𝜑 → ( 𝑞 ∈ ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) ↔ ( 𝑞 ∈ 𝐴 ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 1^st ‘ 𝑝 ) ∧ ( 𝐺 ‘ 𝑞 ) = ( 2^nd ‘ 𝑝 ) ) ) ) )
53	52	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) ) → ( 𝑞 ∈ ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) ↔ ( 𝑞 ∈ 𝐴 ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 1^st ‘ 𝑝 ) ∧ ( 𝐺 ‘ 𝑞 ) = ( 2^nd ‘ 𝑝 ) ) ) ) )
54		cnvimass	⊢ ( ^◡ 𝑅 “ 𝐷 ) ⊆ dom 𝑅
55	4	fndmd	⊢ ( 𝜑 → dom 𝑅 = ( 𝐵 × 𝐶 ) )
56	54 55	sseqtrid	⊢ ( 𝜑 → ( ^◡ 𝑅 “ 𝐷 ) ⊆ ( 𝐵 × 𝐶 ) )
57	56	sselda	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) ) → 𝑝 ∈ ( 𝐵 × 𝐶 ) )
58		1st2nd2	⊢ ( 𝑝 ∈ ( 𝐵 × 𝐶 ) → 𝑝 = ⟨ ( 1^st ‘ 𝑝 ) , ( 2^nd ‘ 𝑝 ) ⟩ )
59		eqeq2	⊢ ( 𝑝 = ⟨ ( 1^st ‘ 𝑝 ) , ( 2^nd ‘ 𝑝 ) ⟩ → ( ⟨ ( 𝐹 ‘ 𝑞 ) , ( 𝐺 ‘ 𝑞 ) ⟩ = 𝑝 ↔ ⟨ ( 𝐹 ‘ 𝑞 ) , ( 𝐺 ‘ 𝑞 ) ⟩ = ⟨ ( 1^st ‘ 𝑝 ) , ( 2^nd ‘ 𝑝 ) ⟩ ) )
60	57 58 59	3syl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) ) → ( ⟨ ( 𝐹 ‘ 𝑞 ) , ( 𝐺 ‘ 𝑞 ) ⟩ = 𝑝 ↔ ⟨ ( 𝐹 ‘ 𝑞 ) , ( 𝐺 ‘ 𝑞 ) ⟩ = ⟨ ( 1^st ‘ 𝑝 ) , ( 2^nd ‘ 𝑝 ) ⟩ ) )
61		fvex	⊢ ( 𝐹 ‘ 𝑞 ) ∈ V
62		fvex	⊢ ( 𝐺 ‘ 𝑞 ) ∈ V
63	61 62	opth	⊢ ( ⟨ ( 𝐹 ‘ 𝑞 ) , ( 𝐺 ‘ 𝑞 ) ⟩ = ⟨ ( 1^st ‘ 𝑝 ) , ( 2^nd ‘ 𝑝 ) ⟩ ↔ ( ( 𝐹 ‘ 𝑞 ) = ( 1^st ‘ 𝑝 ) ∧ ( 𝐺 ‘ 𝑞 ) = ( 2^nd ‘ 𝑝 ) ) )
64	60 63	bitrdi	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) ) → ( ⟨ ( 𝐹 ‘ 𝑞 ) , ( 𝐺 ‘ 𝑞 ) ⟩ = 𝑝 ↔ ( ( 𝐹 ‘ 𝑞 ) = ( 1^st ‘ 𝑝 ) ∧ ( 𝐺 ‘ 𝑞 ) = ( 2^nd ‘ 𝑝 ) ) ) )
65	64	anbi2d	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) ) → ( ( 𝑞 ∈ 𝐴 ∧ ⟨ ( 𝐹 ‘ 𝑞 ) , ( 𝐺 ‘ 𝑞 ) ⟩ = 𝑝 ) ↔ ( 𝑞 ∈ 𝐴 ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 1^st ‘ 𝑝 ) ∧ ( 𝐺 ‘ 𝑞 ) = ( 2^nd ‘ 𝑝 ) ) ) ) )
66	53 65	bitr4d	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) ) → ( 𝑞 ∈ ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) ↔ ( 𝑞 ∈ 𝐴 ∧ ⟨ ( 𝐹 ‘ 𝑞 ) , ( 𝐺 ‘ 𝑞 ) ⟩ = 𝑝 ) ) )
67	66	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) 𝑞 ∈ ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) ↔ ∃ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) ( 𝑞 ∈ 𝐴 ∧ ⟨ ( 𝐹 ‘ 𝑞 ) , ( 𝐺 ‘ 𝑞 ) ⟩ = 𝑝 ) ) )
68		abid	⊢ ( 𝑞 ∈ { 𝑞 ∣ ∃ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) ( 𝑞 ∈ 𝐴 ∧ ⟨ ( 𝐹 ‘ 𝑞 ) , ( 𝐺 ‘ 𝑞 ) ⟩ = 𝑝 ) } ↔ ∃ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) ( 𝑞 ∈ 𝐴 ∧ ⟨ ( 𝐹 ‘ 𝑞 ) , ( 𝐺 ‘ 𝑞 ) ⟩ = 𝑝 ) )
69	67 68	bitr4di	⊢ ( 𝜑 → ( ∃ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) 𝑞 ∈ ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) ↔ 𝑞 ∈ { 𝑞 ∣ ∃ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) ( 𝑞 ∈ 𝐴 ∧ ⟨ ( 𝐹 ‘ 𝑞 ) , ( 𝐺 ‘ 𝑞 ) ⟩ = 𝑝 ) } ) )
70	42 69	syl5rbb	⊢ ( 𝜑 → ( 𝑞 ∈ { 𝑞 ∣ ∃ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) ( 𝑞 ∈ 𝐴 ∧ ⟨ ( 𝐹 ‘ 𝑞 ) , ( 𝐺 ‘ 𝑞 ) ⟩ = 𝑝 ) } ↔ 𝑞 ∈ ∪ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) ) )
71	39 40 41 70	eqrd	⊢ ( 𝜑 → { 𝑞 ∣ ∃ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) ( 𝑞 ∈ 𝐴 ∧ ⟨ ( 𝐹 ‘ 𝑞 ) , ( 𝐺 ‘ 𝑞 ) ⟩ = 𝑝 ) } = ∪ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) )
72	38 71	syl5eq	⊢ ( 𝜑 → { 𝑞 ∣ ∃ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) 𝑝 ^◡ ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) 𝑞 } = ∪ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) )
73	16 72	syl5eq	⊢ ( 𝜑 → ( ^◡ ( 𝑠 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐺 ‘ 𝑠 ) ⟩ ) “ ( ^◡ 𝑅 “ 𝐷 ) ) = ∪ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) )
74	15 73	eqtrd	⊢ ( 𝜑 → ( ^◡ ( 𝐹 ∘_f 𝑅 𝐺 ) “ 𝐷 ) = ∪ 𝑝 ∈ ( ^◡ 𝑅 “ 𝐷 ) ( ( ^◡ 𝐹 “ { ( 1^st ‘ 𝑝 ) } ) ∩ ( ^◡ 𝐺 “ { ( 2^nd ‘ 𝑝 ) } ) ) )

Metamath Proof Explorer

Theorem ofpreima

Proof