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

Theorem xppreima2 30515
 Description: The preimage of a Cartesian product is the intersection of the preimages of each component function. (Contributed by Thierry Arnoux, 7-Jun-2017.)
Hypotheses
Ref Expression
xppreima2.1 (𝜑𝐹:𝐴𝐵)
xppreima2.2 (𝜑𝐺:𝐴𝐶)
xppreima2.3 𝐻 = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)
Assertion
Ref Expression
xppreima2 (𝜑 → (𝐻 “ (𝑌 × 𝑍)) = ((𝐹𝑌) ∩ (𝐺𝑍)))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐶   𝑥,𝐹   𝑥,𝐺   𝑥,𝐻   𝜑,𝑥
Allowed substitution hints:   𝑌(𝑥)   𝑍(𝑥)

Proof of Theorem xppreima2
StepHypRef Expression
1 xppreima2.3 . . . 4 𝐻 = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)
21funmpt2 6378 . . 3 Fun 𝐻
3 xppreima2.1 . . . . . . . 8 (𝜑𝐹:𝐴𝐵)
43ffvelrnda 6847 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐹𝑥) ∈ 𝐵)
5 xppreima2.2 . . . . . . . 8 (𝜑𝐺:𝐴𝐶)
65ffvelrnda 6847 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐺𝑥) ∈ 𝐶)
7 opelxp 5563 . . . . . . 7 (⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ (𝐵 × 𝐶) ↔ ((𝐹𝑥) ∈ 𝐵 ∧ (𝐺𝑥) ∈ 𝐶))
84, 6, 7sylanbrc 586 . . . . . 6 ((𝜑𝑥𝐴) → ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ (𝐵 × 𝐶))
98, 1fmptd 6874 . . . . 5 (𝜑𝐻:𝐴⟶(𝐵 × 𝐶))
109frnd 6509 . . . 4 (𝜑 → ran 𝐻 ⊆ (𝐵 × 𝐶))
11 xpss 5543 . . . 4 (𝐵 × 𝐶) ⊆ (V × V)
1210, 11sstrdi 3906 . . 3 (𝜑 → ran 𝐻 ⊆ (V × V))
13 xppreima 30510 . . 3 ((Fun 𝐻 ∧ ran 𝐻 ⊆ (V × V)) → (𝐻 “ (𝑌 × 𝑍)) = (((1st𝐻) “ 𝑌) ∩ ((2nd𝐻) “ 𝑍)))
142, 12, 13sylancr 590 . 2 (𝜑 → (𝐻 “ (𝑌 × 𝑍)) = (((1st𝐻) “ 𝑌) ∩ ((2nd𝐻) “ 𝑍)))
15 fo1st 7718 . . . . . . . . 9 1st :V–onto→V
16 fofn 6582 . . . . . . . . 9 (1st :V–onto→V → 1st Fn V)
1715, 16ax-mp 5 . . . . . . . 8 1st Fn V
18 opex 5327 . . . . . . . . 9 ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ V
1918, 1fnmpti 6478 . . . . . . . 8 𝐻 Fn 𝐴
20 ssv 3918 . . . . . . . 8 ran 𝐻 ⊆ V
21 fnco 6452 . . . . . . . 8 ((1st Fn V ∧ 𝐻 Fn 𝐴 ∧ ran 𝐻 ⊆ V) → (1st𝐻) Fn 𝐴)
2217, 19, 20, 21mp3an 1458 . . . . . . 7 (1st𝐻) Fn 𝐴
2322a1i 11 . . . . . 6 (𝜑 → (1st𝐻) Fn 𝐴)
243ffnd 6503 . . . . . 6 (𝜑𝐹 Fn 𝐴)
252a1i 11 . . . . . . . . . 10 ((𝜑𝑥𝐴) → Fun 𝐻)
2612adantr 484 . . . . . . . . . 10 ((𝜑𝑥𝐴) → ran 𝐻 ⊆ (V × V))
27 simpr 488 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → 𝑥𝐴)
2818, 1dmmpti 6479 . . . . . . . . . . 11 dom 𝐻 = 𝐴
2927, 28eleqtrrdi 2863 . . . . . . . . . 10 ((𝜑𝑥𝐴) → 𝑥 ∈ dom 𝐻)
30 opfv 30509 . . . . . . . . . 10 (((Fun 𝐻 ∧ ran 𝐻 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐻) → (𝐻𝑥) = ⟨((1st𝐻)‘𝑥), ((2nd𝐻)‘𝑥)⟩)
3125, 26, 29, 30syl21anc 836 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝐻𝑥) = ⟨((1st𝐻)‘𝑥), ((2nd𝐻)‘𝑥)⟩)
321fvmpt2 6774 . . . . . . . . . 10 ((𝑥𝐴 ∧ ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ (𝐵 × 𝐶)) → (𝐻𝑥) = ⟨(𝐹𝑥), (𝐺𝑥)⟩)
3327, 8, 32syl2anc 587 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝐻𝑥) = ⟨(𝐹𝑥), (𝐺𝑥)⟩)
3431, 33eqtr3d 2795 . . . . . . . 8 ((𝜑𝑥𝐴) → ⟨((1st𝐻)‘𝑥), ((2nd𝐻)‘𝑥)⟩ = ⟨(𝐹𝑥), (𝐺𝑥)⟩)
35 fvex 6675 . . . . . . . . 9 ((1st𝐻)‘𝑥) ∈ V
36 fvex 6675 . . . . . . . . 9 ((2nd𝐻)‘𝑥) ∈ V
3735, 36opth 5339 . . . . . . . 8 (⟨((1st𝐻)‘𝑥), ((2nd𝐻)‘𝑥)⟩ = ⟨(𝐹𝑥), (𝐺𝑥)⟩ ↔ (((1st𝐻)‘𝑥) = (𝐹𝑥) ∧ ((2nd𝐻)‘𝑥) = (𝐺𝑥)))
3834, 37sylib 221 . . . . . . 7 ((𝜑𝑥𝐴) → (((1st𝐻)‘𝑥) = (𝐹𝑥) ∧ ((2nd𝐻)‘𝑥) = (𝐺𝑥)))
3938simpld 498 . . . . . 6 ((𝜑𝑥𝐴) → ((1st𝐻)‘𝑥) = (𝐹𝑥))
4023, 24, 39eqfnfvd 6800 . . . . 5 (𝜑 → (1st𝐻) = 𝐹)
4140cnveqd 5720 . . . 4 (𝜑(1st𝐻) = 𝐹)
4241imaeq1d 5904 . . 3 (𝜑 → ((1st𝐻) “ 𝑌) = (𝐹𝑌))
43 fo2nd 7719 . . . . . . . . 9 2nd :V–onto→V
44 fofn 6582 . . . . . . . . 9 (2nd :V–onto→V → 2nd Fn V)
4543, 44ax-mp 5 . . . . . . . 8 2nd Fn V
46 fnco 6452 . . . . . . . 8 ((2nd Fn V ∧ 𝐻 Fn 𝐴 ∧ ran 𝐻 ⊆ V) → (2nd𝐻) Fn 𝐴)
4745, 19, 20, 46mp3an 1458 . . . . . . 7 (2nd𝐻) Fn 𝐴
4847a1i 11 . . . . . 6 (𝜑 → (2nd𝐻) Fn 𝐴)
495ffnd 6503 . . . . . 6 (𝜑𝐺 Fn 𝐴)
5038simprd 499 . . . . . 6 ((𝜑𝑥𝐴) → ((2nd𝐻)‘𝑥) = (𝐺𝑥))
5148, 49, 50eqfnfvd 6800 . . . . 5 (𝜑 → (2nd𝐻) = 𝐺)
5251cnveqd 5720 . . . 4 (𝜑(2nd𝐻) = 𝐺)
5352imaeq1d 5904 . . 3 (𝜑 → ((2nd𝐻) “ 𝑍) = (𝐺𝑍))
5442, 53ineq12d 4120 . 2 (𝜑 → (((1st𝐻) “ 𝑌) ∩ ((2nd𝐻) “ 𝑍)) = ((𝐹𝑌) ∩ (𝐺𝑍)))
5514, 54eqtrd 2793 1 (𝜑 → (𝐻 “ (𝑌 × 𝑍)) = ((𝐹𝑌) ∩ (𝐺𝑍)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  Vcvv 3409   ∩ cin 3859   ⊆ wss 3860  ⟨cop 4531   ↦ cmpt 5115   × cxp 5525  ◡ccnv 5526  dom cdm 5527  ran crn 5528   “ cima 5530   ∘ ccom 5531  Fun wfun 6333   Fn wfn 6334  ⟶wf 6335  –onto→wfo 6337  ‘cfv 6339  1st c1st 7696  2nd c2nd 7697 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5172  ax-nul 5179  ax-pr 5301  ax-un 7464 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5036  df-opab 5098  df-mpt 5116  df-id 5433  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-iota 6298  df-fun 6341  df-fn 6342  df-f 6343  df-fo 6345  df-fv 6347  df-1st 7698  df-2nd 7699 This theorem is referenced by:  mbfmco2  31755
 Copyright terms: Public domain W3C validator