This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mrcssd

Description: Moore closure preserves subset ordering. Deduction form of mrcss . (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses mrcssd.1 ⊢ φ → A ∈ Moore ⁡ X
mrcssd.2 ⊢ N = mrCls ⁡ A
mrcssd.3 ⊢ φ → U ⊆ V
mrcssd.4 ⊢ φ → V ⊆ X
Assertion mrcssd ⊢ φ → N ⁡ U ⊆ N ⁡ V

Proof

Step Hyp Ref Expression
1 mrcssd.1 ⊢ φ → A ∈ Moore ⁡ X
2 mrcssd.2 ⊢ N = mrCls ⁡ A
3 mrcssd.3 ⊢ φ → U ⊆ V
4 mrcssd.4 ⊢ φ → V ⊆ X
5 2 mrcss ⊢ A ∈ Moore ⁡ X ∧ U ⊆ V ∧ V ⊆ X → N ⁡ U ⊆ N ⁡ V
6 1 3 4 5 syl3anc ⊢ φ → N ⁡ U ⊆ N ⁡ V