Step |
Hyp |
Ref |
Expression |
1 |
|
dynkin.p |
⊢ 𝑃 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( fi ‘ 𝑠 ) ⊆ 𝑠 } |
2 |
|
dynkin.l |
⊢ 𝐿 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) } |
3 |
|
dynkin.o |
⊢ ( 𝜑 → 𝑂 ∈ 𝑉 ) |
4 |
|
ldgenpisys.e |
⊢ 𝐸 = ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 } |
5 |
|
ldgenpisys.1 |
⊢ ( 𝜑 → 𝑇 ∈ 𝑃 ) |
6 |
|
ssrab2 |
⊢ { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) } ⊆ 𝒫 𝒫 𝑂 |
7 |
|
ssrab2 |
⊢ { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( fi ‘ 𝑠 ) ⊆ 𝑠 } ⊆ 𝒫 𝒫 𝑂 |
8 |
5 1
|
eleqtrdi |
⊢ ( 𝜑 → 𝑇 ∈ { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( fi ‘ 𝑠 ) ⊆ 𝑠 } ) |
9 |
7 8
|
sseldi |
⊢ ( 𝜑 → 𝑇 ∈ 𝒫 𝒫 𝑂 ) |
10 |
9
|
elpwid |
⊢ ( 𝜑 → 𝑇 ⊆ 𝒫 𝑂 ) |
11 |
2 3 10
|
ldsysgenld |
⊢ ( 𝜑 → ∩ { 𝑡 ∈ 𝐿 ∣ 𝑇 ⊆ 𝑡 } ∈ 𝐿 ) |
12 |
4 11
|
eqeltrid |
⊢ ( 𝜑 → 𝐸 ∈ 𝐿 ) |
13 |
12 2
|
eleqtrdi |
⊢ ( 𝜑 → 𝐸 ∈ { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) } ) |
14 |
6 13
|
sseldi |
⊢ ( 𝜑 → 𝐸 ∈ 𝒫 𝒫 𝑂 ) |
15 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ) ) → 𝑏 ∈ 𝐸 ) |
16 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ) ) → 𝑎 ∈ 𝐸 ) |
17 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) → 𝑂 ∈ 𝑉 ) |
18 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) → 𝑇 ∈ 𝑃 ) |
19 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) → 𝑎 ∈ 𝐸 ) |
20 |
10
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) → 𝑇 ⊆ 𝒫 𝑂 ) |
21 |
20
|
sselda |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝑇 ) → 𝑏 ∈ 𝒫 𝑂 ) |
22 |
|
incom |
⊢ ( 𝑏 ∩ 𝑎 ) = ( 𝑎 ∩ 𝑏 ) |
23 |
3
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝑇 ) → 𝑂 ∈ 𝑉 ) |
24 |
5
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝑇 ) → 𝑇 ∈ 𝑃 ) |
25 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝑇 ) → 𝑏 ∈ 𝑇 ) |
26 |
1 2 23 4 24 25
|
ldgenpisyslem3 |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝑇 ) → 𝐸 ⊆ { 𝑐 ∈ 𝒫 𝑂 ∣ ( 𝑏 ∩ 𝑐 ) ∈ 𝐸 } ) |
27 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝑇 ) → 𝑎 ∈ 𝐸 ) |
28 |
26 27
|
sseldd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝑇 ) → 𝑎 ∈ { 𝑐 ∈ 𝒫 𝑂 ∣ ( 𝑏 ∩ 𝑐 ) ∈ 𝐸 } ) |
29 |
|
ineq2 |
⊢ ( 𝑐 = 𝑎 → ( 𝑏 ∩ 𝑐 ) = ( 𝑏 ∩ 𝑎 ) ) |
30 |
29
|
eleq1d |
⊢ ( 𝑐 = 𝑎 → ( ( 𝑏 ∩ 𝑐 ) ∈ 𝐸 ↔ ( 𝑏 ∩ 𝑎 ) ∈ 𝐸 ) ) |
31 |
30
|
elrab |
⊢ ( 𝑎 ∈ { 𝑐 ∈ 𝒫 𝑂 ∣ ( 𝑏 ∩ 𝑐 ) ∈ 𝐸 } ↔ ( 𝑎 ∈ 𝒫 𝑂 ∧ ( 𝑏 ∩ 𝑎 ) ∈ 𝐸 ) ) |
32 |
28 31
|
sylib |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝑇 ) → ( 𝑎 ∈ 𝒫 𝑂 ∧ ( 𝑏 ∩ 𝑎 ) ∈ 𝐸 ) ) |
33 |
32
|
simprd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝑇 ) → ( 𝑏 ∩ 𝑎 ) ∈ 𝐸 ) |
34 |
22 33
|
eqeltrrid |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝑇 ) → ( 𝑎 ∩ 𝑏 ) ∈ 𝐸 ) |
35 |
21 34
|
jca |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝑇 ) → ( 𝑏 ∈ 𝒫 𝑂 ∧ ( 𝑎 ∩ 𝑏 ) ∈ 𝐸 ) ) |
36 |
|
ineq2 |
⊢ ( 𝑐 = 𝑏 → ( 𝑎 ∩ 𝑐 ) = ( 𝑎 ∩ 𝑏 ) ) |
37 |
36
|
eleq1d |
⊢ ( 𝑐 = 𝑏 → ( ( 𝑎 ∩ 𝑐 ) ∈ 𝐸 ↔ ( 𝑎 ∩ 𝑏 ) ∈ 𝐸 ) ) |
38 |
37
|
elrab |
⊢ ( 𝑏 ∈ { 𝑐 ∈ 𝒫 𝑂 ∣ ( 𝑎 ∩ 𝑐 ) ∈ 𝐸 } ↔ ( 𝑏 ∈ 𝒫 𝑂 ∧ ( 𝑎 ∩ 𝑏 ) ∈ 𝐸 ) ) |
39 |
35 38
|
sylibr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) ∧ 𝑏 ∈ 𝑇 ) → 𝑏 ∈ { 𝑐 ∈ 𝒫 𝑂 ∣ ( 𝑎 ∩ 𝑐 ) ∈ 𝐸 } ) |
40 |
39
|
ex |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) → ( 𝑏 ∈ 𝑇 → 𝑏 ∈ { 𝑐 ∈ 𝒫 𝑂 ∣ ( 𝑎 ∩ 𝑐 ) ∈ 𝐸 } ) ) |
41 |
40
|
ssrdv |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) → 𝑇 ⊆ { 𝑐 ∈ 𝒫 𝑂 ∣ ( 𝑎 ∩ 𝑐 ) ∈ 𝐸 } ) |
42 |
1 2 17 4 18 19 41
|
ldgenpisyslem2 |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐸 ) → 𝐸 ⊆ { 𝑐 ∈ 𝒫 𝑂 ∣ ( 𝑎 ∩ 𝑐 ) ∈ 𝐸 } ) |
43 |
16 42
|
syldan |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ) ) → 𝐸 ⊆ { 𝑐 ∈ 𝒫 𝑂 ∣ ( 𝑎 ∩ 𝑐 ) ∈ 𝐸 } ) |
44 |
|
ssrab |
⊢ ( 𝐸 ⊆ { 𝑐 ∈ 𝒫 𝑂 ∣ ( 𝑎 ∩ 𝑐 ) ∈ 𝐸 } ↔ ( 𝐸 ⊆ 𝒫 𝑂 ∧ ∀ 𝑐 ∈ 𝐸 ( 𝑎 ∩ 𝑐 ) ∈ 𝐸 ) ) |
45 |
43 44
|
sylib |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ) ) → ( 𝐸 ⊆ 𝒫 𝑂 ∧ ∀ 𝑐 ∈ 𝐸 ( 𝑎 ∩ 𝑐 ) ∈ 𝐸 ) ) |
46 |
45
|
simprd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ) ) → ∀ 𝑐 ∈ 𝐸 ( 𝑎 ∩ 𝑐 ) ∈ 𝐸 ) |
47 |
37
|
rspcv |
⊢ ( 𝑏 ∈ 𝐸 → ( ∀ 𝑐 ∈ 𝐸 ( 𝑎 ∩ 𝑐 ) ∈ 𝐸 → ( 𝑎 ∩ 𝑏 ) ∈ 𝐸 ) ) |
48 |
15 46 47
|
sylc |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ) ) → ( 𝑎 ∩ 𝑏 ) ∈ 𝐸 ) |
49 |
48
|
ralrimivva |
⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐸 ∀ 𝑏 ∈ 𝐸 ( 𝑎 ∩ 𝑏 ) ∈ 𝐸 ) |
50 |
|
inficl |
⊢ ( 𝐸 ∈ 𝐿 → ( ∀ 𝑎 ∈ 𝐸 ∀ 𝑏 ∈ 𝐸 ( 𝑎 ∩ 𝑏 ) ∈ 𝐸 ↔ ( fi ‘ 𝐸 ) = 𝐸 ) ) |
51 |
12 50
|
syl |
⊢ ( 𝜑 → ( ∀ 𝑎 ∈ 𝐸 ∀ 𝑏 ∈ 𝐸 ( 𝑎 ∩ 𝑏 ) ∈ 𝐸 ↔ ( fi ‘ 𝐸 ) = 𝐸 ) ) |
52 |
49 51
|
mpbid |
⊢ ( 𝜑 → ( fi ‘ 𝐸 ) = 𝐸 ) |
53 |
|
eqimss |
⊢ ( ( fi ‘ 𝐸 ) = 𝐸 → ( fi ‘ 𝐸 ) ⊆ 𝐸 ) |
54 |
52 53
|
syl |
⊢ ( 𝜑 → ( fi ‘ 𝐸 ) ⊆ 𝐸 ) |
55 |
14 54
|
jca |
⊢ ( 𝜑 → ( 𝐸 ∈ 𝒫 𝒫 𝑂 ∧ ( fi ‘ 𝐸 ) ⊆ 𝐸 ) ) |
56 |
1
|
ispisys |
⊢ ( 𝐸 ∈ 𝑃 ↔ ( 𝐸 ∈ 𝒫 𝒫 𝑂 ∧ ( fi ‘ 𝐸 ) ⊆ 𝐸 ) ) |
57 |
55 56
|
sylibr |
⊢ ( 𝜑 → 𝐸 ∈ 𝑃 ) |