Theorem isrnsiga

Description: The property of being a sigma-algebra on an indefinite base set. (Contributed by Thierry Arnoux, 3-Sep-2016) (Proof shortened by Thierry Arnoux, 23-Oct-2016)

	Ref	Expression
Assertion	isrnsiga	⊢ ( 𝑆 ∈ ∪ ran sigAlgebra ↔ ( 𝑆 ∈ V ∧ ∃ 𝑜 ( 𝑆 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-siga	⊢ sigAlgebra = ( 𝑜 ∈ V ↦ { 𝑠 ∣ ( 𝑠 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) } )
2		sigaex	⊢ { 𝑠 ∣ ( 𝑠 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) } ∈ V
3		sseq1	⊢ ( 𝑠 = 𝑆 → ( 𝑠 ⊆ 𝒫 𝑜 ↔ 𝑆 ⊆ 𝒫 𝑜 ) )
4		eleq2	⊢ ( 𝑠 = 𝑆 → ( 𝑜 ∈ 𝑠 ↔ 𝑜 ∈ 𝑆 ) )
5		eleq2	⊢ ( 𝑠 = 𝑆 → ( ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ↔ ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ) )
6	5	raleqbi1dv	⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ↔ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ) )
7		pweq	⊢ ( 𝑠 = 𝑆 → 𝒫 𝑠 = 𝒫 𝑆 )
8		eleq2	⊢ ( 𝑠 = 𝑆 → ( ∪ 𝑥 ∈ 𝑠 ↔ ∪ 𝑥 ∈ 𝑆 ) )
9	8	imbi2d	⊢ ( 𝑠 = 𝑆 → ( ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ↔ ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) )
10	7 9	raleqbidv	⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ↔ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) )
11	4 6 10	3anbi123d	⊢ ( 𝑠 = 𝑆 → ( ( 𝑜 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ↔ ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) )
12	3 11	anbi12d	⊢ ( 𝑠 = 𝑆 → ( ( 𝑠 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) ↔ ( 𝑆 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) ) )
13	1 2 12	abfmpunirn	⊢ ( 𝑆 ∈ ∪ ran sigAlgebra ↔ ( 𝑆 ∈ V ∧ ∃ 𝑜 ∈ V ( 𝑆 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) ) )
14		rexv	⊢ ( ∃ 𝑜 ∈ V ( 𝑆 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) ↔ ∃ 𝑜 ( 𝑆 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) )
15	14	anbi2i	⊢ ( ( 𝑆 ∈ V ∧ ∃ 𝑜 ∈ V ( 𝑆 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) ) ↔ ( 𝑆 ∈ V ∧ ∃ 𝑜 ( 𝑆 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) ) )
16	13 15	bitri	⊢ ( 𝑆 ∈ ∪ ran sigAlgebra ↔ ( 𝑆 ∈ V ∧ ∃ 𝑜 ( 𝑆 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) ) )