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	⊢ 𝑃 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( fi ‘ 𝑠 ) ⊆ 𝑠 }
	dynkin.l	⊢ 𝐿 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) }
	dynkin.o	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
	dynkin.1	⊢ ( 𝜑 → 𝑆 ∈ 𝐿 )
	dynkin.2	⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
	dynkin.3	⊢ ( 𝜑 → 𝑇 ⊆ 𝑆 )
Assertion	dynkin	⊢ ( 𝜑 → ∩ { 𝑢 ∈ ( sigAlgebra ‘ 𝑂 ) ∣ 𝑇 ⊆ 𝑢 } ⊆ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		dynkin.p	⊢ 𝑃 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( fi ‘ 𝑠 ) ⊆ 𝑠 }
2		dynkin.l	⊢ 𝐿 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) }
3		dynkin.o	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
4		dynkin.1	⊢ ( 𝜑 → 𝑆 ∈ 𝐿 )
5		dynkin.2	⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
6		dynkin.3	⊢ ( 𝜑 → 𝑇 ⊆ 𝑆 )
7		sseq2	⊢ ( 𝑣 = 𝑡 → ( 𝑇 ⊆ 𝑣 ↔ 𝑇 ⊆ 𝑡 ) )
8	7	cbvrabv	⊢ { 𝑣 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑣 } = { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 }
9	8	inteqi	⊢ ∩ { 𝑣 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑣 } = ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 }
10	1 2 3 9 5	ldgenpisys	⊢ ( 𝜑 → ∩ { 𝑣 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑣 } ∈ 𝑃 )
11	1	ispisys2	⊢ ( 𝑇 ∈ 𝑃 ↔ ( 𝑇 ∈ 𝒫 𝒫 𝑂 ∧ ∀ 𝑥 ∈ ( ( 𝒫 𝑇 ∩ Fin ) ∖ { ∅ } ) ∩ 𝑥 ∈ 𝑇 ) )
12	11	simplbi	⊢ ( 𝑇 ∈ 𝑃 → 𝑇 ∈ 𝒫 𝒫 𝑂 )
13	5 12	syl	⊢ ( 𝜑 → 𝑇 ∈ 𝒫 𝒫 𝑂 )
14	13	elpwid	⊢ ( 𝜑 → 𝑇 ⊆ 𝒫 𝑂 )
15	2 3 14	ldsysgenld	⊢ ( 𝜑 → ∩ { 𝑣 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑣 } ∈ 𝐿 )
16	10 15	elind	⊢ ( 𝜑 → ∩ { 𝑣 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑣 } ∈ ( 𝑃 ∩ 𝐿 ) )
17	1 2	sigapildsys	⊢ ( sigAlgebra ‘ 𝑂 ) = ( 𝑃 ∩ 𝐿 )
18	16 17	eleqtrrdi	⊢ ( 𝜑 → ∩ { 𝑣 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑣 } ∈ ( sigAlgebra ‘ 𝑂 ) )
19		ssintub	⊢ 𝑇 ⊆ ∩ { 𝑣 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑣 }
20	19	a1i	⊢ ( 𝜑 → 𝑇 ⊆ ∩ { 𝑣 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑣 } )
21		sseq2	⊢ ( 𝑢 = ∩ { 𝑣 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑣 } → ( 𝑇 ⊆ 𝑢 ↔ 𝑇 ⊆ ∩ { 𝑣 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑣 } ) )
22	21	intminss	⊢ ( ( ∩ { 𝑣 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑣 } ∈ ( sigAlgebra ‘ 𝑂 ) ∧ 𝑇 ⊆ ∩ { 𝑣 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑣 } ) → ∩ { 𝑢 ∈ ( sigAlgebra ‘ 𝑂 ) ∣ 𝑇 ⊆ 𝑢 } ⊆ ∩ { 𝑣 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑣 } )
23	18 20 22	syl2anc	⊢ ( 𝜑 → ∩ { 𝑢 ∈ ( sigAlgebra ‘ 𝑂 ) ∣ 𝑇 ⊆ 𝑢 } ⊆ ∩ { 𝑣 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑣 } )
24		sseq2	⊢ ( 𝑣 = 𝑆 → ( 𝑇 ⊆ 𝑣 ↔ 𝑇 ⊆ 𝑆 ) )
25	24	intminss	⊢ ( ( 𝑆 ∈ 𝐿 ∧ 𝑇 ⊆ 𝑆 ) → ∩ { 𝑣 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑣 } ⊆ 𝑆 )
26	4 6 25	syl2anc	⊢ ( 𝜑 → ∩ { 𝑣 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑣 } ⊆ 𝑆 )
27	23 26	sstrd	⊢ ( 𝜑 → ∩ { 𝑢 ∈ ( sigAlgebra ‘ 𝑂 ) ∣ 𝑇 ⊆ 𝑢 } ⊆ 𝑆 )