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 ∈ s O ∖ x ∈ s ∧ ∀ x ∈ 𝒫 s x ≼ ω ∧ Disj y ∈ x y → ⋃ 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 ∈ s O ∖ x ∈ s ∧ ∀ x ∈ 𝒫 s x ≼ ω ∧ Disj y ∈ x y → ⋃ 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 ∈ s O ∖ x ∈ s ∧ ∀ x ∈ 𝒫 s x ≼ ω ∧ Disj y ∈ x y → ⋃ 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 ∈ s O ∖ x ∈ s ∧ ∀ x ∈ 𝒫 s x ≼ ω ∧ Disj y ∈ x y → ⋃ 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 ∈ E a ∩ c ∈ E
45 43 44 sylib ⊢ φ ∧ a ∈ E ∧ b ∈ E → E ⊆ 𝒫 O ∧ ∀ c ∈ E a ∩ c ∈ E
46 45 simprd ⊢ φ ∧ a ∈ E ∧ b ∈ E → ∀ c ∈ E a ∩ c ∈ E
47 37 rspcv ⊢ b ∈ E → ∀ c ∈ E a ∩ c ∈ E → a ∩ b ∈ E
48 15 46 47 sylc ⊢ φ ∧ a ∈ E ∧ b ∈ E → a ∩ b ∈ E
49 48 ralrimivva ⊢ φ → ∀ a ∈ E ∀ b ∈ E a ∩ b ∈ E
50 inficl ⊢ E ∈ L → ∀ a ∈ E ∀ b ∈ E a ∩ b ∈ E ↔ fi ⁡ E = E
51 12 50 syl ⊢ φ → ∀ a ∈ E ∀ b ∈ E a ∩ 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