MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpoxopn0yelv Structured version   Visualization version   GIF version

Theorem mpoxopn0yelv 8029
Description: If there is an element of the value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, then the second argument is an element of the first component of the first argument. (Contributed by Alexander van der Vekens, 10-Oct-2017.)
Hypothesis
Ref Expression
mpoxopn0yelv.f 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st𝑥) ↦ 𝐶)
Assertion
Ref Expression
mpoxopn0yelv ((𝑉𝑋𝑊𝑌) → (𝑁 ∈ (⟨𝑉, 𝑊𝐹𝐾) → 𝐾𝑉))
Distinct variable groups:   𝑥,𝑦   𝑥,𝐾   𝑥,𝑉   𝑥,𝑊
Allowed substitution hints:   𝐶(𝑥,𝑦)   𝐹(𝑥,𝑦)   𝐾(𝑦)   𝑁(𝑥,𝑦)   𝑉(𝑦)   𝑊(𝑦)   𝑋(𝑥,𝑦)   𝑌(𝑥,𝑦)

Proof of Theorem mpoxopn0yelv
StepHypRef Expression
1 mpoxopn0yelv.f . . . . 5 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st𝑥) ↦ 𝐶)
21dmmpossx 7906 . . . 4 dom 𝐹 𝑥 ∈ V ({𝑥} × (1st𝑥))
3 elfvdm 6806 . . . . 5 (𝑁 ∈ (𝐹‘⟨⟨𝑉, 𝑊⟩, 𝐾⟩) → ⟨⟨𝑉, 𝑊⟩, 𝐾⟩ ∈ dom 𝐹)
4 df-ov 7278 . . . . 5 (⟨𝑉, 𝑊𝐹𝐾) = (𝐹‘⟨⟨𝑉, 𝑊⟩, 𝐾⟩)
53, 4eleq2s 2857 . . . 4 (𝑁 ∈ (⟨𝑉, 𝑊𝐹𝐾) → ⟨⟨𝑉, 𝑊⟩, 𝐾⟩ ∈ dom 𝐹)
62, 5sselid 3919 . . 3 (𝑁 ∈ (⟨𝑉, 𝑊𝐹𝐾) → ⟨⟨𝑉, 𝑊⟩, 𝐾⟩ ∈ 𝑥 ∈ V ({𝑥} × (1st𝑥)))
7 fveq2 6774 . . . . 5 (𝑥 = ⟨𝑉, 𝑊⟩ → (1st𝑥) = (1st ‘⟨𝑉, 𝑊⟩))
87opeliunxp2 5747 . . . 4 (⟨⟨𝑉, 𝑊⟩, 𝐾⟩ ∈ 𝑥 ∈ V ({𝑥} × (1st𝑥)) ↔ (⟨𝑉, 𝑊⟩ ∈ V ∧ 𝐾 ∈ (1st ‘⟨𝑉, 𝑊⟩)))
98simprbi 497 . . 3 (⟨⟨𝑉, 𝑊⟩, 𝐾⟩ ∈ 𝑥 ∈ V ({𝑥} × (1st𝑥)) → 𝐾 ∈ (1st ‘⟨𝑉, 𝑊⟩))
106, 9syl 17 . 2 (𝑁 ∈ (⟨𝑉, 𝑊𝐹𝐾) → 𝐾 ∈ (1st ‘⟨𝑉, 𝑊⟩))
11 op1stg 7843 . . 3 ((𝑉𝑋𝑊𝑌) → (1st ‘⟨𝑉, 𝑊⟩) = 𝑉)
1211eleq2d 2824 . 2 ((𝑉𝑋𝑊𝑌) → (𝐾 ∈ (1st ‘⟨𝑉, 𝑊⟩) ↔ 𝐾𝑉))
1310, 12syl5ib 243 1 ((𝑉𝑋𝑊𝑌) → (𝑁 ∈ (⟨𝑉, 𝑊𝐹𝐾) → 𝐾𝑉))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1539  wcel 2106  Vcvv 3432  {csn 4561  cop 4567   ciun 4924   × cxp 5587  dom cdm 5589  cfv 6433  (class class class)co 7275  cmpo 7277  1st c1st 7829
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280  df-1st 7831  df-2nd 7832
This theorem is referenced by:  mpoxopynvov0g  8030  mpoxopovel  8036
  Copyright terms: Public domain W3C validator