Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  xppreima Structured version   Visualization version   GIF version

Theorem xppreima 30159
Description: The preimage of a Cartesian product is the intersection of the preimages of each component function. (Contributed by Thierry Arnoux, 6-Jun-2017.)
Assertion
Ref Expression
xppreima ((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) → (𝐹 “ (𝑌 × 𝑍)) = (((1st𝐹) “ 𝑌) ∩ ((2nd𝐹) “ 𝑍)))

Proof of Theorem xppreima
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 funfn 6220 . . . . 5 (Fun 𝐹𝐹 Fn dom 𝐹)
2 fncnvima2 6658 . . . . 5 (𝐹 Fn dom 𝐹 → (𝐹 “ (𝑌 × 𝑍)) = {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) ∈ (𝑌 × 𝑍)})
31, 2sylbi 209 . . . 4 (Fun 𝐹 → (𝐹 “ (𝑌 × 𝑍)) = {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) ∈ (𝑌 × 𝑍)})
43adantr 473 . . 3 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) → (𝐹 “ (𝑌 × 𝑍)) = {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) ∈ (𝑌 × 𝑍)})
5 fvco 6589 . . . . . . . . . 10 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ((1st𝐹)‘𝑥) = (1st ‘(𝐹𝑥)))
6 fvco 6589 . . . . . . . . . 10 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ((2nd𝐹)‘𝑥) = (2nd ‘(𝐹𝑥)))
75, 6opeq12d 4686 . . . . . . . . 9 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ⟨((1st𝐹)‘𝑥), ((2nd𝐹)‘𝑥)⟩ = ⟨(1st ‘(𝐹𝑥)), (2nd ‘(𝐹𝑥))⟩)
87eqeq2d 2788 . . . . . . . 8 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ((𝐹𝑥) = ⟨((1st𝐹)‘𝑥), ((2nd𝐹)‘𝑥)⟩ ↔ (𝐹𝑥) = ⟨(1st ‘(𝐹𝑥)), (2nd ‘(𝐹𝑥))⟩))
95eleq1d 2850 . . . . . . . . 9 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (((1st𝐹)‘𝑥) ∈ 𝑌 ↔ (1st ‘(𝐹𝑥)) ∈ 𝑌))
106eleq1d 2850 . . . . . . . . 9 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (((2nd𝐹)‘𝑥) ∈ 𝑍 ↔ (2nd ‘(𝐹𝑥)) ∈ 𝑍))
119, 10anbi12d 621 . . . . . . . 8 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ((((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍) ↔ ((1st ‘(𝐹𝑥)) ∈ 𝑌 ∧ (2nd ‘(𝐹𝑥)) ∈ 𝑍)))
128, 11anbi12d 621 . . . . . . 7 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (((𝐹𝑥) = ⟨((1st𝐹)‘𝑥), ((2nd𝐹)‘𝑥)⟩ ∧ (((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍)) ↔ ((𝐹𝑥) = ⟨(1st ‘(𝐹𝑥)), (2nd ‘(𝐹𝑥))⟩ ∧ ((1st ‘(𝐹𝑥)) ∈ 𝑌 ∧ (2nd ‘(𝐹𝑥)) ∈ 𝑍))))
13 elxp6 7537 . . . . . . 7 ((𝐹𝑥) ∈ (𝑌 × 𝑍) ↔ ((𝐹𝑥) = ⟨(1st ‘(𝐹𝑥)), (2nd ‘(𝐹𝑥))⟩ ∧ ((1st ‘(𝐹𝑥)) ∈ 𝑌 ∧ (2nd ‘(𝐹𝑥)) ∈ 𝑍)))
1412, 13syl6rbbr 282 . . . . . 6 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ((𝐹𝑥) ∈ (𝑌 × 𝑍) ↔ ((𝐹𝑥) = ⟨((1st𝐹)‘𝑥), ((2nd𝐹)‘𝑥)⟩ ∧ (((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍))))
1514adantlr 702 . . . . 5 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐹) → ((𝐹𝑥) ∈ (𝑌 × 𝑍) ↔ ((𝐹𝑥) = ⟨((1st𝐹)‘𝑥), ((2nd𝐹)‘𝑥)⟩ ∧ (((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍))))
16 opfv 30158 . . . . . 6 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐹) → (𝐹𝑥) = ⟨((1st𝐹)‘𝑥), ((2nd𝐹)‘𝑥)⟩)
1716biantrurd 525 . . . . 5 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐹) → ((((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍) ↔ ((𝐹𝑥) = ⟨((1st𝐹)‘𝑥), ((2nd𝐹)‘𝑥)⟩ ∧ (((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍))))
18 fo1st 7523 . . . . . . . . . . 11 1st :V–onto→V
19 fofun 6422 . . . . . . . . . . 11 (1st :V–onto→V → Fun 1st )
2018, 19ax-mp 5 . . . . . . . . . 10 Fun 1st
21 funco 6230 . . . . . . . . . 10 ((Fun 1st ∧ Fun 𝐹) → Fun (1st𝐹))
2220, 21mpan 677 . . . . . . . . 9 (Fun 𝐹 → Fun (1st𝐹))
2322adantr 473 . . . . . . . 8 ((Fun 𝐹𝑥 ∈ dom 𝐹) → Fun (1st𝐹))
24 ssv 3883 . . . . . . . . . . . 12 (𝐹 “ dom 𝐹) ⊆ V
25 fof 6421 . . . . . . . . . . . . 13 (1st :V–onto→V → 1st :V⟶V)
26 fdm 6354 . . . . . . . . . . . . 13 (1st :V⟶V → dom 1st = V)
2718, 25, 26mp2b 10 . . . . . . . . . . . 12 dom 1st = V
2824, 27sseqtr4i 3896 . . . . . . . . . . 11 (𝐹 “ dom 𝐹) ⊆ dom 1st
29 ssid 3881 . . . . . . . . . . . 12 dom 𝐹 ⊆ dom 𝐹
30 funimass3 6651 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ dom 𝐹 ⊆ dom 𝐹) → ((𝐹 “ dom 𝐹) ⊆ dom 1st ↔ dom 𝐹 ⊆ (𝐹 “ dom 1st )))
3129, 30mpan2 678 . . . . . . . . . . 11 (Fun 𝐹 → ((𝐹 “ dom 𝐹) ⊆ dom 1st ↔ dom 𝐹 ⊆ (𝐹 “ dom 1st )))
3228, 31mpbii 225 . . . . . . . . . 10 (Fun 𝐹 → dom 𝐹 ⊆ (𝐹 “ dom 1st ))
3332sselda 3860 . . . . . . . . 9 ((Fun 𝐹𝑥 ∈ dom 𝐹) → 𝑥 ∈ (𝐹 “ dom 1st ))
34 dmco 5948 . . . . . . . . 9 dom (1st𝐹) = (𝐹 “ dom 1st )
3533, 34syl6eleqr 2877 . . . . . . . 8 ((Fun 𝐹𝑥 ∈ dom 𝐹) → 𝑥 ∈ dom (1st𝐹))
36 fvimacnv 6650 . . . . . . . 8 ((Fun (1st𝐹) ∧ 𝑥 ∈ dom (1st𝐹)) → (((1st𝐹)‘𝑥) ∈ 𝑌𝑥 ∈ ((1st𝐹) “ 𝑌)))
3723, 35, 36syl2anc 576 . . . . . . 7 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (((1st𝐹)‘𝑥) ∈ 𝑌𝑥 ∈ ((1st𝐹) “ 𝑌)))
38 fo2nd 7524 . . . . . . . . . . 11 2nd :V–onto→V
39 fofun 6422 . . . . . . . . . . 11 (2nd :V–onto→V → Fun 2nd )
4038, 39ax-mp 5 . . . . . . . . . 10 Fun 2nd
41 funco 6230 . . . . . . . . . 10 ((Fun 2nd ∧ Fun 𝐹) → Fun (2nd𝐹))
4240, 41mpan 677 . . . . . . . . 9 (Fun 𝐹 → Fun (2nd𝐹))
4342adantr 473 . . . . . . . 8 ((Fun 𝐹𝑥 ∈ dom 𝐹) → Fun (2nd𝐹))
44 fof 6421 . . . . . . . . . . . . 13 (2nd :V–onto→V → 2nd :V⟶V)
45 fdm 6354 . . . . . . . . . . . . 13 (2nd :V⟶V → dom 2nd = V)
4638, 44, 45mp2b 10 . . . . . . . . . . . 12 dom 2nd = V
4724, 46sseqtr4i 3896 . . . . . . . . . . 11 (𝐹 “ dom 𝐹) ⊆ dom 2nd
48 funimass3 6651 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ dom 𝐹 ⊆ dom 𝐹) → ((𝐹 “ dom 𝐹) ⊆ dom 2nd ↔ dom 𝐹 ⊆ (𝐹 “ dom 2nd )))
4929, 48mpan2 678 . . . . . . . . . . 11 (Fun 𝐹 → ((𝐹 “ dom 𝐹) ⊆ dom 2nd ↔ dom 𝐹 ⊆ (𝐹 “ dom 2nd )))
5047, 49mpbii 225 . . . . . . . . . 10 (Fun 𝐹 → dom 𝐹 ⊆ (𝐹 “ dom 2nd ))
5150sselda 3860 . . . . . . . . 9 ((Fun 𝐹𝑥 ∈ dom 𝐹) → 𝑥 ∈ (𝐹 “ dom 2nd ))
52 dmco 5948 . . . . . . . . 9 dom (2nd𝐹) = (𝐹 “ dom 2nd )
5351, 52syl6eleqr 2877 . . . . . . . 8 ((Fun 𝐹𝑥 ∈ dom 𝐹) → 𝑥 ∈ dom (2nd𝐹))
54 fvimacnv 6650 . . . . . . . 8 ((Fun (2nd𝐹) ∧ 𝑥 ∈ dom (2nd𝐹)) → (((2nd𝐹)‘𝑥) ∈ 𝑍𝑥 ∈ ((2nd𝐹) “ 𝑍)))
5543, 53, 54syl2anc 576 . . . . . . 7 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (((2nd𝐹)‘𝑥) ∈ 𝑍𝑥 ∈ ((2nd𝐹) “ 𝑍)))
5637, 55anbi12d 621 . . . . . 6 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ((((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍) ↔ (𝑥 ∈ ((1st𝐹) “ 𝑌) ∧ 𝑥 ∈ ((2nd𝐹) “ 𝑍))))
5756adantlr 702 . . . . 5 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐹) → ((((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍) ↔ (𝑥 ∈ ((1st𝐹) “ 𝑌) ∧ 𝑥 ∈ ((2nd𝐹) “ 𝑍))))
5815, 17, 573bitr2d 299 . . . 4 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐹) → ((𝐹𝑥) ∈ (𝑌 × 𝑍) ↔ (𝑥 ∈ ((1st𝐹) “ 𝑌) ∧ 𝑥 ∈ ((2nd𝐹) “ 𝑍))))
5958rabbidva 3402 . . 3 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) → {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) ∈ (𝑌 × 𝑍)} = {𝑥 ∈ dom 𝐹 ∣ (𝑥 ∈ ((1st𝐹) “ 𝑌) ∧ 𝑥 ∈ ((2nd𝐹) “ 𝑍))})
604, 59eqtrd 2814 . 2 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) → (𝐹 “ (𝑌 × 𝑍)) = {𝑥 ∈ dom 𝐹 ∣ (𝑥 ∈ ((1st𝐹) “ 𝑌) ∧ 𝑥 ∈ ((2nd𝐹) “ 𝑍))})
61 dfin5 3839 . . . 4 (dom 𝐹 ∩ ((1st𝐹) “ 𝑌)) = {𝑥 ∈ dom 𝐹𝑥 ∈ ((1st𝐹) “ 𝑌)}
62 dfin5 3839 . . . 4 (dom 𝐹 ∩ ((2nd𝐹) “ 𝑍)) = {𝑥 ∈ dom 𝐹𝑥 ∈ ((2nd𝐹) “ 𝑍)}
6361, 62ineq12i 4076 . . 3 ((dom 𝐹 ∩ ((1st𝐹) “ 𝑌)) ∩ (dom 𝐹 ∩ ((2nd𝐹) “ 𝑍))) = ({𝑥 ∈ dom 𝐹𝑥 ∈ ((1st𝐹) “ 𝑌)} ∩ {𝑥 ∈ dom 𝐹𝑥 ∈ ((2nd𝐹) “ 𝑍)})
64 cnvimass 5791 . . . . . 6 ((1st𝐹) “ 𝑌) ⊆ dom (1st𝐹)
65 dmcoss 5685 . . . . . 6 dom (1st𝐹) ⊆ dom 𝐹
6664, 65sstri 3869 . . . . 5 ((1st𝐹) “ 𝑌) ⊆ dom 𝐹
67 sseqin2 4081 . . . . 5 (((1st𝐹) “ 𝑌) ⊆ dom 𝐹 ↔ (dom 𝐹 ∩ ((1st𝐹) “ 𝑌)) = ((1st𝐹) “ 𝑌))
6866, 67mpbi 222 . . . 4 (dom 𝐹 ∩ ((1st𝐹) “ 𝑌)) = ((1st𝐹) “ 𝑌)
69 cnvimass 5791 . . . . . 6 ((2nd𝐹) “ 𝑍) ⊆ dom (2nd𝐹)
70 dmcoss 5685 . . . . . 6 dom (2nd𝐹) ⊆ dom 𝐹
7169, 70sstri 3869 . . . . 5 ((2nd𝐹) “ 𝑍) ⊆ dom 𝐹
72 sseqin2 4081 . . . . 5 (((2nd𝐹) “ 𝑍) ⊆ dom 𝐹 ↔ (dom 𝐹 ∩ ((2nd𝐹) “ 𝑍)) = ((2nd𝐹) “ 𝑍))
7371, 72mpbi 222 . . . 4 (dom 𝐹 ∩ ((2nd𝐹) “ 𝑍)) = ((2nd𝐹) “ 𝑍)
7468, 73ineq12i 4076 . . 3 ((dom 𝐹 ∩ ((1st𝐹) “ 𝑌)) ∩ (dom 𝐹 ∩ ((2nd𝐹) “ 𝑍))) = (((1st𝐹) “ 𝑌) ∩ ((2nd𝐹) “ 𝑍))
75 inrab 4164 . . 3 ({𝑥 ∈ dom 𝐹𝑥 ∈ ((1st𝐹) “ 𝑌)} ∩ {𝑥 ∈ dom 𝐹𝑥 ∈ ((2nd𝐹) “ 𝑍)}) = {𝑥 ∈ dom 𝐹 ∣ (𝑥 ∈ ((1st𝐹) “ 𝑌) ∧ 𝑥 ∈ ((2nd𝐹) “ 𝑍))}
7663, 74, 753eqtr3ri 2811 . 2 {𝑥 ∈ dom 𝐹 ∣ (𝑥 ∈ ((1st𝐹) “ 𝑌) ∧ 𝑥 ∈ ((2nd𝐹) “ 𝑍))} = (((1st𝐹) “ 𝑌) ∩ ((2nd𝐹) “ 𝑍))
7760, 76syl6eq 2830 1 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) → (𝐹 “ (𝑌 × 𝑍)) = (((1st𝐹) “ 𝑌) ∩ ((2nd𝐹) “ 𝑍)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387   = wceq 1507  wcel 2050  {crab 3092  Vcvv 3415  cin 3830  wss 3831  cop 4448   × cxp 5406  ccnv 5407  dom cdm 5408  ran crn 5409  cima 5411  ccom 5412  Fun wfun 6184   Fn wfn 6185  wf 6186  ontowfo 6188  cfv 6190  1st c1st 7501  2nd c2nd 7502
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5061  ax-nul 5068  ax-pow 5120  ax-pr 5187  ax-un 7281
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-sbc 3684  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4181  df-if 4352  df-sn 4443  df-pr 4445  df-op 4449  df-uni 4714  df-br 4931  df-opab 4993  df-mpt 5010  df-id 5313  df-xp 5414  df-rel 5415  df-cnv 5416  df-co 5417  df-dm 5418  df-rn 5419  df-res 5420  df-ima 5421  df-iota 6154  df-fun 6192  df-fn 6193  df-f 6194  df-fo 6196  df-fv 6198  df-1st 7503  df-2nd 7504
This theorem is referenced by:  xppreima2  30160
  Copyright terms: Public domain W3C validator