# Metamath Proof Explorer

## Theorem sigapildsyslem

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

Ref Expression
Hypotheses dynkin.p ${⊢}{P}=\left\{{s}\in 𝒫𝒫{O}|\mathrm{fi}\left({s}\right)\subseteq {s}\right\}$
dynkin.l ${⊢}{L}=\left\{{s}\in 𝒫𝒫{O}|\left(\varnothing \in {s}\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}{O}\setminus {x}\in {s}\wedge \forall {x}\in 𝒫{s}\phantom{\rule{.4em}{0ex}}\left(\left({x}\preccurlyeq \mathrm{\omega }\wedge \underset{{y}\in {x}}{Disj}{y}\right)\to \bigcup {x}\in {s}\right)\right)\right\}$
sigapildsyslem.n ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}{\phi }$
sigapildsyslem.1 ${⊢}{\phi }\to {t}\in \left({P}\cap {L}\right)$
sigapildsyslem.2 ${⊢}{\phi }\to {A}\in {t}$
sigapildsyslem.3 ${⊢}{\phi }\to {N}\in \mathrm{Fin}$
sigapildsyslem.4 ${⊢}\left({\phi }\wedge {n}\in {N}\right)\to {B}\in {t}$
Assertion sigapildsyslem ${⊢}{\phi }\to {A}\setminus \bigcup _{{n}\in {N}}{B}\in {t}$

### Proof

