Theorem issros

Description: The property of being a semirings of sets, i.e., collections of sets containing the empty set, closed under finite intersection, and where complements can be written as finite disjoint unions. (Contributed by Thierry Arnoux, 18-Jul-2020)

	Ref	Expression
Hypothesis	issros.1	⊢ 𝑁 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑠 ∧ ∃ 𝑧 ∈ 𝒫 𝑠 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) ) }
Assertion	issros	⊢ ( 𝑆 ∈ 𝑁 ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∅ ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑆 ∧ ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		issros.1	⊢ 𝑁 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑠 ∧ ∃ 𝑧 ∈ 𝒫 𝑠 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) ) }
2		eleq2	⊢ ( 𝑠 = 𝑆 → ( ∅ ∈ 𝑠 ↔ ∅ ∈ 𝑆 ) )
3		eleq2	⊢ ( 𝑠 = 𝑆 → ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑠 ↔ ( 𝑥 ∩ 𝑦 ) ∈ 𝑆 ) )
4		pweq	⊢ ( 𝑠 = 𝑆 → 𝒫 𝑠 = 𝒫 𝑆 )
5	4	rexeqdv	⊢ ( 𝑠 = 𝑆 → ( ∃ 𝑧 ∈ 𝒫 𝑠 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ↔ ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) )
6	3 5	anbi12d	⊢ ( 𝑠 = 𝑆 → ( ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑠 ∧ ∃ 𝑧 ∈ 𝒫 𝑠 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) ↔ ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑆 ∧ ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) ) )
7	6	raleqbi1dv	⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑠 ∧ ∃ 𝑧 ∈ 𝒫 𝑠 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) ↔ ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑆 ∧ ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) ) )
8	7	raleqbi1dv	⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑠 ∧ ∃ 𝑧 ∈ 𝒫 𝑠 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑆 ∧ ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) ) )
9	2 8	anbi12d	⊢ ( 𝑠 = 𝑆 → ( ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑠 ∧ ∃ 𝑧 ∈ 𝒫 𝑠 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) ) ↔ ( ∅ ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑆 ∧ ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) ) ) )
10	9 1	elrab2	⊢ ( 𝑆 ∈ 𝑁 ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ( ∅ ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑆 ∧ ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) ) ) )
11		3anass	⊢ ( ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∅ ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑆 ∧ ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) ) ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ( ∅ ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑆 ∧ ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) ) ) )
12	10 11	bitr4i	⊢ ( 𝑆 ∈ 𝑁 ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∅ ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑆 ∧ ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) ) )