Step | Hyp | Ref
| Expression |
1 | | simpll 786 |
. . . . . . 7
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → 𝐶 ∈ (Moore‘𝑋)) |
2 | | elpwi 4117 |
. . . . . . . 8
⊢ (𝑡 ∈ 𝒫 𝒫
𝑋 → 𝑡 ⊆ 𝒫 𝑋) |
3 | 2 | ad2antrl 760 |
. . . . . . 7
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → 𝑡 ⊆ 𝒫 𝑋) |
4 | | acsdrscl.f |
. . . . . . . 8
⊢ 𝐹 = (mrCls‘𝐶) |
5 | 4 | mrcuni 16104 |
. . . . . . 7
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡 ⊆ 𝒫 𝑋) → (𝐹‘∪ 𝑡) = (𝐹‘∪ (𝐹 “ 𝑡))) |
6 | 1, 3, 5 | syl2anc 691 |
. . . . . 6
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → (𝐹‘∪ 𝑡) =
(𝐹‘∪ (𝐹
“ 𝑡))) |
7 | 4 | mrcf 16092 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐹:𝒫 𝑋⟶𝐶) |
8 | 7 | ffnd 5959 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐹 Fn 𝒫 𝑋) |
9 | 8 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ (𝑡 ∈ 𝒫 𝒫 𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → 𝐹 Fn 𝒫 𝑋) |
10 | | simpll 786 |
. . . . . . . . . . 11
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ (𝑡 ∈ 𝒫 𝒫 𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) ∧ (𝑥 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑋)) → 𝐶 ∈ (Moore‘𝑋)) |
11 | | simprl 790 |
. . . . . . . . . . 11
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ (𝑡 ∈ 𝒫 𝒫 𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) ∧ (𝑥 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑋)) → 𝑥 ⊆ 𝑦) |
12 | | simprr 792 |
. . . . . . . . . . 11
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ (𝑡 ∈ 𝒫 𝒫 𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) ∧ (𝑥 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑋)) → 𝑦 ⊆ 𝑋) |
13 | 10, 4, 11, 12 | mrcssd 16107 |
. . . . . . . . . 10
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ (𝑡 ∈ 𝒫 𝒫 𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) ∧ (𝑥 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑋)) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦)) |
14 | | simprr 792 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ (𝑡 ∈ 𝒫 𝒫 𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → (toInc‘𝑡) ∈
Dirset) |
15 | 2 | ad2antrl 760 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ (𝑡 ∈ 𝒫 𝒫 𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → 𝑡 ⊆ 𝒫 𝑋) |
16 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢
(mrCls‘𝐶)
∈ V |
17 | 4, 16 | eqeltri 2684 |
. . . . . . . . . . . 12
⊢ 𝐹 ∈ V |
18 | 17 | imaex 6996 |
. . . . . . . . . . 11
⊢ (𝐹 “ 𝑡) ∈ V |
19 | 18 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ (𝑡 ∈ 𝒫 𝒫 𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → (𝐹 “ 𝑡) ∈ V) |
20 | 9, 13, 14, 15, 19 | ipodrsima 16988 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ (𝑡 ∈ 𝒫 𝒫 𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → (toInc‘(𝐹 “ 𝑡)) ∈ Dirset) |
21 | 20 | adantlr 747 |
. . . . . . . 8
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) →
(toInc‘(𝐹 “
𝑡)) ∈
Dirset) |
22 | | imassrn 5396 |
. . . . . . . . . . . 12
⊢ (𝐹 “ 𝑡) ⊆ ran 𝐹 |
23 | | frn 5966 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝒫 𝑋⟶𝐶 → ran 𝐹 ⊆ 𝐶) |
24 | 7, 23 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ (Moore‘𝑋) → ran 𝐹 ⊆ 𝐶) |
25 | 22, 24 | syl5ss 3579 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (Moore‘𝑋) → (𝐹 “ 𝑡) ⊆ 𝐶) |
26 | 18 | elpw 4114 |
. . . . . . . . . . 11
⊢ ((𝐹 “ 𝑡) ∈ 𝒫 𝐶 ↔ (𝐹 “ 𝑡) ⊆ 𝐶) |
27 | 25, 26 | sylibr 223 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (Moore‘𝑋) → (𝐹 “ 𝑡) ∈ 𝒫 𝐶) |
28 | 27 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → (𝐹 “ 𝑡) ∈ 𝒫 𝐶) |
29 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) →
∀𝑠 ∈ 𝒫
𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) |
30 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑠 = (𝐹 “ 𝑡) → (toInc‘𝑠) = (toInc‘(𝐹 “ 𝑡))) |
31 | 30 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑠 = (𝐹 “ 𝑡) → ((toInc‘𝑠) ∈ Dirset ↔ (toInc‘(𝐹 “ 𝑡)) ∈ Dirset)) |
32 | | unieq 4380 |
. . . . . . . . . . . 12
⊢ (𝑠 = (𝐹 “ 𝑡) → ∪ 𝑠 = ∪
(𝐹 “ 𝑡)) |
33 | 32 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑠 = (𝐹 “ 𝑡) → (∪ 𝑠 ∈ 𝐶 ↔ ∪ (𝐹 “ 𝑡) ∈ 𝐶)) |
34 | 31, 33 | imbi12d 333 |
. . . . . . . . . 10
⊢ (𝑠 = (𝐹 “ 𝑡) → (((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶) ↔
((toInc‘(𝐹 “
𝑡)) ∈ Dirset →
∪ (𝐹 “ 𝑡) ∈ 𝐶))) |
35 | 34 | rspcva 3280 |
. . . . . . . . 9
⊢ (((𝐹 “ 𝑡) ∈ 𝒫 𝐶 ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) →
((toInc‘(𝐹 “
𝑡)) ∈ Dirset →
∪ (𝐹 “ 𝑡) ∈ 𝐶)) |
36 | 28, 29, 35 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) →
((toInc‘(𝐹 “
𝑡)) ∈ Dirset →
∪ (𝐹 “ 𝑡) ∈ 𝐶)) |
37 | 21, 36 | mpd 15 |
. . . . . . 7
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → ∪ (𝐹
“ 𝑡) ∈ 𝐶) |
38 | 4 | mrcid 16096 |
. . . . . . 7
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∪ (𝐹
“ 𝑡) ∈ 𝐶) → (𝐹‘∪ (𝐹 “ 𝑡)) = ∪ (𝐹 “ 𝑡)) |
39 | 1, 37, 38 | syl2anc 691 |
. . . . . 6
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → (𝐹‘∪ (𝐹
“ 𝑡)) = ∪ (𝐹
“ 𝑡)) |
40 | 6, 39 | eqtrd 2644 |
. . . . 5
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → (𝐹‘∪ 𝑡) =
∪ (𝐹 “ 𝑡)) |
41 | 40 | exp32 629 |
. . . 4
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) → (𝑡 ∈ 𝒫 𝒫
𝑋 →
((toInc‘𝑡) ∈
Dirset → (𝐹‘∪ 𝑡) = ∪
(𝐹 “ 𝑡)))) |
42 | 41 | ralrimiv 2948 |
. . 3
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) →
∀𝑡 ∈ 𝒫
𝒫 𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) = ∪
(𝐹 “ 𝑡))) |
43 | 42 | ex 449 |
. 2
⊢ (𝐶 ∈ (Moore‘𝑋) → (∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶) →
∀𝑡 ∈ 𝒫
𝒫 𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) = ∪
(𝐹 “ 𝑡)))) |
44 | 43 | imdistani 722 |
1
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) → (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑡 ∈ 𝒫 𝒫
𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) =
∪ (𝐹 “ 𝑡)))) |