sigapisys

Description: All sigma-algebras are pi-systems. (Contributed by Thierry Arnoux, 13-Jun-2020)

		Ref	Expression
	Hypothesis	ispisys.p	$⊢ P = \{s \in 𝒫 𝒫 O \| fi (s) \subseteq s\}$
	Assertion	sigapisys	$⊢ sigAlgebra (O) \subseteq P$

Proof

Step	Hyp	Ref	Expression
1		ispisys.p	$⊢ P = \{s \in 𝒫 𝒫 O \| fi (s) \subseteq s\}$
2		sigasspw	$⊢ t \in sigAlgebra (O) \to t \subseteq 𝒫 O$
3		velpw	$⊢ t \in 𝒫 𝒫 O \leftrightarrow t \subseteq 𝒫 O$
4	2 3	sylibr	$⊢ t \in sigAlgebra (O) \to t \in 𝒫 𝒫 O$
5		elrnsiga	$⊢ t \in sigAlgebra (O) \to t \in ⋃ ran sigAlgebra$
6	5	adantr	$⊢ (t \in sigAlgebra (O) \land x \in ((𝒫 t \cap Fin) ∖ \{\emptyset\})) \to t \in ⋃ ran sigAlgebra$
7		eldifsn	$⊢ x \in ((𝒫 t \cap Fin) ∖ \{\emptyset\}) \leftrightarrow (x \in (𝒫 t \cap Fin) \land x \neq \emptyset)$
8	7	biimpi	$⊢ x \in ((𝒫 t \cap Fin) ∖ \{\emptyset\}) \to (x \in (𝒫 t \cap Fin) \land x \neq \emptyset)$
9	8	adantl	$⊢ (t \in sigAlgebra (O) \land x \in ((𝒫 t \cap Fin) ∖ \{\emptyset\})) \to (x \in (𝒫 t \cap Fin) \land x \neq \emptyset)$
10	9	simpld	$⊢ (t \in sigAlgebra (O) \land x \in ((𝒫 t \cap Fin) ∖ \{\emptyset\})) \to x \in (𝒫 t \cap Fin)$
11	10	elin1d	$⊢ (t \in sigAlgebra (O) \land x \in ((𝒫 t \cap Fin) ∖ \{\emptyset\})) \to x \in 𝒫 t$
12	10	elin2d	$⊢ (t \in sigAlgebra (O) \land x \in ((𝒫 t \cap Fin) ∖ \{\emptyset\})) \to x \in Fin$
13		fict	$⊢ x \in Fin \to x ≼ ω$
14	12 13	syl	$⊢ (t \in sigAlgebra (O) \land x \in ((𝒫 t \cap Fin) ∖ \{\emptyset\})) \to x ≼ ω$
15	9	simprd	$⊢ (t \in sigAlgebra (O) \land x \in ((𝒫 t \cap Fin) ∖ \{\emptyset\})) \to x \neq \emptyset$
16		sigaclci	$⊢ ((t \in ⋃ ran sigAlgebra \land x \in 𝒫 t) \land (x ≼ ω \land x \neq \emptyset)) \to ⋂ x \in t$
17	6 11 14 15 16	syl22anc	$⊢ (t \in sigAlgebra (O) \land x \in ((𝒫 t \cap Fin) ∖ \{\emptyset\})) \to ⋂ x \in t$
18	17	ralrimiva	$⊢ t \in sigAlgebra (O) \to \forall x \in ((𝒫 t \cap Fin) ∖ \{\emptyset\}) ⋂ x \in t$
19	4 18	jca	$⊢ t \in sigAlgebra (O) \to (t \in 𝒫 𝒫 O \land \forall x \in ((𝒫 t \cap Fin) ∖ \{\emptyset\}) ⋂ x \in t)$
20	1	ispisys2	$⊢ t \in P \leftrightarrow (t \in 𝒫 𝒫 O \land \forall x \in ((𝒫 t \cap Fin) ∖ \{\emptyset\}) ⋂ x \in t)$
21	19 20	sylibr	$⊢ t \in sigAlgebra (O) \to t \in P$
22	21	ssriv	$⊢ sigAlgebra (O) \subseteq P$

Metamath Proof Explorer

Theorem sigapisys

Proof