sigaclci

Description: A sigma-algebra is closed under countable intersections. Deduction version. (Contributed by Thierry Arnoux, 19-Sep-2016)

		Ref	Expression
	Assertion	sigaclci	$⊢ ((S \in ⋃ ran sigAlgebra \land A \in 𝒫 S) \land (A ≼ ω \land A \neq \emptyset)) \to ⋂ A \in S$

Proof

Step	Hyp	Ref	Expression
1		isrnsigau	$⊢ 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)))$
2	1	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))$
3	2	simp2d	$⊢ S \in ⋃ ran sigAlgebra \to \forall x \in S ⋃ S ∖ x \in S$
4	3	adantr	$⊢ (S \in ⋃ ran sigAlgebra \land A \in 𝒫 S) \to \forall x \in S ⋃ S ∖ x \in S$
5		elpwi	$⊢ A \in 𝒫 S \to A \subseteq S$
6		ssrexv	$⊢ A \subseteq S \to (\exists z \in A y = ⋃ S ∖ z \to \exists z \in S y = ⋃ S ∖ z)$
7	5 6	syl	$⊢ A \in 𝒫 S \to (\exists z \in A y = ⋃ S ∖ z \to \exists z \in S y = ⋃ S ∖ z)$
8	7	ss2abdv	$⊢ A \in 𝒫 S \to \{y \| \exists z \in A y = ⋃ S ∖ z\} \subseteq \{y \| \exists z \in S y = ⋃ S ∖ z\}$
9		isrnsigau	$⊢ S \in ⋃ ran sigAlgebra \to (S \subseteq 𝒫 ⋃ S \land (⋃ S \in S \land \forall z \in S ⋃ S ∖ z \in S \land \forall z \in 𝒫 S (z ≼ ω \to ⋃ z \in S)))$
10	9	simprd	$⊢ S \in ⋃ ran sigAlgebra \to (⋃ S \in S \land \forall z \in S ⋃ S ∖ z \in S \land \forall z \in 𝒫 S (z ≼ ω \to ⋃ z \in S))$
11	10	simp2d	$⊢ S \in ⋃ ran sigAlgebra \to \forall z \in S ⋃ S ∖ z \in S$
12		uniiunlem	$⊢ \forall z \in S ⋃ S ∖ z \in S \to (\forall z \in S ⋃ S ∖ z \in S \leftrightarrow \{y \| \exists z \in S y = ⋃ S ∖ z\} \subseteq S)$
13	11 12	syl	$⊢ S \in ⋃ ran sigAlgebra \to (\forall z \in S ⋃ S ∖ z \in S \leftrightarrow \{y \| \exists z \in S y = ⋃ S ∖ z\} \subseteq S)$
14	11 13	mpbid	$⊢ S \in ⋃ ran sigAlgebra \to \{y \| \exists z \in S y = ⋃ S ∖ z\} \subseteq S$
15	8 14	sylan9ssr	$⊢ (S \in ⋃ ran sigAlgebra \land A \in 𝒫 S) \to \{y \| \exists z \in A y = ⋃ S ∖ z\} \subseteq S$
16		abrexexg	$⊢ A \in 𝒫 S \to \{y \| \exists z \in A y = ⋃ S ∖ z\} \in V$
17		elpwg	$⊢ \{y \| \exists z \in A y = ⋃ S ∖ z\} \in V \to (\{y \| \exists z \in A y = ⋃ S ∖ z\} \in 𝒫 S \leftrightarrow \{y \| \exists z \in A y = ⋃ S ∖ z\} \subseteq S)$
18	16 17	syl	$⊢ A \in 𝒫 S \to (\{y \| \exists z \in A y = ⋃ S ∖ z\} \in 𝒫 S \leftrightarrow \{y \| \exists z \in A y = ⋃ S ∖ z\} \subseteq S)$
19	18	adantl	$⊢ (S \in ⋃ ran sigAlgebra \land A \in 𝒫 S) \to (\{y \| \exists z \in A y = ⋃ S ∖ z\} \in 𝒫 S \leftrightarrow \{y \| \exists z \in A y = ⋃ S ∖ z\} \subseteq S)$
20	15 19	mpbird	$⊢ (S \in ⋃ ran sigAlgebra \land A \in 𝒫 S) \to \{y \| \exists z \in A y = ⋃ S ∖ z\} \in 𝒫 S$
21	2	simp3d	$⊢ S \in ⋃ ran sigAlgebra \to \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S)$
22	21	adantr	$⊢ (S \in ⋃ ran sigAlgebra \land A \in 𝒫 S) \to \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S)$
23	20 22	jca	$⊢ (S \in ⋃ ran sigAlgebra \land A \in 𝒫 S) \to (\{y \| \exists z \in A y = ⋃ S ∖ z\} \in 𝒫 S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S))$
24		abrexdom2jm	$⊢ A \in 𝒫 S \to \{y \| \exists z \in A y = ⋃ S ∖ z\} ≼ A$
25		domtr	$⊢ (\{y \| \exists z \in A y = ⋃ S ∖ z\} ≼ A \land A ≼ ω) \to \{y \| \exists z \in A y = ⋃ S ∖ z\} ≼ ω$
26	24 25	sylan	$⊢ (A \in 𝒫 S \land A ≼ ω) \to \{y \| \exists z \in A y = ⋃ S ∖ z\} ≼ ω$
27	26	ex	$⊢ A \in 𝒫 S \to (A ≼ ω \to \{y \| \exists z \in A y = ⋃ S ∖ z\} ≼ ω)$
28	27	adantl	$⊢ (S \in ⋃ ran sigAlgebra \land A \in 𝒫 S) \to (A ≼ ω \to \{y \| \exists z \in A y = ⋃ S ∖ z\} ≼ ω)$
29		breq1	$⊢ x = \{y \| \exists z \in A y = ⋃ S ∖ z\} \to (x ≼ ω \leftrightarrow \{y \| \exists z \in A y = ⋃ S ∖ z\} ≼ ω)$
30		unieq	$⊢ x = \{y \| \exists z \in A y = ⋃ S ∖ z\} \to ⋃ x = ⋃ \{y \| \exists z \in A y = ⋃ S ∖ z\}$
31	30	eleq1d	$⊢ x = \{y \| \exists z \in A y = ⋃ S ∖ z\} \to (⋃ x \in S \leftrightarrow ⋃ \{y \| \exists z \in A y = ⋃ S ∖ z\} \in S)$
32	29 31	imbi12d	$⊢ x = \{y \| \exists z \in A y = ⋃ S ∖ z\} \to ((x ≼ ω \to ⋃ x \in S) \leftrightarrow (\{y \| \exists z \in A y = ⋃ S ∖ z\} ≼ ω \to ⋃ \{y \| \exists z \in A y = ⋃ S ∖ z\} \in S))$
33	32	rspcva	$⊢ (\{y \| \exists z \in A y = ⋃ S ∖ z\} \in 𝒫 S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S)) \to (\{y \| \exists z \in A y = ⋃ S ∖ z\} ≼ ω \to ⋃ \{y \| \exists z \in A y = ⋃ S ∖ z\} \in S)$
34	23 28 33	sylsyld	$⊢ (S \in ⋃ ran sigAlgebra \land A \in 𝒫 S) \to (A ≼ ω \to ⋃ \{y \| \exists z \in A y = ⋃ S ∖ z\} \in S)$
35	5	adantl	$⊢ (S \in ⋃ ran sigAlgebra \land A \in 𝒫 S) \to A \subseteq S$
36	11	adantr	$⊢ (S \in ⋃ ran sigAlgebra \land A \in 𝒫 S) \to \forall z \in S ⋃ S ∖ z \in S$
37		ssralv	$⊢ A \subseteq S \to (\forall z \in S ⋃ S ∖ z \in S \to \forall z \in A ⋃ S ∖ z \in S)$
38	35 36 37	sylc	$⊢ (S \in ⋃ ran sigAlgebra \land A \in 𝒫 S) \to \forall z \in A ⋃ S ∖ z \in S$
39		dfiun2g	$⊢ \forall z \in A ⋃ S ∖ z \in S \to ⋃_{z \in A} (⋃ S ∖ z) = ⋃ \{y \| \exists z \in A y = ⋃ S ∖ z\}$
40		eleq1	$⊢ ⋃_{z \in A} (⋃ S ∖ z) = ⋃ \{y \| \exists z \in A y = ⋃ S ∖ z\} \to (⋃_{z \in A} (⋃ S ∖ z) \in S \leftrightarrow ⋃ \{y \| \exists z \in A y = ⋃ S ∖ z\} \in S)$
41	38 39 40	3syl	$⊢ (S \in ⋃ ran sigAlgebra \land A \in 𝒫 S) \to (⋃_{z \in A} (⋃ S ∖ z) \in S \leftrightarrow ⋃ \{y \| \exists z \in A y = ⋃ S ∖ z\} \in S)$
42	34 41	sylibrd	$⊢ (S \in ⋃ ran sigAlgebra \land A \in 𝒫 S) \to (A ≼ ω \to ⋃_{z \in A} (⋃ S ∖ z) \in S)$
43		difeq2	$⊢ x = ⋃_{z \in A} (⋃ S ∖ z) \to ⋃ S ∖ x = ⋃ S ∖ ⋃_{z \in A} (⋃ S ∖ z)$
44	43	eleq1d	$⊢ x = ⋃_{z \in A} (⋃ S ∖ z) \to (⋃ S ∖ x \in S \leftrightarrow ⋃ S ∖ ⋃_{z \in A} (⋃ S ∖ z) \in S)$
45	44	rspccv	$⊢ \forall x \in S ⋃ S ∖ x \in S \to (⋃_{z \in A} (⋃ S ∖ z) \in S \to ⋃ S ∖ ⋃_{z \in A} (⋃ S ∖ z) \in S)$
46	4 42 45	sylsyld	$⊢ (S \in ⋃ ran sigAlgebra \land A \in 𝒫 S) \to (A ≼ ω \to ⋃ S ∖ ⋃_{z \in A} (⋃ S ∖ z) \in S)$
47	46	adantrd	$⊢ (S \in ⋃ ran sigAlgebra \land A \in 𝒫 S) \to ((A ≼ ω \land A \neq \emptyset) \to ⋃ S ∖ ⋃_{z \in A} (⋃ S ∖ z) \in S)$
48	47	imp	$⊢ ((S \in ⋃ ran sigAlgebra \land A \in 𝒫 S) \land (A ≼ ω \land A \neq \emptyset)) \to ⋃ S ∖ ⋃_{z \in A} (⋃ S ∖ z) \in S$
49		simpr	$⊢ (S \in ⋃ ran sigAlgebra \land A \in 𝒫 S) \to A \in 𝒫 S$
50		pwuni	$⊢ S \subseteq 𝒫 ⋃ S$
51	5 50	sstrdi	$⊢ A \in 𝒫 S \to A \subseteq 𝒫 ⋃ S$
52		iundifdifd	$⊢ A \subseteq 𝒫 ⋃ S \to (A \neq \emptyset \to ⋂ A = ⋃ S ∖ ⋃_{z \in A} (⋃ S ∖ z))$
53	49 51 52	3syl	$⊢ (S \in ⋃ ran sigAlgebra \land A \in 𝒫 S) \to (A \neq \emptyset \to ⋂ A = ⋃ S ∖ ⋃_{z \in A} (⋃ S ∖ z))$
54	53	adantld	$⊢ (S \in ⋃ ran sigAlgebra \land A \in 𝒫 S) \to ((A ≼ ω \land A \neq \emptyset) \to ⋂ A = ⋃ S ∖ ⋃_{z \in A} (⋃ S ∖ z))$
55		eleq1	$⊢ ⋂ A = ⋃ S ∖ ⋃_{z \in A} (⋃ S ∖ z) \to (⋂ A \in S \leftrightarrow ⋃ S ∖ ⋃_{z \in A} (⋃ S ∖ z) \in S)$
56	54 55	syl6	$⊢ (S \in ⋃ ran sigAlgebra \land A \in 𝒫 S) \to ((A ≼ ω \land A \neq \emptyset) \to (⋂ A \in S \leftrightarrow ⋃ S ∖ ⋃_{z \in A} (⋃ S ∖ z) \in S))$
57	56	imp	$⊢ ((S \in ⋃ ran sigAlgebra \land A \in 𝒫 S) \land (A ≼ ω \land A \neq \emptyset)) \to (⋂ A \in S \leftrightarrow ⋃ S ∖ ⋃_{z \in A} (⋃ S ∖ z) \in S)$
58	48 57	mpbird	$⊢ ((S \in ⋃ ran sigAlgebra \land A \in 𝒫 S) \land (A ≼ ω \land A \neq \emptyset)) \to ⋂ A \in S$

Metamath Proof Explorer

Theorem sigaclci

Proof