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

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 ⊢ φ → C ⊆ 𝒫 X
ismred2.in ⊢ φ ∧ s ⊆ C → X ∩ ⋂ s ∈ C
Assertion ismred2 ⊢ φ → C ∈ Moore ⁡ X

Proof

Step Hyp Ref Expression
1 ismred2.ss ⊢ φ → C ⊆ 𝒫 X
2 ismred2.in ⊢ φ ∧ s ⊆ C → X ∩ ⋂ s ∈ C
3 eqid ⊢ ∅ = ∅
4 rint0 ⊢ ∅ = ∅ → X ∩ ⋂ ∅ = X
5 3 4 ax-mp ⊢ X ∩ ⋂ ∅ = X
6 0ss ⊢ ∅ ⊆ C
7 0ex ⊢ ∅ ∈ V
8 sseq1 ⊢ s = ∅ → s ⊆ C ↔ ∅ ⊆ C
9 8 anbi2d ⊢ s = ∅ → φ ∧ s ⊆ C ↔ φ ∧ ∅ ⊆ C
10 inteq ⊢ s = ∅ → ⋂ s = ⋂ ∅
11 10 ineq2d ⊢ s = ∅ → X ∩ ⋂ s = X ∩ ⋂ ∅
12 11 eleq1d ⊢ s = ∅ → X ∩ ⋂ s ∈ C ↔ X ∩ ⋂ ∅ ∈ C
13 9 12 imbi12d ⊢ s = ∅ → φ ∧ s ⊆ C → X ∩ ⋂ s ∈ C ↔ φ ∧ ∅ ⊆ C → X ∩ ⋂ ∅ ∈ C
14 7 13 2 vtocl ⊢ φ ∧ ∅ ⊆ C → X ∩ ⋂ ∅ ∈ C
15 6 14 mpan2 ⊢ φ → X ∩ ⋂ ∅ ∈ C
16 5 15 eqeltrrid ⊢ φ → X ∈ C
17 simp2 ⊢ φ ∧ s ⊆ C ∧ s ≠ ∅ → s ⊆ C
18 1 3ad2ant1 ⊢ φ ∧ s ⊆ C ∧ s ≠ ∅ → C ⊆ 𝒫 X
19 17 18 sstrd ⊢ φ ∧ s ⊆ C ∧ s ≠ ∅ → s ⊆ 𝒫 X
20 simp3 ⊢ φ ∧ s ⊆ C ∧ s ≠ ∅ → s ≠ ∅
21 rintn0 ⊢ s ⊆ 𝒫 X ∧ s ≠ ∅ → X ∩ ⋂ s = ⋂ s
22 19 20 21 syl2anc ⊢ φ ∧ s ⊆ C ∧ s ≠ ∅ → X ∩ ⋂ s = ⋂ s
23 2 3adant3 ⊢ φ ∧ s ⊆ C ∧ s ≠ ∅ → X ∩ ⋂ s ∈ C
24 22 23 eqeltrrd ⊢ φ ∧ s ⊆ C ∧ s ≠ ∅ → ⋂ s ∈ C
25 1 16 24 ismred ⊢ φ → C ∈ Moore ⁡ X