Metamath Proof Explorer

Theorem ldgenpisys

Description: The lambda system E generated by a pi-system T is also a pi-system. (Contributed by Thierry Arnoux, 18-Jun-2020)

Ref Expression
Hypotheses dynkin.p ⊢P=s∈𝒫𝒫O|fi⁡s⊆s
dynkin.l ⊢L=s∈𝒫𝒫O|∅∈s∧∀x∈sO∖x∈s∧∀x∈𝒫sx≼ω∧Disjy∈xy→⋃x∈s
dynkin.o ⊢φ→O∈V
ldgenpisys.e ⊢E=⋂t∈L|T⊆t
ldgenpisys.1 ⊢φ→T∈P
Assertion ldgenpisys ⊢φ→E∈P

Proof

Step Hyp Ref Expression
1 dynkin.p ⊢P=s∈𝒫𝒫O|fi⁡s⊆s
2 dynkin.l ⊢L=s∈𝒫𝒫O|∅∈s∧∀x∈sO∖x∈s∧∀x∈𝒫sx≼ω∧Disjy∈xy→⋃x∈s
3 dynkin.o ⊢φ→O∈V
4 ldgenpisys.e ⊢E=⋂t∈L|T⊆t
5 ldgenpisys.1 ⊢φ→T∈P
6 ssrab2 ⊢s∈𝒫𝒫O|∅∈s∧∀x∈sO∖x∈s∧∀x∈𝒫sx≼ω∧Disjy∈xy→⋃x∈s⊆𝒫𝒫O
7 ssrab2 ⊢s∈𝒫𝒫O|fi⁡s⊆s⊆𝒫𝒫O
8 5 1 eleqtrdi ⊢φ→T∈s∈𝒫𝒫O|fi⁡s⊆s
9 7 8 sselid ⊢φ→T∈𝒫𝒫O
10 9 elpwid ⊢φ→T⊆𝒫O
11 2 3 10 ldsysgenld ⊢φ→⋂t∈L|T⊆t∈L
12 4 11 eqeltrid ⊢φ→E∈L
13 12 2 eleqtrdi ⊢φ→E∈s∈𝒫𝒫O|∅∈s∧∀x∈sO∖x∈s∧∀x∈𝒫sx≼ω∧Disjy∈xy→⋃x∈s
14 6 13 sselid ⊢φ→E∈𝒫𝒫O
15 simprr ⊢φ∧a∈E∧b∈E→b∈E
16 simprl ⊢φ∧a∈E∧b∈E→a∈E
17 3 adantr ⊢φ∧a∈E→O∈V
18 5 adantr ⊢φ∧a∈E→T∈P
19 simpr ⊢φ∧a∈E→a∈E
20 10 adantr ⊢φ∧a∈E→T⊆𝒫O
21 20 sselda ⊢φ∧a∈E∧b∈T→b∈𝒫O
22 incom ⊢b∩a=a∩b
23 3 ad2antrr ⊢φ∧a∈E∧b∈T→O∈V
24 5 ad2antrr ⊢φ∧a∈E∧b∈T→T∈P
25 simpr ⊢φ∧a∈E∧b∈T→b∈T
26 1 2 23 4 24 25 ldgenpisyslem3 ⊢φ∧a∈E∧b∈T→E⊆c∈𝒫O|b∩c∈E
27 simplr ⊢φ∧a∈E∧b∈T→a∈E
28 26 27 sseldd ⊢φ∧a∈E∧b∈T→a∈c∈𝒫O|b∩c∈E
29 ineq2 ⊢c=a→b∩c=b∩a
30 29 eleq1d ⊢c=a→b∩c∈E↔b∩a∈E
31 30 elrab ⊢a∈c∈𝒫O|b∩c∈E↔a∈𝒫O∧b∩a∈E
32 28 31 sylib ⊢φ∧a∈E∧b∈T→a∈𝒫O∧b∩a∈E
33 32 simprd ⊢φ∧a∈E∧b∈T→b∩a∈E
34 22 33 eqeltrrid ⊢φ∧a∈E∧b∈T→a∩b∈E
35 21 34 jca ⊢φ∧a∈E∧b∈T→b∈𝒫O∧a∩b∈E
36 ineq2 ⊢c=b→a∩c=a∩b
37 36 eleq1d ⊢c=b→a∩c∈E↔a∩b∈E
38 37 elrab ⊢b∈c∈𝒫O|a∩c∈E↔b∈𝒫O∧a∩b∈E
39 35 38 sylibr ⊢φ∧a∈E∧b∈T→b∈c∈𝒫O|a∩c∈E
40 39 ex ⊢φ∧a∈E→b∈T→b∈c∈𝒫O|a∩c∈E
41 40 ssrdv ⊢φ∧a∈E→T⊆c∈𝒫O|a∩c∈E
42 1 2 17 4 18 19 41 ldgenpisyslem2 ⊢φ∧a∈E→E⊆c∈𝒫O|a∩c∈E
43 16 42 syldan ⊢φ∧a∈E∧b∈E→E⊆c∈𝒫O|a∩c∈E
44 ssrab ⊢E⊆c∈𝒫O|a∩c∈E↔E⊆𝒫O∧∀c∈Ea∩c∈E
45 43 44 sylib ⊢φ∧a∈E∧b∈E→E⊆𝒫O∧∀c∈Ea∩c∈E
46 45 simprd ⊢φ∧a∈E∧b∈E→∀c∈Ea∩c∈E
47 37 rspcv ⊢b∈E→∀c∈Ea∩c∈E→a∩b∈E
48 15 46 47 sylc ⊢φ∧a∈E∧b∈E→a∩b∈E
49 48 ralrimivva ⊢φ→∀a∈E∀b∈Ea∩b∈E
50 inficl ⊢E∈L→∀a∈E∀b∈Ea∩b∈E↔fi⁡E=E
51 12 50 syl ⊢φ→∀a∈E∀b∈Ea∩b∈E↔fi⁡E=E
52 49 51 mpbid ⊢φ→fi⁡E=E
53 eqimss ⊢fi⁡E=E→fi⁡E⊆E
54 52 53 syl ⊢φ→fi⁡E⊆E
55 14 54 jca ⊢φ→E∈𝒫𝒫O∧fi⁡E⊆E
56 1 ispisys ⊢E∈P↔E∈𝒫𝒫O∧fi⁡E⊆E
57 55 56 sylibr ⊢φ→E∈P