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 32661
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 6597 . . . . 5 (Fun 𝐹𝐹 Fn dom 𝐹)
2 fncnvima2 7080 . . . . 5 (𝐹 Fn dom 𝐹 → (𝐹 “ (𝑌 × 𝑍)) = {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) ∈ (𝑌 × 𝑍)})
31, 2sylbi 217 . . . 4 (Fun 𝐹 → (𝐹 “ (𝑌 × 𝑍)) = {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) ∈ (𝑌 × 𝑍)})
43adantr 480 . . 3 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) → (𝐹 “ (𝑌 × 𝑍)) = {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) ∈ (𝑌 × 𝑍)})
5 elxp6 8046 . . . . . . 7 ((𝐹𝑥) ∈ (𝑌 × 𝑍) ↔ ((𝐹𝑥) = ⟨(1st ‘(𝐹𝑥)), (2nd ‘(𝐹𝑥))⟩ ∧ ((1st ‘(𝐹𝑥)) ∈ 𝑌 ∧ (2nd ‘(𝐹𝑥)) ∈ 𝑍)))
6 fvco 7006 . . . . . . . . . 10 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ((1st𝐹)‘𝑥) = (1st ‘(𝐹𝑥)))
7 fvco 7006 . . . . . . . . . 10 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ((2nd𝐹)‘𝑥) = (2nd ‘(𝐹𝑥)))
86, 7opeq12d 4885 . . . . . . . . 9 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ⟨((1st𝐹)‘𝑥), ((2nd𝐹)‘𝑥)⟩ = ⟨(1st ‘(𝐹𝑥)), (2nd ‘(𝐹𝑥))⟩)
98eqeq2d 2745 . . . . . . . 8 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ((𝐹𝑥) = ⟨((1st𝐹)‘𝑥), ((2nd𝐹)‘𝑥)⟩ ↔ (𝐹𝑥) = ⟨(1st ‘(𝐹𝑥)), (2nd ‘(𝐹𝑥))⟩))
106eleq1d 2823 . . . . . . . . 9 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (((1st𝐹)‘𝑥) ∈ 𝑌 ↔ (1st ‘(𝐹𝑥)) ∈ 𝑌))
117eleq1d 2823 . . . . . . . . 9 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (((2nd𝐹)‘𝑥) ∈ 𝑍 ↔ (2nd ‘(𝐹𝑥)) ∈ 𝑍))
1210, 11anbi12d 632 . . . . . . . 8 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ((((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍) ↔ ((1st ‘(𝐹𝑥)) ∈ 𝑌 ∧ (2nd ‘(𝐹𝑥)) ∈ 𝑍)))
139, 12anbi12d 632 . . . . . . 7 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (((𝐹𝑥) = ⟨((1st𝐹)‘𝑥), ((2nd𝐹)‘𝑥)⟩ ∧ (((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍)) ↔ ((𝐹𝑥) = ⟨(1st ‘(𝐹𝑥)), (2nd ‘(𝐹𝑥))⟩ ∧ ((1st ‘(𝐹𝑥)) ∈ 𝑌 ∧ (2nd ‘(𝐹𝑥)) ∈ 𝑍))))
145, 13bitr4id 290 . . . . . 6 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ((𝐹𝑥) ∈ (𝑌 × 𝑍) ↔ ((𝐹𝑥) = ⟨((1st𝐹)‘𝑥), ((2nd𝐹)‘𝑥)⟩ ∧ (((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍))))
1514adantlr 715 . . . . 5 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐹) → ((𝐹𝑥) ∈ (𝑌 × 𝑍) ↔ ((𝐹𝑥) = ⟨((1st𝐹)‘𝑥), ((2nd𝐹)‘𝑥)⟩ ∧ (((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍))))
16 opfv 32660 . . . . . 6 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐹) → (𝐹𝑥) = ⟨((1st𝐹)‘𝑥), ((2nd𝐹)‘𝑥)⟩)
1716biantrurd 532 . . . . 5 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐹) → ((((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍) ↔ ((𝐹𝑥) = ⟨((1st𝐹)‘𝑥), ((2nd𝐹)‘𝑥)⟩ ∧ (((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍))))
18 fo1st 8032 . . . . . . . . . . 11 1st :V–onto→V
19 fofun 6821 . . . . . . . . . . 11 (1st :V–onto→V → Fun 1st )
2018, 19ax-mp 5 . . . . . . . . . 10 Fun 1st
21 funco 6607 . . . . . . . . . 10 ((Fun 1st ∧ Fun 𝐹) → Fun (1st𝐹))
2220, 21mpan 690 . . . . . . . . 9 (Fun 𝐹 → Fun (1st𝐹))
2322adantr 480 . . . . . . . 8 ((Fun 𝐹𝑥 ∈ dom 𝐹) → Fun (1st𝐹))
24 ssv 4019 . . . . . . . . . . . 12 (𝐹 “ dom 𝐹) ⊆ V
25 fof 6820 . . . . . . . . . . . . 13 (1st :V–onto→V → 1st :V⟶V)
26 fdm 6745 . . . . . . . . . . . . 13 (1st :V⟶V → dom 1st = V)
2718, 25, 26mp2b 10 . . . . . . . . . . . 12 dom 1st = V
2824, 27sseqtrri 4032 . . . . . . . . . . 11 (𝐹 “ dom 𝐹) ⊆ dom 1st
29 ssid 4017 . . . . . . . . . . . 12 dom 𝐹 ⊆ dom 𝐹
30 funimass3 7073 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ dom 𝐹 ⊆ dom 𝐹) → ((𝐹 “ dom 𝐹) ⊆ dom 1st ↔ dom 𝐹 ⊆ (𝐹 “ dom 1st )))
3129, 30mpan2 691 . . . . . . . . . . 11 (Fun 𝐹 → ((𝐹 “ dom 𝐹) ⊆ dom 1st ↔ dom 𝐹 ⊆ (𝐹 “ dom 1st )))
3228, 31mpbii 233 . . . . . . . . . 10 (Fun 𝐹 → dom 𝐹 ⊆ (𝐹 “ dom 1st ))
3332sselda 3994 . . . . . . . . 9 ((Fun 𝐹𝑥 ∈ dom 𝐹) → 𝑥 ∈ (𝐹 “ dom 1st ))
34 dmco 6275 . . . . . . . . 9 dom (1st𝐹) = (𝐹 “ dom 1st )
3533, 34eleqtrrdi 2849 . . . . . . . 8 ((Fun 𝐹𝑥 ∈ dom 𝐹) → 𝑥 ∈ dom (1st𝐹))
36 fvimacnv 7072 . . . . . . . 8 ((Fun (1st𝐹) ∧ 𝑥 ∈ dom (1st𝐹)) → (((1st𝐹)‘𝑥) ∈ 𝑌𝑥 ∈ ((1st𝐹) “ 𝑌)))
3723, 35, 36syl2anc 584 . . . . . . 7 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (((1st𝐹)‘𝑥) ∈ 𝑌𝑥 ∈ ((1st𝐹) “ 𝑌)))
38 fo2nd 8033 . . . . . . . . . . 11 2nd :V–onto→V
39 fofun 6821 . . . . . . . . . . 11 (2nd :V–onto→V → Fun 2nd )
4038, 39ax-mp 5 . . . . . . . . . 10 Fun 2nd
41 funco 6607 . . . . . . . . . 10 ((Fun 2nd ∧ Fun 𝐹) → Fun (2nd𝐹))
4240, 41mpan 690 . . . . . . . . 9 (Fun 𝐹 → Fun (2nd𝐹))
4342adantr 480 . . . . . . . 8 ((Fun 𝐹𝑥 ∈ dom 𝐹) → Fun (2nd𝐹))
44 fof 6820 . . . . . . . . . . . . 13 (2nd :V–onto→V → 2nd :V⟶V)
45 fdm 6745 . . . . . . . . . . . . 13 (2nd :V⟶V → dom 2nd = V)
4638, 44, 45mp2b 10 . . . . . . . . . . . 12 dom 2nd = V
4724, 46sseqtrri 4032 . . . . . . . . . . 11 (𝐹 “ dom 𝐹) ⊆ dom 2nd
48 funimass3 7073 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ dom 𝐹 ⊆ dom 𝐹) → ((𝐹 “ dom 𝐹) ⊆ dom 2nd ↔ dom 𝐹 ⊆ (𝐹 “ dom 2nd )))
4929, 48mpan2 691 . . . . . . . . . . 11 (Fun 𝐹 → ((𝐹 “ dom 𝐹) ⊆ dom 2nd ↔ dom 𝐹 ⊆ (𝐹 “ dom 2nd )))
5047, 49mpbii 233 . . . . . . . . . 10 (Fun 𝐹 → dom 𝐹 ⊆ (𝐹 “ dom 2nd ))
5150sselda 3994 . . . . . . . . 9 ((Fun 𝐹𝑥 ∈ dom 𝐹) → 𝑥 ∈ (𝐹 “ dom 2nd ))
52 dmco 6275 . . . . . . . . 9 dom (2nd𝐹) = (𝐹 “ dom 2nd )
5351, 52eleqtrrdi 2849 . . . . . . . 8 ((Fun 𝐹𝑥 ∈ dom 𝐹) → 𝑥 ∈ dom (2nd𝐹))
54 fvimacnv 7072 . . . . . . . 8 ((Fun (2nd𝐹) ∧ 𝑥 ∈ dom (2nd𝐹)) → (((2nd𝐹)‘𝑥) ∈ 𝑍𝑥 ∈ ((2nd𝐹) “ 𝑍)))
5543, 53, 54syl2anc 584 . . . . . . 7 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (((2nd𝐹)‘𝑥) ∈ 𝑍𝑥 ∈ ((2nd𝐹) “ 𝑍)))
5637, 55anbi12d 632 . . . . . 6 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ((((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍) ↔ (𝑥 ∈ ((1st𝐹) “ 𝑌) ∧ 𝑥 ∈ ((2nd𝐹) “ 𝑍))))
5756adantlr 715 . . . . 5 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐹) → ((((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍) ↔ (𝑥 ∈ ((1st𝐹) “ 𝑌) ∧ 𝑥 ∈ ((2nd𝐹) “ 𝑍))))
5815, 17, 573bitr2d 307 . . . 4 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐹) → ((𝐹𝑥) ∈ (𝑌 × 𝑍) ↔ (𝑥 ∈ ((1st𝐹) “ 𝑌) ∧ 𝑥 ∈ ((2nd𝐹) “ 𝑍))))
5958rabbidva 3439 . . 3 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) → {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) ∈ (𝑌 × 𝑍)} = {𝑥 ∈ dom 𝐹 ∣ (𝑥 ∈ ((1st𝐹) “ 𝑌) ∧ 𝑥 ∈ ((2nd𝐹) “ 𝑍))})
604, 59eqtrd 2774 . 2 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) → (𝐹 “ (𝑌 × 𝑍)) = {𝑥 ∈ dom 𝐹 ∣ (𝑥 ∈ ((1st𝐹) “ 𝑌) ∧ 𝑥 ∈ ((2nd𝐹) “ 𝑍))})
61 dfin5 3970 . . . 4 (dom 𝐹 ∩ ((1st𝐹) “ 𝑌)) = {𝑥 ∈ dom 𝐹𝑥 ∈ ((1st𝐹) “ 𝑌)}
62 dfin5 3970 . . . 4 (dom 𝐹 ∩ ((2nd𝐹) “ 𝑍)) = {𝑥 ∈ dom 𝐹𝑥 ∈ ((2nd𝐹) “ 𝑍)}
6361, 62ineq12i 4225 . . 3 ((dom 𝐹 ∩ ((1st𝐹) “ 𝑌)) ∩ (dom 𝐹 ∩ ((2nd𝐹) “ 𝑍))) = ({𝑥 ∈ dom 𝐹𝑥 ∈ ((1st𝐹) “ 𝑌)} ∩ {𝑥 ∈ dom 𝐹𝑥 ∈ ((2nd𝐹) “ 𝑍)})
64 cnvimass 6101 . . . . . 6 ((1st𝐹) “ 𝑌) ⊆ dom (1st𝐹)
65 dmcoss 5987 . . . . . 6 dom (1st𝐹) ⊆ dom 𝐹
6664, 65sstri 4004 . . . . 5 ((1st𝐹) “ 𝑌) ⊆ dom 𝐹
67 sseqin2 4230 . . . . 5 (((1st𝐹) “ 𝑌) ⊆ dom 𝐹 ↔ (dom 𝐹 ∩ ((1st𝐹) “ 𝑌)) = ((1st𝐹) “ 𝑌))
6866, 67mpbi 230 . . . 4 (dom 𝐹 ∩ ((1st𝐹) “ 𝑌)) = ((1st𝐹) “ 𝑌)
69 cnvimass 6101 . . . . . 6 ((2nd𝐹) “ 𝑍) ⊆ dom (2nd𝐹)
70 dmcoss 5987 . . . . . 6 dom (2nd𝐹) ⊆ dom 𝐹
7169, 70sstri 4004 . . . . 5 ((2nd𝐹) “ 𝑍) ⊆ dom 𝐹
72 sseqin2 4230 . . . . 5 (((2nd𝐹) “ 𝑍) ⊆ dom 𝐹 ↔ (dom 𝐹 ∩ ((2nd𝐹) “ 𝑍)) = ((2nd𝐹) “ 𝑍))
7371, 72mpbi 230 . . . 4 (dom 𝐹 ∩ ((2nd𝐹) “ 𝑍)) = ((2nd𝐹) “ 𝑍)
7468, 73ineq12i 4225 . . 3 ((dom 𝐹 ∩ ((1st𝐹) “ 𝑌)) ∩ (dom 𝐹 ∩ ((2nd𝐹) “ 𝑍))) = (((1st𝐹) “ 𝑌) ∩ ((2nd𝐹) “ 𝑍))
75 inrab 4321 . . 3 ({𝑥 ∈ dom 𝐹𝑥 ∈ ((1st𝐹) “ 𝑌)} ∩ {𝑥 ∈ dom 𝐹𝑥 ∈ ((2nd𝐹) “ 𝑍)}) = {𝑥 ∈ dom 𝐹 ∣ (𝑥 ∈ ((1st𝐹) “ 𝑌) ∧ 𝑥 ∈ ((2nd𝐹) “ 𝑍))}
7663, 74, 753eqtr3ri 2771 . 2 {𝑥 ∈ dom 𝐹 ∣ (𝑥 ∈ ((1st𝐹) “ 𝑌) ∧ 𝑥 ∈ ((2nd𝐹) “ 𝑍))} = (((1st𝐹) “ 𝑌) ∩ ((2nd𝐹) “ 𝑍))
7760, 76eqtrdi 2790 1 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) → (𝐹 “ (𝑌 × 𝑍)) = (((1st𝐹) “ 𝑌) ∩ ((2nd𝐹) “ 𝑍)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1536  wcel 2105  {crab 3432  Vcvv 3477  cin 3961  wss 3962  cop 4636   × cxp 5686  ccnv 5687  dom cdm 5688  ran crn 5689  cima 5691  ccom 5692  Fun wfun 6556   Fn wfn 6557  wf 6558  ontowfo 6560  cfv 6562  1st c1st 8010  2nd c2nd 8011
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fo 6568  df-fv 6570  df-1st 8012  df-2nd 8013
This theorem is referenced by:  xppreima2  32667
  Copyright terms: Public domain W3C validator