xppreima

Description: The preimage of a Cartesian product is the intersection of the preimages of each component function. (Contributed by Thierry Arnoux, 6-Jun-2017)

		Ref	Expression
	Assertion	xppreima	⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( V × V ) ) → ( ^◡ 𝐹 “ ( 𝑌 × 𝑍 ) ) = ( ( ^◡ ( 1^st ∘ 𝐹 ) “ 𝑌 ) ∩ ( ^◡ ( 2^nd ∘ 𝐹 ) “ 𝑍 ) ) )

Proof

Step	Hyp	Ref	Expression
1		funfn	⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
2		fncnvima2	⊢ ( 𝐹 Fn dom 𝐹 → ( ^◡ 𝐹 “ ( 𝑌 × 𝑍 ) ) = { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑌 × 𝑍 ) } )
3	1 2	sylbi	⊢ ( Fun 𝐹 → ( ^◡ 𝐹 “ ( 𝑌 × 𝑍 ) ) = { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑌 × 𝑍 ) } )
4	3	adantr	⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( V × V ) ) → ( ^◡ 𝐹 “ ( 𝑌 × 𝑍 ) ) = { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑌 × 𝑍 ) } )
5		elxp6	⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑌 × 𝑍 ) ↔ ( ( 𝐹 ‘ 𝑥 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ ∧ ( ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝑌 ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝑍 ) ) )
6		fvco	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( 1^st ∘ 𝐹 ) ‘ 𝑥 ) = ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) )
7		fvco	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( 2^nd ∘ 𝐹 ) ‘ 𝑥 ) = ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) )
8	6 7	opeq12d	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ⟨ ( ( 1^st ∘ 𝐹 ) ‘ 𝑥 ) , ( ( 2^nd ∘ 𝐹 ) ‘ 𝑥 ) ⟩ = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ )
9	8	eqeq2d	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑥 ) = ⟨ ( ( 1^st ∘ 𝐹 ) ‘ 𝑥 ) , ( ( 2^nd ∘ 𝐹 ) ‘ 𝑥 ) ⟩ ↔ ( 𝐹 ‘ 𝑥 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ ) )
10	6	eleq1d	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( ( 1^st ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑌 ↔ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝑌 ) )
11	7	eleq1d	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( ( 2^nd ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑍 ↔ ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝑍 ) )
12	10 11	anbi12d	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( ( ( 1^st ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑌 ∧ ( ( 2^nd ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑍 ) ↔ ( ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝑌 ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝑍 ) ) )
13	9 12	anbi12d	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( ( 𝐹 ‘ 𝑥 ) = ⟨ ( ( 1^st ∘ 𝐹 ) ‘ 𝑥 ) , ( ( 2^nd ∘ 𝐹 ) ‘ 𝑥 ) ⟩ ∧ ( ( ( 1^st ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑌 ∧ ( ( 2^nd ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑍 ) ) ↔ ( ( 𝐹 ‘ 𝑥 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ⟩ ∧ ( ( 1^st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝑌 ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝑍 ) ) ) )
14	5 13	bitr4id	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑌 × 𝑍 ) ↔ ( ( 𝐹 ‘ 𝑥 ) = ⟨ ( ( 1^st ∘ 𝐹 ) ‘ 𝑥 ) , ( ( 2^nd ∘ 𝐹 ) ‘ 𝑥 ) ⟩ ∧ ( ( ( 1^st ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑌 ∧ ( ( 2^nd ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑍 ) ) ) )
15	14	adantlr	⊢ ( ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( V × V ) ) ∧ 𝑥 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑌 × 𝑍 ) ↔ ( ( 𝐹 ‘ 𝑥 ) = ⟨ ( ( 1^st ∘ 𝐹 ) ‘ 𝑥 ) , ( ( 2^nd ∘ 𝐹 ) ‘ 𝑥 ) ⟩ ∧ ( ( ( 1^st ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑌 ∧ ( ( 2^nd ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑍 ) ) ) )
16		opfv	⊢ ( ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( V × V ) ) ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) = ⟨ ( ( 1^st ∘ 𝐹 ) ‘ 𝑥 ) , ( ( 2^nd ∘ 𝐹 ) ‘ 𝑥 ) ⟩ )
17	16	biantrurd	⊢ ( ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( V × V ) ) ∧ 𝑥 ∈ dom 𝐹 ) → ( ( ( ( 1^st ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑌 ∧ ( ( 2^nd ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑍 ) ↔ ( ( 𝐹 ‘ 𝑥 ) = ⟨ ( ( 1^st ∘ 𝐹 ) ‘ 𝑥 ) , ( ( 2^nd ∘ 𝐹 ) ‘ 𝑥 ) ⟩ ∧ ( ( ( 1^st ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑌 ∧ ( ( 2^nd ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑍 ) ) ) )
18		fo1st	⊢ 1^st : V –onto→ V
19		fofun	⊢ ( 1^st : V –onto→ V → Fun 1^st )
20	18 19	ax-mp	⊢ Fun 1^st
21		funco	⊢ ( ( Fun 1^st ∧ Fun 𝐹 ) → Fun ( 1^st ∘ 𝐹 ) )
22	20 21	mpan	⊢ ( Fun 𝐹 → Fun ( 1^st ∘ 𝐹 ) )
23	22	adantr	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → Fun ( 1^st ∘ 𝐹 ) )
24		ssv	⊢ ( 𝐹 “ dom 𝐹 ) ⊆ V
25		fof	⊢ ( 1^st : V –onto→ V → 1^st : V ⟶ V )
26		fdm	⊢ ( 1^st : V ⟶ V → dom 1^st = V )
27	18 25 26	mp2b	⊢ dom 1^st = V
28	24 27	sseqtrri	⊢ ( 𝐹 “ dom 𝐹 ) ⊆ dom 1^st
29		ssid	⊢ dom 𝐹 ⊆ dom 𝐹
30		funimass3	⊢ ( ( Fun 𝐹 ∧ dom 𝐹 ⊆ dom 𝐹 ) → ( ( 𝐹 “ dom 𝐹 ) ⊆ dom 1^st ↔ dom 𝐹 ⊆ ( ^◡ 𝐹 “ dom 1^st ) ) )
31	29 30	mpan2	⊢ ( Fun 𝐹 → ( ( 𝐹 “ dom 𝐹 ) ⊆ dom 1^st ↔ dom 𝐹 ⊆ ( ^◡ 𝐹 “ dom 1^st ) ) )
32	28 31	mpbii	⊢ ( Fun 𝐹 → dom 𝐹 ⊆ ( ^◡ 𝐹 “ dom 1^st ) )
33	32	sselda	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → 𝑥 ∈ ( ^◡ 𝐹 “ dom 1^st ) )
34		dmco	⊢ dom ( 1^st ∘ 𝐹 ) = ( ^◡ 𝐹 “ dom 1^st )
35	33 34	eleqtrrdi	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → 𝑥 ∈ dom ( 1^st ∘ 𝐹 ) )
36		fvimacnv	⊢ ( ( Fun ( 1^st ∘ 𝐹 ) ∧ 𝑥 ∈ dom ( 1^st ∘ 𝐹 ) ) → ( ( ( 1^st ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑌 ↔ 𝑥 ∈ ( ^◡ ( 1^st ∘ 𝐹 ) “ 𝑌 ) ) )
37	23 35 36	syl2anc	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( ( 1^st ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑌 ↔ 𝑥 ∈ ( ^◡ ( 1^st ∘ 𝐹 ) “ 𝑌 ) ) )
38		fo2nd	⊢ 2^nd : V –onto→ V
39		fofun	⊢ ( 2^nd : V –onto→ V → Fun 2^nd )
40	38 39	ax-mp	⊢ Fun 2^nd
41		funco	⊢ ( ( Fun 2^nd ∧ Fun 𝐹 ) → Fun ( 2^nd ∘ 𝐹 ) )
42	40 41	mpan	⊢ ( Fun 𝐹 → Fun ( 2^nd ∘ 𝐹 ) )
43	42	adantr	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → Fun ( 2^nd ∘ 𝐹 ) )
44		fof	⊢ ( 2^nd : V –onto→ V → 2^nd : V ⟶ V )
45		fdm	⊢ ( 2^nd : V ⟶ V → dom 2^nd = V )
46	38 44 45	mp2b	⊢ dom 2^nd = V
47	24 46	sseqtrri	⊢ ( 𝐹 “ dom 𝐹 ) ⊆ dom 2^nd
48		funimass3	⊢ ( ( Fun 𝐹 ∧ dom 𝐹 ⊆ dom 𝐹 ) → ( ( 𝐹 “ dom 𝐹 ) ⊆ dom 2^nd ↔ dom 𝐹 ⊆ ( ^◡ 𝐹 “ dom 2^nd ) ) )
49	29 48	mpan2	⊢ ( Fun 𝐹 → ( ( 𝐹 “ dom 𝐹 ) ⊆ dom 2^nd ↔ dom 𝐹 ⊆ ( ^◡ 𝐹 “ dom 2^nd ) ) )
50	47 49	mpbii	⊢ ( Fun 𝐹 → dom 𝐹 ⊆ ( ^◡ 𝐹 “ dom 2^nd ) )
51	50	sselda	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → 𝑥 ∈ ( ^◡ 𝐹 “ dom 2^nd ) )
52		dmco	⊢ dom ( 2^nd ∘ 𝐹 ) = ( ^◡ 𝐹 “ dom 2^nd )
53	51 52	eleqtrrdi	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → 𝑥 ∈ dom ( 2^nd ∘ 𝐹 ) )
54		fvimacnv	⊢ ( ( Fun ( 2^nd ∘ 𝐹 ) ∧ 𝑥 ∈ dom ( 2^nd ∘ 𝐹 ) ) → ( ( ( 2^nd ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑍 ↔ 𝑥 ∈ ( ^◡ ( 2^nd ∘ 𝐹 ) “ 𝑍 ) ) )
55	43 53 54	syl2anc	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( ( 2^nd ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑍 ↔ 𝑥 ∈ ( ^◡ ( 2^nd ∘ 𝐹 ) “ 𝑍 ) ) )
56	37 55	anbi12d	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( ( ( 1^st ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑌 ∧ ( ( 2^nd ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑍 ) ↔ ( 𝑥 ∈ ( ^◡ ( 1^st ∘ 𝐹 ) “ 𝑌 ) ∧ 𝑥 ∈ ( ^◡ ( 2^nd ∘ 𝐹 ) “ 𝑍 ) ) ) )
57	56	adantlr	⊢ ( ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( V × V ) ) ∧ 𝑥 ∈ dom 𝐹 ) → ( ( ( ( 1^st ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑌 ∧ ( ( 2^nd ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑍 ) ↔ ( 𝑥 ∈ ( ^◡ ( 1^st ∘ 𝐹 ) “ 𝑌 ) ∧ 𝑥 ∈ ( ^◡ ( 2^nd ∘ 𝐹 ) “ 𝑍 ) ) ) )
58	15 17 57	3bitr2d	⊢ ( ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( V × V ) ) ∧ 𝑥 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑌 × 𝑍 ) ↔ ( 𝑥 ∈ ( ^◡ ( 1^st ∘ 𝐹 ) “ 𝑌 ) ∧ 𝑥 ∈ ( ^◡ ( 2^nd ∘ 𝐹 ) “ 𝑍 ) ) ) )
59	58	rabbidva	⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( V × V ) ) → { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑌 × 𝑍 ) } = { 𝑥 ∈ dom 𝐹 ∣ ( 𝑥 ∈ ( ^◡ ( 1^st ∘ 𝐹 ) “ 𝑌 ) ∧ 𝑥 ∈ ( ^◡ ( 2^nd ∘ 𝐹 ) “ 𝑍 ) ) } )
60	4 59	eqtrd	⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( V × V ) ) → ( ^◡ 𝐹 “ ( 𝑌 × 𝑍 ) ) = { 𝑥 ∈ dom 𝐹 ∣ ( 𝑥 ∈ ( ^◡ ( 1^st ∘ 𝐹 ) “ 𝑌 ) ∧ 𝑥 ∈ ( ^◡ ( 2^nd ∘ 𝐹 ) “ 𝑍 ) ) } )
61		dfin5	⊢ ( dom 𝐹 ∩ ( ^◡ ( 1^st ∘ 𝐹 ) “ 𝑌 ) ) = { 𝑥 ∈ dom 𝐹 ∣ 𝑥 ∈ ( ^◡ ( 1^st ∘ 𝐹 ) “ 𝑌 ) }
62		dfin5	⊢ ( dom 𝐹 ∩ ( ^◡ ( 2^nd ∘ 𝐹 ) “ 𝑍 ) ) = { 𝑥 ∈ dom 𝐹 ∣ 𝑥 ∈ ( ^◡ ( 2^nd ∘ 𝐹 ) “ 𝑍 ) }
63	61 62	ineq12i	⊢ ( ( dom 𝐹 ∩ ( ^◡ ( 1^st ∘ 𝐹 ) “ 𝑌 ) ) ∩ ( dom 𝐹 ∩ ( ^◡ ( 2^nd ∘ 𝐹 ) “ 𝑍 ) ) ) = ( { 𝑥 ∈ dom 𝐹 ∣ 𝑥 ∈ ( ^◡ ( 1^st ∘ 𝐹 ) “ 𝑌 ) } ∩ { 𝑥 ∈ dom 𝐹 ∣ 𝑥 ∈ ( ^◡ ( 2^nd ∘ 𝐹 ) “ 𝑍 ) } )
64		cnvimass	⊢ ( ^◡ ( 1^st ∘ 𝐹 ) “ 𝑌 ) ⊆ dom ( 1^st ∘ 𝐹 )
65		dmcoss	⊢ dom ( 1^st ∘ 𝐹 ) ⊆ dom 𝐹
66	64 65	sstri	⊢ ( ^◡ ( 1^st ∘ 𝐹 ) “ 𝑌 ) ⊆ dom 𝐹
67		sseqin2	⊢ ( ( ^◡ ( 1^st ∘ 𝐹 ) “ 𝑌 ) ⊆ dom 𝐹 ↔ ( dom 𝐹 ∩ ( ^◡ ( 1^st ∘ 𝐹 ) “ 𝑌 ) ) = ( ^◡ ( 1^st ∘ 𝐹 ) “ 𝑌 ) )
68	66 67	mpbi	⊢ ( dom 𝐹 ∩ ( ^◡ ( 1^st ∘ 𝐹 ) “ 𝑌 ) ) = ( ^◡ ( 1^st ∘ 𝐹 ) “ 𝑌 )
69		cnvimass	⊢ ( ^◡ ( 2^nd ∘ 𝐹 ) “ 𝑍 ) ⊆ dom ( 2^nd ∘ 𝐹 )
70		dmcoss	⊢ dom ( 2^nd ∘ 𝐹 ) ⊆ dom 𝐹
71	69 70	sstri	⊢ ( ^◡ ( 2^nd ∘ 𝐹 ) “ 𝑍 ) ⊆ dom 𝐹
72		sseqin2	⊢ ( ( ^◡ ( 2^nd ∘ 𝐹 ) “ 𝑍 ) ⊆ dom 𝐹 ↔ ( dom 𝐹 ∩ ( ^◡ ( 2^nd ∘ 𝐹 ) “ 𝑍 ) ) = ( ^◡ ( 2^nd ∘ 𝐹 ) “ 𝑍 ) )
73	71 72	mpbi	⊢ ( dom 𝐹 ∩ ( ^◡ ( 2^nd ∘ 𝐹 ) “ 𝑍 ) ) = ( ^◡ ( 2^nd ∘ 𝐹 ) “ 𝑍 )
74	68 73	ineq12i	⊢ ( ( dom 𝐹 ∩ ( ^◡ ( 1^st ∘ 𝐹 ) “ 𝑌 ) ) ∩ ( dom 𝐹 ∩ ( ^◡ ( 2^nd ∘ 𝐹 ) “ 𝑍 ) ) ) = ( ( ^◡ ( 1^st ∘ 𝐹 ) “ 𝑌 ) ∩ ( ^◡ ( 2^nd ∘ 𝐹 ) “ 𝑍 ) )
75		inrab	⊢ ( { 𝑥 ∈ dom 𝐹 ∣ 𝑥 ∈ ( ^◡ ( 1^st ∘ 𝐹 ) “ 𝑌 ) } ∩ { 𝑥 ∈ dom 𝐹 ∣ 𝑥 ∈ ( ^◡ ( 2^nd ∘ 𝐹 ) “ 𝑍 ) } ) = { 𝑥 ∈ dom 𝐹 ∣ ( 𝑥 ∈ ( ^◡ ( 1^st ∘ 𝐹 ) “ 𝑌 ) ∧ 𝑥 ∈ ( ^◡ ( 2^nd ∘ 𝐹 ) “ 𝑍 ) ) }
76	63 74 75	3eqtr3ri	⊢ { 𝑥 ∈ dom 𝐹 ∣ ( 𝑥 ∈ ( ^◡ ( 1^st ∘ 𝐹 ) “ 𝑌 ) ∧ 𝑥 ∈ ( ^◡ ( 2^nd ∘ 𝐹 ) “ 𝑍 ) ) } = ( ( ^◡ ( 1^st ∘ 𝐹 ) “ 𝑌 ) ∩ ( ^◡ ( 2^nd ∘ 𝐹 ) “ 𝑍 ) )
77	60 76	eqtrdi	⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( V × V ) ) → ( ^◡ 𝐹 “ ( 𝑌 × 𝑍 ) ) = ( ( ^◡ ( 1^st ∘ 𝐹 ) “ 𝑌 ) ∩ ( ^◡ ( 2^nd ∘ 𝐹 ) “ 𝑍 ) ) )

Metamath Proof Explorer

Theorem xppreima

Proof