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 29758
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 6079 . . . . 5 (Fun 𝐹𝐹 Fn dom 𝐹)
2 fncnvima2 6502 . . . . 5 (𝐹 Fn dom 𝐹 → (𝐹 “ (𝑌 × 𝑍)) = {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) ∈ (𝑌 × 𝑍)})
31, 2sylbi 207 . . . 4 (Fun 𝐹 → (𝐹 “ (𝑌 × 𝑍)) = {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) ∈ (𝑌 × 𝑍)})
43adantr 472 . . 3 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) → (𝐹 “ (𝑌 × 𝑍)) = {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) ∈ (𝑌 × 𝑍)})
5 fvco 6436 . . . . . . . . . 10 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ((1st𝐹)‘𝑥) = (1st ‘(𝐹𝑥)))
6 fvco 6436 . . . . . . . . . 10 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ((2nd𝐹)‘𝑥) = (2nd ‘(𝐹𝑥)))
75, 6opeq12d 4561 . . . . . . . . 9 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ⟨((1st𝐹)‘𝑥), ((2nd𝐹)‘𝑥)⟩ = ⟨(1st ‘(𝐹𝑥)), (2nd ‘(𝐹𝑥))⟩)
87eqeq2d 2770 . . . . . . . 8 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ((𝐹𝑥) = ⟨((1st𝐹)‘𝑥), ((2nd𝐹)‘𝑥)⟩ ↔ (𝐹𝑥) = ⟨(1st ‘(𝐹𝑥)), (2nd ‘(𝐹𝑥))⟩))
95eleq1d 2824 . . . . . . . . 9 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (((1st𝐹)‘𝑥) ∈ 𝑌 ↔ (1st ‘(𝐹𝑥)) ∈ 𝑌))
106eleq1d 2824 . . . . . . . . 9 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (((2nd𝐹)‘𝑥) ∈ 𝑍 ↔ (2nd ‘(𝐹𝑥)) ∈ 𝑍))
119, 10anbi12d 749 . . . . . . . 8 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ((((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍) ↔ ((1st ‘(𝐹𝑥)) ∈ 𝑌 ∧ (2nd ‘(𝐹𝑥)) ∈ 𝑍)))
128, 11anbi12d 749 . . . . . . 7 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (((𝐹𝑥) = ⟨((1st𝐹)‘𝑥), ((2nd𝐹)‘𝑥)⟩ ∧ (((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍)) ↔ ((𝐹𝑥) = ⟨(1st ‘(𝐹𝑥)), (2nd ‘(𝐹𝑥))⟩ ∧ ((1st ‘(𝐹𝑥)) ∈ 𝑌 ∧ (2nd ‘(𝐹𝑥)) ∈ 𝑍))))
13 elxp6 7367 . . . . . . 7 ((𝐹𝑥) ∈ (𝑌 × 𝑍) ↔ ((𝐹𝑥) = ⟨(1st ‘(𝐹𝑥)), (2nd ‘(𝐹𝑥))⟩ ∧ ((1st ‘(𝐹𝑥)) ∈ 𝑌 ∧ (2nd ‘(𝐹𝑥)) ∈ 𝑍)))
1412, 13syl6rbbr 279 . . . . . 6 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ((𝐹𝑥) ∈ (𝑌 × 𝑍) ↔ ((𝐹𝑥) = ⟨((1st𝐹)‘𝑥), ((2nd𝐹)‘𝑥)⟩ ∧ (((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍))))
1514adantlr 753 . . . . 5 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐹) → ((𝐹𝑥) ∈ (𝑌 × 𝑍) ↔ ((𝐹𝑥) = ⟨((1st𝐹)‘𝑥), ((2nd𝐹)‘𝑥)⟩ ∧ (((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍))))
16 opfv 29757 . . . . . 6 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐹) → (𝐹𝑥) = ⟨((1st𝐹)‘𝑥), ((2nd𝐹)‘𝑥)⟩)
1716biantrurd 530 . . . . 5 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐹) → ((((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍) ↔ ((𝐹𝑥) = ⟨((1st𝐹)‘𝑥), ((2nd𝐹)‘𝑥)⟩ ∧ (((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍))))
18 fo1st 7353 . . . . . . . . . . 11 1st :V–onto→V
19 fofun 6277 . . . . . . . . . . 11 (1st :V–onto→V → Fun 1st )
2018, 19ax-mp 5 . . . . . . . . . 10 Fun 1st
21 funco 6089 . . . . . . . . . 10 ((Fun 1st ∧ Fun 𝐹) → Fun (1st𝐹))
2220, 21mpan 708 . . . . . . . . 9 (Fun 𝐹 → Fun (1st𝐹))
2322adantr 472 . . . . . . . 8 ((Fun 𝐹𝑥 ∈ dom 𝐹) → Fun (1st𝐹))
24 ssv 3766 . . . . . . . . . . . 12 (𝐹 “ dom 𝐹) ⊆ V
25 fof 6276 . . . . . . . . . . . . 13 (1st :V–onto→V → 1st :V⟶V)
26 fdm 6212 . . . . . . . . . . . . 13 (1st :V⟶V → dom 1st = V)
2718, 25, 26mp2b 10 . . . . . . . . . . . 12 dom 1st = V
2824, 27sseqtr4i 3779 . . . . . . . . . . 11 (𝐹 “ dom 𝐹) ⊆ dom 1st
29 ssid 3765 . . . . . . . . . . . 12 dom 𝐹 ⊆ dom 𝐹
30 funimass3 6496 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ dom 𝐹 ⊆ dom 𝐹) → ((𝐹 “ dom 𝐹) ⊆ dom 1st ↔ dom 𝐹 ⊆ (𝐹 “ dom 1st )))
3129, 30mpan2 709 . . . . . . . . . . 11 (Fun 𝐹 → ((𝐹 “ dom 𝐹) ⊆ dom 1st ↔ dom 𝐹 ⊆ (𝐹 “ dom 1st )))
3228, 31mpbii 223 . . . . . . . . . 10 (Fun 𝐹 → dom 𝐹 ⊆ (𝐹 “ dom 1st ))
3332sselda 3744 . . . . . . . . 9 ((Fun 𝐹𝑥 ∈ dom 𝐹) → 𝑥 ∈ (𝐹 “ dom 1st ))
34 dmco 5804 . . . . . . . . 9 dom (1st𝐹) = (𝐹 “ dom 1st )
3533, 34syl6eleqr 2850 . . . . . . . 8 ((Fun 𝐹𝑥 ∈ dom 𝐹) → 𝑥 ∈ dom (1st𝐹))
36 fvimacnv 6495 . . . . . . . 8 ((Fun (1st𝐹) ∧ 𝑥 ∈ dom (1st𝐹)) → (((1st𝐹)‘𝑥) ∈ 𝑌𝑥 ∈ ((1st𝐹) “ 𝑌)))
3723, 35, 36syl2anc 696 . . . . . . 7 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (((1st𝐹)‘𝑥) ∈ 𝑌𝑥 ∈ ((1st𝐹) “ 𝑌)))
38 fo2nd 7354 . . . . . . . . . . 11 2nd :V–onto→V
39 fofun 6277 . . . . . . . . . . 11 (2nd :V–onto→V → Fun 2nd )
4038, 39ax-mp 5 . . . . . . . . . 10 Fun 2nd
41 funco 6089 . . . . . . . . . 10 ((Fun 2nd ∧ Fun 𝐹) → Fun (2nd𝐹))
4240, 41mpan 708 . . . . . . . . 9 (Fun 𝐹 → Fun (2nd𝐹))
4342adantr 472 . . . . . . . 8 ((Fun 𝐹𝑥 ∈ dom 𝐹) → Fun (2nd𝐹))
44 fof 6276 . . . . . . . . . . . . 13 (2nd :V–onto→V → 2nd :V⟶V)
45 fdm 6212 . . . . . . . . . . . . 13 (2nd :V⟶V → dom 2nd = V)
4638, 44, 45mp2b 10 . . . . . . . . . . . 12 dom 2nd = V
4724, 46sseqtr4i 3779 . . . . . . . . . . 11 (𝐹 “ dom 𝐹) ⊆ dom 2nd
48 funimass3 6496 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ dom 𝐹 ⊆ dom 𝐹) → ((𝐹 “ dom 𝐹) ⊆ dom 2nd ↔ dom 𝐹 ⊆ (𝐹 “ dom 2nd )))
4929, 48mpan2 709 . . . . . . . . . . 11 (Fun 𝐹 → ((𝐹 “ dom 𝐹) ⊆ dom 2nd ↔ dom 𝐹 ⊆ (𝐹 “ dom 2nd )))
5047, 49mpbii 223 . . . . . . . . . 10 (Fun 𝐹 → dom 𝐹 ⊆ (𝐹 “ dom 2nd ))
5150sselda 3744 . . . . . . . . 9 ((Fun 𝐹𝑥 ∈ dom 𝐹) → 𝑥 ∈ (𝐹 “ dom 2nd ))
52 dmco 5804 . . . . . . . . 9 dom (2nd𝐹) = (𝐹 “ dom 2nd )
5351, 52syl6eleqr 2850 . . . . . . . 8 ((Fun 𝐹𝑥 ∈ dom 𝐹) → 𝑥 ∈ dom (2nd𝐹))
54 fvimacnv 6495 . . . . . . . 8 ((Fun (2nd𝐹) ∧ 𝑥 ∈ dom (2nd𝐹)) → (((2nd𝐹)‘𝑥) ∈ 𝑍𝑥 ∈ ((2nd𝐹) “ 𝑍)))
5543, 53, 54syl2anc 696 . . . . . . 7 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (((2nd𝐹)‘𝑥) ∈ 𝑍𝑥 ∈ ((2nd𝐹) “ 𝑍)))
5637, 55anbi12d 749 . . . . . 6 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ((((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍) ↔ (𝑥 ∈ ((1st𝐹) “ 𝑌) ∧ 𝑥 ∈ ((2nd𝐹) “ 𝑍))))
5756adantlr 753 . . . . 5 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐹) → ((((1st𝐹)‘𝑥) ∈ 𝑌 ∧ ((2nd𝐹)‘𝑥) ∈ 𝑍) ↔ (𝑥 ∈ ((1st𝐹) “ 𝑌) ∧ 𝑥 ∈ ((2nd𝐹) “ 𝑍))))
5815, 17, 573bitr2d 296 . . . 4 (((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐹) → ((𝐹𝑥) ∈ (𝑌 × 𝑍) ↔ (𝑥 ∈ ((1st𝐹) “ 𝑌) ∧ 𝑥 ∈ ((2nd𝐹) “ 𝑍))))
5958rabbidva 3328 . . 3 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) → {𝑥 ∈ dom 𝐹 ∣ (𝐹𝑥) ∈ (𝑌 × 𝑍)} = {𝑥 ∈ dom 𝐹 ∣ (𝑥 ∈ ((1st𝐹) “ 𝑌) ∧ 𝑥 ∈ ((2nd𝐹) “ 𝑍))})
604, 59eqtrd 2794 . 2 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) → (𝐹 “ (𝑌 × 𝑍)) = {𝑥 ∈ dom 𝐹 ∣ (𝑥 ∈ ((1st𝐹) “ 𝑌) ∧ 𝑥 ∈ ((2nd𝐹) “ 𝑍))})
61 dfin5 3723 . . . 4 (dom 𝐹 ∩ ((1st𝐹) “ 𝑌)) = {𝑥 ∈ dom 𝐹𝑥 ∈ ((1st𝐹) “ 𝑌)}
62 dfin5 3723 . . . 4 (dom 𝐹 ∩ ((2nd𝐹) “ 𝑍)) = {𝑥 ∈ dom 𝐹𝑥 ∈ ((2nd𝐹) “ 𝑍)}
6361, 62ineq12i 3955 . . 3 ((dom 𝐹 ∩ ((1st𝐹) “ 𝑌)) ∩ (dom 𝐹 ∩ ((2nd𝐹) “ 𝑍))) = ({𝑥 ∈ dom 𝐹𝑥 ∈ ((1st𝐹) “ 𝑌)} ∩ {𝑥 ∈ dom 𝐹𝑥 ∈ ((2nd𝐹) “ 𝑍)})
64 cnvimass 5643 . . . . . 6 ((1st𝐹) “ 𝑌) ⊆ dom (1st𝐹)
65 dmcoss 5540 . . . . . 6 dom (1st𝐹) ⊆ dom 𝐹
6664, 65sstri 3753 . . . . 5 ((1st𝐹) “ 𝑌) ⊆ dom 𝐹
67 sseqin2 3960 . . . . 5 (((1st𝐹) “ 𝑌) ⊆ dom 𝐹 ↔ (dom 𝐹 ∩ ((1st𝐹) “ 𝑌)) = ((1st𝐹) “ 𝑌))
6866, 67mpbi 220 . . . 4 (dom 𝐹 ∩ ((1st𝐹) “ 𝑌)) = ((1st𝐹) “ 𝑌)
69 cnvimass 5643 . . . . . 6 ((2nd𝐹) “ 𝑍) ⊆ dom (2nd𝐹)
70 dmcoss 5540 . . . . . 6 dom (2nd𝐹) ⊆ dom 𝐹
7169, 70sstri 3753 . . . . 5 ((2nd𝐹) “ 𝑍) ⊆ dom 𝐹
72 sseqin2 3960 . . . . 5 (((2nd𝐹) “ 𝑍) ⊆ dom 𝐹 ↔ (dom 𝐹 ∩ ((2nd𝐹) “ 𝑍)) = ((2nd𝐹) “ 𝑍))
7371, 72mpbi 220 . . . 4 (dom 𝐹 ∩ ((2nd𝐹) “ 𝑍)) = ((2nd𝐹) “ 𝑍)
7468, 73ineq12i 3955 . . 3 ((dom 𝐹 ∩ ((1st𝐹) “ 𝑌)) ∩ (dom 𝐹 ∩ ((2nd𝐹) “ 𝑍))) = (((1st𝐹) “ 𝑌) ∩ ((2nd𝐹) “ 𝑍))
75 inrab 4042 . . 3 ({𝑥 ∈ dom 𝐹𝑥 ∈ ((1st𝐹) “ 𝑌)} ∩ {𝑥 ∈ dom 𝐹𝑥 ∈ ((2nd𝐹) “ 𝑍)}) = {𝑥 ∈ dom 𝐹 ∣ (𝑥 ∈ ((1st𝐹) “ 𝑌) ∧ 𝑥 ∈ ((2nd𝐹) “ 𝑍))}
7663, 74, 753eqtr3ri 2791 . 2 {𝑥 ∈ dom 𝐹 ∣ (𝑥 ∈ ((1st𝐹) “ 𝑌) ∧ 𝑥 ∈ ((2nd𝐹) “ 𝑍))} = (((1st𝐹) “ 𝑌) ∩ ((2nd𝐹) “ 𝑍))
7760, 76syl6eq 2810 1 ((Fun 𝐹 ∧ ran 𝐹 ⊆ (V × V)) → (𝐹 “ (𝑌 × 𝑍)) = (((1st𝐹) “ 𝑌) ∩ ((2nd𝐹) “ 𝑍)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1632  wcel 2139  {crab 3054  Vcvv 3340  cin 3714  wss 3715  cop 4327   × cxp 5264  ccnv 5265  dom cdm 5266  ran crn 5267  cima 5269  ccom 5270  Fun wfun 6043   Fn wfn 6044  wf 6045  ontowfo 6047  cfv 6049  1st c1st 7331  2nd c2nd 7332
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-fo 6055  df-fv 6057  df-1st 7333  df-2nd 7334
This theorem is referenced by:  xppreima2  29759
  Copyright terms: Public domain W3C validator