issgon

Description: Property of being a sigma-algebra with a given base set, noting that the base set of a sigma-algebra is actually its union set. (Contributed by Thierry Arnoux, 24-Sep-2016) (Revised by Thierry Arnoux, 23-Oct-2016)

		Ref	Expression
	Assertion	issgon	$⊢ S \in sigAlgebra (O) \leftrightarrow (S \in ⋃ ran sigAlgebra \land O = ⋃ S)$

Proof

Step	Hyp	Ref	Expression
1		fvssunirn	$⊢ sigAlgebra (O) \subseteq ⋃ ran sigAlgebra$
2	1	sseli	$⊢ S \in sigAlgebra (O) \to S \in ⋃ ran sigAlgebra$
3		elex	$⊢ S \in sigAlgebra (O) \to S \in V$
4		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))))$
5		elpwuni	$⊢ O \in S \to (S \subseteq 𝒫 O \leftrightarrow ⋃ S = O)$
6	5	biimpa	$⊢ (O \in S \land S \subseteq 𝒫 O) \to ⋃ S = O$
7		ancom	$⊢ (S \subseteq 𝒫 O \land O \in S) \leftrightarrow (O \in S \land S \subseteq 𝒫 O)$
8		eqcom	$⊢ O = ⋃ S \leftrightarrow ⋃ S = O$
9	6 7 8	3imtr4i	$⊢ (S \subseteq 𝒫 O \land O \in S) \to O = ⋃ S$
10	9	3ad2antr1	$⊢ (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 = ⋃ S$
11	4 10	biimtrdi	$⊢ S \in V \to (S \in sigAlgebra (O) \to O = ⋃ S)$
12	3 11	mpcom	$⊢ S \in sigAlgebra (O) \to O = ⋃ S$
13	2 12	jca	$⊢ S \in sigAlgebra (O) \to (S \in ⋃ ran sigAlgebra \land O = ⋃ S)$
14		elex	$⊢ S \in ⋃ ran sigAlgebra \to S \in V$
15		isrnsiga	$⊢ S \in ⋃ ran sigAlgebra \leftrightarrow (S \in V \land \exists o (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))))$
16	15	simprbi	$⊢ S \in ⋃ ran sigAlgebra \to \exists o (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)))$
17		elpwuni	$⊢ o \in S \to (S \subseteq 𝒫 o \leftrightarrow ⋃ S = o)$
18	17	biimpa	$⊢ (o \in S \land S \subseteq 𝒫 o) \to ⋃ S = o$
19		ancom	$⊢ (S \subseteq 𝒫 o \land o \in S) \leftrightarrow (o \in S \land S \subseteq 𝒫 o)$
20		eqcom	$⊢ o = ⋃ S \leftrightarrow ⋃ S = o$
21	18 19 20	3imtr4i	$⊢ (S \subseteq 𝒫 o \land o \in S) \to o = ⋃ S$
22	21	3ad2antr1	$⊢ (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 = ⋃ S$
23		pweq	$⊢ o = ⋃ S \to 𝒫 o = 𝒫 ⋃ S$
24	23	sseq2d	$⊢ o = ⋃ S \to (S \subseteq 𝒫 o \leftrightarrow S \subseteq 𝒫 ⋃ S)$
25		eleq1	$⊢ o = ⋃ S \to (o \in S \leftrightarrow ⋃ S \in S)$
26		difeq1	$⊢ o = ⋃ S \to o ∖ x = ⋃ S ∖ x$
27	26	eleq1d	$⊢ o = ⋃ S \to (o ∖ x \in S \leftrightarrow ⋃ S ∖ x \in S)$
28	27	ralbidv	$⊢ o = ⋃ S \to (\forall x \in S o ∖ x \in S \leftrightarrow \forall x \in S ⋃ S ∖ x \in S)$
29	25 28	3anbi12d	$⊢ o = ⋃ 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 (⋃ S \in S \land \forall x \in S ⋃ S ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S)))$
30	24 29	anbi12d	$⊢ o = ⋃ 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 𝒫 ⋃ S \land (⋃ S \in S \land \forall x \in S ⋃ S ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S))))$
31	22 30	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 ((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 𝒫 ⋃ S \land (⋃ S \in S \land \forall x \in S ⋃ S ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S))))$
32	31	ibi	$⊢ (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 (S \subseteq 𝒫 ⋃ S \land (⋃ S \in S \land \forall x \in S ⋃ S ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S)))$
33	32	exlimiv	$⊢ \exists o (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 (S \subseteq 𝒫 ⋃ S \land (⋃ S \in S \land \forall x \in S ⋃ S ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S)))$
34	16 33	syl	$⊢ S \in ⋃ ran sigAlgebra \to (S \subseteq 𝒫 ⋃ S \land (⋃ S \in S \land \forall x \in S ⋃ S ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S)))$
35	34	simprd	$⊢ S \in ⋃ ran sigAlgebra \to (⋃ S \in S \land \forall x \in S ⋃ S ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S))$
36	14 35	jca	$⊢ S \in ⋃ ran sigAlgebra \to (S \in V \land (⋃ S \in S \land \forall x \in S ⋃ S ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S)))$
37		eleq1	$⊢ O = ⋃ S \to (O \in S \leftrightarrow ⋃ S \in S)$
38		difeq1	$⊢ O = ⋃ S \to O ∖ x = ⋃ S ∖ x$
39	38	eleq1d	$⊢ O = ⋃ S \to (O ∖ x \in S \leftrightarrow ⋃ S ∖ x \in S)$
40	39	ralbidv	$⊢ O = ⋃ S \to (\forall x \in S O ∖ x \in S \leftrightarrow \forall x \in S ⋃ S ∖ x \in S)$
41	37 40	3anbi12d	$⊢ O = ⋃ 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 (⋃ S \in S \land \forall x \in S ⋃ S ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S)))$
42	41	biimprd	$⊢ O = ⋃ S \to ((⋃ S \in S \land \forall x \in S ⋃ S ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S)) \to (O \in S \land \forall x \in S O ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S)))$
43		pwuni	$⊢ S \subseteq 𝒫 ⋃ S$
44		pweq	$⊢ O = ⋃ S \to 𝒫 O = 𝒫 ⋃ S$
45	43 44	sseqtrrid	$⊢ O = ⋃ S \to S \subseteq 𝒫 O$
46	42 45	jctild	$⊢ O = ⋃ S \to ((⋃ S \in S \land \forall x \in S ⋃ S ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in 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))))$
47	46	anim2d	$⊢ O = ⋃ S \to ((S \in V \land (⋃ S \in S \land \forall x \in S ⋃ S ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S))) \to (S \in V \land (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)))))$
48	4	biimpar	$⊢ (S \in V \land (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 S \in sigAlgebra (O)$
49	36 47 48	syl56	$⊢ O = ⋃ S \to (S \in ⋃ ran sigAlgebra \to S \in sigAlgebra (O))$
50	49	impcom	$⊢ (S \in ⋃ ran sigAlgebra \land O = ⋃ S) \to S \in sigAlgebra (O)$
51	13 50	impbii	$⊢ S \in sigAlgebra (O) \leftrightarrow (S \in ⋃ ran sigAlgebra \land O = ⋃ S)$

Metamath Proof Explorer

Theorem issgon

Proof