ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpoxopn0yelv GIF version

Theorem mpoxopn0yelv 6243
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 6203 . . . 4 dom 𝐹 𝑥 ∈ V ({𝑥} × (1st𝑥))
31mpofun 5980 . . . . . . 7 Fun 𝐹
4 funrel 5235 . . . . . . 7 (Fun 𝐹 → Rel 𝐹)
53, 4ax-mp 5 . . . . . 6 Rel 𝐹
6 relelfvdm 5549 . . . . . 6 ((Rel 𝐹𝑁 ∈ (𝐹‘⟨⟨𝑉, 𝑊⟩, 𝐾⟩)) → ⟨⟨𝑉, 𝑊⟩, 𝐾⟩ ∈ dom 𝐹)
75, 6mpan 424 . . . . 5 (𝑁 ∈ (𝐹‘⟨⟨𝑉, 𝑊⟩, 𝐾⟩) → ⟨⟨𝑉, 𝑊⟩, 𝐾⟩ ∈ dom 𝐹)
8 df-ov 5881 . . . . 5 (⟨𝑉, 𝑊𝐹𝐾) = (𝐹‘⟨⟨𝑉, 𝑊⟩, 𝐾⟩)
97, 8eleq2s 2272 . . . 4 (𝑁 ∈ (⟨𝑉, 𝑊𝐹𝐾) → ⟨⟨𝑉, 𝑊⟩, 𝐾⟩ ∈ dom 𝐹)
102, 9sselid 3155 . . 3 (𝑁 ∈ (⟨𝑉, 𝑊𝐹𝐾) → ⟨⟨𝑉, 𝑊⟩, 𝐾⟩ ∈ 𝑥 ∈ V ({𝑥} × (1st𝑥)))
11 fveq2 5517 . . . . 5 (𝑥 = ⟨𝑉, 𝑊⟩ → (1st𝑥) = (1st ‘⟨𝑉, 𝑊⟩))
1211opeliunxp2 4769 . . . 4 (⟨⟨𝑉, 𝑊⟩, 𝐾⟩ ∈ 𝑥 ∈ V ({𝑥} × (1st𝑥)) ↔ (⟨𝑉, 𝑊⟩ ∈ V ∧ 𝐾 ∈ (1st ‘⟨𝑉, 𝑊⟩)))
1312simprbi 275 . . 3 (⟨⟨𝑉, 𝑊⟩, 𝐾⟩ ∈ 𝑥 ∈ V ({𝑥} × (1st𝑥)) → 𝐾 ∈ (1st ‘⟨𝑉, 𝑊⟩))
1410, 13syl 14 . 2 (𝑁 ∈ (⟨𝑉, 𝑊𝐹𝐾) → 𝐾 ∈ (1st ‘⟨𝑉, 𝑊⟩))
15 op1stg 6154 . . 3 ((𝑉𝑋𝑊𝑌) → (1st ‘⟨𝑉, 𝑊⟩) = 𝑉)
1615eleq2d 2247 . 2 ((𝑉𝑋𝑊𝑌) → (𝐾 ∈ (1st ‘⟨𝑉, 𝑊⟩) ↔ 𝐾𝑉))
1714, 16imbitrid 154 1 ((𝑉𝑋𝑊𝑌) → (𝑁 ∈ (⟨𝑉, 𝑊𝐹𝐾) → 𝐾𝑉))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104   = wceq 1353  wcel 2148  Vcvv 2739  {csn 3594  cop 3597   ciun 3888   × cxp 4626  dom cdm 4628  Rel wrel 4633  Fun wfun 5212  cfv 5218  (class class class)co 5878  cmpo 5880  1st c1st 6142
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4123  ax-pow 4176  ax-pr 4211  ax-un 4435
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-id 4295  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fv 5226  df-ov 5881  df-oprab 5882  df-mpo 5883  df-1st 6144  df-2nd 6145
This theorem is referenced by:  mpoxopovel  6245
  Copyright terms: Public domain W3C validator