Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ldsysgenld Structured version   Visualization version   Unicode version

Theorem ldsysgenld 29031
Description: The intersection of all lambda-systems containing a given collection of sets  A, which is called the lambda-system generated by  A, is itself also a lambda-system. (Contributed by Thierry Arnoux, 16-Jun-2020.)
Hypotheses
Ref Expression
isldsys.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
) ) }
ldsysgenld.1  |-  ( ph  ->  O  e.  V )
ldsysgenld.2  |-  ( ph  ->  A  C_  ~P O
)
Assertion
Ref Expression
ldsysgenld  |-  ( ph  ->  |^| { t  e.  L  |  A  C_  t }  e.  L
)
Distinct variable groups:    y, s    t, L    O, s, t, x   
x, V    y, t    A, s, t, x    L, s, x    ph, t, x
Allowed substitution hints:    ph( y, s)    A( y)    L( y)    O( y)    V( y, t, s)

Proof of Theorem ldsysgenld
Dummy variable  u is distinct from all other variables.
StepHypRef Expression
1 ldsysgenld.1 . . . . 5  |-  ( ph  ->  O  e.  V )
2 pwsiga 29001 . . . . 5  |-  ( O  e.  V  ->  ~P O  e.  (sigAlgebra `  O
) )
31, 2syl 17 . . . 4  |-  ( ph  ->  ~P O  e.  (sigAlgebra `  O ) )
4 isldsys.l . . . . . . . 8  |-  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
) ) }
54sigaldsys 29030 . . . . . . 7  |-  (sigAlgebra `  O
)  C_  L
65, 3sseldi 3442 . . . . . 6  |-  ( ph  ->  ~P O  e.  L
)
7 ldsysgenld.2 . . . . . 6  |-  ( ph  ->  A  C_  ~P O
)
8 sseq2 3466 . . . . . . 7  |-  ( t  =  ~P O  -> 
( A  C_  t  <->  A 
C_  ~P O ) )
98elrab 3208 . . . . . 6  |-  ( ~P O  e.  { t  e.  L  |  A  C_  t }  <->  ( ~P O  e.  L  /\  A  C_  ~P O ) )
106, 7, 9sylanbrc 675 . . . . 5  |-  ( ph  ->  ~P O  e.  {
t  e.  L  |  A  C_  t } )
11 intss1 4263 . . . . 5  |-  ( ~P O  e.  { t  e.  L  |  A  C_  t }  ->  |^| { t  e.  L  |  A  C_  t }  C_  ~P O )
1210, 11syl 17 . . . 4  |-  ( ph  ->  |^| { t  e.  L  |  A  C_  t }  C_  ~P O
)
133, 12sselpwd 28202 . . 3  |-  ( ph  ->  |^| { t  e.  L  |  A  C_  t }  e.  ~P ~P O )
144isldsys 29027 . . . . . . . . . 10  |-  ( 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 ) ) ) )
1514simprbi 470 . . . . . . . . 9  |-  ( t  e.  L  ->  ( (/) 
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
) ) )
1615simp1d 1026 . . . . . . . 8  |-  ( t  e.  L  ->  (/)  e.  t )
1716adantl 472 . . . . . . 7  |-  ( (
ph  /\  t  e.  L )  ->  (/)  e.  t )
1817a1d 26 . . . . . 6  |-  ( (
ph  /\  t  e.  L )  ->  ( A  C_  t  ->  (/)  e.  t ) )
1918ralrimiva 2814 . . . . 5  |-  ( ph  ->  A. t  e.  L  ( A  C_  t  ->  (/) 
e.  t ) )
20 0ex 4549 . . . . . 6  |-  (/)  e.  _V
2120elintrab 4260 . . . . 5  |-  ( (/)  e.  |^| { t  e.  L  |  A  C_  t }  <->  A. t  e.  L  ( A  C_  t  ->  (/) 
e.  t ) )
2219, 21sylibr 217 . . . 4  |-  ( ph  -> 
(/)  e.  |^| { t  e.  L  |  A  C_  t } )
23 nfv 1772 . . . . . . . 8  |-  F/ t
ph
24 nfcv 2603 . . . . . . . . 9  |-  F/_ t
x
25 nfrab1 2983 . . . . . . . . . 10  |-  F/_ t { t  e.  L  |  A  C_  t }
2625nfint 4258 . . . . . . . . 9  |-  F/_ t |^| { t  e.  L  |  A  C_  t }
2724, 26nfel 2615 . . . . . . . 8  |-  F/ t  x  e.  |^| { t  e.  L  |  A  C_  t }
2823, 27nfan 2022 . . . . . . 7  |-  F/ t ( ph  /\  x  e.  |^| { t  e.  L  |  A  C_  t } )
29 simplr 767 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  |^| { t  e.  L  |  A  C_  t } )  /\  t  e.  L )  /\  A  C_  t )  ->  t  e.  L
)
30 vex 3060 . . . . . . . . . . . . . . 15  |-  x  e. 
_V
3130elintrab 4260 . . . . . . . . . . . . . 14  |-  ( x  e.  |^| { t  e.  L  |  A  C_  t }  <->  A. t  e.  L  ( A  C_  t  ->  x  e.  t )
)
3231biimpi 199 . . . . . . . . . . . . 13  |-  ( x  e.  |^| { t  e.  L  |  A  C_  t }  ->  A. t  e.  L  ( A  C_  t  ->  x  e.  t ) )
3332adantl 472 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  |^|
{ t  e.  L  |  A  C_  t } )  ->  A. t  e.  L  ( A  C_  t  ->  x  e.  t ) )
3433r19.21bi 2769 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  |^| { t  e.  L  |  A  C_  t } )  /\  t  e.  L )  ->  ( A  C_  t  ->  x  e.  t ) )
3534imp 435 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  |^| { t  e.  L  |  A  C_  t } )  /\  t  e.  L )  /\  A  C_  t )  ->  x  e.  t )
3615simp2d 1027 . . . . . . . . . . 11  |-  ( t  e.  L  ->  A. x  e.  t  ( O  \  x )  e.  t )
3736r19.21bi 2769 . . . . . . . . . 10  |-  ( ( t  e.  L  /\  x  e.  t )  ->  ( O  \  x
)  e.  t )
3829, 35, 37syl2anc 671 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  |^| { t  e.  L  |  A  C_  t } )  /\  t  e.  L )  /\  A  C_  t )  ->  ( O  \  x )  e.  t )
3938ex 440 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  |^| { t  e.  L  |  A  C_  t } )  /\  t  e.  L )  ->  ( A  C_  t  ->  ( O  \  x )  e.  t ) )
4039ex 440 . . . . . . 7  |-  ( (
ph  /\  x  e.  |^|
{ t  e.  L  |  A  C_  t } )  ->  ( t  e.  L  ->  ( A 
C_  t  ->  ( O  \  x )  e.  t ) ) )
4128, 40ralrimi 2800 . . . . . 6  |-  ( (
ph  /\  x  e.  |^|
{ t  e.  L  |  A  C_  t } )  ->  A. t  e.  L  ( A  C_  t  ->  ( O  \  x )  e.  t ) )
42 difexg 4565 . . . . . . . 8  |-  ( O  e.  V  ->  ( O  \  x )  e. 
_V )
43 elintrabg 4261 . . . . . . . 8  |-  ( ( O  \  x )  e.  _V  ->  (
( O  \  x
)  e.  |^| { t  e.  L  |  A  C_  t }  <->  A. t  e.  L  ( A  C_  t  ->  ( O  \  x )  e.  t ) ) )
441, 42, 433syl 18 . . . . . . 7  |-  ( ph  ->  ( ( O  \  x )  e.  |^| { t  e.  L  |  A  C_  t }  <->  A. t  e.  L  ( A  C_  t  ->  ( O  \  x )  e.  t ) ) )
4544adantr 471 . . . . . 6  |-  ( (
ph  /\  x  e.  |^|
{ t  e.  L  |  A  C_  t } )  ->  ( ( O  \  x )  e. 
|^| { t  e.  L  |  A  C_  t }  <->  A. t  e.  L  ( A  C_  t  -> 
( O  \  x
)  e.  t ) ) )
4641, 45mpbird 240 . . . . 5  |-  ( (
ph  /\  x  e.  |^|
{ t  e.  L  |  A  C_  t } )  ->  ( O  \  x )  e.  |^| { t  e.  L  |  A  C_  t } )
4746ralrimiva 2814 . . . 4  |-  ( ph  ->  A. x  e.  |^| { t  e.  L  |  A  C_  t }  ( O  \  x )  e. 
|^| { t  e.  L  |  A  C_  t } )
4826nfpw 3975 . . . . . . . . . . 11  |-  F/_ t ~P |^| { t  e.  L  |  A  C_  t }
4924, 48nfel 2615 . . . . . . . . . 10  |-  F/ t  x  e.  ~P |^| { t  e.  L  |  A  C_  t }
5023, 49nfan 2022 . . . . . . . . 9  |-  F/ t ( ph  /\  x  e.  ~P |^| { t  e.  L  |  A  C_  t } )
51 nfv 1772 . . . . . . . . 9  |-  F/ t ( x  ~<_  om  /\ Disj  y  e.  x  y )
5250, 51nfan 2022 . . . . . . . 8  |-  F/ t ( ( ph  /\  x  e.  ~P |^| { t  e.  L  |  A  C_  t } )  /\  ( x  ~<_  om  /\ Disj  y  e.  x  y ) )
53 simplr 767 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  x  e.  ~P |^| { t  e.  L  |  A  C_  t } )  /\  ( x  ~<_  om 
/\ Disj  y  e.  x  y ) )  /\  t  e.  L )  /\  A  C_  t )  ->  t  e.  L )
54 simpr 467 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  x  e.  ~P |^| { t  e.  L  |  A  C_  t } )  /\  (
x  ~<_  om  /\ Disj  y  e.  x  y ) )  /\  t  e.  L
)  /\  A  C_  t
)  /\  u  e.  |^|
{ t  e.  L  |  A  C_  t } )  ->  u  e.  |^|
{ t  e.  L  |  A  C_  t } )
55 simpllr 774 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  x  e.  ~P |^| { t  e.  L  |  A  C_  t } )  /\  (
x  ~<_  om  /\ Disj  y  e.  x  y ) )  /\  t  e.  L
)  /\  A  C_  t
)  /\  u  e.  |^|
{ t  e.  L  |  A  C_  t } )  ->  t  e.  L )
56 simplr 767 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  x  e.  ~P |^| { t  e.  L  |  A  C_  t } )  /\  (
x  ~<_  om  /\ Disj  y  e.  x  y ) )  /\  t  e.  L
)  /\  A  C_  t
)  /\  u  e.  |^|
{ t  e.  L  |  A  C_  t } )  ->  A  C_  t
)
57 vex 3060 . . . . . . . . . . . . . . . . . . . 20  |-  u  e. 
_V
5857elintrab 4260 . . . . . . . . . . . . . . . . . . 19  |-  ( u  e.  |^| { t  e.  L  |  A  C_  t }  <->  A. t  e.  L  ( A  C_  t  ->  u  e.  t )
)
5958biimpi 199 . . . . . . . . . . . . . . . . . 18  |-  ( u  e.  |^| { t  e.  L  |  A  C_  t }  ->  A. t  e.  L  ( A  C_  t  ->  u  e.  t ) )
6059r19.21bi 2769 . . . . . . . . . . . . . . . . 17  |-  ( ( u  e.  |^| { t  e.  L  |  A  C_  t }  /\  t  e.  L )  ->  ( A  C_  t  ->  u  e.  t ) )
6160imp 435 . . . . . . . . . . . . . . . 16  |-  ( ( ( u  e.  |^| { t  e.  L  |  A  C_  t }  /\  t  e.  L )  /\  A  C_  t )  ->  u  e.  t )
6254, 55, 56, 61syl21anc 1275 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  x  e.  ~P |^| { t  e.  L  |  A  C_  t } )  /\  (
x  ~<_  om  /\ Disj  y  e.  x  y ) )  /\  t  e.  L
)  /\  A  C_  t
)  /\  u  e.  |^|
{ t  e.  L  |  A  C_  t } )  ->  u  e.  t )
6362ex 440 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  x  e.  ~P |^| { t  e.  L  |  A  C_  t } )  /\  ( x  ~<_  om 
/\ Disj  y  e.  x  y ) )  /\  t  e.  L )  /\  A  C_  t )  ->  (
u  e.  |^| { t  e.  L  |  A  C_  t }  ->  u  e.  t ) )
6463ssrdv 3450 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  x  e.  ~P |^| { t  e.  L  |  A  C_  t } )  /\  ( x  ~<_  om 
/\ Disj  y  e.  x  y ) )  /\  t  e.  L )  /\  A  C_  t )  ->  |^| { t  e.  L  |  A  C_  t }  C_  t
)
65 sspwb 4663 . . . . . . . . . . . . 13  |-  ( |^| { t  e.  L  |  A  C_  t }  C_  t 
<->  ~P |^| { t  e.  L  |  A  C_  t }  C_  ~P t )
6664, 65sylib 201 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  x  e.  ~P |^| { t  e.  L  |  A  C_  t } )  /\  ( x  ~<_  om 
/\ Disj  y  e.  x  y ) )  /\  t  e.  L )  /\  A  C_  t )  ->  ~P |^|
{ t  e.  L  |  A  C_  t } 
C_  ~P t )
67 simp-4r 782 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  x  e.  ~P |^| { t  e.  L  |  A  C_  t } )  /\  ( x  ~<_  om 
/\ Disj  y  e.  x  y ) )  /\  t  e.  L )  /\  A  C_  t )  ->  x  e.  ~P |^| { t  e.  L  |  A  C_  t } )
6866, 67sseldd 3445 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  x  e.  ~P |^| { t  e.  L  |  A  C_  t } )  /\  ( x  ~<_  om 
/\ Disj  y  e.  x  y ) )  /\  t  e.  L )  /\  A  C_  t )  ->  x  e.  ~P t )
69 simpllr 774 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  x  e.  ~P |^| { t  e.  L  |  A  C_  t } )  /\  ( x  ~<_  om 
/\ Disj  y  e.  x  y ) )  /\  t  e.  L )  /\  A  C_  t )  ->  (
x  ~<_  om  /\ Disj  y  e.  x  y ) )
7015simp3d 1028 . . . . . . . . . . . . 13  |-  ( t  e.  L  ->  A. x  e.  ~P  t ( ( x  ~<_  om  /\ Disj  y  e.  x  y )  ->  U. x  e.  t
) )
7170r19.21bi 2769 . . . . . . . . . . . 12  |-  ( ( t  e.  L  /\  x  e.  ~P t
)  ->  ( (
x  ~<_  om  /\ Disj  y  e.  x  y )  ->  U. x  e.  t
) )
7271imp 435 . . . . . . . . . . 11  |-  ( ( ( t  e.  L  /\  x  e.  ~P t )  /\  (
x  ~<_  om  /\ Disj  y  e.  x  y ) )  ->  U. x  e.  t )
7353, 68, 69, 72syl21anc 1275 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  x  e.  ~P |^| { t  e.  L  |  A  C_  t } )  /\  ( x  ~<_  om 
/\ Disj  y  e.  x  y ) )  /\  t  e.  L )  /\  A  C_  t )  ->  U. x  e.  t )
7473ex 440 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  ~P |^| { t  e.  L  |  A  C_  t } )  /\  ( x  ~<_  om  /\ Disj  y  e.  x  y ) )  /\  t  e.  L
)  ->  ( A  C_  t  ->  U. x  e.  t ) )
7574ex 440 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ~P |^| { t  e.  L  |  A  C_  t } )  /\  ( x  ~<_  om  /\ Disj  y  e.  x  y ) )  ->  ( t  e.  L  ->  ( A  C_  t  ->  U. x  e.  t ) ) )
7652, 75ralrimi 2800 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ~P |^| { t  e.  L  |  A  C_  t } )  /\  ( x  ~<_  om  /\ Disj  y  e.  x  y ) )  ->  A. t  e.  L  ( A  C_  t  ->  U. x  e.  t
) )
7730uniex 6614 . . . . . . . 8  |-  U. x  e.  _V
7877elintrab 4260 . . . . . . 7  |-  ( U. x  e.  |^| { t  e.  L  |  A  C_  t }  <->  A. t  e.  L  ( A  C_  t  ->  U. x  e.  t ) )
7976, 78sylibr 217 . . . . . 6  |-  ( ( ( ph  /\  x  e.  ~P |^| { t  e.  L  |  A  C_  t } )  /\  ( x  ~<_  om  /\ Disj  y  e.  x  y ) )  ->  U. x  e.  |^| { t  e.  L  |  A  C_  t } )
8079ex 440 . . . . 5  |-  ( (
ph  /\  x  e.  ~P |^| { t  e.  L  |  A  C_  t } )  ->  (
( x  ~<_  om  /\ Disj  y  e.  x  y )  ->  U. x  e.  |^| { t  e.  L  |  A  C_  t } ) )
8180ralrimiva 2814 . . . 4  |-  ( ph  ->  A. x  e.  ~P  |^|
{ t  e.  L  |  A  C_  t }  ( ( x  ~<_  om 
/\ Disj  y  e.  x  y )  ->  U. x  e.  |^| { t  e.  L  |  A  C_  t } ) )
8222, 47, 813jca 1194 . . 3  |-  ( ph  ->  ( (/)  e.  |^| { t  e.  L  |  A  C_  t }  /\  A. x  e.  |^| { t  e.  L  |  A  C_  t }  ( O 
\  x )  e. 
|^| { t  e.  L  |  A  C_  t }  /\  A. x  e. 
~P  |^| { t  e.  L  |  A  C_  t }  ( (
x  ~<_  om  /\ Disj  y  e.  x  y )  ->  U. x  e.  |^| { t  e.  L  |  A  C_  t } ) ) )
8313, 82jca 539 . 2  |-  ( ph  ->  ( |^| { t  e.  L  |  A  C_  t }  e.  ~P ~P O  /\  ( (/) 
e.  |^| { t  e.  L  |  A  C_  t }  /\  A. x  e.  |^| { t  e.  L  |  A  C_  t }  ( O  \  x )  e.  |^| { t  e.  L  |  A  C_  t }  /\  A. x  e.  ~P  |^| { t  e.  L  |  A  C_  t }  (
( x  ~<_  om  /\ Disj  y  e.  x  y )  ->  U. x  e.  |^| { t  e.  L  |  A  C_  t } ) ) ) )
844isldsys 29027 . 2  |-  ( |^| { t  e.  L  |  A  C_  t }  e.  L 
<->  ( |^| { t  e.  L  |  A  C_  t }  e.  ~P ~P O  /\  ( (/) 
e.  |^| { t  e.  L  |  A  C_  t }  /\  A. x  e.  |^| { t  e.  L  |  A  C_  t }  ( O  \  x )  e.  |^| { t  e.  L  |  A  C_  t }  /\  A. x  e.  ~P  |^| { t  e.  L  |  A  C_  t }  (
( x  ~<_  om  /\ Disj  y  e.  x  y )  ->  U. x  e.  |^| { t  e.  L  |  A  C_  t } ) ) ) )
8583, 84sylibr 217 1  |-  ( ph  ->  |^| { t  e.  L  |  A  C_  t }  e.  L
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375    /\ w3a 991    = wceq 1455    e. wcel 1898   A.wral 2749   {crab 2753   _Vcvv 3057    \ cdif 3413    C_ wss 3416   (/)c0 3743   ~Pcpw 3963   U.cuni 4212   |^|cint 4248  Disj wdisj 4387   class class class wbr 4416   ` cfv 5601   omcom 6719    ~<_ cdom 7593  sigAlgebracsiga 28978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4529  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-inf2 8172  ax-ac2 8919
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-fal 1461  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-iin 4295  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-se 4813  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-isom 5610  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-om 6720  df-1st 6820  df-2nd 6821  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-1o 7208  df-2o 7209  df-oadd 7212  df-er 7389  df-map 7500  df-en 7596  df-dom 7597  df-sdom 7598  df-fin 7599  df-oi 8051  df-card 8399  df-acn 8402  df-ac 8573  df-cda 8624  df-siga 28979
This theorem is referenced by:  ldgenpisys  29037  dynkin  29038
  Copyright terms: Public domain W3C validator