Theorem ldgenpisyslem3

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	⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
	ldgenpisyslem3.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑇 )
Assertion	ldgenpisyslem3	⊢ ( 𝜑 → 𝐸 ⊆ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } )

Proof

Step	Hyp	Ref	Expression
1		dynkin.p	⊢ 𝑃 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( fi ‘ 𝑠 ) ⊆ 𝑠 }
2		dynkin.l	⊢ 𝐿 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) }
3		dynkin.o	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
4		ldgenpisys.e	⊢ 𝐸 = ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 }
5		ldgenpisys.1	⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
6		ldgenpisyslem3.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑇 )
7		id	⊢ ( 𝑇 ⊆ 𝑡 → 𝑇 ⊆ 𝑡 )
8	7	rgenw	⊢ ∀ 𝑡 ∈ 𝐿 ( 𝑇 ⊆ 𝑡 → 𝑇 ⊆ 𝑡 )
9		ssintrab	⊢ ( 𝑇 ⊆ ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 } ↔ ∀ 𝑡 ∈ 𝐿 ( 𝑇 ⊆ 𝑡 → 𝑇 ⊆ 𝑡 ) )
10	8 9	mpbir	⊢ 𝑇 ⊆ ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 }
11	10 4	sseqtrri	⊢ 𝑇 ⊆ 𝐸
12	11 6	sseldi	⊢ ( 𝜑 → 𝐴 ∈ 𝐸 )
13	1	ispisys	⊢ ( 𝑇 ∈ 𝑃 ↔ ( 𝑇 ∈ 𝒫 𝒫 𝑂 ∧ ( fi ‘ 𝑇 ) ⊆ 𝑇 ) )
14	5 13	sylib	⊢ ( 𝜑 → ( 𝑇 ∈ 𝒫 𝒫 𝑂 ∧ ( fi ‘ 𝑇 ) ⊆ 𝑇 ) )
15	14	simpld	⊢ ( 𝜑 → 𝑇 ∈ 𝒫 𝒫 𝑂 )
16		elpwi	⊢ ( 𝑇 ∈ 𝒫 𝒫 𝑂 → 𝑇 ⊆ 𝒫 𝑂 )
17	15 16	syl	⊢ ( 𝜑 → 𝑇 ⊆ 𝒫 𝑂 )
18	5	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑇 ) → 𝑇 ∈ 𝑃 )
19	6	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑇 ) → 𝐴 ∈ 𝑇 )
20		simpr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑇 ) → 𝑏 ∈ 𝑇 )
21	1	inelpisys	⊢ ( ( 𝑇 ∈ 𝑃 ∧ 𝐴 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ) → ( 𝐴 ∩ 𝑏 ) ∈ 𝑇 )
22	18 19 20 21	syl3anc	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑇 ) → ( 𝐴 ∩ 𝑏 ) ∈ 𝑇 )
23	11 22	sseldi	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑇 ) → ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 )
24	23	ralrimiva	⊢ ( 𝜑 → ∀ 𝑏 ∈ 𝑇 ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 )
25	17 24	jca	⊢ ( 𝜑 → ( 𝑇 ⊆ 𝒫 𝑂 ∧ ∀ 𝑏 ∈ 𝑇 ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 ) )
26		ssrab	⊢ ( 𝑇 ⊆ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } ↔ ( 𝑇 ⊆ 𝒫 𝑂 ∧ ∀ 𝑏 ∈ 𝑇 ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 ) )
27	25 26	sylibr	⊢ ( 𝜑 → 𝑇 ⊆ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } )
28	1 2 3 4 5 12 27	ldgenpisyslem2	⊢ ( 𝜑 → 𝐸 ⊆ { 𝑏 ∈ 𝒫 𝑂 ∣ ( 𝐴 ∩ 𝑏 ) ∈ 𝐸 } )