Metamath Proof Explorer

Theorem ldgenpisyslem3

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
ldgenpisyslem3.1 ⊢ φ → A ∈ T
Assertion ldgenpisyslem3 ⊢ φ → 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 ldgenpisyslem3.1 ⊢ φ → A ∈ T
7 id ⊢ T ⊆ t → T ⊆ t
8 7 rgenw ⊢ ∀ t ∈ L T ⊆ t → T ⊆ t
9 ssintrab ⊢ T ⊆ ⋂ t ∈ L | T ⊆ t ↔ ∀ t ∈ L T ⊆ t → T ⊆ t
10 8 9 mpbir ⊢ T ⊆ ⋂ t ∈ L | T ⊆ t
11 10 4 sseqtrri ⊢ T ⊆ E
12 11 6 sselid ⊢ φ → A ∈ E
13 1 ispisys ⊢ T ∈ P ↔ T ∈ 𝒫 𝒫 O ∧ fi ⁡ T ⊆ T
14 5 13 sylib ⊢ φ → T ∈ 𝒫 𝒫 O ∧ fi ⁡ T ⊆ T
15 14 simpld ⊢ φ → T ∈ 𝒫 𝒫 O
16 elpwi ⊢ T ∈ 𝒫 𝒫 O → T ⊆ 𝒫 O
17 15 16 syl ⊢ φ → T ⊆ 𝒫 O
18 5 adantr ⊢ φ ∧ b ∈ T → T ∈ P
19 6 adantr ⊢ φ ∧ b ∈ T → A ∈ T
20 simpr ⊢ φ ∧ b ∈ T → b ∈ T
21 1 inelpisys ⊢ T ∈ P ∧ A ∈ T ∧ b ∈ T → A ∩ b ∈ T
22 18 19 20 21 syl3anc ⊢ φ ∧ b ∈ T → A ∩ b ∈ T
23 11 22 sselid ⊢ φ ∧ b ∈ T → A ∩ b ∈ E
24 23 ralrimiva ⊢ φ → ∀ b ∈ T A ∩ b ∈ E
25 17 24 jca ⊢ φ → T ⊆ 𝒫 O ∧ ∀ b ∈ T A ∩ b ∈ E
26 ssrab ⊢ T ⊆ b ∈ 𝒫 O | A ∩ b ∈ E ↔ T ⊆ 𝒫 O ∧ ∀ b ∈ T A ∩ b ∈ E
27 25 26 sylibr ⊢ φ → T ⊆ b ∈ 𝒫 O | A ∩ b ∈ E
28 1 2 3 4 5 12 27 ldgenpisyslem2 ⊢ φ → E ⊆ b ∈ 𝒫 O | A ∩ b ∈ E