Theorem 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=\left\{s\in 𝒫𝒫O|\mathrm{fi}\left(s\right)\subseteq s\right\}$$
	dynkin.l	$$⊢L=\left\{s\in 𝒫𝒫O|\left(\varnothing \in s\wedge \forall x\in sO\setminus x\in s\wedge \forall x\in 𝒫s\left(\left(x\preccurlyeq \mathrm{\omega }\wedge \underset{y\in x}{Disj}y\right)\to \bigcup x\in s\right)\right)\right\}$$
	dynkin.o	$$⊢\phi \to O\in V$$
	dynkin.1	$$⊢\phi \to S\in L$$
	dynkin.2	$$⊢\phi \to T\in P$$
	dynkin.3	$$⊢\phi \to T\subseteq S$$
Assertion	dynkin	$$⊢\phi \to \bigcap \left\{u\in \mathrm{sigAlgebra}\left(O\right)|T\subseteq u\right\}\subseteq S$$

Proof

Step	Hyp	Ref	Expression
1		dynkin.p	$$⊢P=\left\{s\in 𝒫𝒫O|\mathrm{fi}\left(s\right)\subseteq s\right\}$$
2		dynkin.l	$$⊢L=\left\{s\in 𝒫𝒫O|\left(\varnothing \in s\wedge \forall x\in sO\setminus x\in s\wedge \forall x\in 𝒫s\left(\left(x\preccurlyeq \mathrm{\omega }\wedge \underset{y\in x}{Disj}y\right)\to \bigcup x\in s\right)\right)\right\}$$
3		dynkin.o	$$⊢\phi \to O\in V$$
4		dynkin.1	$$⊢\phi \to S\in L$$
5		dynkin.2	$$⊢\phi \to T\in P$$
6		dynkin.3	$$⊢\phi \to T\subseteq S$$
7		sseq2	$$⊢v=t\to \left(T\subseteq v\leftrightarrow T\subseteq t\right)$$
8	7	cbvrabv	$$⊢\left\{v\in L|T\subseteq v\right\}=\left\{t\in L|T\subseteq t\right\}$$
9	8	inteqi	$$⊢\bigcap \left\{v\in L|T\subseteq v\right\}=\bigcap \left\{t\in L|T\subseteq t\right\}$$
10	1 2 3 9 5	ldgenpisys	$$⊢\phi \to \bigcap \left\{v\in L|T\subseteq v\right\}\in P$$
11	1	ispisys2	$$⊢T\in P\leftrightarrow \left(T\in 𝒫𝒫O\wedge \forall x\in \left(\left(𝒫T\cap \mathrm{Fin}\right)\setminus \left\{\varnothing \right\}\right)\bigcap x\in T\right)$$
12	11	simplbi	$$⊢T\in P\to T\in 𝒫𝒫O$$
13	5 12	syl	$$⊢\phi \to T\in 𝒫𝒫O$$
14	13	elpwid	$$⊢\phi \to T\subseteq 𝒫O$$
15	2 3 14	ldsysgenld	$$⊢\phi \to \bigcap \left\{v\in L|T\subseteq v\right\}\in L$$
16	10 15	elind	$$⊢\phi \to \bigcap \left\{v\in L|T\subseteq v\right\}\in \left(P\cap L\right)$$
17	1 2	sigapildsys	$$⊢\mathrm{sigAlgebra}\left(O\right)=P\cap L$$
18	16 17	eleqtrrdi	$$⊢\phi \to \bigcap \left\{v\in L|T\subseteq v\right\}\in \mathrm{sigAlgebra}\left(O\right)$$
19		ssintub	$$⊢T\subseteq \bigcap \left\{v\in L|T\subseteq v\right\}$$
20	19	a1i	$$⊢\phi \to T\subseteq \bigcap \left\{v\in L|T\subseteq v\right\}$$
21		sseq2	$$⊢u=\bigcap \left\{v\in L|T\subseteq v\right\}\to \left(T\subseteq u\leftrightarrow T\subseteq \bigcap \left\{v\in L|T\subseteq v\right\}\right)$$
22	21	intminss	$$⊢\left(\bigcap \left\{v\in L|T\subseteq v\right\}\in \mathrm{sigAlgebra}\left(O\right)\wedge T\subseteq \bigcap \left\{v\in L|T\subseteq v\right\}\right)\to \bigcap \left\{u\in \mathrm{sigAlgebra}\left(O\right)|T\subseteq u\right\}\subseteq \bigcap \left\{v\in L|T\subseteq v\right\}$$
23	18 20 22	syl2anc	$$⊢\phi \to \bigcap \left\{u\in \mathrm{sigAlgebra}\left(O\right)|T\subseteq u\right\}\subseteq \bigcap \left\{v\in L|T\subseteq v\right\}$$
24		sseq2	$$⊢v=S\to \left(T\subseteq v\leftrightarrow T\subseteq S\right)$$
25	24	intminss	$$⊢\left(S\in L\wedge T\subseteq S\right)\to \bigcap \left\{v\in L|T\subseteq v\right\}\subseteq S$$
26	4 6 25	syl2anc	$$⊢\phi \to \bigcap \left\{v\in L|T\subseteq v\right\}\subseteq S$$
27	23 26	sstrd	$$⊢\phi \to \bigcap \left\{u\in \mathrm{sigAlgebra}\left(O\right)|T\subseteq u\right\}\subseteq S$$