insiga

Description: The intersection of a collection of sigma-algebras of same base is a sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016)

		Ref	Expression
	Assertion	insiga	$⊢ (A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \to ⋂ A \in sigAlgebra (O)$

Proof

Step	Hyp	Ref	Expression
1		intex	$⊢ A \neq \emptyset \leftrightarrow ⋂ A \in V$
2	1	birani	$⊢ (A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \to ⋂ A \in V$
3		intssuni	$⊢ A \neq \emptyset \to ⋂ A \subseteq ⋃ A$
4	3	adantr	$⊢ (A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \to ⋂ A \subseteq ⋃ A$
5		simpr	$⊢ (A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \to A \in 𝒫 sigAlgebra (O)$
6		elpwi	$⊢ A \in 𝒫 sigAlgebra (O) \to A \subseteq sigAlgebra (O)$
7		sigasspw	$⊢ s \in sigAlgebra (O) \to s \subseteq 𝒫 O$
8		velpw	$⊢ s \in 𝒫 𝒫 O \leftrightarrow s \subseteq 𝒫 O$
9	7 8	sylibr	$⊢ s \in sigAlgebra (O) \to s \in 𝒫 𝒫 O$
10	9	ssriv	$⊢ sigAlgebra (O) \subseteq 𝒫 𝒫 O$
11	6 10	sstrdi	$⊢ A \in 𝒫 sigAlgebra (O) \to A \subseteq 𝒫 𝒫 O$
12	5 11	syl	$⊢ (A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \to A \subseteq 𝒫 𝒫 O$
13		sspwuni	$⊢ A \subseteq 𝒫 𝒫 O \leftrightarrow ⋃ A \subseteq 𝒫 O$
14	12 13	sylib	$⊢ (A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \to ⋃ A \subseteq 𝒫 O$
15	4 14	sstrd	$⊢ (A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \to ⋂ A \subseteq 𝒫 O$
16		simpr	$⊢ ((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land s \in A) \to s \in A$
17		simplr	$⊢ ((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land s \in A) \to A \in 𝒫 sigAlgebra (O)$
18		elelpwi	$⊢ (s \in A \land A \in 𝒫 sigAlgebra (O)) \to s \in sigAlgebra (O)$
19	16 17 18	syl2anc	$⊢ ((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land s \in A) \to s \in sigAlgebra (O)$
20		vex	$⊢ s \in V$
21		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))))$
22	20 21	ax-mp	$⊢ 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)))$
23	19 22	sylib	$⊢ ((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land s \in A) \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)))$
24	23	simprd	$⊢ ((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land s \in A) \to (O \in s \land \forall x \in s O ∖ x \in s \land \forall x \in 𝒫 s (x ≼ ω \to ⋃ x \in s))$
25	24	simp1d	$⊢ ((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land s \in A) \to O \in s$
26	25	ralrimiva	$⊢ (A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \to \forall s \in A O \in s$
27		n0	$⊢ A \neq \emptyset \leftrightarrow \exists s s \in A$
28	27	birani	$⊢ (A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \to \exists s s \in A$
29	19	ex	$⊢ (A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \to (s \in A \to s \in sigAlgebra (O))$
30	29	eximdv	$⊢ (A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \to (\exists s s \in A \to \exists s s \in sigAlgebra (O))$
31	28 30	mpd	$⊢ (A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \to \exists s s \in sigAlgebra (O)$
32		elfvex	$⊢ s \in sigAlgebra (O) \to O \in V$
33	32	exlimiv	$⊢ \exists s s \in sigAlgebra (O) \to O \in V$
34	31 33	syl	$⊢ (A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \to O \in V$
35		elintg	$⊢ O \in V \to (O \in ⋂ A \leftrightarrow \forall s \in A O \in s)$
36	34 35	syl	$⊢ (A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \to (O \in ⋂ A \leftrightarrow \forall s \in A O \in s)$
37	26 36	mpbird	$⊢ (A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \to O \in ⋂ A$
38		simpll	$⊢ (((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land x \in ⋂ A) \land s \in A) \to (A \neq \emptyset \land A \in 𝒫 sigAlgebra (O))$
39		simpr	$⊢ (((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land x \in ⋂ A) \land s \in A) \to s \in A$
40	38 39	jca	$⊢ (((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land x \in ⋂ A) \land s \in A) \to ((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land s \in A)$
41		elinti	$⊢ x \in ⋂ A \to (s \in A \to x \in s)$
42	41	imp	$⊢ (x \in ⋂ A \land s \in A) \to x \in s$
43	42	adantll	$⊢ (((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land x \in ⋂ A) \land s \in A) \to x \in s$
44	24	simp2d	$⊢ ((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land s \in A) \to \forall x \in s O ∖ x \in s$
45	44	r19.21bi	$⊢ (((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land s \in A) \land x \in s) \to O ∖ x \in s$
46	40 43 45	syl2anc	$⊢ (((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land x \in ⋂ A) \land s \in A) \to O ∖ x \in s$
47	46	ralrimiva	$⊢ ((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land x \in ⋂ A) \to \forall s \in A O ∖ x \in s$
48	34	difexd	$⊢ (A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \to O ∖ x \in V$
49	48	adantr	$⊢ ((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land x \in ⋂ A) \to O ∖ x \in V$
50		elintg	$⊢ O ∖ x \in V \to (O ∖ x \in ⋂ A \leftrightarrow \forall s \in A O ∖ x \in s)$
51	49 50	syl	$⊢ ((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land x \in ⋂ A) \to (O ∖ x \in ⋂ A \leftrightarrow \forall s \in A O ∖ x \in s)$
52	47 51	mpbird	$⊢ ((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land x \in ⋂ A) \to O ∖ x \in ⋂ A$
53	52	ralrimiva	$⊢ (A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \to \forall x \in ⋂ A O ∖ x \in ⋂ A$
54		simplll	$⊢ ((((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land x \in 𝒫 ⋂ A) \land x ≼ ω) \land s \in A) \to (A \neq \emptyset \land A \in 𝒫 sigAlgebra (O))$
55		simpr	$⊢ ((((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land x \in 𝒫 ⋂ A) \land x ≼ ω) \land s \in A) \to s \in A$
56	54 55	jca	$⊢ ((((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land x \in 𝒫 ⋂ A) \land x ≼ ω) \land s \in A) \to ((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land s \in A)$
57		simpllr	$⊢ ((((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land x \in 𝒫 ⋂ A) \land x ≼ ω) \land s \in A) \to x \in 𝒫 ⋂ A$
58		elpwi	$⊢ x \in 𝒫 ⋂ A \to x \subseteq ⋂ A$
59		intss1	$⊢ s \in A \to ⋂ A \subseteq s$
60	58 59	sylan9ss	$⊢ (x \in 𝒫 ⋂ A \land s \in A) \to x \subseteq s$
61		velpw	$⊢ x \in 𝒫 s \leftrightarrow x \subseteq s$
62	60 61	sylibr	$⊢ (x \in 𝒫 ⋂ A \land s \in A) \to x \in 𝒫 s$
63	57 62	sylancom	$⊢ ((((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land x \in 𝒫 ⋂ A) \land x ≼ ω) \land s \in A) \to x \in 𝒫 s$
64	56 63	jca	$⊢ ((((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land x \in 𝒫 ⋂ A) \land x ≼ ω) \land s \in A) \to (((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land s \in A) \land x \in 𝒫 s)$
65		simplr	$⊢ ((((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land x \in 𝒫 ⋂ A) \land x ≼ ω) \land s \in A) \to x ≼ ω$
66	24	simp3d	$⊢ ((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land s \in A) \to \forall x \in 𝒫 s (x ≼ ω \to ⋃ x \in s)$
67	66	r19.21bi	$⊢ (((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land s \in A) \land x \in 𝒫 s) \to (x ≼ ω \to ⋃ x \in s)$
68	64 65 67	sylc	$⊢ ((((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land x \in 𝒫 ⋂ A) \land x ≼ ω) \land s \in A) \to ⋃ x \in s$
69	68	ralrimiva	$⊢ (((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land x \in 𝒫 ⋂ A) \land x ≼ ω) \to \forall s \in A ⋃ x \in s$
70		uniexg	$⊢ x \in 𝒫 ⋂ A \to ⋃ x \in V$
71	70	ad2antlr	$⊢ (((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land x \in 𝒫 ⋂ A) \land x ≼ ω) \to ⋃ x \in V$
72		elintg	$⊢ ⋃ x \in V \to (⋃ x \in ⋂ A \leftrightarrow \forall s \in A ⋃ x \in s)$
73	71 72	syl	$⊢ (((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land x \in 𝒫 ⋂ A) \land x ≼ ω) \to (⋃ x \in ⋂ A \leftrightarrow \forall s \in A ⋃ x \in s)$
74	69 73	mpbird	$⊢ (((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land x \in 𝒫 ⋂ A) \land x ≼ ω) \to ⋃ x \in ⋂ A$
75	74	ex	$⊢ ((A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \land x \in 𝒫 ⋂ A) \to (x ≼ ω \to ⋃ x \in ⋂ A)$
76	75	ralrimiva	$⊢ (A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \to \forall x \in 𝒫 ⋂ A (x ≼ ω \to ⋃ x \in ⋂ A)$
77	37 53 76	3jca	$⊢ (A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \to (O \in ⋂ A \land \forall x \in ⋂ A O ∖ x \in ⋂ A \land \forall x \in 𝒫 ⋂ A (x ≼ ω \to ⋃ x \in ⋂ A))$
78		issiga	$⊢ ⋂ A \in V \to (⋂ A \in sigAlgebra (O) \leftrightarrow (⋂ A \subseteq 𝒫 O \land (O \in ⋂ A \land \forall x \in ⋂ A O ∖ x \in ⋂ A \land \forall x \in 𝒫 ⋂ A (x ≼ ω \to ⋃ x \in ⋂ A))))$
79	78	biimpar	$⊢ (⋂ A \in V \land (⋂ A \subseteq 𝒫 O \land (O \in ⋂ A \land \forall x \in ⋂ A O ∖ x \in ⋂ A \land \forall x \in 𝒫 ⋂ A (x ≼ ω \to ⋃ x \in ⋂ A)))) \to ⋂ A \in sigAlgebra (O)$
80	2 15 77 79	syl12anc	$⊢ (A \neq \emptyset \land A \in 𝒫 sigAlgebra (O)) \to ⋂ A \in sigAlgebra (O)$

Metamath Proof Explorer

Theorem insiga

Proof