Step | Hyp | Ref
| Expression |
1 | | simpll 764 |
. . . . . . 7
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → 𝐶 ∈ (Moore‘𝑋)) |
2 | | elpwi 4542 |
. . . . . . . 8
⊢ (𝑡 ∈ 𝒫 𝒫
𝑋 → 𝑡 ⊆ 𝒫 𝑋) |
3 | 2 | ad2antrl 725 |
. . . . . . 7
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → 𝑡 ⊆ 𝒫 𝑋) |
4 | | acsdrscl.f |
. . . . . . . 8
⊢ 𝐹 = (mrCls‘𝐶) |
5 | 4 | mrcuni 17340 |
. . . . . . 7
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡 ⊆ 𝒫 𝑋) → (𝐹‘∪ 𝑡) = (𝐹‘∪ (𝐹 “ 𝑡))) |
6 | 1, 3, 5 | syl2anc 584 |
. . . . . 6
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → (𝐹‘∪ 𝑡) =
(𝐹‘∪ (𝐹
“ 𝑡))) |
7 | 4 | mrcf 17328 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐹:𝒫 𝑋⟶𝐶) |
8 | 7 | ffnd 6593 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐹 Fn 𝒫 𝑋) |
9 | 8 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ (𝑡 ∈ 𝒫 𝒫 𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → 𝐹 Fn 𝒫 𝑋) |
10 | | simpll 764 |
. . . . . . . . . . 11
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ (𝑡 ∈ 𝒫 𝒫 𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) ∧ (𝑥 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑋)) → 𝐶 ∈ (Moore‘𝑋)) |
11 | | simprl 768 |
. . . . . . . . . . 11
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ (𝑡 ∈ 𝒫 𝒫 𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) ∧ (𝑥 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑋)) → 𝑥 ⊆ 𝑦) |
12 | | simprr 770 |
. . . . . . . . . . 11
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ (𝑡 ∈ 𝒫 𝒫 𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) ∧ (𝑥 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑋)) → 𝑦 ⊆ 𝑋) |
13 | 10, 4, 11, 12 | mrcssd 17343 |
. . . . . . . . . 10
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ (𝑡 ∈ 𝒫 𝒫 𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) ∧ (𝑥 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑋)) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦)) |
14 | | simprr 770 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ (𝑡 ∈ 𝒫 𝒫 𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → (toInc‘𝑡) ∈
Dirset) |
15 | 2 | ad2antrl 725 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ (𝑡 ∈ 𝒫 𝒫 𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → 𝑡 ⊆ 𝒫 𝑋) |
16 | 4 | fvexi 6780 |
. . . . . . . . . . . 12
⊢ 𝐹 ∈ V |
17 | 16 | imaex 7753 |
. . . . . . . . . . 11
⊢ (𝐹 “ 𝑡) ∈ V |
18 | 17 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ (𝑡 ∈ 𝒫 𝒫 𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → (𝐹 “ 𝑡) ∈ V) |
19 | 9, 13, 14, 15, 18 | ipodrsima 18269 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ (𝑡 ∈ 𝒫 𝒫 𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → (toInc‘(𝐹 “ 𝑡)) ∈ Dirset) |
20 | 19 | adantlr 712 |
. . . . . . . 8
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) →
(toInc‘(𝐹 “
𝑡)) ∈
Dirset) |
21 | | fveq2 6766 |
. . . . . . . . . . 11
⊢ (𝑠 = (𝐹 “ 𝑡) → (toInc‘𝑠) = (toInc‘(𝐹 “ 𝑡))) |
22 | 21 | eleq1d 2823 |
. . . . . . . . . 10
⊢ (𝑠 = (𝐹 “ 𝑡) → ((toInc‘𝑠) ∈ Dirset ↔ (toInc‘(𝐹 “ 𝑡)) ∈ Dirset)) |
23 | | unieq 4850 |
. . . . . . . . . . 11
⊢ (𝑠 = (𝐹 “ 𝑡) → ∪ 𝑠 = ∪
(𝐹 “ 𝑡)) |
24 | 23 | eleq1d 2823 |
. . . . . . . . . 10
⊢ (𝑠 = (𝐹 “ 𝑡) → (∪ 𝑠 ∈ 𝐶 ↔ ∪ (𝐹 “ 𝑡) ∈ 𝐶)) |
25 | 22, 24 | imbi12d 345 |
. . . . . . . . 9
⊢ (𝑠 = (𝐹 “ 𝑡) → (((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶) ↔
((toInc‘(𝐹 “
𝑡)) ∈ Dirset →
∪ (𝐹 “ 𝑡) ∈ 𝐶))) |
26 | | simplr 766 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) →
∀𝑠 ∈ 𝒫
𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) |
27 | | imassrn 5973 |
. . . . . . . . . . . 12
⊢ (𝐹 “ 𝑡) ⊆ ran 𝐹 |
28 | 7 | frnd 6600 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ (Moore‘𝑋) → ran 𝐹 ⊆ 𝐶) |
29 | 27, 28 | sstrid 3931 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (Moore‘𝑋) → (𝐹 “ 𝑡) ⊆ 𝐶) |
30 | 17 | elpw 4537 |
. . . . . . . . . . 11
⊢ ((𝐹 “ 𝑡) ∈ 𝒫 𝐶 ↔ (𝐹 “ 𝑡) ⊆ 𝐶) |
31 | 29, 30 | sylibr 233 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (Moore‘𝑋) → (𝐹 “ 𝑡) ∈ 𝒫 𝐶) |
32 | 31 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → (𝐹 “ 𝑡) ∈ 𝒫 𝐶) |
33 | 25, 26, 32 | rspcdva 3561 |
. . . . . . . 8
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) →
((toInc‘(𝐹 “
𝑡)) ∈ Dirset →
∪ (𝐹 “ 𝑡) ∈ 𝐶)) |
34 | 20, 33 | mpd 15 |
. . . . . . 7
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → ∪ (𝐹
“ 𝑡) ∈ 𝐶) |
35 | 4 | mrcid 17332 |
. . . . . . 7
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∪ (𝐹
“ 𝑡) ∈ 𝐶) → (𝐹‘∪ (𝐹 “ 𝑡)) = ∪ (𝐹 “ 𝑡)) |
36 | 1, 34, 35 | syl2anc 584 |
. . . . . 6
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → (𝐹‘∪ (𝐹
“ 𝑡)) = ∪ (𝐹
“ 𝑡)) |
37 | 6, 36 | eqtrd 2778 |
. . . . 5
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → (𝐹‘∪ 𝑡) =
∪ (𝐹 “ 𝑡)) |
38 | 37 | exp32 421 |
. . . 4
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) → (𝑡 ∈ 𝒫 𝒫
𝑋 →
((toInc‘𝑡) ∈
Dirset → (𝐹‘∪ 𝑡) = ∪
(𝐹 “ 𝑡)))) |
39 | 38 | ralrimiv 3107 |
. . 3
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) →
∀𝑡 ∈ 𝒫
𝒫 𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) = ∪
(𝐹 “ 𝑡))) |
40 | 39 | ex 413 |
. 2
⊢ (𝐶 ∈ (Moore‘𝑋) → (∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶) →
∀𝑡 ∈ 𝒫
𝒫 𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) = ∪
(𝐹 “ 𝑡)))) |
41 | 40 | imdistani 569 |
1
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) → (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑡 ∈ 𝒫 𝒫
𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) =
∪ (𝐹 “ 𝑡)))) |