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

Metamath Proof Explorer

Theorem insiga

Proof