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