Step Hyp Ref Expression
1 dynkin.p ${⊢}{P}=\left\{{s}\in 𝒫𝒫{O}|\mathrm{fi}\left({s}\right)\subseteq {s}\right\}$
2 dynkin.l ${⊢}{L}=\left\{{s}\in 𝒫𝒫{O}|\left(\varnothing \in {s}\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}{O}\setminus {x}\in {s}\wedge \forall {x}\in 𝒫{s}\phantom{\rule{.4em}{0ex}}\left(\left({x}\preccurlyeq \mathrm{\omega }\wedge \underset{{y}\in {x}}{Disj}{y}\right)\to \bigcup {x}\in {s}\right)\right)\right\}$
3 sigapildsyslem.n ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}{\phi }$
4 sigapildsyslem.1 ${⊢}{\phi }\to {t}\in \left({P}\cap {L}\right)$
5 sigapildsyslem.2 ${⊢}{\phi }\to {A}\in {t}$
6 sigapildsyslem.3 ${⊢}{\phi }\to {N}\in \mathrm{Fin}$
7 sigapildsyslem.4 ${⊢}\left({\phi }\wedge {n}\in {N}\right)\to {B}\in {t}$
8 iuneq1 ${⊢}{N}=\varnothing \to \bigcup _{{n}\in {N}}{B}=\bigcup _{{n}\in \varnothing }{B}$
9 0iun ${⊢}\bigcup _{{n}\in \varnothing }{B}=\varnothing$
10 8 9 syl6eq ${⊢}{N}=\varnothing \to \bigcup _{{n}\in {N}}{B}=\varnothing$
11 10 difeq2d ${⊢}{N}=\varnothing \to {A}\setminus \bigcup _{{n}\in {N}}{B}={A}\setminus \varnothing$
12 dif0 ${⊢}{A}\setminus \varnothing ={A}$
13 11 12 syl6eq ${⊢}{N}=\varnothing \to {A}\setminus \bigcup _{{n}\in {N}}{B}={A}$
14 13 adantl ${⊢}\left({\phi }\wedge {N}=\varnothing \right)\to {A}\setminus \bigcup _{{n}\in {N}}{B}={A}$
15 5 adantr ${⊢}\left({\phi }\wedge {N}=\varnothing \right)\to {A}\in {t}$
16 14 15 eqeltrd ${⊢}\left({\phi }\wedge {N}=\varnothing \right)\to {A}\setminus \bigcup _{{n}\in {N}}{B}\in {t}$
17 iindif2 ${⊢}{N}\ne \varnothing \to \bigcap _{{n}\in {N}}\left({A}\setminus {B}\right)={A}\setminus \bigcup _{{n}\in {N}}{B}$
18 17 adantl ${⊢}\left({\phi }\wedge {N}\ne \varnothing \right)\to \bigcap _{{n}\in {N}}\left({A}\setminus {B}\right)={A}\setminus \bigcup _{{n}\in {N}}{B}$
19 4 adantr ${⊢}\left({\phi }\wedge {N}\ne \varnothing \right)\to {t}\in \left({P}\cap {L}\right)$
20 19 elin1d ${⊢}\left({\phi }\wedge {N}\ne \varnothing \right)\to {t}\in {P}$
21 1 ispisys ${⊢}{t}\in {P}↔\left({t}\in 𝒫𝒫{O}\wedge \mathrm{fi}\left({t}\right)\subseteq {t}\right)$
22 20 21 sylib ${⊢}\left({\phi }\wedge {N}\ne \varnothing \right)\to \left({t}\in 𝒫𝒫{O}\wedge \mathrm{fi}\left({t}\right)\subseteq {t}\right)$
23 22 simprd ${⊢}\left({\phi }\wedge {N}\ne \varnothing \right)\to \mathrm{fi}\left({t}\right)\subseteq {t}$
24 nfv ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}{N}\ne \varnothing$
25 3 24 nfan ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {N}\ne \varnothing \right)$
26 22 simpld ${⊢}\left({\phi }\wedge {N}\ne \varnothing \right)\to {t}\in 𝒫𝒫{O}$
27 26 elpwid ${⊢}\left({\phi }\wedge {N}\ne \varnothing \right)\to {t}\subseteq 𝒫{O}$
28 5 adantr ${⊢}\left({\phi }\wedge {N}\ne \varnothing \right)\to {A}\in {t}$
29 27 28 sseldd ${⊢}\left({\phi }\wedge {N}\ne \varnothing \right)\to {A}\in 𝒫{O}$
30 29 elpwid ${⊢}\left({\phi }\wedge {N}\ne \varnothing \right)\to {A}\subseteq {O}$
31 30 adantr ${⊢}\left(\left({\phi }\wedge {N}\ne \varnothing \right)\wedge {n}\in {N}\right)\to {A}\subseteq {O}$
32 difin2 ${⊢}{A}\subseteq {O}\to {A}\setminus {B}=\left({O}\setminus {B}\right)\cap {A}$
33 31 32 syl ${⊢}\left(\left({\phi }\wedge {N}\ne \varnothing \right)\wedge {n}\in {N}\right)\to {A}\setminus {B}=\left({O}\setminus {B}\right)\cap {A}$
34 23 adantr ${⊢}\left(\left({\phi }\wedge {N}\ne \varnothing \right)\wedge {n}\in {N}\right)\to \mathrm{fi}\left({t}\right)\subseteq {t}$
35 19 adantr ${⊢}\left(\left({\phi }\wedge {N}\ne \varnothing \right)\wedge {n}\in {N}\right)\to {t}\in \left({P}\cap {L}\right)$
36 19 elin2d ${⊢}\left({\phi }\wedge {N}\ne \varnothing \right)\to {t}\in {L}$
37 2 isldsys ${⊢}{t}\in {L}↔\left({t}\in 𝒫𝒫{O}\wedge \left(\varnothing \in {t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}{O}\setminus {x}\in {t}\wedge \forall {x}\in 𝒫{t}\phantom{\rule{.4em}{0ex}}\left(\left({x}\preccurlyeq \mathrm{\omega }\wedge \underset{{y}\in {x}}{Disj}{y}\right)\to \bigcup {x}\in {t}\right)\right)\right)$
38 36 37 sylib ${⊢}\left({\phi }\wedge {N}\ne \varnothing \right)\to \left({t}\in 𝒫𝒫{O}\wedge \left(\varnothing \in {t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}{O}\setminus {x}\in {t}\wedge \forall {x}\in 𝒫{t}\phantom{\rule{.4em}{0ex}}\left(\left({x}\preccurlyeq \mathrm{\omega }\wedge \underset{{y}\in {x}}{Disj}{y}\right)\to \bigcup {x}\in {t}\right)\right)\right)$
39 38 simprd ${⊢}\left({\phi }\wedge {N}\ne \varnothing \right)\to \left(\varnothing \in {t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}{O}\setminus {x}\in {t}\wedge \forall {x}\in 𝒫{t}\phantom{\rule{.4em}{0ex}}\left(\left({x}\preccurlyeq \mathrm{\omega }\wedge \underset{{y}\in {x}}{Disj}{y}\right)\to \bigcup {x}\in {t}\right)\right)$
40 39 simp2d ${⊢}\left({\phi }\wedge {N}\ne \varnothing \right)\to \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}{O}\setminus {x}\in {t}$
41 40 adantr ${⊢}\left(\left({\phi }\wedge {N}\ne \varnothing \right)\wedge {n}\in {N}\right)\to \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}{O}\setminus {x}\in {t}$
42 7 adantlr ${⊢}\left(\left({\phi }\wedge {N}\ne \varnothing \right)\wedge {n}\in {N}\right)\to {B}\in {t}$
43 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{O}\setminus {B}\in {t}$
44 difeq2 ${⊢}{x}={B}\to {O}\setminus {x}={O}\setminus {B}$
45 44 eleq1d ${⊢}{x}={B}\to \left({O}\setminus {x}\in {t}↔{O}\setminus {B}\in {t}\right)$
46 43 45 rspc ${⊢}{B}\in {t}\to \left(\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}{O}\setminus {x}\in {t}\to {O}\setminus {B}\in {t}\right)$
47 42 46 syl ${⊢}\left(\left({\phi }\wedge {N}\ne \varnothing \right)\wedge {n}\in {N}\right)\to \left(\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}{O}\setminus {x}\in {t}\to {O}\setminus {B}\in {t}\right)$
48 41 47 mpd ${⊢}\left(\left({\phi }\wedge {N}\ne \varnothing \right)\wedge {n}\in {N}\right)\to {O}\setminus {B}\in {t}$
49 28 adantr ${⊢}\left(\left({\phi }\wedge {N}\ne \varnothing \right)\wedge {n}\in {N}\right)\to {A}\in {t}$
50 inelfi ${⊢}\left({t}\in \left({P}\cap {L}\right)\wedge {O}\setminus {B}\in {t}\wedge {A}\in {t}\right)\to \left({O}\setminus {B}\right)\cap {A}\in \mathrm{fi}\left({t}\right)$
51 35 48 49 50 syl3anc ${⊢}\left(\left({\phi }\wedge {N}\ne \varnothing \right)\wedge {n}\in {N}\right)\to \left({O}\setminus {B}\right)\cap {A}\in \mathrm{fi}\left({t}\right)$
52 34 51 sseldd ${⊢}\left(\left({\phi }\wedge {N}\ne \varnothing \right)\wedge {n}\in {N}\right)\to \left({O}\setminus {B}\right)\cap {A}\in {t}$
53 33 52 eqeltrd ${⊢}\left(\left({\phi }\wedge {N}\ne \varnothing \right)\wedge {n}\in {N}\right)\to {A}\setminus {B}\in {t}$
54 53 ex ${⊢}\left({\phi }\wedge {N}\ne \varnothing \right)\to \left({n}\in {N}\to {A}\setminus {B}\in {t}\right)$
55 25 54 ralrimi ${⊢}\left({\phi }\wedge {N}\ne \varnothing \right)\to \forall {n}\in {N}\phantom{\rule{.4em}{0ex}}{A}\setminus {B}\in {t}$
56 simpr ${⊢}\left({\phi }\wedge {N}\ne \varnothing \right)\to {N}\ne \varnothing$
57 6 adantr ${⊢}\left({\phi }\wedge {N}\ne \varnothing \right)\to {N}\in \mathrm{Fin}$
58 vex ${⊢}{t}\in \mathrm{V}$
59 iinfi ${⊢}\left({t}\in \mathrm{V}\wedge \left(\forall {n}\in {N}\phantom{\rule{.4em}{0ex}}{A}\setminus {B}\in {t}\wedge {N}\ne \varnothing \wedge {N}\in \mathrm{Fin}\right)\right)\to \bigcap _{{n}\in {N}}\left({A}\setminus {B}\right)\in \mathrm{fi}\left({t}\right)$
60 58 59 mpan ${⊢}\left(\forall {n}\in {N}\phantom{\rule{.4em}{0ex}}{A}\setminus {B}\in {t}\wedge {N}\ne \varnothing \wedge {N}\in \mathrm{Fin}\right)\to \bigcap _{{n}\in {N}}\left({A}\setminus {B}\right)\in \mathrm{fi}\left({t}\right)$
61 55 56 57 60 syl3anc ${⊢}\left({\phi }\wedge {N}\ne \varnothing \right)\to \bigcap _{{n}\in {N}}\left({A}\setminus {B}\right)\in \mathrm{fi}\left({t}\right)$
62 23 61 sseldd ${⊢}\left({\phi }\wedge {N}\ne \varnothing \right)\to \bigcap _{{n}\in {N}}\left({A}\setminus {B}\right)\in {t}$
63 18 62 eqeltrrd ${⊢}\left({\phi }\wedge {N}\ne \varnothing \right)\to {A}\setminus \bigcup _{{n}\in {N}}{B}\in {t}$
64 16 63 pm2.61dane ${⊢}{\phi }\to {A}\setminus \bigcup _{{n}\in {N}}{B}\in {t}$