Metamath Proof Explorer

Theorem sigapildsyslem

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

Ref Expression
Hypotheses dynkin.p 
|- P = { s e. ~P ~P O | ( fi ` s ) C_ s }
dynkin.l 
|- L = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. s ) ) }
sigapildsyslem.n 
|- F/ n ph
sigapildsyslem.1 
|- ( ph -> t e. ( P i^i L ) )
sigapildsyslem.2 
|- ( ph -> A e. t )
sigapildsyslem.3 
|- ( ph -> N e. Fin )
sigapildsyslem.4 
|- ( ( ph /\ n e. N ) -> B e. t )
Assertion sigapildsyslem 
|- ( ph -> ( A \ U_ n e. N B ) e. t )

Proof

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