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 30405
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 6373 . . . . 5 (Fun 𝐹𝐹 Fn dom 𝐹)
2 fncnvima2 6822 . . . . 5 (𝐹 Fn dom 𝐹 → (𝐹 “ (𝑌 × 𝑍)) = {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) ∈ (𝑌 × 𝑍)})
31, 2sylbi 220 . . . 4 (Fun 𝐹 → (𝐹 “ (𝑌 × 𝑍)) = {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) ∈ (𝑌 × 𝑍)})
43adantr 484 . . 3 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) → (𝐹 “ (𝑌 × 𝑍)) = {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) ∈ (𝑌 × 𝑍)})
5 fvco 6750 . . . . . . . . . 10 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ((1st𝐹)‘𝑥) = (1st ‘(𝐹𝑥)))
6 fvco 6750 . . . . . . . . . 10 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ((2nd𝐹)‘𝑥) = (2nd ‘(𝐹𝑥)))
75, 6opeq12d 4797 . . . . . . . . 9 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ⟨((1st𝐹)‘𝑥), ((2nd𝐹)‘𝑥)⟩ = ⟨(1st ‘(𝐹𝑥)), (2nd ‘(𝐹𝑥))⟩)
87eqeq2d 2835 . . . . . . . 8 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ((𝐹𝑥) = ⟨((1st𝐹)‘𝑥), ((2nd𝐹)‘𝑥)⟩ ↔ (𝐹𝑥) = ⟨(1st ‘(𝐹𝑥)), (2nd ‘(𝐹𝑥))⟩))
95eleq1d 2900 . . . . . . . . 9 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (((1st𝐹)‘𝑥) ∈ 𝑌 ↔ (1st ‘(𝐹𝑥)) ∈ 𝑌))
106eleq1d 2900 . . . . . . . . 9 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (((2nd𝐹)‘𝑥) ∈ 𝑍 ↔ (2nd ‘(𝐹𝑥)) ∈ 𝑍))
119, 10anbi12d 633 . . . . . . . 8 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ((((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍) ↔ ((1st ‘(𝐹𝑥)) ∈ 𝑌 ∧ (2nd ‘(𝐹𝑥)) ∈ 𝑍)))
128, 11anbi12d 633 . . . . . . 7 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (((𝐹𝑥) = ⟨((1st𝐹)‘𝑥), ((2nd𝐹)‘𝑥)⟩ ∧ (((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍)) ↔ ((𝐹𝑥) = ⟨(1st ‘(𝐹𝑥)), (2nd ‘(𝐹𝑥))⟩ ∧ ((1st ‘(𝐹𝑥)) ∈ 𝑌 ∧ (2nd ‘(𝐹𝑥)) ∈ 𝑍))))
13 elxp6 7718 . . . . . . 7 ((𝐹𝑥) ∈ (𝑌 × 𝑍) ↔ ((𝐹𝑥) = ⟨(1st ‘(𝐹𝑥)), (2nd ‘(𝐹𝑥))⟩ ∧ ((1st ‘(𝐹𝑥)) ∈ 𝑌 ∧ (2nd ‘(𝐹𝑥)) ∈ 𝑍)))
1412, 13syl6rbbr 293 . . . . . 6 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ((𝐹𝑥) ∈ (𝑌 × 𝑍) ↔ ((𝐹𝑥) = ⟨((1st𝐹)‘𝑥), ((2nd𝐹)‘𝑥)⟩ ∧ (((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍))))
1514adantlr 714 . . . . 5 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐹) → ((𝐹𝑥) ∈ (𝑌 × 𝑍) ↔ ((𝐹𝑥) = ⟨((1st𝐹)‘𝑥), ((2nd𝐹)‘𝑥)⟩ ∧ (((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍))))
16 opfv 30404 . . . . . 6 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐹) → (𝐹𝑥) = ⟨((1st𝐹)‘𝑥), ((2nd𝐹)‘𝑥)⟩)
1716biantrurd 536 . . . . 5 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐹) → ((((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍) ↔ ((𝐹𝑥) = ⟨((1st𝐹)‘𝑥), ((2nd𝐹)‘𝑥)⟩ ∧ (((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍))))
18 fo1st 7704 . . . . . . . . . . 11 1st :V–onto→V
19 fofun 6582 . . . . . . . . . . 11 (1st :V–onto→V → Fun 1st )
2018, 19ax-mp 5 . . . . . . . . . 10 Fun 1st
21 funco 6383 . . . . . . . . . 10 ((Fun 1st ∧ Fun 𝐹) → Fun (1st𝐹))
2220, 21mpan 689 . . . . . . . . 9 (Fun 𝐹 → Fun (1st𝐹))
2322adantr 484 . . . . . . . 8 ((Fun 𝐹𝑥 ∈ dom 𝐹) → Fun (1st𝐹))
24 ssv 3977 . . . . . . . . . . . 12 (𝐹 “ dom 𝐹) ⊆ V
25 fof 6581 . . . . . . . . . . . . 13 (1st :V–onto→V → 1st :V⟶V)
26 fdm 6511 . . . . . . . . . . . . 13 (1st :V⟶V → dom 1st = V)
2718, 25, 26mp2b 10 . . . . . . . . . . . 12 dom 1st = V
2824, 27sseqtrri 3990 . . . . . . . . . . 11 (𝐹 “ dom 𝐹) ⊆ dom 1st
29 ssid 3975 . . . . . . . . . . . 12 dom 𝐹 ⊆ dom 𝐹
30 funimass3 6815 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ dom 𝐹 ⊆ dom 𝐹) → ((𝐹 “ dom 𝐹) ⊆ dom 1st ↔ dom 𝐹 ⊆ (𝐹 “ dom 1st )))
3129, 30mpan2 690 . . . . . . . . . . 11 (Fun 𝐹 → ((𝐹 “ dom 𝐹) ⊆ dom 1st ↔ dom 𝐹 ⊆ (𝐹 “ dom 1st )))
3228, 31mpbii 236 . . . . . . . . . 10 (Fun 𝐹 → dom 𝐹 ⊆ (𝐹 “ dom 1st ))
3332sselda 3953 . . . . . . . . 9 ((Fun 𝐹𝑥 ∈ dom 𝐹) → 𝑥 ∈ (𝐹 “ dom 1st ))
34 dmco 6094 . . . . . . . . 9 dom (1st𝐹) = (𝐹 “ dom 1st )
3533, 34eleqtrrdi 2927 . . . . . . . 8 ((Fun 𝐹𝑥 ∈ dom 𝐹) → 𝑥 ∈ dom (1st𝐹))
36 fvimacnv 6814 . . . . . . . 8 ((Fun (1st𝐹) ∧ 𝑥 ∈ dom (1st𝐹)) → (((1st𝐹)‘𝑥) ∈ 𝑌𝑥 ∈ ((1st𝐹) “ 𝑌)))
3723, 35, 36syl2anc 587 . . . . . . 7 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (((1st𝐹)‘𝑥) ∈ 𝑌𝑥 ∈ ((1st𝐹) “ 𝑌)))
38 fo2nd 7705 . . . . . . . . . . 11 2nd :V–onto→V
39 fofun 6582 . . . . . . . . . . 11 (2nd :V–onto→V → Fun 2nd )
4038, 39ax-mp 5 . . . . . . . . . 10 Fun 2nd
41 funco 6383 . . . . . . . . . 10 ((Fun 2nd ∧ Fun 𝐹) → Fun (2nd𝐹))
4240, 41mpan 689 . . . . . . . . 9 (Fun 𝐹 → Fun (2nd𝐹))
4342adantr 484 . . . . . . . 8 ((Fun 𝐹𝑥 ∈ dom 𝐹) → Fun (2nd𝐹))
44 fof 6581 . . . . . . . . . . . . 13 (2nd :V–onto→V → 2nd :V⟶V)
45 fdm 6511 . . . . . . . . . . . . 13 (2nd :V⟶V → dom 2nd = V)
4638, 44, 45mp2b 10 . . . . . . . . . . . 12 dom 2nd = V
4724, 46sseqtrri 3990 . . . . . . . . . . 11 (𝐹 “ dom 𝐹) ⊆ dom 2nd
48 funimass3 6815 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ dom 𝐹 ⊆ dom 𝐹) → ((𝐹 “ dom 𝐹) ⊆ dom 2nd ↔ dom 𝐹 ⊆ (𝐹 “ dom 2nd )))
4929, 48mpan2 690 . . . . . . . . . . 11 (Fun 𝐹 → ((𝐹 “ dom 𝐹) ⊆ dom 2nd ↔ dom 𝐹 ⊆ (𝐹 “ dom 2nd )))
5047, 49mpbii 236 . . . . . . . . . 10 (Fun 𝐹 → dom 𝐹 ⊆ (𝐹 “ dom 2nd ))
5150sselda 3953 . . . . . . . . 9 ((Fun 𝐹𝑥 ∈ dom 𝐹) → 𝑥 ∈ (𝐹 “ dom 2nd ))
52 dmco 6094 . . . . . . . . 9 dom (2nd𝐹) = (𝐹 “ dom 2nd )
5351, 52eleqtrrdi 2927 . . . . . . . 8 ((Fun 𝐹𝑥 ∈ dom 𝐹) → 𝑥 ∈ dom (2nd𝐹))
54 fvimacnv 6814 . . . . . . . 8 ((Fun (2nd𝐹) ∧ 𝑥 ∈ dom (2nd𝐹)) → (((2nd𝐹)‘𝑥) ∈ 𝑍𝑥 ∈ ((2nd𝐹) “ 𝑍)))
5543, 53, 54syl2anc 587 . . . . . . 7 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (((2nd𝐹)‘𝑥) ∈ 𝑍𝑥 ∈ ((2nd𝐹) “ 𝑍)))
5637, 55anbi12d 633 . . . . . 6 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ((((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍) ↔ (𝑥 ∈ ((1st𝐹) “ 𝑌) ∧ 𝑥 ∈ ((2nd𝐹) “ 𝑍))))
5756adantlr 714 . . . . 5 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐹) → ((((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍) ↔ (𝑥 ∈ ((1st𝐹) “ 𝑌) ∧ 𝑥 ∈ ((2nd𝐹) “ 𝑍))))
5815, 17, 573bitr2d 310 . . . 4 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐹) → ((𝐹𝑥) ∈ (𝑌 × 𝑍) ↔ (𝑥 ∈ ((1st𝐹) “ 𝑌) ∧ 𝑥 ∈ ((2nd𝐹) “ 𝑍))))
5958rabbidva 3463 . . 3 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) → {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) ∈ (𝑌 × 𝑍)} = {𝑥 ∈ dom 𝐹 ∣ (𝑥 ∈ ((1st𝐹) “ 𝑌) ∧ 𝑥 ∈ ((2nd𝐹) “ 𝑍))})
604, 59eqtrd 2859 . 2 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) → (𝐹 “ (𝑌 × 𝑍)) = {𝑥 ∈ dom 𝐹 ∣ (𝑥 ∈ ((1st𝐹) “ 𝑌) ∧ 𝑥 ∈ ((2nd𝐹) “ 𝑍))})
61 dfin5 3927 . . . 4 (dom 𝐹 ∩ ((1st𝐹) “ 𝑌)) = {𝑥 ∈ dom 𝐹𝑥 ∈ ((1st𝐹) “ 𝑌)}
62 dfin5 3927 . . . 4 (dom 𝐹 ∩ ((2nd𝐹) “ 𝑍)) = {𝑥 ∈ dom 𝐹𝑥 ∈ ((2nd𝐹) “ 𝑍)}
6361, 62ineq12i 4172 . . 3 ((dom 𝐹 ∩ ((1st𝐹) “ 𝑌)) ∩ (dom 𝐹 ∩ ((2nd𝐹) “ 𝑍))) = ({𝑥 ∈ dom 𝐹𝑥 ∈ ((1st𝐹) “ 𝑌)} ∩ {𝑥 ∈ dom 𝐹𝑥 ∈ ((2nd𝐹) “ 𝑍)})
64 cnvimass 5936 . . . . . 6 ((1st𝐹) “ 𝑌) ⊆ dom (1st𝐹)
65 dmcoss 5829 . . . . . 6 dom (1st𝐹) ⊆ dom 𝐹
6664, 65sstri 3962 . . . . 5 ((1st𝐹) “ 𝑌) ⊆ dom 𝐹
67 sseqin2 4177 . . . . 5 (((1st𝐹) “ 𝑌) ⊆ dom 𝐹 ↔ (dom 𝐹 ∩ ((1st𝐹) “ 𝑌)) = ((1st𝐹) “ 𝑌))
6866, 67mpbi 233 . . . 4 (dom 𝐹 ∩ ((1st𝐹) “ 𝑌)) = ((1st𝐹) “ 𝑌)
69 cnvimass 5936 . . . . . 6 ((2nd𝐹) “ 𝑍) ⊆ dom (2nd𝐹)
70 dmcoss 5829 . . . . . 6 dom (2nd𝐹) ⊆ dom 𝐹
7169, 70sstri 3962 . . . . 5 ((2nd𝐹) “ 𝑍) ⊆ dom 𝐹
72 sseqin2 4177 . . . . 5 (((2nd𝐹) “ 𝑍) ⊆ dom 𝐹 ↔ (dom 𝐹 ∩ ((2nd𝐹) “ 𝑍)) = ((2nd𝐹) “ 𝑍))
7371, 72mpbi 233 . . . 4 (dom 𝐹 ∩ ((2nd𝐹) “ 𝑍)) = ((2nd𝐹) “ 𝑍)
7468, 73ineq12i 4172 . . 3 ((dom 𝐹 ∩ ((1st𝐹) “ 𝑌)) ∩ (dom 𝐹 ∩ ((2nd𝐹) “ 𝑍))) = (((1st𝐹) “ 𝑌) ∩ ((2nd𝐹) “ 𝑍))
75 inrab 4260 . . 3 ({𝑥 ∈ dom 𝐹𝑥 ∈ ((1st𝐹) “ 𝑌)} ∩ {𝑥 ∈ dom 𝐹𝑥 ∈ ((2nd𝐹) “ 𝑍)}) = {𝑥 ∈ dom 𝐹 ∣ (𝑥 ∈ ((1st𝐹) “ 𝑌) ∧ 𝑥 ∈ ((2nd𝐹) “ 𝑍))}
7663, 74, 753eqtr3ri 2856 . 2 {𝑥 ∈ dom 𝐹 ∣ (𝑥 ∈ ((1st𝐹) “ 𝑌) ∧ 𝑥 ∈ ((2nd𝐹) “ 𝑍))} = (((1st𝐹) “ 𝑌) ∩ ((2nd𝐹) “ 𝑍))
7760, 76syl6eq 2875 1 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) → (𝐹 “ (𝑌 × 𝑍)) = (((1st𝐹) “ 𝑌) ∩ ((2nd𝐹) “ 𝑍)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wcel 2115  {crab 3137  Vcvv 3480  cin 3918  wss 3919  cop 4556   × cxp 5540  ccnv 5541  dom cdm 5542  ran crn 5543  cima 5545  ccom 5546  Fun wfun 6337   Fn wfn 6338  wf 6339  ontowfo 6341  cfv 6343  1st c1st 7682  2nd c2nd 7683
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-sbc 3759  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5447  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-fo 6349  df-fv 6351  df-1st 7684  df-2nd 7685
This theorem is referenced by:  xppreima2  30406
  Copyright terms: Public domain W3C validator