sigainb

Description: Building a sigma-algebra from intersections with a given set. (Contributed by Thierry Arnoux, 26-Dec-2016)

		Ref	Expression
	Assertion	sigainb	$⊢ (S \in ⋃ ran sigAlgebra \land A \in S) \to S \cap 𝒫 A \in sigAlgebra (A)$

Proof

Step	Hyp	Ref	Expression
1		inex1g	$⊢ S \in ⋃ ran sigAlgebra \to S \cap 𝒫 A \in V$
2	1	adantr	$⊢ (S \in ⋃ ran sigAlgebra \land A \in S) \to S \cap 𝒫 A \in V$
3		inss2	$⊢ S \cap 𝒫 A \subseteq 𝒫 A$
4	3	a1i	$⊢ (S \in ⋃ ran sigAlgebra \land A \in S) \to S \cap 𝒫 A \subseteq 𝒫 A$
5		simpr	$⊢ (S \in ⋃ ran sigAlgebra \land A \in S) \to A \in S$
6		pwidg	$⊢ A \in S \to A \in 𝒫 A$
7	5 6	syl	$⊢ (S \in ⋃ ran sigAlgebra \land A \in S) \to A \in 𝒫 A$
8	5 7	elind	$⊢ (S \in ⋃ ran sigAlgebra \land A \in S) \to A \in (S \cap 𝒫 A)$
9		simpll	$⊢ ((S \in ⋃ ran sigAlgebra \land A \in S) \land x \in (S \cap 𝒫 A)) \to S \in ⋃ ran sigAlgebra$
10		simplr	$⊢ ((S \in ⋃ ran sigAlgebra \land A \in S) \land x \in (S \cap 𝒫 A)) \to A \in S$
11		inss1	$⊢ S \cap 𝒫 A \subseteq S$
12		simpr	$⊢ ((S \in ⋃ ran sigAlgebra \land A \in S) \land x \in (S \cap 𝒫 A)) \to x \in (S \cap 𝒫 A)$
13	11 12	sselid	$⊢ ((S \in ⋃ ran sigAlgebra \land A \in S) \land x \in (S \cap 𝒫 A)) \to x \in S$
14		difelsiga	$⊢ (S \in ⋃ ran sigAlgebra \land A \in S \land x \in S) \to A ∖ x \in S$
15	9 10 13 14	syl3anc	$⊢ ((S \in ⋃ ran sigAlgebra \land A \in S) \land x \in (S \cap 𝒫 A)) \to A ∖ x \in S$
16		difss	$⊢ A ∖ x \subseteq A$
17		elpwg	$⊢ A ∖ x \in S \to (A ∖ x \in 𝒫 A \leftrightarrow A ∖ x \subseteq A)$
18	16 17	mpbiri	$⊢ A ∖ x \in S \to A ∖ x \in 𝒫 A$
19	15 18	syl	$⊢ ((S \in ⋃ ran sigAlgebra \land A \in S) \land x \in (S \cap 𝒫 A)) \to A ∖ x \in 𝒫 A$
20	15 19	elind	$⊢ ((S \in ⋃ ran sigAlgebra \land A \in S) \land x \in (S \cap 𝒫 A)) \to A ∖ x \in (S \cap 𝒫 A)$
21	20	ralrimiva	$⊢ (S \in ⋃ ran sigAlgebra \land A \in S) \to \forall x \in (S \cap 𝒫 A) A ∖ x \in (S \cap 𝒫 A)$
22		simplll	$⊢ (((S \in ⋃ ran sigAlgebra \land A \in S) \land x \in 𝒫 (S \cap 𝒫 A)) \land x ≼ ω) \to S \in ⋃ ran sigAlgebra$
23		simplr	$⊢ (((S \in ⋃ ran sigAlgebra \land A \in S) \land x \in 𝒫 (S \cap 𝒫 A)) \land x ≼ ω) \to x \in 𝒫 (S \cap 𝒫 A)$
24		elpwi	$⊢ x \in 𝒫 (S \cap 𝒫 A) \to x \subseteq S \cap 𝒫 A$
25		sstr	$⊢ (x \subseteq S \cap 𝒫 A \land S \cap 𝒫 A \subseteq S) \to x \subseteq S$
26	11 25	mpan2	$⊢ x \subseteq S \cap 𝒫 A \to x \subseteq S$
27	23 24 26	3syl	$⊢ (((S \in ⋃ ran sigAlgebra \land A \in S) \land x \in 𝒫 (S \cap 𝒫 A)) \land x ≼ ω) \to x \subseteq S$
28		elpwg	$⊢ x \in 𝒫 (S \cap 𝒫 A) \to (x \in 𝒫 S \leftrightarrow x \subseteq S)$
29	28	biimpar	$⊢ (x \in 𝒫 (S \cap 𝒫 A) \land x \subseteq S) \to x \in 𝒫 S$
30	23 27 29	syl2anc	$⊢ (((S \in ⋃ ran sigAlgebra \land A \in S) \land x \in 𝒫 (S \cap 𝒫 A)) \land x ≼ ω) \to x \in 𝒫 S$
31		simpr	$⊢ (((S \in ⋃ ran sigAlgebra \land A \in S) \land x \in 𝒫 (S \cap 𝒫 A)) \land x ≼ ω) \to x ≼ ω$
32		sigaclcu	$⊢ (S \in ⋃ ran sigAlgebra \land x \in 𝒫 S \land x ≼ ω) \to ⋃ x \in S$
33	22 30 31 32	syl3anc	$⊢ (((S \in ⋃ ran sigAlgebra \land A \in S) \land x \in 𝒫 (S \cap 𝒫 A)) \land x ≼ ω) \to ⋃ x \in S$
34		sstr	$⊢ (x \subseteq S \cap 𝒫 A \land S \cap 𝒫 A \subseteq 𝒫 A) \to x \subseteq 𝒫 A$
35	3 34	mpan2	$⊢ x \subseteq S \cap 𝒫 A \to x \subseteq 𝒫 A$
36	23 24 35	3syl	$⊢ (((S \in ⋃ ran sigAlgebra \land A \in S) \land x \in 𝒫 (S \cap 𝒫 A)) \land x ≼ ω) \to x \subseteq 𝒫 A$
37		sspwuni	$⊢ x \subseteq 𝒫 A \leftrightarrow ⋃ x \subseteq A$
38		vuniex	$⊢ ⋃ x \in V$
39	38	elpw	$⊢ ⋃ x \in 𝒫 A \leftrightarrow ⋃ x \subseteq A$
40	37 39	bitr4i	$⊢ x \subseteq 𝒫 A \leftrightarrow ⋃ x \in 𝒫 A$
41	36 40	sylib	$⊢ (((S \in ⋃ ran sigAlgebra \land A \in S) \land x \in 𝒫 (S \cap 𝒫 A)) \land x ≼ ω) \to ⋃ x \in 𝒫 A$
42	33 41	elind	$⊢ (((S \in ⋃ ran sigAlgebra \land A \in S) \land x \in 𝒫 (S \cap 𝒫 A)) \land x ≼ ω) \to ⋃ x \in (S \cap 𝒫 A)$
43	42	ex	$⊢ ((S \in ⋃ ran sigAlgebra \land A \in S) \land x \in 𝒫 (S \cap 𝒫 A)) \to (x ≼ ω \to ⋃ x \in (S \cap 𝒫 A))$
44	43	ralrimiva	$⊢ (S \in ⋃ ran sigAlgebra \land A \in S) \to \forall x \in 𝒫 (S \cap 𝒫 A) (x ≼ ω \to ⋃ x \in (S \cap 𝒫 A))$
45	8 21 44	3jca	$⊢ (S \in ⋃ ran sigAlgebra \land A \in S) \to (A \in (S \cap 𝒫 A) \land \forall x \in (S \cap 𝒫 A) A ∖ x \in (S \cap 𝒫 A) \land \forall x \in 𝒫 (S \cap 𝒫 A) (x ≼ ω \to ⋃ x \in (S \cap 𝒫 A)))$
46		issiga	$⊢ S \cap 𝒫 A \in V \to (S \cap 𝒫 A \in sigAlgebra (A) \leftrightarrow (S \cap 𝒫 A \subseteq 𝒫 A \land (A \in (S \cap 𝒫 A) \land \forall x \in (S \cap 𝒫 A) A ∖ x \in (S \cap 𝒫 A) \land \forall x \in 𝒫 (S \cap 𝒫 A) (x ≼ ω \to ⋃ x \in (S \cap 𝒫 A)))))$
47	46	biimpar	$⊢ (S \cap 𝒫 A \in V \land (S \cap 𝒫 A \subseteq 𝒫 A \land (A \in (S \cap 𝒫 A) \land \forall x \in (S \cap 𝒫 A) A ∖ x \in (S \cap 𝒫 A) \land \forall x \in 𝒫 (S \cap 𝒫 A) (x ≼ ω \to ⋃ x \in (S \cap 𝒫 A))))) \to S \cap 𝒫 A \in sigAlgebra (A)$
48	2 4 45 47	syl12anc	$⊢ (S \in ⋃ ran sigAlgebra \land A \in S) \to S \cap 𝒫 A \in sigAlgebra (A)$

Metamath Proof Explorer

Theorem sigainb

Proof