Theorem mrcssidd 16637

Description: A set is contained in its Moore closure. Deduction form of mrcssid 16629. (Contributed by David Moews, 1-May-2017.)

Hypotheses

Ref	Expression
mrcssidd.1	⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))
mrcssidd.2	⊢ 𝑁 = (mrCls‘𝐴)
mrcssidd.3	⊢ (𝜑 → 𝑈 ⊆ 𝑋)

Assertion

Ref	Expression
mrcssidd	⊢ (𝜑 → 𝑈 ⊆ (𝑁‘𝑈))

Proof of Theorem mrcssidd

Step	Hyp	Ref	Expression
1		mrcssidd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))
2		mrcssidd.3	. 2 ⊢ (𝜑 → 𝑈 ⊆ 𝑋)
3		mrcssidd.2	. . 3 ⊢ 𝑁 = (mrCls‘𝐴)
4	3	mrcssid 16629	. 2 ⊢ ((𝐴 ∈ (Moore‘𝑋) ∧ 𝑈 ⊆ 𝑋) → 𝑈 ⊆ (𝑁‘𝑈))
5	1, 2, 4	syl2anc 581	1 ⊢ (𝜑 → 𝑈 ⊆ (𝑁‘𝑈))

Syntax hints:   → wi 4   = wceq 1658   ∈ wcel 2166   ⊆ wss 3797  ‘cfv 6122  Moorecmre 16594  mrClscmrc 16595

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2390  ax-ext 2802  ax-sep 5004  ax-nul 5012  ax-pow 5064  ax-pr 5126  ax-un 7208

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2604  df-eu 2639  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-ne 2999  df-ral 3121  df-rex 3122  df-rab 3125  df-v 3415  df-sbc 3662  df-csb 3757  df-dif 3800  df-un 3802  df-in 3804  df-ss 3811  df-nul 4144  df-if 4306  df-pw 4379  df-sn 4397  df-pr 4399  df-op 4403  df-uni 4658  df-int 4697  df-br 4873  df-opab 4935  df-mpt 4952  df-id 5249  df-xp 5347  df-rel 5348  df-cnv 5349  df-co 5350  df-dm 5351  df-rn 5352  df-res 5353  df-ima 5354  df-iota 6085  df-fun 6124  df-fn 6125  df-f 6126  df-fv 6130  df-mre 16598  df-mrc 16599

This theorem is referenced by:  submrc  16640  mrieqvlemd  16641  mrieqv2d  16651  mreexmrid  16655  mreexexlem2d  16657  mreexexlem3d  16658  mreexfidimd  16662  isacs2  16665  acsmap2d  17531  cycsubg2cl  17982  odf1o1  18337  gsumzsplit  18679  gsumzoppg  18696  gsumpt  18713  dprdfeq0  18774  dprdspan  18779  subgdmdprd  18786  subgdprd  18787  dprd2dlem1  18793  dprd2da  18794  dmdprdsplit2lem  18797  pgpfac1lem1  18826  pgpfac1lem3a  18828  pgpfac1lem3  18829  pgpfac1lem5  18831  pgpfaclem2  18834  proot1mul  38619