# 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 ‘ 𝑋 ) )