Metamath Proof Explorer

Theorem ldgenpisyslem2

Description: Lemma for ldgenpisys . (Contributed by Thierry Arnoux, 18-Jul-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
ldgenpisyslem1.1 ⊢φ→A∈E
ldgenpisyslem2.1 ⊢φ→T⊆b∈𝒫O|A∩b∈E
Assertion ldgenpisyslem2 ⊢φ→E⊆b∈𝒫O|A∩b∈E

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 ldgenpisyslem1.1 ⊢φ→A∈E
7 ldgenpisyslem2.1 ⊢φ→T⊆b∈𝒫O|A∩b∈E
8 1 2 3 4 5 6 ldgenpisyslem1 ⊢φ→b∈𝒫O|A∩b∈E∈L
9 8 7 jca ⊢φ→b∈𝒫O|A∩b∈E∈L∧T⊆b∈𝒫O|A∩b∈E
10 sseq2 ⊢t=b∈𝒫O|A∩b∈E→T⊆t↔T⊆b∈𝒫O|A∩b∈E
11 10 elrab ⊢b∈𝒫O|A∩b∈E∈t∈L|T⊆t↔b∈𝒫O|A∩b∈E∈L∧T⊆b∈𝒫O|A∩b∈E
12 9 11 sylibr ⊢φ→b∈𝒫O|A∩b∈E∈t∈L|T⊆t
13 intss1 ⊢b∈𝒫O|A∩b∈E∈t∈L|T⊆t→⋂t∈L|T⊆t⊆b∈𝒫O|A∩b∈E
14 12 13 syl ⊢φ→⋂t∈L|T⊆t⊆b∈𝒫O|A∩b∈E
15 4 14 eqsstrid ⊢φ→E⊆b∈𝒫O|A∩b∈E