# Metamath Proof Explorer

## Theorem ismred2

Description: Properties that determine a Moore collection, using restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015)

Ref Expression
Hypotheses ismred2.ss ${⊢}{\phi }\to {C}\subseteq 𝒫{X}$
ismred2.in ${⊢}\left({\phi }\wedge {s}\subseteq {C}\right)\to {X}\cap \bigcap {s}\in {C}$
Assertion ismred2 ${⊢}{\phi }\to {C}\in \mathrm{Moore}\left({X}\right)$

### Proof

Step Hyp Ref Expression
1 ismred2.ss ${⊢}{\phi }\to {C}\subseteq 𝒫{X}$
2 ismred2.in ${⊢}\left({\phi }\wedge {s}\subseteq {C}\right)\to {X}\cap \bigcap {s}\in {C}$
3 eqid ${⊢}\varnothing =\varnothing$
4 rint0 ${⊢}\varnothing =\varnothing \to {X}\cap \bigcap \varnothing ={X}$
5 3 4 ax-mp ${⊢}{X}\cap \bigcap \varnothing ={X}$
6 0ss ${⊢}\varnothing \subseteq {C}$
7 0ex ${⊢}\varnothing \in \mathrm{V}$
8 sseq1 ${⊢}{s}=\varnothing \to \left({s}\subseteq {C}↔\varnothing \subseteq {C}\right)$
9 8 anbi2d ${⊢}{s}=\varnothing \to \left(\left({\phi }\wedge {s}\subseteq {C}\right)↔\left({\phi }\wedge \varnothing \subseteq {C}\right)\right)$
10 inteq ${⊢}{s}=\varnothing \to \bigcap {s}=\bigcap \varnothing$
11 10 ineq2d ${⊢}{s}=\varnothing \to {X}\cap \bigcap {s}={X}\cap \bigcap \varnothing$
12 11 eleq1d ${⊢}{s}=\varnothing \to \left({X}\cap \bigcap {s}\in {C}↔{X}\cap \bigcap \varnothing \in {C}\right)$
13 9 12 imbi12d ${⊢}{s}=\varnothing \to \left(\left(\left({\phi }\wedge {s}\subseteq {C}\right)\to {X}\cap \bigcap {s}\in {C}\right)↔\left(\left({\phi }\wedge \varnothing \subseteq {C}\right)\to {X}\cap \bigcap \varnothing \in {C}\right)\right)$
14 7 13 2 vtocl ${⊢}\left({\phi }\wedge \varnothing \subseteq {C}\right)\to {X}\cap \bigcap \varnothing \in {C}$
15 6 14 mpan2 ${⊢}{\phi }\to {X}\cap \bigcap \varnothing \in {C}$
16 5 15 eqeltrrid ${⊢}{\phi }\to {X}\in {C}$
17 simp2 ${⊢}\left({\phi }\wedge {s}\subseteq {C}\wedge {s}\ne \varnothing \right)\to {s}\subseteq {C}$
18 1 3ad2ant1 ${⊢}\left({\phi }\wedge {s}\subseteq {C}\wedge {s}\ne \varnothing \right)\to {C}\subseteq 𝒫{X}$
19 17 18 sstrd ${⊢}\left({\phi }\wedge {s}\subseteq {C}\wedge {s}\ne \varnothing \right)\to {s}\subseteq 𝒫{X}$
20 simp3 ${⊢}\left({\phi }\wedge {s}\subseteq {C}\wedge {s}\ne \varnothing \right)\to {s}\ne \varnothing$
21 rintn0 ${⊢}\left({s}\subseteq 𝒫{X}\wedge {s}\ne \varnothing \right)\to {X}\cap \bigcap {s}=\bigcap {s}$
22 19 20 21 syl2anc ${⊢}\left({\phi }\wedge {s}\subseteq {C}\wedge {s}\ne \varnothing \right)\to {X}\cap \bigcap {s}=\bigcap {s}$
23 2 3adant3 ${⊢}\left({\phi }\wedge {s}\subseteq {C}\wedge {s}\ne \varnothing \right)\to {X}\cap \bigcap {s}\in {C}$
24 22 23 eqeltrrd ${⊢}\left({\phi }\wedge {s}\subseteq {C}\wedge {s}\ne \varnothing \right)\to \bigcap {s}\in {C}$
25 1 16 24 ismred ${⊢}{\phi }\to {C}\in \mathrm{Moore}\left({X}\right)$