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

Theorem dprddomcld 19912
Description: If a family of subgroups is a family of subgroups for an internal direct product, then it is indexed by a set. (Contributed by AV, 13-Jul-2019.)
Hypotheses
Ref Expression
dprddomcld.1 (𝜑𝐺dom DProd 𝑆)
dprddomcld.2 (𝜑 → dom 𝑆 = 𝐼)
Assertion
Ref Expression
dprddomcld (𝜑𝐼 ∈ V)

Proof of Theorem dprddomcld
StepHypRef Expression
1 dprddomcld.2 . 2 (𝜑 → dom 𝑆 = 𝐼)
2 dprddomcld.1 . 2 (𝜑𝐺dom DProd 𝑆)
3 df-nel 3045 . . . . 5 (dom 𝑆 ∉ V ↔ ¬ dom 𝑆 ∈ V)
4 dprddomprc 19911 . . . . 5 (dom 𝑆 ∉ V → ¬ 𝐺dom DProd 𝑆)
53, 4sylbir 234 . . . 4 (¬ dom 𝑆 ∈ V → ¬ 𝐺dom DProd 𝑆)
65con4i 114 . . 3 (𝐺dom DProd 𝑆 → dom 𝑆 ∈ V)
7 eleq1 2819 . . 3 (dom 𝑆 = 𝐼 → (dom 𝑆 ∈ V ↔ 𝐼 ∈ V))
86, 7imbitrid 243 . 2 (dom 𝑆 = 𝐼 → (𝐺dom DProd 𝑆𝐼 ∈ V))
91, 2, 8sylc 65 1 (𝜑𝐼 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1539  wcel 2104  wnel 3044  Vcvv 3472   class class class wbr 5147  dom cdm 5675   DProd cdprd 19904
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-nel 3045  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-xp 5681  df-rel 5682  df-cnv 5683  df-dm 5685  df-rn 5686  df-oprab 7415  df-mpo 7416  df-dprd 19906
This theorem is referenced by:  dprdcntz  19919  dprddisj  19920  dprdw  19921  dprdwd  19922  dprdfid  19928  dprdfinv  19930  dprdfadd  19931  dprdfsub  19932  dprdfeq0  19933  dprdf11  19934  dprdlub  19937  dprdres  19939  dprdss  19940  dprdf1o  19943  dmdprdsplitlem  19948  dprddisj2  19950  dmdprdsplit2  19957  dpjfval  19966  dpjidcl  19969
  Copyright terms: Public domain W3C validator