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 ⊢ ( 𝜑 → 𝐶 ⊆ 𝒫 𝑋 )
ismred2.in ⊢ ( ( 𝜑 ∧ 𝑠 ⊆ 𝐶 ) → ( 𝑋 ∩ ∩ 𝑠 ) ∈ 𝐶 )
Assertion ismred2 ( 𝜑 → 𝐶 ∈ ( Moore ‘ 𝑋 ) )

Proof

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