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

Theorem mptelixpg 8149
Description: Condition for an explicit member of an indexed product. (Contributed by Stefan O'Rear, 4-Jan-2015.)
Assertion
Ref Expression
mptelixpg (𝐼𝑉 → ((𝑥𝐼𝐽) ∈ X𝑥𝐼 𝐾 ↔ ∀𝑥𝐼 𝐽𝐾))
Distinct variable group:   𝑥,𝐼
Allowed substitution hints:   𝐽(𝑥)   𝐾(𝑥)   𝑉(𝑥)

Proof of Theorem mptelixpg
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 elex 3364 . 2 (𝐼𝑉𝐼 ∈ V)
2 nfcv 2906 . . . . . 6 𝑦𝐾
3 nfcsb1v 3706 . . . . . 6 𝑥𝑦 / 𝑥𝐾
4 csbeq1a 3699 . . . . . 6 (𝑥 = 𝑦𝐾 = 𝑦 / 𝑥𝐾)
52, 3, 4cbvixp 8129 . . . . 5 X𝑥𝐼 𝐾 = X𝑦𝐼 𝑦 / 𝑥𝐾
65eleq2i 2835 . . . 4 ((𝑥𝐼𝐽) ∈ X𝑥𝐼 𝐾 ↔ (𝑥𝐼𝐽) ∈ X𝑦𝐼 𝑦 / 𝑥𝐾)
7 elixp2 8116 . . . 4 ((𝑥𝐼𝐽) ∈ X𝑦𝐼 𝑦 / 𝑥𝐾 ↔ ((𝑥𝐼𝐽) ∈ V ∧ (𝑥𝐼𝐽) Fn 𝐼 ∧ ∀𝑦𝐼 ((𝑥𝐼𝐽)‘𝑦) ∈ 𝑦 / 𝑥𝐾))
8 3anass 1116 . . . 4 (((𝑥𝐼𝐽) ∈ V ∧ (𝑥𝐼𝐽) Fn 𝐼 ∧ ∀𝑦𝐼 ((𝑥𝐼𝐽)‘𝑦) ∈ 𝑦 / 𝑥𝐾) ↔ ((𝑥𝐼𝐽) ∈ V ∧ ((𝑥𝐼𝐽) Fn 𝐼 ∧ ∀𝑦𝐼 ((𝑥𝐼𝐽)‘𝑦) ∈ 𝑦 / 𝑥𝐾)))
96, 7, 83bitri 288 . . 3 ((𝑥𝐼𝐽) ∈ X𝑥𝐼 𝐾 ↔ ((𝑥𝐼𝐽) ∈ V ∧ ((𝑥𝐼𝐽) Fn 𝐼 ∧ ∀𝑦𝐼 ((𝑥𝐼𝐽)‘𝑦) ∈ 𝑦 / 𝑥𝐾)))
10 eqid 2764 . . . . . . . 8 (𝑥𝐼𝐽) = (𝑥𝐼𝐽)
1110fnmpt 6197 . . . . . . 7 (∀𝑥𝐼 𝐽𝐾 → (𝑥𝐼𝐽) Fn 𝐼)
1210fvmpt2 6479 . . . . . . . . 9 ((𝑥𝐼𝐽𝐾) → ((𝑥𝐼𝐽)‘𝑥) = 𝐽)
13 simpr 477 . . . . . . . . 9 ((𝑥𝐼𝐽𝐾) → 𝐽𝐾)
1412, 13eqeltrd 2843 . . . . . . . 8 ((𝑥𝐼𝐽𝐾) → ((𝑥𝐼𝐽)‘𝑥) ∈ 𝐾)
1514ralimiaa 3097 . . . . . . 7 (∀𝑥𝐼 𝐽𝐾 → ∀𝑥𝐼 ((𝑥𝐼𝐽)‘𝑥) ∈ 𝐾)
1611, 15jca 507 . . . . . 6 (∀𝑥𝐼 𝐽𝐾 → ((𝑥𝐼𝐽) Fn 𝐼 ∧ ∀𝑥𝐼 ((𝑥𝐼𝐽)‘𝑥) ∈ 𝐾))
17 dffn2 6224 . . . . . . . 8 ((𝑥𝐼𝐽) Fn 𝐼 ↔ (𝑥𝐼𝐽):𝐼⟶V)
1810fmpt 6569 . . . . . . . . 9 (∀𝑥𝐼 𝐽 ∈ V ↔ (𝑥𝐼𝐽):𝐼⟶V)
1910fvmpt2 6479 . . . . . . . . . . . . 13 ((𝑥𝐼𝐽 ∈ V) → ((𝑥𝐼𝐽)‘𝑥) = 𝐽)
2019eleq1d 2828 . . . . . . . . . . . 12 ((𝑥𝐼𝐽 ∈ V) → (((𝑥𝐼𝐽)‘𝑥) ∈ 𝐾𝐽𝐾))
2120biimpd 220 . . . . . . . . . . 11 ((𝑥𝐼𝐽 ∈ V) → (((𝑥𝐼𝐽)‘𝑥) ∈ 𝐾𝐽𝐾))
2221ralimiaa 3097 . . . . . . . . . 10 (∀𝑥𝐼 𝐽 ∈ V → ∀𝑥𝐼 (((𝑥𝐼𝐽)‘𝑥) ∈ 𝐾𝐽𝐾))
23 ralim 3094 . . . . . . . . . 10 (∀𝑥𝐼 (((𝑥𝐼𝐽)‘𝑥) ∈ 𝐾𝐽𝐾) → (∀𝑥𝐼 ((𝑥𝐼𝐽)‘𝑥) ∈ 𝐾 → ∀𝑥𝐼 𝐽𝐾))
2422, 23syl 17 . . . . . . . . 9 (∀𝑥𝐼 𝐽 ∈ V → (∀𝑥𝐼 ((𝑥𝐼𝐽)‘𝑥) ∈ 𝐾 → ∀𝑥𝐼 𝐽𝐾))
2518, 24sylbir 226 . . . . . . . 8 ((𝑥𝐼𝐽):𝐼⟶V → (∀𝑥𝐼 ((𝑥𝐼𝐽)‘𝑥) ∈ 𝐾 → ∀𝑥𝐼 𝐽𝐾))
2617, 25sylbi 208 . . . . . . 7 ((𝑥𝐼𝐽) Fn 𝐼 → (∀𝑥𝐼 ((𝑥𝐼𝐽)‘𝑥) ∈ 𝐾 → ∀𝑥𝐼 𝐽𝐾))
2726imp 395 . . . . . 6 (((𝑥𝐼𝐽) Fn 𝐼 ∧ ∀𝑥𝐼 ((𝑥𝐼𝐽)‘𝑥) ∈ 𝐾) → ∀𝑥𝐼 𝐽𝐾)
2816, 27impbii 200 . . . . 5 (∀𝑥𝐼 𝐽𝐾 ↔ ((𝑥𝐼𝐽) Fn 𝐼 ∧ ∀𝑥𝐼 ((𝑥𝐼𝐽)‘𝑥) ∈ 𝐾))
29 nfv 2009 . . . . . . 7 𝑦((𝑥𝐼𝐽)‘𝑥) ∈ 𝐾
30 nffvmpt1 6385 . . . . . . . 8 𝑥((𝑥𝐼𝐽)‘𝑦)
3130, 3nfel 2919 . . . . . . 7 𝑥((𝑥𝐼𝐽)‘𝑦) ∈ 𝑦 / 𝑥𝐾
32 fveq2 6374 . . . . . . . 8 (𝑥 = 𝑦 → ((𝑥𝐼𝐽)‘𝑥) = ((𝑥𝐼𝐽)‘𝑦))
3332, 4eleq12d 2837 . . . . . . 7 (𝑥 = 𝑦 → (((𝑥𝐼𝐽)‘𝑥) ∈ 𝐾 ↔ ((𝑥𝐼𝐽)‘𝑦) ∈ 𝑦 / 𝑥𝐾))
3429, 31, 33cbvral 3314 . . . . . 6 (∀𝑥𝐼 ((𝑥𝐼𝐽)‘𝑥) ∈ 𝐾 ↔ ∀𝑦𝐼 ((𝑥𝐼𝐽)‘𝑦) ∈ 𝑦 / 𝑥𝐾)
3534anbi2i 616 . . . . 5 (((𝑥𝐼𝐽) Fn 𝐼 ∧ ∀𝑥𝐼 ((𝑥𝐼𝐽)‘𝑥) ∈ 𝐾) ↔ ((𝑥𝐼𝐽) Fn 𝐼 ∧ ∀𝑦𝐼 ((𝑥𝐼𝐽)‘𝑦) ∈ 𝑦 / 𝑥𝐾))
3628, 35bitri 266 . . . 4 (∀𝑥𝐼 𝐽𝐾 ↔ ((𝑥𝐼𝐽) Fn 𝐼 ∧ ∀𝑦𝐼 ((𝑥𝐼𝐽)‘𝑦) ∈ 𝑦 / 𝑥𝐾))
37 mptexg 6676 . . . . 5 (𝐼 ∈ V → (𝑥𝐼𝐽) ∈ V)
3837biantrurd 528 . . . 4 (𝐼 ∈ V → (((𝑥𝐼𝐽) Fn 𝐼 ∧ ∀𝑦𝐼 ((𝑥𝐼𝐽)‘𝑦) ∈ 𝑦 / 𝑥𝐾) ↔ ((𝑥𝐼𝐽) ∈ V ∧ ((𝑥𝐼𝐽) Fn 𝐼 ∧ ∀𝑦𝐼 ((𝑥𝐼𝐽)‘𝑦) ∈ 𝑦 / 𝑥𝐾))))
3936, 38syl5rbb 275 . . 3 (𝐼 ∈ V → (((𝑥𝐼𝐽) ∈ V ∧ ((𝑥𝐼𝐽) Fn 𝐼 ∧ ∀𝑦𝐼 ((𝑥𝐼𝐽)‘𝑦) ∈ 𝑦 / 𝑥𝐾)) ↔ ∀𝑥𝐼 𝐽𝐾))
409, 39syl5bb 274 . 2 (𝐼 ∈ V → ((𝑥𝐼𝐽) ∈ X𝑥𝐼 𝐾 ↔ ∀𝑥𝐼 𝐽𝐾))
411, 40syl 17 1 (𝐼𝑉 → ((𝑥𝐼𝐽) ∈ X𝑥𝐼 𝐾 ↔ ∀𝑥𝐼 𝐽𝐾))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107  wcel 2155  wral 3054  Vcvv 3349  csb 3690  cmpt 4887   Fn wfn 6062  wf 6063  cfv 6067  Xcixp 8112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-ral 3059  df-rex 3060  df-reu 3061  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-nul 4079  df-if 4243  df-sn 4334  df-pr 4336  df-op 4340  df-uni 4594  df-iun 4677  df-br 4809  df-opab 4871  df-mpt 4888  df-id 5184  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-ixp 8113
This theorem is referenced by:  resixpfo  8150  ixpiunwdom  8702  dfac9  9210  prdsbasmpt  16397  prdsbasmpt2  16409  idfucl  16807  fuccocl  16890  fucidcl  16891  invfuc  16900  curf2cl  17138  yonedalem4c  17184  dprdwd  18676  ptpjopn  21694  dfac14lem  21699  ptcnplem  21703  ptcnp  21704  ptcn  21709  ptcmplem2  22135  tmdgsum2  22178  upixp  33879  kelac1  38242
  Copyright terms: Public domain W3C validator