Theorem dprddomcld 19917

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

Step	Hyp	Ref	Expression
1		dprddomcld.2	. 2 ⊢ (𝜑 → dom 𝑆 = 𝐼)
2		dprddomcld.1	. 2 ⊢ (𝜑 → 𝐺dom DProd 𝑆)
3		df-nel 3030	. . . . 5 ⊢ (dom 𝑆 ∉ V ↔ ¬ dom 𝑆 ∈ V)
4		dprddomprc 19916	. . . . 5 ⊢ (dom 𝑆 ∉ V → ¬ 𝐺dom DProd 𝑆)
5	3, 4	sylbir 235	. . . 4 ⊢ (¬ dom 𝑆 ∈ V → ¬ 𝐺dom DProd 𝑆)
6	5	con4i 114	. . 3 ⊢ (𝐺dom DProd 𝑆 → dom 𝑆 ∈ V)
7		eleq1 2816	. . 3 ⊢ (dom 𝑆 = 𝐼 → (dom 𝑆 ∈ V ↔ 𝐼 ∈ V))
8	6, 7	imbitrid 244	. 2 ⊢ (dom 𝑆 = 𝐼 → (𝐺dom DProd 𝑆 → 𝐼 ∈ V))
9	1, 2, 8	sylc 65	1 ⊢ (𝜑 → 𝐼 ∈ V)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ∈ wcel 2109   ∉ wnel 3029  Vcvv 3444   class class class wbr 5102  dom cdm 5631   DProd cdprd 19909

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-xp 5637  df-rel 5638  df-cnv 5639  df-dm 5641  df-rn 5642  df-oprab 7373  df-mpo 7374  df-dprd 19911

This theorem is referenced by:  dprdcntz  19924  dprddisj  19925  dprdw  19926  dprdwd  19927  dprdfid  19933  dprdfinv  19935  dprdfadd  19936  dprdfsub  19937  dprdfeq0  19938  dprdf11  19939  dprdlub  19942  dprdres  19944  dprdss  19945  dprdf1o  19948  dmdprdsplitlem  19953  dprddisj2  19955  dmdprdsplit2  19962  dpjfval  19971  dpjidcl  19974