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

Theorem xppreima2 29751
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 6080 . . 3 Fun 𝐻
3 xppreima2.1 . . . . . . . 8 (𝜑𝐹:𝐴𝐵)
43ffvelrnda 6514 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐹𝑥) ∈ 𝐵)
5 xppreima2.2 . . . . . . . 8 (𝜑𝐺:𝐴𝐶)
65ffvelrnda 6514 . . . . . . 7 ((𝜑𝑥𝐴) → (𝐺𝑥) ∈ 𝐶)
7 opelxp 5295 . . . . . . 7 (⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ (𝐵 × 𝐶) ↔ ((𝐹𝑥) ∈ 𝐵 ∧ (𝐺𝑥) ∈ 𝐶))
84, 6, 7sylanbrc 701 . . . . . 6 ((𝜑𝑥𝐴) → ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ (𝐵 × 𝐶))
98, 1fmptd 6540 . . . . 5 (𝜑𝐻:𝐴⟶(𝐵 × 𝐶))
10 frn 6206 . . . . 5 (𝐻:𝐴⟶(𝐵 × 𝐶) → ran 𝐻 ⊆ (𝐵 × 𝐶))
119, 10syl 17 . . . 4 (𝜑 → ran 𝐻 ⊆ (𝐵 × 𝐶))
12 xpss 5274 . . . 4 (𝐵 × 𝐶) ⊆ (V × V)
1311, 12syl6ss 3748 . . 3 (𝜑 → ran 𝐻 ⊆ (V × V))
14 xppreima 29750 . . 3 ((Fun 𝐻 ∧ ran 𝐻 ⊆ (V × V)) → (𝐻 “ (𝑌 × 𝑍)) = (((1st𝐻) “ 𝑌) ∩ ((2nd𝐻) “ 𝑍)))
152, 13, 14sylancr 698 . 2 (𝜑 → (𝐻 “ (𝑌 × 𝑍)) = (((1st𝐻) “ 𝑌) ∩ ((2nd𝐻) “ 𝑍)))
16 fo1st 7345 . . . . . . . . 9 1st :V–onto→V
17 fofn 6270 . . . . . . . . 9 (1st :V–onto→V → 1st Fn V)
1816, 17ax-mp 5 . . . . . . . 8 1st Fn V
19 opex 5073 . . . . . . . . 9 ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ V
2019, 1fnmpti 6175 . . . . . . . 8 𝐻 Fn 𝐴
21 ssv 3758 . . . . . . . 8 ran 𝐻 ⊆ V
22 fnco 6152 . . . . . . . 8 ((1st Fn V ∧ 𝐻 Fn 𝐴 ∧ ran 𝐻 ⊆ V) → (1st𝐻) Fn 𝐴)
2318, 20, 21, 22mp3an 1565 . . . . . . 7 (1st𝐻) Fn 𝐴
2423a1i 11 . . . . . 6 (𝜑 → (1st𝐻) Fn 𝐴)
25 ffn 6198 . . . . . . 7 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
263, 25syl 17 . . . . . 6 (𝜑𝐹 Fn 𝐴)
272a1i 11 . . . . . . . . . 10 ((𝜑𝑥𝐴) → Fun 𝐻)
2813adantr 472 . . . . . . . . . 10 ((𝜑𝑥𝐴) → ran 𝐻 ⊆ (V × V))
29 simpr 479 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → 𝑥𝐴)
3019, 1dmmpti 6176 . . . . . . . . . . 11 dom 𝐻 = 𝐴
3129, 30syl6eleqr 2842 . . . . . . . . . 10 ((𝜑𝑥𝐴) → 𝑥 ∈ dom 𝐻)
32 opfv 29749 . . . . . . . . . 10 (((Fun 𝐻 ∧ ran 𝐻 ⊆ (V × V)) ∧ 𝑥 ∈ dom 𝐻) → (𝐻𝑥) = ⟨((1st𝐻)‘𝑥), ((2nd𝐻)‘𝑥)⟩)
3327, 28, 31, 32syl21anc 1472 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝐻𝑥) = ⟨((1st𝐻)‘𝑥), ((2nd𝐻)‘𝑥)⟩)
341fvmpt2 6445 . . . . . . . . . 10 ((𝑥𝐴 ∧ ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ (𝐵 × 𝐶)) → (𝐻𝑥) = ⟨(𝐹𝑥), (𝐺𝑥)⟩)
3529, 8, 34syl2anc 696 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝐻𝑥) = ⟨(𝐹𝑥), (𝐺𝑥)⟩)
3633, 35eqtr3d 2788 . . . . . . . 8 ((𝜑𝑥𝐴) → ⟨((1st𝐻)‘𝑥), ((2nd𝐻)‘𝑥)⟩ = ⟨(𝐹𝑥), (𝐺𝑥)⟩)
37 fvex 6354 . . . . . . . . 9 ((1st𝐻)‘𝑥) ∈ V
38 fvex 6354 . . . . . . . . 9 ((2nd𝐻)‘𝑥) ∈ V
3937, 38opth 5085 . . . . . . . 8 (⟨((1st𝐻)‘𝑥), ((2nd𝐻)‘𝑥)⟩ = ⟨(𝐹𝑥), (𝐺𝑥)⟩ ↔ (((1st𝐻)‘𝑥) = (𝐹𝑥) ∧ ((2nd𝐻)‘𝑥) = (𝐺𝑥)))
4036, 39sylib 208 . . . . . . 7 ((𝜑𝑥𝐴) → (((1st𝐻)‘𝑥) = (𝐹𝑥) ∧ ((2nd𝐻)‘𝑥) = (𝐺𝑥)))
4140simpld 477 . . . . . 6 ((𝜑𝑥𝐴) → ((1st𝐻)‘𝑥) = (𝐹𝑥))
4224, 26, 41eqfnfvd 6469 . . . . 5 (𝜑 → (1st𝐻) = 𝐹)
4342cnveqd 5445 . . . 4 (𝜑(1st𝐻) = 𝐹)
4443imaeq1d 5615 . . 3 (𝜑 → ((1st𝐻) “ 𝑌) = (𝐹𝑌))
45 fo2nd 7346 . . . . . . . . 9 2nd :V–onto→V
46 fofn 6270 . . . . . . . . 9 (2nd :V–onto→V → 2nd Fn V)
4745, 46ax-mp 5 . . . . . . . 8 2nd Fn V
48 fnco 6152 . . . . . . . 8 ((2nd Fn V ∧ 𝐻 Fn 𝐴 ∧ ran 𝐻 ⊆ V) → (2nd𝐻) Fn 𝐴)
4947, 20, 21, 48mp3an 1565 . . . . . . 7 (2nd𝐻) Fn 𝐴
5049a1i 11 . . . . . 6 (𝜑 → (2nd𝐻) Fn 𝐴)
51 ffn 6198 . . . . . . 7 (𝐺:𝐴𝐶𝐺 Fn 𝐴)
525, 51syl 17 . . . . . 6 (𝜑𝐺 Fn 𝐴)
5340simprd 482 . . . . . 6 ((𝜑𝑥𝐴) → ((2nd𝐻)‘𝑥) = (𝐺𝑥))
5450, 52, 53eqfnfvd 6469 . . . . 5 (𝜑 → (2nd𝐻) = 𝐺)
5554cnveqd 5445 . . . 4 (𝜑(2nd𝐻) = 𝐺)
5655imaeq1d 5615 . . 3 (𝜑 → ((2nd𝐻) “ 𝑍) = (𝐺𝑍))
5744, 56ineq12d 3950 . 2 (𝜑 → (((1st𝐻) “ 𝑌) ∩ ((2nd𝐻) “ 𝑍)) = ((𝐹𝑌) ∩ (𝐺𝑍)))
5815, 57eqtrd 2786 1 (𝜑 → (𝐻 “ (𝑌 × 𝑍)) = ((𝐹𝑌) ∩ (𝐺𝑍)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1624  wcel 2131  Vcvv 3332  cin 3706  wss 3707  cop 4319  cmpt 4873   × cxp 5256  ccnv 5257  dom cdm 5258  ran crn 5259  cima 5261  ccom 5262  Fun wfun 6035   Fn wfn 6036  wf 6037  ontowfo 6039  cfv 6041  1st c1st 7323  2nd c2nd 7324
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-ral 3047  df-rex 3048  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-br 4797  df-opab 4857  df-mpt 4874  df-id 5166  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-fo 6047  df-fv 6049  df-1st 7325  df-2nd 7326
This theorem is referenced by:  mbfmco2  30628
  Copyright terms: Public domain W3C validator