Theorem rossspw

Description: A ring of sets is a collection of subsets of O . (Contributed by Thierry Arnoux, 18-Jul-2020)

	Ref	Expression
Hypothesis	isros.1	⊢ 𝑄 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑠 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑠 ) ) }
Assertion	rossspw	⊢ ( 𝑆 ∈ 𝑄 → 𝑆 ⊆ 𝒫 𝑂 )

Proof

Step	Hyp	Ref	Expression
1		isros.1	⊢ 𝑄 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑠 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑠 ) ) }
2	1	isros	⊢ ( 𝑆 ∈ 𝑄 ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∅ ∈ 𝑆 ∧ ∀ 𝑢 ∈ 𝑆 ∀ 𝑣 ∈ 𝑆 ( ( 𝑢 ∪ 𝑣 ) ∈ 𝑆 ∧ ( 𝑢 ∖ 𝑣 ) ∈ 𝑆 ) ) )
3	2	simp1bi	⊢ ( 𝑆 ∈ 𝑄 → 𝑆 ∈ 𝒫 𝒫 𝑂 )
4	3	elpwid	⊢ ( 𝑆 ∈ 𝑄 → 𝑆 ⊆ 𝒫 𝑂 )