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 ∈ 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
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 ∈ 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 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