Metamath Proof Explorer


Theorem 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 ) ) → ( 𝐹 “ ( 𝑌 × 𝑍 ) ) = ( ( ( 1st𝐹 ) “ 𝑌 ) ∩ ( ( 2nd𝐹 ) “ 𝑍 ) ) )

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