dynkin

Description: Dynkin's lambda-pi theorem: if a lambda-system contains a pi-system, it also contains the sigma-algebra generated by that pi-system. (Contributed by Thierry Arnoux, 16-Jun-2020)

	Ref	Expression
Hypotheses	dynkin.p	$⊢ P = \{s \in 𝒫 𝒫 O \| fi (s) \subseteq s\}$
	dynkin.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))\}$
	dynkin.o	$⊢ φ \to O \in V$
	dynkin.1	$⊢ φ \to S \in L$
	dynkin.2	$⊢ φ \to T \in P$
	dynkin.3	$⊢ φ \to T \subseteq S$
Assertion	dynkin	$⊢ φ \to ⋂ \{u \in sigAlgebra (O) \| T \subseteq u\} \subseteq S$

Proof

Step	Hyp	Ref	Expression
1		dynkin.p	$⊢ P = \{s \in 𝒫 𝒫 O \| fi (s) \subseteq s\}$
2		dynkin.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))\}$
3		dynkin.o	$⊢ φ \to O \in V$
4		dynkin.1	$⊢ φ \to S \in L$
5		dynkin.2	$⊢ φ \to T \in P$
6		dynkin.3	$⊢ φ \to T \subseteq S$
7		sseq2	$⊢ v = t \to (T \subseteq v \leftrightarrow T \subseteq t)$
8	7	cbvrabv	$⊢ \{v \in L \| T \subseteq v\} = \{t \in L \| T \subseteq t\}$
9	8	inteqi	$⊢ ⋂ \{v \in L \| T \subseteq v\} = ⋂ \{t \in L \| T \subseteq t\}$
10	1 2 3 9 5	ldgenpisys	$⊢ φ \to ⋂ \{v \in L \| T \subseteq v\} \in P$
11	1	ispisys2	$⊢ T \in P \leftrightarrow (T \in 𝒫 𝒫 O \land \forall x \in ((𝒫 T \cap Fin) ∖ \{\emptyset\}) ⋂ x \in T)$
12	11	simplbi	$⊢ T \in P \to T \in 𝒫 𝒫 O$
13	5 12	syl	$⊢ φ \to T \in 𝒫 𝒫 O$
14	13	elpwid	$⊢ φ \to T \subseteq 𝒫 O$
15	2 3 14	ldsysgenld	$⊢ φ \to ⋂ \{v \in L \| T \subseteq v\} \in L$
16	10 15	elind	$⊢ φ \to ⋂ \{v \in L \| T \subseteq v\} \in (P \cap L)$
17	1 2	sigapildsys	$⊢ sigAlgebra (O) = P \cap L$
18	16 17	eleqtrrdi	$⊢ φ \to ⋂ \{v \in L \| T \subseteq v\} \in sigAlgebra (O)$
19		ssintub	$⊢ T \subseteq ⋂ \{v \in L \| T \subseteq v\}$
20	19	a1i	$⊢ φ \to T \subseteq ⋂ \{v \in L \| T \subseteq v\}$
21		sseq2	$⊢ u = ⋂ \{v \in L \| T \subseteq v\} \to (T \subseteq u \leftrightarrow T \subseteq ⋂ \{v \in L \| T \subseteq v\})$
22	21	intminss	$⊢ (⋂ \{v \in L \| T \subseteq v\} \in sigAlgebra (O) \land T \subseteq ⋂ \{v \in L \| T \subseteq v\}) \to ⋂ \{u \in sigAlgebra (O) \| T \subseteq u\} \subseteq ⋂ \{v \in L \| T \subseteq v\}$
23	18 20 22	syl2anc	$⊢ φ \to ⋂ \{u \in sigAlgebra (O) \| T \subseteq u\} \subseteq ⋂ \{v \in L \| T \subseteq v\}$
24		sseq2	$⊢ v = S \to (T \subseteq v \leftrightarrow T \subseteq S)$
25	24	intminss	$⊢ (S \in L \land T \subseteq S) \to ⋂ \{v \in L \| T \subseteq v\} \subseteq S$
26	4 6 25	syl2anc	$⊢ φ \to ⋂ \{v \in L \| T \subseteq v\} \subseteq S$
27	23 26	sstrd	$⊢ φ \to ⋂ \{u \in sigAlgebra (O) \| T \subseteq u\} \subseteq S$

Metamath Proof Explorer

Theorem dynkin

Proof