Theorem ldgenpisys

Description: The lambda system E generated by a pi-system T is also a pi-system. (Contributed by Thierry Arnoux, 18-Jun-2020)

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

Proof

Step	Hyp	Ref	Expression
1		dynkin.p	⊢ 𝑃 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( fi ‘ 𝑠 ) ⊆ 𝑠 }
2		dynkin.l	⊢ 𝐿 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) }
3		dynkin.o	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
4		ldgenpisys.e	⊢ 𝐸 = ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 }
5		ldgenpisys.1	⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
6		ssrab2	⊢ { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) } ⊆ 𝒫 𝒫 𝑂
7		ssrab2	⊢ { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( fi ‘ 𝑠 ) ⊆ 𝑠 } ⊆ 𝒫 𝒫 𝑂
8	5 1	eleqtrdi	⊢ ( 𝜑 → 𝑇 ∈ { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( fi ‘ 𝑠 ) ⊆ 𝑠 } )
9	7 8	sselid	⊢ ( 𝜑 → 𝑇 ∈ 𝒫 𝒫 𝑂 )
10	9	elpwid	⊢ ( 𝜑 → 𝑇 ⊆ 𝒫 𝑂 )
11	2 3 10	ldsysgenld	⊢ ( 𝜑 → ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 } ∈ 𝐿 )
12	4 11	eqeltrid	⊢ ( 𝜑 → 𝐸 ∈ 𝐿 )
13	12 2	eleqtrdi	⊢ ( 𝜑 → 𝐸 ∈ { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) } )
14	6 13	sselid	⊢ ( 𝜑 → 𝐸 ∈ 𝒫 𝒫 𝑂 )
15		simprr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ) ) → 𝑏 ∈ 𝐸 )
16		simprl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ) ) → 𝑎 ∈ 𝐸 )
17	3	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) → 𝑂 ∈ 𝑉 )
18	5	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) → 𝑇 ∈ 𝑃 )
19		simpr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) → 𝑎 ∈ 𝐸 )
20	10	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) → 𝑇 ⊆ 𝒫 𝑂 )
21	20	sselda	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝑇 ) → 𝑏 ∈ 𝒫 𝑂 )
22		incom	⊢ ( 𝑏 ∩ 𝑎 ) = ( 𝑎 ∩ 𝑏 )
23	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝑇 ) → 𝑂 ∈ 𝑉 )
24	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝑇 ) → 𝑇 ∈ 𝑃 )
25		simpr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝑇 ) → 𝑏 ∈ 𝑇 )
26	1 2 23 4 24 25	ldgenpisyslem3	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝑇 ) → 𝐸 ⊆ { 𝑐 ∈ 𝒫 𝑂 ∣ ( 𝑏 ∩ 𝑐 ) ∈ 𝐸 } )
27		simplr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝑇 ) → 𝑎 ∈ 𝐸 )
28	26 27	sseldd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝑇 ) → 𝑎 ∈ { 𝑐 ∈ 𝒫 𝑂 ∣ ( 𝑏 ∩ 𝑐 ) ∈ 𝐸 } )
29		ineq2	⊢ ( 𝑐 = 𝑎 → ( 𝑏 ∩ 𝑐 ) = ( 𝑏 ∩ 𝑎 ) )
30	29	eleq1d	⊢ ( 𝑐 = 𝑎 → ( ( 𝑏 ∩ 𝑐 ) ∈ 𝐸 ↔ ( 𝑏 ∩ 𝑎 ) ∈ 𝐸 ) )
31	30	elrab	⊢ ( 𝑎 ∈ { 𝑐 ∈ 𝒫 𝑂 ∣ ( 𝑏 ∩ 𝑐 ) ∈ 𝐸 } ↔ ( 𝑎 ∈ 𝒫 𝑂 ∧ ( 𝑏 ∩ 𝑎 ) ∈ 𝐸 ) )
32	28 31	sylib	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝑇 ) → ( 𝑎 ∈ 𝒫 𝑂 ∧ ( 𝑏 ∩ 𝑎 ) ∈ 𝐸 ) )
33	32	simprd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝑇 ) → ( 𝑏 ∩ 𝑎 ) ∈ 𝐸 )
34	22 33	eqeltrrid	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝑇 ) → ( 𝑎 ∩ 𝑏 ) ∈ 𝐸 )
35	21 34	jca	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝑇 ) → ( 𝑏 ∈ 𝒫 𝑂 ∧ ( 𝑎 ∩ 𝑏 ) ∈ 𝐸 ) )
36		ineq2	⊢ ( 𝑐 = 𝑏 → ( 𝑎 ∩ 𝑐 ) = ( 𝑎 ∩ 𝑏 ) )
37	36	eleq1d	⊢ ( 𝑐 = 𝑏 → ( ( 𝑎 ∩ 𝑐 ) ∈ 𝐸 ↔ ( 𝑎 ∩ 𝑏 ) ∈ 𝐸 ) )
38	37	elrab	⊢ ( 𝑏 ∈ { 𝑐 ∈ 𝒫 𝑂 ∣ ( 𝑎 ∩ 𝑐 ) ∈ 𝐸 } ↔ ( 𝑏 ∈ 𝒫 𝑂 ∧ ( 𝑎 ∩ 𝑏 ) ∈ 𝐸 ) )
39	35 38	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝑇 ) → 𝑏 ∈ { 𝑐 ∈ 𝒫 𝑂 ∣ ( 𝑎 ∩ 𝑐 ) ∈ 𝐸 } )
40	39	ex	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) → ( 𝑏 ∈ 𝑇 → 𝑏 ∈ { 𝑐 ∈ 𝒫 𝑂 ∣ ( 𝑎 ∩ 𝑐 ) ∈ 𝐸 } ) )
41	40	ssrdv	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) → 𝑇 ⊆ { 𝑐 ∈ 𝒫 𝑂 ∣ ( 𝑎 ∩ 𝑐 ) ∈ 𝐸 } )
42	1 2 17 4 18 19 41	ldgenpisyslem2	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) → 𝐸 ⊆ { 𝑐 ∈ 𝒫 𝑂 ∣ ( 𝑎 ∩ 𝑐 ) ∈ 𝐸 } )
43	16 42	syldan	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ) ) → 𝐸 ⊆ { 𝑐 ∈ 𝒫 𝑂 ∣ ( 𝑎 ∩ 𝑐 ) ∈ 𝐸 } )
44		ssrab	⊢ ( 𝐸 ⊆ { 𝑐 ∈ 𝒫 𝑂 ∣ ( 𝑎 ∩ 𝑐 ) ∈ 𝐸 } ↔ ( 𝐸 ⊆ 𝒫 𝑂 ∧ ∀ 𝑐 ∈ 𝐸 ( 𝑎 ∩ 𝑐 ) ∈ 𝐸 ) )
45	43 44	sylib	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ) ) → ( 𝐸 ⊆ 𝒫 𝑂 ∧ ∀ 𝑐 ∈ 𝐸 ( 𝑎 ∩ 𝑐 ) ∈ 𝐸 ) )
46	45	simprd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ) ) → ∀ 𝑐 ∈ 𝐸 ( 𝑎 ∩ 𝑐 ) ∈ 𝐸 )
47	37	rspcv	⊢ ( 𝑏 ∈ 𝐸 → ( ∀ 𝑐 ∈ 𝐸 ( 𝑎 ∩ 𝑐 ) ∈ 𝐸 → ( 𝑎 ∩ 𝑏 ) ∈ 𝐸 ) )
48	15 46 47	sylc	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ) ) → ( 𝑎 ∩ 𝑏 ) ∈ 𝐸 )
49	48	ralrimivva	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐸 ∀ 𝑏 ∈ 𝐸 ( 𝑎 ∩ 𝑏 ) ∈ 𝐸 )
50		inficl	⊢ ( 𝐸 ∈ 𝐿 → ( ∀ 𝑎 ∈ 𝐸 ∀ 𝑏 ∈ 𝐸 ( 𝑎 ∩ 𝑏 ) ∈ 𝐸 ↔ ( fi ‘ 𝐸 ) = 𝐸 ) )
51	12 50	syl	⊢ ( 𝜑 → ( ∀ 𝑎 ∈ 𝐸 ∀ 𝑏 ∈ 𝐸 ( 𝑎 ∩ 𝑏 ) ∈ 𝐸 ↔ ( fi ‘ 𝐸 ) = 𝐸 ) )
52	49 51	mpbid	⊢ ( 𝜑 → ( fi ‘ 𝐸 ) = 𝐸 )
53		eqimss	⊢ ( ( fi ‘ 𝐸 ) = 𝐸 → ( fi ‘ 𝐸 ) ⊆ 𝐸 )
54	52 53	syl	⊢ ( 𝜑 → ( fi ‘ 𝐸 ) ⊆ 𝐸 )
55	14 54	jca	⊢ ( 𝜑 → ( 𝐸 ∈ 𝒫 𝒫 𝑂 ∧ ( fi ‘ 𝐸 ) ⊆ 𝐸 ) )
56	1	ispisys	⊢ ( 𝐸 ∈ 𝑃 ↔ ( 𝐸 ∈ 𝒫 𝒫 𝑂 ∧ ( fi ‘ 𝐸 ) ⊆ 𝐸 ) )
57	55 56	sylibr	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )