Step |
Hyp |
Ref |
Expression |
1 |
|
acsdrscl.f |
⊢ 𝐹 = ( mrCls ‘ 𝐶 ) |
2 |
|
simpll |
⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) ) |
3 |
|
elpwi |
⊢ ( 𝑡 ∈ 𝒫 𝒫 𝑋 → 𝑡 ⊆ 𝒫 𝑋 ) |
4 |
3
|
ad2antrl |
⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → 𝑡 ⊆ 𝒫 𝑋 ) |
5 |
1
|
mrcuni |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑡 ⊆ 𝒫 𝑋 ) → ( 𝐹 ‘ ∪ 𝑡 ) = ( 𝐹 ‘ ∪ ( 𝐹 “ 𝑡 ) ) ) |
6 |
2 4 5
|
syl2anc |
⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → ( 𝐹 ‘ ∪ 𝑡 ) = ( 𝐹 ‘ ∪ ( 𝐹 “ 𝑡 ) ) ) |
7 |
1
|
mrcf |
⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐹 : 𝒫 𝑋 ⟶ 𝐶 ) |
8 |
7
|
ffnd |
⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐹 Fn 𝒫 𝑋 ) |
9 |
8
|
adantr |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → 𝐹 Fn 𝒫 𝑋 ) |
10 |
|
simpll |
⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) ∧ ( 𝑥 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑋 ) ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) ) |
11 |
|
simprl |
⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) ∧ ( 𝑥 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑋 ) ) → 𝑥 ⊆ 𝑦 ) |
12 |
|
simprr |
⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) ∧ ( 𝑥 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑋 ) ) → 𝑦 ⊆ 𝑋 ) |
13 |
10 1 11 12
|
mrcssd |
⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) ∧ ( 𝑥 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑋 ) ) → ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑦 ) ) |
14 |
|
simprr |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → ( toInc ‘ 𝑡 ) ∈ Dirset ) |
15 |
3
|
ad2antrl |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → 𝑡 ⊆ 𝒫 𝑋 ) |
16 |
1
|
fvexi |
⊢ 𝐹 ∈ V |
17 |
16
|
imaex |
⊢ ( 𝐹 “ 𝑡 ) ∈ V |
18 |
17
|
a1i |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → ( 𝐹 “ 𝑡 ) ∈ V ) |
19 |
9 13 14 15 18
|
ipodrsima |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → ( toInc ‘ ( 𝐹 “ 𝑡 ) ) ∈ Dirset ) |
20 |
19
|
adantlr |
⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → ( toInc ‘ ( 𝐹 “ 𝑡 ) ) ∈ Dirset ) |
21 |
|
fveq2 |
⊢ ( 𝑠 = ( 𝐹 “ 𝑡 ) → ( toInc ‘ 𝑠 ) = ( toInc ‘ ( 𝐹 “ 𝑡 ) ) ) |
22 |
21
|
eleq1d |
⊢ ( 𝑠 = ( 𝐹 “ 𝑡 ) → ( ( toInc ‘ 𝑠 ) ∈ Dirset ↔ ( toInc ‘ ( 𝐹 “ 𝑡 ) ) ∈ Dirset ) ) |
23 |
|
unieq |
⊢ ( 𝑠 = ( 𝐹 “ 𝑡 ) → ∪ 𝑠 = ∪ ( 𝐹 “ 𝑡 ) ) |
24 |
23
|
eleq1d |
⊢ ( 𝑠 = ( 𝐹 “ 𝑡 ) → ( ∪ 𝑠 ∈ 𝐶 ↔ ∪ ( 𝐹 “ 𝑡 ) ∈ 𝐶 ) ) |
25 |
22 24
|
imbi12d |
⊢ ( 𝑠 = ( 𝐹 “ 𝑡 ) → ( ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ↔ ( ( toInc ‘ ( 𝐹 “ 𝑡 ) ) ∈ Dirset → ∪ ( 𝐹 “ 𝑡 ) ∈ 𝐶 ) ) ) |
26 |
|
simplr |
⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) |
27 |
|
imassrn |
⊢ ( 𝐹 “ 𝑡 ) ⊆ ran 𝐹 |
28 |
7
|
frnd |
⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ran 𝐹 ⊆ 𝐶 ) |
29 |
27 28
|
sstrid |
⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( 𝐹 “ 𝑡 ) ⊆ 𝐶 ) |
30 |
17
|
elpw |
⊢ ( ( 𝐹 “ 𝑡 ) ∈ 𝒫 𝐶 ↔ ( 𝐹 “ 𝑡 ) ⊆ 𝐶 ) |
31 |
29 30
|
sylibr |
⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( 𝐹 “ 𝑡 ) ∈ 𝒫 𝐶 ) |
32 |
31
|
ad2antrr |
⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → ( 𝐹 “ 𝑡 ) ∈ 𝒫 𝐶 ) |
33 |
25 26 32
|
rspcdva |
⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → ( ( toInc ‘ ( 𝐹 “ 𝑡 ) ) ∈ Dirset → ∪ ( 𝐹 “ 𝑡 ) ∈ 𝐶 ) ) |
34 |
20 33
|
mpd |
⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → ∪ ( 𝐹 “ 𝑡 ) ∈ 𝐶 ) |
35 |
1
|
mrcid |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∪ ( 𝐹 “ 𝑡 ) ∈ 𝐶 ) → ( 𝐹 ‘ ∪ ( 𝐹 “ 𝑡 ) ) = ∪ ( 𝐹 “ 𝑡 ) ) |
36 |
2 34 35
|
syl2anc |
⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → ( 𝐹 ‘ ∪ ( 𝐹 “ 𝑡 ) ) = ∪ ( 𝐹 “ 𝑡 ) ) |
37 |
6 36
|
eqtrd |
⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) ∧ ( 𝑡 ∈ 𝒫 𝒫 𝑋 ∧ ( toInc ‘ 𝑡 ) ∈ Dirset ) ) → ( 𝐹 ‘ ∪ 𝑡 ) = ∪ ( 𝐹 “ 𝑡 ) ) |
38 |
37
|
exp32 |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) → ( 𝑡 ∈ 𝒫 𝒫 𝑋 → ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑡 ) = ∪ ( 𝐹 “ 𝑡 ) ) ) ) |
39 |
38
|
ralrimiv |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) → ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑡 ) = ∪ ( 𝐹 “ 𝑡 ) ) ) |
40 |
39
|
ex |
⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) → ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑡 ) = ∪ ( 𝐹 “ 𝑡 ) ) ) ) |
41 |
40
|
imdistani |
⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑡 ∈ 𝒫 𝒫 𝑋 ( ( toInc ‘ 𝑡 ) ∈ Dirset → ( 𝐹 ‘ ∪ 𝑡 ) = ∪ ( 𝐹 “ 𝑡 ) ) ) ) |