issiga

Description: An alternative definition of the sigma-algebra, for a given base set. (Contributed by Thierry Arnoux, 19-Sep-2016)

		Ref	Expression
	Assertion	issiga	$⊢ S \in V \to (S \in sigAlgebra (O) \leftrightarrow (S \subseteq 𝒫 O \land (O \in S \land \forall x \in S O ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S))))$

Proof

Step	Hyp	Ref	Expression
1		elfvex	$⊢ S \in sigAlgebra (O) \to O \in V$
2		elex	$⊢ S \in sigAlgebra (O) \to S \in V$
3	1 2	jca	$⊢ S \in sigAlgebra (O) \to (O \in V \land S \in V)$
4	3	a1i	$⊢ S \in V \to (S \in sigAlgebra (O) \to (O \in V \land S \in V))$
5		simpr1	$⊢ (S \subseteq 𝒫 O \land (O \in S \land \forall x \in S O ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S))) \to O \in S$
6		elex	$⊢ O \in S \to O \in V$
7	5 6	syl	$⊢ (S \subseteq 𝒫 O \land (O \in S \land \forall x \in S O ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S))) \to O \in V$
8	7	a1i	$⊢ S \in V \to ((S \subseteq 𝒫 O \land (O \in S \land \forall x \in S O ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S))) \to O \in V)$
9	8	anc2ri	$⊢ S \in V \to ((S \subseteq 𝒫 O \land (O \in S \land \forall x \in S O ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S))) \to (O \in V \land S \in V))$
10		df-siga	$⊢ sigAlgebra = (o \in V ⟼ \{s \| (s \subseteq 𝒫 o \land (o \in s \land \forall x \in s o ∖ x \in s \land \forall x \in 𝒫 s (x ≼ ω \to ⋃ x \in s)))\})$
11		sigaex	$⊢ \{s \| (s \subseteq 𝒫 o \land (o \in s \land \forall x \in s o ∖ x \in s \land \forall x \in 𝒫 s (x ≼ ω \to ⋃ x \in s)))\} \in V$
12		pweq	$⊢ o = O \to 𝒫 o = 𝒫 O$
13	12	sseq2d	$⊢ o = O \to (s \subseteq 𝒫 o \leftrightarrow s \subseteq 𝒫 O)$
14		sseq1	$⊢ s = S \to (s \subseteq 𝒫 O \leftrightarrow S \subseteq 𝒫 O)$
15	13 14	sylan9bb	$⊢ (o = O \land s = S) \to (s \subseteq 𝒫 o \leftrightarrow S \subseteq 𝒫 O)$
16		eleq12	$⊢ (o = O \land s = S) \to (o \in s \leftrightarrow O \in S)$
17		simpr	$⊢ (o = O \land s = S) \to s = S$
18		difeq1	$⊢ o = O \to o ∖ x = O ∖ x$
19	18	adantr	$⊢ (o = O \land s = S) \to o ∖ x = O ∖ x$
20	19	eleq1d	$⊢ (o = O \land s = S) \to (o ∖ x \in s \leftrightarrow O ∖ x \in s)$
21		eleq2	$⊢ s = S \to (O ∖ x \in s \leftrightarrow O ∖ x \in S)$
22	21	adantl	$⊢ (o = O \land s = S) \to (O ∖ x \in s \leftrightarrow O ∖ x \in S)$
23	20 22	bitrd	$⊢ (o = O \land s = S) \to (o ∖ x \in s \leftrightarrow O ∖ x \in S)$
24	17 23	raleqbidv	$⊢ (o = O \land s = S) \to (\forall x \in s o ∖ x \in s \leftrightarrow \forall x \in S O ∖ x \in S)$
25		pweq	$⊢ s = S \to 𝒫 s = 𝒫 S$
26		eleq2	$⊢ s = S \to (⋃ x \in s \leftrightarrow ⋃ x \in S)$
27	26	imbi2d	$⊢ s = S \to ((x ≼ ω \to ⋃ x \in s) \leftrightarrow (x ≼ ω \to ⋃ x \in S))$
28	25 27	raleqbidv	$⊢ s = S \to (\forall x \in 𝒫 s (x ≼ ω \to ⋃ x \in s) \leftrightarrow \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S))$
29	28	adantl	$⊢ (o = O \land s = S) \to (\forall x \in 𝒫 s (x ≼ ω \to ⋃ x \in s) \leftrightarrow \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S))$
30	16 24 29	3anbi123d	$⊢ (o = O \land s = S) \to ((o \in s \land \forall x \in s o ∖ x \in s \land \forall x \in 𝒫 s (x ≼ ω \to ⋃ x \in s)) \leftrightarrow (O \in S \land \forall x \in S O ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S)))$
31	15 30	anbi12d	$⊢ (o = O \land s = S) \to ((s \subseteq 𝒫 o \land (o \in s \land \forall x \in s o ∖ x \in s \land \forall x \in 𝒫 s (x ≼ ω \to ⋃ x \in s))) \leftrightarrow (S \subseteq 𝒫 O \land (O \in S \land \forall x \in S O ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S))))$
32	10 11 31	abfmpel	$⊢ (O \in V \land S \in V) \to (S \in sigAlgebra (O) \leftrightarrow (S \subseteq 𝒫 O \land (O \in S \land \forall x \in S O ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S))))$
33	32	a1i	$⊢ S \in V \to ((O \in V \land S \in V) \to (S \in sigAlgebra (O) \leftrightarrow (S \subseteq 𝒫 O \land (O \in S \land \forall x \in S O ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S)))))$
34	4 9 33	pm5.21ndd	$⊢ S \in V \to (S \in sigAlgebra (O) \leftrightarrow (S \subseteq 𝒫 O \land (O \in S \land \forall x \in S O ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S))))$

Metamath Proof Explorer

Theorem issiga

Proof