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

Theorem ldsysgenld 30351
 Description: The intersection of all lambda-systems containing a given collection of sets 𝐴, which is called the lambda-system generated by 𝐴, is itself also a lambda-system. (Contributed by Thierry Arnoux, 16-Jun-2020.)
Hypotheses
Ref Expression
isldsys.l 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥𝑠 (𝑂𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑠))}
ldsysgenld.1 (𝜑𝑂𝑉)
ldsysgenld.2 (𝜑𝐴 ⊆ 𝒫 𝑂)
Assertion
Ref Expression
ldsysgenld (𝜑 {𝑡𝐿𝐴𝑡} ∈ 𝐿)
Distinct variable groups:   𝑦,𝑠   𝑡,𝐿   𝑂,𝑠,𝑡,𝑥   𝑥,𝑉   𝑦,𝑡   𝐴,𝑠,𝑡,𝑥   𝐿,𝑠,𝑥   𝜑,𝑡,𝑥
Allowed substitution hints:   𝜑(𝑦,𝑠)   𝐴(𝑦)   𝐿(𝑦)   𝑂(𝑦)   𝑉(𝑦,𝑡,𝑠)

Proof of Theorem ldsysgenld
Dummy variable 𝑢 is distinct from all other variables.
StepHypRef Expression
1 ldsysgenld.1 . . . . 5 (𝜑𝑂𝑉)
2 pwsiga 30321 . . . . 5 (𝑂𝑉 → 𝒫 𝑂 ∈ (sigAlgebra‘𝑂))
31, 2syl 17 . . . 4 (𝜑 → 𝒫 𝑂 ∈ (sigAlgebra‘𝑂))
4 isldsys.l . . . . . . . 8 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥𝑠 (𝑂𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑠))}
54sigaldsys 30350 . . . . . . 7 (sigAlgebra‘𝑂) ⊆ 𝐿
65, 3sseldi 3634 . . . . . 6 (𝜑 → 𝒫 𝑂𝐿)
7 ldsysgenld.2 . . . . . 6 (𝜑𝐴 ⊆ 𝒫 𝑂)
8 sseq2 3660 . . . . . . 7 (𝑡 = 𝒫 𝑂 → (𝐴𝑡𝐴 ⊆ 𝒫 𝑂))
98elrab 3396 . . . . . 6 (𝒫 𝑂 ∈ {𝑡𝐿𝐴𝑡} ↔ (𝒫 𝑂𝐿𝐴 ⊆ 𝒫 𝑂))
106, 7, 9sylanbrc 699 . . . . 5 (𝜑 → 𝒫 𝑂 ∈ {𝑡𝐿𝐴𝑡})
11 intss1 4524 . . . . 5 (𝒫 𝑂 ∈ {𝑡𝐿𝐴𝑡} → {𝑡𝐿𝐴𝑡} ⊆ 𝒫 𝑂)
1210, 11syl 17 . . . 4 (𝜑 {𝑡𝐿𝐴𝑡} ⊆ 𝒫 𝑂)
133, 12sselpwd 4840 . . 3 (𝜑 {𝑡𝐿𝐴𝑡} ∈ 𝒫 𝒫 𝑂)
144isldsys 30347 . . . . . . . . . 10 (𝑡𝐿 ↔ (𝑡 ∈ 𝒫 𝒫 𝑂 ∧ (∅ ∈ 𝑡 ∧ ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡))))
1514simprbi 479 . . . . . . . . 9 (𝑡𝐿 → (∅ ∈ 𝑡 ∧ ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡)))
1615simp1d 1093 . . . . . . . 8 (𝑡𝐿 → ∅ ∈ 𝑡)
1716adantl 481 . . . . . . 7 ((𝜑𝑡𝐿) → ∅ ∈ 𝑡)
1817a1d 25 . . . . . 6 ((𝜑𝑡𝐿) → (𝐴𝑡 → ∅ ∈ 𝑡))
1918ralrimiva 2995 . . . . 5 (𝜑 → ∀𝑡𝐿 (𝐴𝑡 → ∅ ∈ 𝑡))
20 0ex 4823 . . . . . 6 ∅ ∈ V
2120elintrab 4520 . . . . 5 (∅ ∈ {𝑡𝐿𝐴𝑡} ↔ ∀𝑡𝐿 (𝐴𝑡 → ∅ ∈ 𝑡))
2219, 21sylibr 224 . . . 4 (𝜑 → ∅ ∈ {𝑡𝐿𝐴𝑡})
23 nfv 1883 . . . . . . . 8 𝑡𝜑
24 nfcv 2793 . . . . . . . . 9 𝑡𝑥
25 nfrab1 3152 . . . . . . . . . 10 𝑡{𝑡𝐿𝐴𝑡}
2625nfint 4518 . . . . . . . . 9 𝑡 {𝑡𝐿𝐴𝑡}
2724, 26nfel 2806 . . . . . . . 8 𝑡 𝑥 {𝑡𝐿𝐴𝑡}
2823, 27nfan 1868 . . . . . . 7 𝑡(𝜑𝑥 {𝑡𝐿𝐴𝑡})
29 simplr 807 . . . . . . . . . 10 ((((𝜑𝑥 {𝑡𝐿𝐴𝑡}) ∧ 𝑡𝐿) ∧ 𝐴𝑡) → 𝑡𝐿)
30 vex 3234 . . . . . . . . . . . . . . 15 𝑥 ∈ V
3130elintrab 4520 . . . . . . . . . . . . . 14 (𝑥 {𝑡𝐿𝐴𝑡} ↔ ∀𝑡𝐿 (𝐴𝑡𝑥𝑡))
3231biimpi 206 . . . . . . . . . . . . 13 (𝑥 {𝑡𝐿𝐴𝑡} → ∀𝑡𝐿 (𝐴𝑡𝑥𝑡))
3332adantl 481 . . . . . . . . . . . 12 ((𝜑𝑥 {𝑡𝐿𝐴𝑡}) → ∀𝑡𝐿 (𝐴𝑡𝑥𝑡))
3433r19.21bi 2961 . . . . . . . . . . 11 (((𝜑𝑥 {𝑡𝐿𝐴𝑡}) ∧ 𝑡𝐿) → (𝐴𝑡𝑥𝑡))
3534imp 444 . . . . . . . . . 10 ((((𝜑𝑥 {𝑡𝐿𝐴𝑡}) ∧ 𝑡𝐿) ∧ 𝐴𝑡) → 𝑥𝑡)
3615simp2d 1094 . . . . . . . . . . 11 (𝑡𝐿 → ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡)
3736r19.21bi 2961 . . . . . . . . . 10 ((𝑡𝐿𝑥𝑡) → (𝑂𝑥) ∈ 𝑡)
3829, 35, 37syl2anc 694 . . . . . . . . 9 ((((𝜑𝑥 {𝑡𝐿𝐴𝑡}) ∧ 𝑡𝐿) ∧ 𝐴𝑡) → (𝑂𝑥) ∈ 𝑡)
3938ex 449 . . . . . . . 8 (((𝜑𝑥 {𝑡𝐿𝐴𝑡}) ∧ 𝑡𝐿) → (𝐴𝑡 → (𝑂𝑥) ∈ 𝑡))
4039ex 449 . . . . . . 7 ((𝜑𝑥 {𝑡𝐿𝐴𝑡}) → (𝑡𝐿 → (𝐴𝑡 → (𝑂𝑥) ∈ 𝑡)))
4128, 40ralrimi 2986 . . . . . 6 ((𝜑𝑥 {𝑡𝐿𝐴𝑡}) → ∀𝑡𝐿 (𝐴𝑡 → (𝑂𝑥) ∈ 𝑡))
42 difexg 4841 . . . . . . . 8 (𝑂𝑉 → (𝑂𝑥) ∈ V)
43 elintrabg 4521 . . . . . . . 8 ((𝑂𝑥) ∈ V → ((𝑂𝑥) ∈ {𝑡𝐿𝐴𝑡} ↔ ∀𝑡𝐿 (𝐴𝑡 → (𝑂𝑥) ∈ 𝑡)))
441, 42, 433syl 18 . . . . . . 7 (𝜑 → ((𝑂𝑥) ∈ {𝑡𝐿𝐴𝑡} ↔ ∀𝑡𝐿 (𝐴𝑡 → (𝑂𝑥) ∈ 𝑡)))
4544adantr 480 . . . . . 6 ((𝜑𝑥 {𝑡𝐿𝐴𝑡}) → ((𝑂𝑥) ∈ {𝑡𝐿𝐴𝑡} ↔ ∀𝑡𝐿 (𝐴𝑡 → (𝑂𝑥) ∈ 𝑡)))
4641, 45mpbird 247 . . . . 5 ((𝜑𝑥 {𝑡𝐿𝐴𝑡}) → (𝑂𝑥) ∈ {𝑡𝐿𝐴𝑡})
4746ralrimiva 2995 . . . 4 (𝜑 → ∀𝑥 {𝑡𝐿𝐴𝑡} (𝑂𝑥) ∈ {𝑡𝐿𝐴𝑡})
4826nfpw 4205 . . . . . . . . . . 11 𝑡𝒫 {𝑡𝐿𝐴𝑡}
4924, 48nfel 2806 . . . . . . . . . 10 𝑡 𝑥 ∈ 𝒫 {𝑡𝐿𝐴𝑡}
5023, 49nfan 1868 . . . . . . . . 9 𝑡(𝜑𝑥 ∈ 𝒫 {𝑡𝐿𝐴𝑡})
51 nfv 1883 . . . . . . . . 9 𝑡(𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)
5250, 51nfan 1868 . . . . . . . 8 𝑡((𝜑𝑥 ∈ 𝒫 {𝑡𝐿𝐴𝑡}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦))
53 simplr 807 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ 𝒫 {𝑡𝐿𝐴𝑡}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝐴𝑡) → 𝑡𝐿)
54 simpr 476 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑥 ∈ 𝒫 {𝑡𝐿𝐴𝑡}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝐴𝑡) ∧ 𝑢 {𝑡𝐿𝐴𝑡}) → 𝑢 {𝑡𝐿𝐴𝑡})
55 simpllr 815 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑥 ∈ 𝒫 {𝑡𝐿𝐴𝑡}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝐴𝑡) ∧ 𝑢 {𝑡𝐿𝐴𝑡}) → 𝑡𝐿)
56 simplr 807 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑥 ∈ 𝒫 {𝑡𝐿𝐴𝑡}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝐴𝑡) ∧ 𝑢 {𝑡𝐿𝐴𝑡}) → 𝐴𝑡)
57 vex 3234 . . . . . . . . . . . . . . . . . . . 20 𝑢 ∈ V
5857elintrab 4520 . . . . . . . . . . . . . . . . . . 19 (𝑢 {𝑡𝐿𝐴𝑡} ↔ ∀𝑡𝐿 (𝐴𝑡𝑢𝑡))
5958biimpi 206 . . . . . . . . . . . . . . . . . 18 (𝑢 {𝑡𝐿𝐴𝑡} → ∀𝑡𝐿 (𝐴𝑡𝑢𝑡))
6059r19.21bi 2961 . . . . . . . . . . . . . . . . 17 ((𝑢 {𝑡𝐿𝐴𝑡} ∧ 𝑡𝐿) → (𝐴𝑡𝑢𝑡))
6160imp 444 . . . . . . . . . . . . . . . 16 (((𝑢 {𝑡𝐿𝐴𝑡} ∧ 𝑡𝐿) ∧ 𝐴𝑡) → 𝑢𝑡)
6254, 55, 56, 61syl21anc 1365 . . . . . . . . . . . . . . 15 ((((((𝜑𝑥 ∈ 𝒫 {𝑡𝐿𝐴𝑡}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝐴𝑡) ∧ 𝑢 {𝑡𝐿𝐴𝑡}) → 𝑢𝑡)
6362ex 449 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ 𝒫 {𝑡𝐿𝐴𝑡}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝐴𝑡) → (𝑢 {𝑡𝐿𝐴𝑡} → 𝑢𝑡))
6463ssrdv 3642 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ 𝒫 {𝑡𝐿𝐴𝑡}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝐴𝑡) → {𝑡𝐿𝐴𝑡} ⊆ 𝑡)
65 sspwb 4947 . . . . . . . . . . . . 13 ( {𝑡𝐿𝐴𝑡} ⊆ 𝑡 ↔ 𝒫 {𝑡𝐿𝐴𝑡} ⊆ 𝒫 𝑡)
6664, 65sylib 208 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ 𝒫 {𝑡𝐿𝐴𝑡}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝐴𝑡) → 𝒫 {𝑡𝐿𝐴𝑡} ⊆ 𝒫 𝑡)
67 simp-4r 824 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ 𝒫 {𝑡𝐿𝐴𝑡}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝐴𝑡) → 𝑥 ∈ 𝒫 {𝑡𝐿𝐴𝑡})
6866, 67sseldd 3637 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ 𝒫 {𝑡𝐿𝐴𝑡}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝐴𝑡) → 𝑥 ∈ 𝒫 𝑡)
69 simpllr 815 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ 𝒫 {𝑡𝐿𝐴𝑡}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝐴𝑡) → (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦))
7015simp3d 1095 . . . . . . . . . . . . 13 (𝑡𝐿 → ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡))
7170r19.21bi 2961 . . . . . . . . . . . 12 ((𝑡𝐿𝑥 ∈ 𝒫 𝑡) → ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡))
7271imp 444 . . . . . . . . . . 11 (((𝑡𝐿𝑥 ∈ 𝒫 𝑡) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → 𝑥𝑡)
7353, 68, 69, 72syl21anc 1365 . . . . . . . . . 10 (((((𝜑𝑥 ∈ 𝒫 {𝑡𝐿𝐴𝑡}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) ∧ 𝐴𝑡) → 𝑥𝑡)
7473ex 449 . . . . . . . . 9 ((((𝜑𝑥 ∈ 𝒫 {𝑡𝐿𝐴𝑡}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑡𝐿) → (𝐴𝑡 𝑥𝑡))
7574ex 449 . . . . . . . 8 (((𝜑𝑥 ∈ 𝒫 {𝑡𝐿𝐴𝑡}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → (𝑡𝐿 → (𝐴𝑡 𝑥𝑡)))
7652, 75ralrimi 2986 . . . . . . 7 (((𝜑𝑥 ∈ 𝒫 {𝑡𝐿𝐴𝑡}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → ∀𝑡𝐿 (𝐴𝑡 𝑥𝑡))
77 vuniex 6996 . . . . . . . 8 𝑥 ∈ V
7877elintrab 4520 . . . . . . 7 ( 𝑥 {𝑡𝐿𝐴𝑡} ↔ ∀𝑡𝐿 (𝐴𝑡 𝑥𝑡))
7976, 78sylibr 224 . . . . . 6 (((𝜑𝑥 ∈ 𝒫 {𝑡𝐿𝐴𝑡}) ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → 𝑥 {𝑡𝐿𝐴𝑡})
8079ex 449 . . . . 5 ((𝜑𝑥 ∈ 𝒫 {𝑡𝐿𝐴𝑡}) → ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥 {𝑡𝐿𝐴𝑡}))
8180ralrimiva 2995 . . . 4 (𝜑 → ∀𝑥 ∈ 𝒫 {𝑡𝐿𝐴𝑡} ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥 {𝑡𝐿𝐴𝑡}))
8222, 47, 813jca 1261 . . 3 (𝜑 → (∅ ∈ {𝑡𝐿𝐴𝑡} ∧ ∀𝑥 {𝑡𝐿𝐴𝑡} (𝑂𝑥) ∈ {𝑡𝐿𝐴𝑡} ∧ ∀𝑥 ∈ 𝒫 {𝑡𝐿𝐴𝑡} ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥 {𝑡𝐿𝐴𝑡})))
8313, 82jca 553 . 2 (𝜑 → ( {𝑡𝐿𝐴𝑡} ∈ 𝒫 𝒫 𝑂 ∧ (∅ ∈ {𝑡𝐿𝐴𝑡} ∧ ∀𝑥 {𝑡𝐿𝐴𝑡} (𝑂𝑥) ∈ {𝑡𝐿𝐴𝑡} ∧ ∀𝑥 ∈ 𝒫 {𝑡𝐿𝐴𝑡} ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥 {𝑡𝐿𝐴𝑡}))))
844isldsys 30347 . 2 ( {𝑡𝐿𝐴𝑡} ∈ 𝐿 ↔ ( {𝑡𝐿𝐴𝑡} ∈ 𝒫 𝒫 𝑂 ∧ (∅ ∈ {𝑡𝐿𝐴𝑡} ∧ ∀𝑥 {𝑡𝐿𝐴𝑡} (𝑂𝑥) ∈ {𝑡𝐿𝐴𝑡} ∧ ∀𝑥 ∈ 𝒫 {𝑡𝐿𝐴𝑡} ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥 {𝑡𝐿𝐴𝑡}))))
8583, 84sylibr 224 1 (𝜑 {𝑡𝐿𝐴𝑡} ∈ 𝐿)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030  ∀wral 2941  {crab 2945  Vcvv 3231   ∖ cdif 3604   ⊆ wss 3607  ∅c0 3948  𝒫 cpw 4191  ∪ cuni 4468  ∩ cint 4507  Disj wdisj 4652   class class class wbr 4685  ‘cfv 5926  ωcom 7107   ≼ cdom 7995  sigAlgebracsiga 30298 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-ac2 9323 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-oi 8456  df-card 8803  df-acn 8806  df-ac 8977  df-cda 9028  df-siga 30299 This theorem is referenced by:  ldgenpisys  30357  dynkin  30358
 Copyright terms: Public domain W3C validator