Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mrieqvlemd Structured version   Unicode version

Theorem mrieqvlemd 14900
 Description: In a Moore system, if is a member of , and have the same closure if and only if is in the closure of . Used in the proof of mrieqvd 14909 and mrieqv2d 14910. Deduction form. (Contributed by David Moews, 1-May-2017.)
Hypotheses
Ref Expression
mrieqvlemd.1 Moore
mrieqvlemd.2 mrCls
mrieqvlemd.3
mrieqvlemd.4
Assertion
Ref Expression
mrieqvlemd

Proof of Theorem mrieqvlemd
StepHypRef Expression
1 mrieqvlemd.1 . . . . 5 Moore
21adantr 465 . . . 4 Moore
3 mrieqvlemd.2 . . . 4 mrCls
4 undif1 3908 . . . . . 6
5 mrieqvlemd.3 . . . . . . . . . 10
65adantr 465 . . . . . . . . 9
76ssdifssd 3647 . . . . . . . 8
82, 3, 7mrcssidd 14896 . . . . . . 7
9 simpr 461 . . . . . . . 8
109snssd 4178 . . . . . . 7
118, 10unssd 3685 . . . . . 6
124, 11syl5eqssr 3554 . . . . 5
1312unssad 3686 . . . 4
14 difssd 3637 . . . 4
152, 3, 13, 14mressmrcd 14898 . . 3
1615eqcomd 2475 . 2
171, 3, 5mrcssidd 14896 . . . . 5
18 mrieqvlemd.4 . . . . 5
1917, 18sseldd 3510 . . . 4