Metamath Proof Explorer


Theorem sigapildsyslem

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

Ref Expression
Hypotheses dynkin.p P = s 𝒫 𝒫 O | fi s s
dynkin.l L = s 𝒫 𝒫 O | s x s O x s x 𝒫 s x ω Disj y x y x s
sigapildsyslem.n n φ
sigapildsyslem.1 φ t P L
sigapildsyslem.2 φ A t
sigapildsyslem.3 φ N Fin
sigapildsyslem.4 φ n N B t
Assertion sigapildsyslem φ A n N B t

Proof

Step Hyp Ref Expression
1 dynkin.p P = s 𝒫 𝒫 O | fi s s
2 dynkin.l L = s 𝒫 𝒫 O | s x s O x s x 𝒫 s x ω Disj y x y x s
3 sigapildsyslem.n n φ
4 sigapildsyslem.1 φ t P L
5 sigapildsyslem.2 φ A t
6 sigapildsyslem.3 φ N Fin
7 sigapildsyslem.4 φ n N B t
8 iuneq1 N = n N B = n B
9 0iun n B =
10 8 9 syl6eq N = n N B =
11 10 difeq2d N = A n N B = A
12 dif0 A = A
13 11 12 syl6eq N = A n N B = A
14 13 adantl φ N = A n N B = A
15 5 adantr φ N = A t
16 14 15 eqeltrd φ N = A n N B t
17 iindif2 N n N A B = A n N B
18 17 adantl φ N n N A B = A n N B
19 4 adantr φ N t P L
20 19 elin1d φ N t P
21 1 ispisys t P t 𝒫 𝒫 O fi t t
22 20 21 sylib φ N t 𝒫 𝒫 O fi t t
23 22 simprd φ N fi t t
24 nfv n N
25 3 24 nfan n φ N
26 22 simpld φ N t 𝒫 𝒫 O
27 26 elpwid φ N t 𝒫 O
28 5 adantr φ N A t
29 27 28 sseldd φ N A 𝒫 O
30 29 elpwid φ N A O
31 30 adantr φ N n N A O
32 difin2 A O A B = O B A
33 31 32 syl φ N n N A B = O B A
34 23 adantr φ N n N fi t t
35 19 adantr φ N n N t P L
36 19 elin2d φ N t L
37 2 isldsys t L t 𝒫 𝒫 O t x t O x t x 𝒫 t x ω Disj y x y x t
38 36 37 sylib φ N t 𝒫 𝒫 O t x t O x t x 𝒫 t x ω Disj y x y x t
39 38 simprd φ N t x t O x t x 𝒫 t x ω Disj y x y x t
40 39 simp2d φ N x t O x t
41 40 adantr φ N n N x t O x t
42 7 adantlr φ N n N B t
43 nfv x O B t
44 difeq2 x = B O x = O B
45 44 eleq1d x = B O x t O B t
46 43 45 rspc B t x t O x t O B t
47 42 46 syl φ N n N x t O x t O B t
48 41 47 mpd φ N n N O B t
49 28 adantr φ N n N A t
50 inelfi t P L O B t A t O B A fi t
51 35 48 49 50 syl3anc φ N n N O B A fi t
52 34 51 sseldd φ N n N O B A t
53 33 52 eqeltrd φ N n N A B t
54 53 ex φ N n N A B t
55 25 54 ralrimi φ N n N A B t
56 simpr φ N N
57 6 adantr φ N N Fin
58 vex t V
59 iinfi t V n N A B t N N Fin n N A B fi t
60 58 59 mpan n N A B t N N Fin n N A B fi t
61 55 56 57 60 syl3anc φ N n N A B fi t
62 23 61 sseldd φ N n N A B t
63 18 62 eqeltrrd φ N A n N B t
64 16 63 pm2.61dane φ A n N B t