Theorem ldgenpisyslem2

Description: Lemma for ldgenpisys . (Contributed by Thierry Arnoux, 18-Jul-2020)

	Ref	Expression
Hypotheses	dynkin.p	⊢ 𝑃 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( fi ‘ 𝑠 ) ⊆ 𝑠 }
	dynkin.l	⊢ 𝐿 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) }
	dynkin.o	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
	ldgenpisys.e	⊢ 𝐸 = ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 }
	ldgenpisys.1	⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
	ldgenpisyslem1.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐸 )
	ldgenpisyslem2.1	⊢ ( 𝜑 → 𝑇 ⊆ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } )
Assertion	ldgenpisyslem2	⊢ ( 𝜑 → 𝐸 ⊆ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } )

Proof

Step	Hyp	Ref	Expression
1		dynkin.p	⊢ 𝑃 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( fi ‘ 𝑠 ) ⊆ 𝑠 }
2		dynkin.l	⊢ 𝐿 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) }
3		dynkin.o	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
4		ldgenpisys.e	⊢ 𝐸 = ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 }
5		ldgenpisys.1	⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
6		ldgenpisyslem1.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐸 )
7		ldgenpisyslem2.1	⊢ ( 𝜑 → 𝑇 ⊆ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } )
8	1 2 3 4 5 6	ldgenpisyslem1	⊢ ( 𝜑 → { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ∈ 𝐿 )
9	8 7	jca	⊢ ( 𝜑 → ( { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ∈ 𝐿 ∧ 𝑇 ⊆ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) )
10		sseq2	⊢ ( 𝑡 = { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } → ( 𝑇 ⊆ 𝑡 ↔ 𝑇 ⊆ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) )
11	10	elrab	⊢ ( { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ∈ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 } ↔ ( { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ∈ 𝐿 ∧ 𝑇 ⊆ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ) )
12	9 11	sylibr	⊢ ( 𝜑 → { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ∈ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 } )
13		intss1	⊢ ( { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ∈ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 } → ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 } ⊆ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } )
14	12 13	syl	⊢ ( 𝜑 → ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 } ⊆ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } )
15	4 14	eqsstrid	⊢ ( 𝜑 → 𝐸 ⊆ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } )