Metamath Proof Explorer

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 ⊢ S ∈ ⋃ ran ⁡ sigAlgebra ↔ S ∈ V ∧ ∃ o S ⊆ 𝒫 o ∧ o ∈ S ∧ ∀ x ∈ S o ∖ x ∈ S ∧ ∀ x ∈ 𝒫 S x ≼ ω → ⋃ x ∈ S

Proof

Step Hyp Ref Expression
1 df-siga ⊢ sigAlgebra = o ∈ V ⟼ s | s ⊆ 𝒫 o ∧ o ∈ s ∧ ∀ x ∈ s o ∖ x ∈ s ∧ ∀ x ∈ 𝒫 s x ≼ ω → ⋃ x ∈ s
2 sigaex ⊢ s | s ⊆ 𝒫 o ∧ o ∈ s ∧ ∀ x ∈ s o ∖ x ∈ s ∧ ∀ x ∈ 𝒫 s x ≼ ω → ⋃ x ∈ s ∈ V
3 sseq1 ⊢ s = S → s ⊆ 𝒫 o ↔ S ⊆ 𝒫 o
4 eleq2 ⊢ s = S → o ∈ s ↔ o ∈ S
5 eleq2 ⊢ s = S → o ∖ x ∈ s ↔ o ∖ x ∈ S
6 5 raleqbi1dv ⊢ s = S → ∀ x ∈ s o ∖ x ∈ s ↔ ∀ x ∈ S o ∖ x ∈ S
7 pweq ⊢ s = S → 𝒫 s = 𝒫 S
8 eleq2 ⊢ s = S → ⋃ x ∈ s ↔ ⋃ x ∈ S
9 8 imbi2d ⊢ s = S → x ≼ ω → ⋃ x ∈ s ↔ x ≼ ω → ⋃ x ∈ S
10 7 9 raleqbidv ⊢ s = S → ∀ x ∈ 𝒫 s x ≼ ω → ⋃ x ∈ s ↔ ∀ x ∈ 𝒫 S x ≼ ω → ⋃ x ∈ S
11 4 6 10 3anbi123d ⊢ s = S → o ∈ s ∧ ∀ x ∈ s o ∖ x ∈ s ∧ ∀ x ∈ 𝒫 s x ≼ ω → ⋃ x ∈ s ↔ o ∈ S ∧ ∀ x ∈ S o ∖ x ∈ S ∧ ∀ x ∈ 𝒫 S x ≼ ω → ⋃ x ∈ S
12 3 11 anbi12d ⊢ s = S → s ⊆ 𝒫 o ∧ o ∈ s ∧ ∀ x ∈ s o ∖ x ∈ s ∧ ∀ x ∈ 𝒫 s x ≼ ω → ⋃ x ∈ s ↔ S ⊆ 𝒫 o ∧ o ∈ S ∧ ∀ x ∈ S o ∖ x ∈ S ∧ ∀ x ∈ 𝒫 S x ≼ ω → ⋃ x ∈ S
13 1 2 12 abfmpunirn ⊢ S ∈ ⋃ ran ⁡ sigAlgebra ↔ S ∈ V ∧ ∃ o ∈ V S ⊆ 𝒫 o ∧ o ∈ S ∧ ∀ x ∈ S o ∖ x ∈ S ∧ ∀ x ∈ 𝒫 S x ≼ ω → ⋃ x ∈ S
14 rexv ⊢ ∃ o ∈ V S ⊆ 𝒫 o ∧ o ∈ S ∧ ∀ x ∈ S o ∖ x ∈ S ∧ ∀ x ∈ 𝒫 S x ≼ ω → ⋃ x ∈ S ↔ ∃ o S ⊆ 𝒫 o ∧ o ∈ S ∧ ∀ x ∈ S o ∖ x ∈ S ∧ ∀ x ∈ 𝒫 S x ≼ ω → ⋃ x ∈ S
15 14 anbi2i ⊢ S ∈ V ∧ ∃ o ∈ V S ⊆ 𝒫 o ∧ o ∈ S ∧ ∀ x ∈ S o ∖ x ∈ S ∧ ∀ x ∈ 𝒫 S x ≼ ω → ⋃ x ∈ S ↔ S ∈ V ∧ ∃ o S ⊆ 𝒫 o ∧ o ∈ S ∧ ∀ x ∈ S o ∖ x ∈ S ∧ ∀ x ∈ 𝒫 S x ≼ ω → ⋃ x ∈ S
16 13 15 bitri ⊢ S ∈ ⋃ ran ⁡ sigAlgebra ↔ S ∈ V ∧ ∃ o S ⊆ 𝒫 o ∧ o ∈ S ∧ ∀ x ∈ S o ∖ x ∈ S ∧ ∀ x ∈ 𝒫 S x ≼ ω → ⋃ x ∈ S