sigaldsys

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

		Ref	Expression
	Hypothesis	isldsys.l	$⊢ L = \{s \in 𝒫 𝒫 O \| (\emptyset \in s \land \forall x \in s O ∖ x \in s \land \forall x \in 𝒫 s ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in s))\}$
	Assertion	sigaldsys	$⊢ sigAlgebra (O) \subseteq L$

Proof

Step	Hyp	Ref	Expression
1		isldsys.l	$⊢ L = \{s \in 𝒫 𝒫 O \| (\emptyset \in s \land \forall x \in s O ∖ x \in s \land \forall x \in 𝒫 s ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in 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		0elsiga	$⊢ t \in ⋃ ran sigAlgebra \to \emptyset \in t$
7	5 6	syl	$⊢ t \in sigAlgebra (O) \to \emptyset \in t$
8	5	adantr	$⊢ (t \in sigAlgebra (O) \land x \in t) \to t \in ⋃ ran sigAlgebra$
9		baselsiga	$⊢ t \in sigAlgebra (O) \to O \in t$
10	9	adantr	$⊢ (t \in sigAlgebra (O) \land x \in t) \to O \in t$
11		simpr	$⊢ (t \in sigAlgebra (O) \land x \in t) \to x \in t$
12		difelsiga	$⊢ (t \in ⋃ ran sigAlgebra \land O \in t \land x \in t) \to O ∖ x \in t$
13	8 10 11 12	syl3anc	$⊢ (t \in sigAlgebra (O) \land x \in t) \to O ∖ x \in t$
14	13	ralrimiva	$⊢ t \in sigAlgebra (O) \to \forall x \in t O ∖ x \in t$
15	5	ad2antrr	$⊢ ((t \in sigAlgebra (O) \land x \in 𝒫 t) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to t \in ⋃ ran sigAlgebra$
16		simplr	$⊢ ((t \in sigAlgebra (O) \land x \in 𝒫 t) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to x \in 𝒫 t$
17		simprl	$⊢ ((t \in sigAlgebra (O) \land x \in 𝒫 t) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to x ≼ ω$
18		sigaclcu	$⊢ (t \in ⋃ ran sigAlgebra \land x \in 𝒫 t \land x ≼ ω) \to ⋃ x \in t$
19	15 16 17 18	syl3anc	$⊢ ((t \in sigAlgebra (O) \land x \in 𝒫 t) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to ⋃ x \in t$
20	19	ex	$⊢ (t \in sigAlgebra (O) \land x \in 𝒫 t) \to ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in t)$
21	20	ralrimiva	$⊢ t \in sigAlgebra (O) \to \forall x \in 𝒫 t ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in t)$
22	7 14 21	3jca	$⊢ t \in sigAlgebra (O) \to (\emptyset \in t \land \forall x \in t O ∖ x \in t \land \forall x \in 𝒫 t ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in t))$
23	4 22	jca	$⊢ t \in sigAlgebra (O) \to (t \in 𝒫 𝒫 O \land (\emptyset \in t \land \forall x \in t O ∖ x \in t \land \forall x \in 𝒫 t ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in t)))$
24	1	isldsys	$⊢ t \in L \leftrightarrow (t \in 𝒫 𝒫 O \land (\emptyset \in t \land \forall x \in t O ∖ x \in t \land \forall x \in 𝒫 t ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ⋃ x \in t)))$
25	23 24	sylibr	$⊢ t \in sigAlgebra (O) \to t \in L$
26	25	ssriv	$⊢ sigAlgebra (O) \subseteq L$

Metamath Proof Explorer

Theorem sigaldsys

Proof