Theorem sigapildsyslem

Description: Lemma for sigapildsys . (Contributed by Thierry Arnoux, 13-Jun-2020)

	Ref	Expression
Hypotheses	dynkin.p	⊢ 𝑃 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( fi ‘ 𝑠 ) ⊆ 𝑠 }
	dynkin.l	⊢ 𝐿 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) }
	sigapildsyslem.n	⊢ Ⅎ 𝑛 𝜑
	sigapildsyslem.1	⊢ ( 𝜑 → 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) )
	sigapildsyslem.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑡 )
	sigapildsyslem.3	⊢ ( 𝜑 → 𝑁 ∈ Fin )
	sigapildsyslem.4	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → 𝐵 ∈ 𝑡 )
Assertion	sigapildsyslem	⊢ ( 𝜑 → ( 𝐴 ∖ ∪ 𝑛 ∈ 𝑁 𝐵 ) ∈ 𝑡 )

Proof

Step	Hyp	Ref	Expression
1		dynkin.p	⊢ 𝑃 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( fi ‘ 𝑠 ) ⊆ 𝑠 }
2		dynkin.l	⊢ 𝐿 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) }
3		sigapildsyslem.n	⊢ Ⅎ 𝑛 𝜑
4		sigapildsyslem.1	⊢ ( 𝜑 → 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) )
5		sigapildsyslem.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑡 )
6		sigapildsyslem.3	⊢ ( 𝜑 → 𝑁 ∈ Fin )
7		sigapildsyslem.4	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → 𝐵 ∈ 𝑡 )
8		iuneq1	⊢ ( 𝑁 = ∅ → ∪ 𝑛 ∈ 𝑁 𝐵 = ∪ 𝑛 ∈ ∅ 𝐵 )
9		0iun	⊢ ∪ 𝑛 ∈ ∅ 𝐵 = ∅
10	8 9	eqtrdi	⊢ ( 𝑁 = ∅ → ∪ 𝑛 ∈ 𝑁 𝐵 = ∅ )
11	10	difeq2d	⊢ ( 𝑁 = ∅ → ( 𝐴 ∖ ∪ 𝑛 ∈ 𝑁 𝐵 ) = ( 𝐴 ∖ ∅ ) )
12		dif0	⊢ ( 𝐴 ∖ ∅ ) = 𝐴
13	11 12	eqtrdi	⊢ ( 𝑁 = ∅ → ( 𝐴 ∖ ∪ 𝑛 ∈ 𝑁 𝐵 ) = 𝐴 )
14	13	adantl	⊢ ( ( 𝜑 ∧ 𝑁 = ∅ ) → ( 𝐴 ∖ ∪ 𝑛 ∈ 𝑁 𝐵 ) = 𝐴 )
15	5	adantr	⊢ ( ( 𝜑 ∧ 𝑁 = ∅ ) → 𝐴 ∈ 𝑡 )
16	14 15	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑁 = ∅ ) → ( 𝐴 ∖ ∪ 𝑛 ∈ 𝑁 𝐵 ) ∈ 𝑡 )
17		iindif2	⊢ ( 𝑁 ≠ ∅ → ∩ 𝑛 ∈ 𝑁 ( 𝐴 ∖ 𝐵 ) = ( 𝐴 ∖ ∪ 𝑛 ∈ 𝑁 𝐵 ) )
18	17	adantl	⊢ ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) → ∩ 𝑛 ∈ 𝑁 ( 𝐴 ∖ 𝐵 ) = ( 𝐴 ∖ ∪ 𝑛 ∈ 𝑁 𝐵 ) )
19	4	adantr	⊢ ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) → 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) )
20	19	elin1d	⊢ ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) → 𝑡 ∈ 𝑃 )
21	1	ispisys	⊢ ( 𝑡 ∈ 𝑃 ↔ ( 𝑡 ∈ 𝒫 𝒫 𝑂 ∧ ( fi ‘ 𝑡 ) ⊆ 𝑡 ) )
22	20 21	sylib	⊢ ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) → ( 𝑡 ∈ 𝒫 𝒫 𝑂 ∧ ( fi ‘ 𝑡 ) ⊆ 𝑡 ) )
23	22	simprd	⊢ ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) → ( fi ‘ 𝑡 ) ⊆ 𝑡 )
24		nfv	⊢ Ⅎ 𝑛 𝑁 ≠ ∅
25	3 24	nfan	⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑁 ≠ ∅ )
26	22	simpld	⊢ ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) → 𝑡 ∈ 𝒫 𝒫 𝑂 )
27	26	elpwid	⊢ ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) → 𝑡 ⊆ 𝒫 𝑂 )
28	5	adantr	⊢ ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) → 𝐴 ∈ 𝑡 )
29	27 28	sseldd	⊢ ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) → 𝐴 ∈ 𝒫 𝑂 )
30	29	elpwid	⊢ ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) → 𝐴 ⊆ 𝑂 )
31	30	adantr	⊢ ( ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) ∧ 𝑛 ∈ 𝑁 ) → 𝐴 ⊆ 𝑂 )
32		difin2	⊢ ( 𝐴 ⊆ 𝑂 → ( 𝐴 ∖ 𝐵 ) = ( ( 𝑂 ∖ 𝐵 ) ∩ 𝐴 ) )
33	31 32	syl	⊢ ( ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) ∧ 𝑛 ∈ 𝑁 ) → ( 𝐴 ∖ 𝐵 ) = ( ( 𝑂 ∖ 𝐵 ) ∩ 𝐴 ) )
34	23	adantr	⊢ ( ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) ∧ 𝑛 ∈ 𝑁 ) → ( fi ‘ 𝑡 ) ⊆ 𝑡 )
35	19	adantr	⊢ ( ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) ∧ 𝑛 ∈ 𝑁 ) → 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) )
36	19	elin2d	⊢ ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) → 𝑡 ∈ 𝐿 )
37	2	isldsys	⊢ ( 𝑡 ∈ 𝐿 ↔ ( 𝑡 ∈ 𝒫 𝒫 𝑂 ∧ ( ∅ ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝒫 𝑡 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) ) ) )
38	36 37	sylib	⊢ ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) → ( 𝑡 ∈ 𝒫 𝒫 𝑂 ∧ ( ∅ ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝒫 𝑡 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) ) ) )
39	38	simprd	⊢ ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) → ( ∅ ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝒫 𝑡 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) ) )
40	39	simp2d	⊢ ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) → ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 )
41	40	adantr	⊢ ( ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) ∧ 𝑛 ∈ 𝑁 ) → ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 )
42	7	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) ∧ 𝑛 ∈ 𝑁 ) → 𝐵 ∈ 𝑡 )
43		nfv	⊢ Ⅎ 𝑥 ( 𝑂 ∖ 𝐵 ) ∈ 𝑡
44		difeq2	⊢ ( 𝑥 = 𝐵 → ( 𝑂 ∖ 𝑥 ) = ( 𝑂 ∖ 𝐵 ) )
45	44	eleq1d	⊢ ( 𝑥 = 𝐵 → ( ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ↔ ( 𝑂 ∖ 𝐵 ) ∈ 𝑡 ) )
46	43 45	rspc	⊢ ( 𝐵 ∈ 𝑡 → ( ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 → ( 𝑂 ∖ 𝐵 ) ∈ 𝑡 ) )
47	42 46	syl	⊢ ( ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) ∧ 𝑛 ∈ 𝑁 ) → ( ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 → ( 𝑂 ∖ 𝐵 ) ∈ 𝑡 ) )
48	41 47	mpd	⊢ ( ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) ∧ 𝑛 ∈ 𝑁 ) → ( 𝑂 ∖ 𝐵 ) ∈ 𝑡 )
49	28	adantr	⊢ ( ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) ∧ 𝑛 ∈ 𝑁 ) → 𝐴 ∈ 𝑡 )
50		inelfi	⊢ ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ ( 𝑂 ∖ 𝐵 ) ∈ 𝑡 ∧ 𝐴 ∈ 𝑡 ) → ( ( 𝑂 ∖ 𝐵 ) ∩ 𝐴 ) ∈ ( fi ‘ 𝑡 ) )
51	35 48 49 50	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) ∧ 𝑛 ∈ 𝑁 ) → ( ( 𝑂 ∖ 𝐵 ) ∩ 𝐴 ) ∈ ( fi ‘ 𝑡 ) )
52	34 51	sseldd	⊢ ( ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) ∧ 𝑛 ∈ 𝑁 ) → ( ( 𝑂 ∖ 𝐵 ) ∩ 𝐴 ) ∈ 𝑡 )
53	33 52	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) ∧ 𝑛 ∈ 𝑁 ) → ( 𝐴 ∖ 𝐵 ) ∈ 𝑡 )
54	53	ex	⊢ ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) → ( 𝑛 ∈ 𝑁 → ( 𝐴 ∖ 𝐵 ) ∈ 𝑡 ) )
55	25 54	ralrimi	⊢ ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) → ∀ 𝑛 ∈ 𝑁 ( 𝐴 ∖ 𝐵 ) ∈ 𝑡 )
56		simpr	⊢ ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) → 𝑁 ≠ ∅ )
57	6	adantr	⊢ ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) → 𝑁 ∈ Fin )
58		vex	⊢ 𝑡 ∈ V
59		iinfi	⊢ ( ( 𝑡 ∈ V ∧ ( ∀ 𝑛 ∈ 𝑁 ( 𝐴 ∖ 𝐵 ) ∈ 𝑡 ∧ 𝑁 ≠ ∅ ∧ 𝑁 ∈ Fin ) ) → ∩ 𝑛 ∈ 𝑁 ( 𝐴 ∖ 𝐵 ) ∈ ( fi ‘ 𝑡 ) )
60	58 59	mpan	⊢ ( ( ∀ 𝑛 ∈ 𝑁 ( 𝐴 ∖ 𝐵 ) ∈ 𝑡 ∧ 𝑁 ≠ ∅ ∧ 𝑁 ∈ Fin ) → ∩ 𝑛 ∈ 𝑁 ( 𝐴 ∖ 𝐵 ) ∈ ( fi ‘ 𝑡 ) )
61	55 56 57 60	syl3anc	⊢ ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) → ∩ 𝑛 ∈ 𝑁 ( 𝐴 ∖ 𝐵 ) ∈ ( fi ‘ 𝑡 ) )
62	23 61	sseldd	⊢ ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) → ∩ 𝑛 ∈ 𝑁 ( 𝐴 ∖ 𝐵 ) ∈ 𝑡 )
63	18 62	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑁 ≠ ∅ ) → ( 𝐴 ∖ ∪ 𝑛 ∈ 𝑁 𝐵 ) ∈ 𝑡 )
64	16 63	pm2.61dane	⊢ ( 𝜑 → ( 𝐴 ∖ ∪ 𝑛 ∈ 𝑁 𝐵 ) ∈ 𝑡 )