| Step | Hyp | Ref
| Expression |
| 1 | | simpll 767 |
. . . . . . 7
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → 𝐶 ∈ (Moore‘𝑋)) |
| 2 | | elpwi 4607 |
. . . . . . . 8
⊢ (𝑡 ∈ 𝒫 𝒫
𝑋 → 𝑡 ⊆ 𝒫 𝑋) |
| 3 | 2 | ad2antrl 728 |
. . . . . . 7
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → 𝑡 ⊆ 𝒫 𝑋) |
| 4 | | acsdrscl.f |
. . . . . . . 8
⊢ 𝐹 = (mrCls‘𝐶) |
| 5 | 4 | mrcuni 17664 |
. . . . . . 7
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑡 ⊆ 𝒫 𝑋) → (𝐹‘∪ 𝑡) = (𝐹‘∪ (𝐹 “ 𝑡))) |
| 6 | 1, 3, 5 | syl2anc 584 |
. . . . . 6
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → (𝐹‘∪ 𝑡) =
(𝐹‘∪ (𝐹
“ 𝑡))) |
| 7 | 4 | mrcf 17652 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐹:𝒫 𝑋⟶𝐶) |
| 8 | 7 | ffnd 6737 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (Moore‘𝑋) → 𝐹 Fn 𝒫 𝑋) |
| 9 | 8 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ (𝑡 ∈ 𝒫 𝒫 𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → 𝐹 Fn 𝒫 𝑋) |
| 10 | | simpll 767 |
. . . . . . . . . . 11
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ (𝑡 ∈ 𝒫 𝒫 𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) ∧ (𝑥 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑋)) → 𝐶 ∈ (Moore‘𝑋)) |
| 11 | | simprl 771 |
. . . . . . . . . . 11
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ (𝑡 ∈ 𝒫 𝒫 𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) ∧ (𝑥 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑋)) → 𝑥 ⊆ 𝑦) |
| 12 | | simprr 773 |
. . . . . . . . . . 11
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ (𝑡 ∈ 𝒫 𝒫 𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) ∧ (𝑥 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑋)) → 𝑦 ⊆ 𝑋) |
| 13 | 10, 4, 11, 12 | mrcssd 17667 |
. . . . . . . . . 10
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ (𝑡 ∈ 𝒫 𝒫 𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) ∧ (𝑥 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑋)) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦)) |
| 14 | | simprr 773 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ (𝑡 ∈ 𝒫 𝒫 𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → (toInc‘𝑡) ∈
Dirset) |
| 15 | 2 | ad2antrl 728 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ (𝑡 ∈ 𝒫 𝒫 𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → 𝑡 ⊆ 𝒫 𝑋) |
| 16 | 4 | fvexi 6920 |
. . . . . . . . . . . 12
⊢ 𝐹 ∈ V |
| 17 | 16 | imaex 7936 |
. . . . . . . . . . 11
⊢ (𝐹 “ 𝑡) ∈ V |
| 18 | 17 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ (𝑡 ∈ 𝒫 𝒫 𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → (𝐹 “ 𝑡) ∈ V) |
| 19 | 9, 13, 14, 15, 18 | ipodrsima 18586 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ (𝑡 ∈ 𝒫 𝒫 𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → (toInc‘(𝐹 “ 𝑡)) ∈ Dirset) |
| 20 | 19 | adantlr 715 |
. . . . . . . 8
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) →
(toInc‘(𝐹 “
𝑡)) ∈
Dirset) |
| 21 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑠 = (𝐹 “ 𝑡) → (toInc‘𝑠) = (toInc‘(𝐹 “ 𝑡))) |
| 22 | 21 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑠 = (𝐹 “ 𝑡) → ((toInc‘𝑠) ∈ Dirset ↔ (toInc‘(𝐹 “ 𝑡)) ∈ Dirset)) |
| 23 | | unieq 4918 |
. . . . . . . . . . 11
⊢ (𝑠 = (𝐹 “ 𝑡) → ∪ 𝑠 = ∪
(𝐹 “ 𝑡)) |
| 24 | 23 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑠 = (𝐹 “ 𝑡) → (∪ 𝑠 ∈ 𝐶 ↔ ∪ (𝐹 “ 𝑡) ∈ 𝐶)) |
| 25 | 22, 24 | imbi12d 344 |
. . . . . . . . 9
⊢ (𝑠 = (𝐹 “ 𝑡) → (((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶) ↔
((toInc‘(𝐹 “
𝑡)) ∈ Dirset →
∪ (𝐹 “ 𝑡) ∈ 𝐶))) |
| 26 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) →
∀𝑠 ∈ 𝒫
𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) |
| 27 | | imassrn 6089 |
. . . . . . . . . . . 12
⊢ (𝐹 “ 𝑡) ⊆ ran 𝐹 |
| 28 | 7 | frnd 6744 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ (Moore‘𝑋) → ran 𝐹 ⊆ 𝐶) |
| 29 | 27, 28 | sstrid 3995 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (Moore‘𝑋) → (𝐹 “ 𝑡) ⊆ 𝐶) |
| 30 | 17 | elpw 4604 |
. . . . . . . . . . 11
⊢ ((𝐹 “ 𝑡) ∈ 𝒫 𝐶 ↔ (𝐹 “ 𝑡) ⊆ 𝐶) |
| 31 | 29, 30 | sylibr 234 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (Moore‘𝑋) → (𝐹 “ 𝑡) ∈ 𝒫 𝐶) |
| 32 | 31 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → (𝐹 “ 𝑡) ∈ 𝒫 𝐶) |
| 33 | 25, 26, 32 | rspcdva 3623 |
. . . . . . . 8
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) →
((toInc‘(𝐹 “
𝑡)) ∈ Dirset →
∪ (𝐹 “ 𝑡) ∈ 𝐶)) |
| 34 | 20, 33 | mpd 15 |
. . . . . . 7
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → ∪ (𝐹
“ 𝑡) ∈ 𝐶) |
| 35 | 4 | mrcid 17656 |
. . . . . . 7
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∪ (𝐹
“ 𝑡) ∈ 𝐶) → (𝐹‘∪ (𝐹 “ 𝑡)) = ∪ (𝐹 “ 𝑡)) |
| 36 | 1, 34, 35 | syl2anc 584 |
. . . . . 6
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → (𝐹‘∪ (𝐹
“ 𝑡)) = ∪ (𝐹
“ 𝑡)) |
| 37 | 6, 36 | eqtrd 2777 |
. . . . 5
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) ∧ (𝑡 ∈ 𝒫 𝒫
𝑋 ∧ (toInc‘𝑡) ∈ Dirset)) → (𝐹‘∪ 𝑡) =
∪ (𝐹 “ 𝑡)) |
| 38 | 37 | exp32 420 |
. . . 4
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) → (𝑡 ∈ 𝒫 𝒫
𝑋 →
((toInc‘𝑡) ∈
Dirset → (𝐹‘∪ 𝑡) = ∪
(𝐹 “ 𝑡)))) |
| 39 | 38 | ralrimiv 3145 |
. . 3
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) →
∀𝑡 ∈ 𝒫
𝒫 𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) = ∪
(𝐹 “ 𝑡))) |
| 40 | 39 | ex 412 |
. 2
⊢ (𝐶 ∈ (Moore‘𝑋) → (∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶) →
∀𝑡 ∈ 𝒫
𝒫 𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) = ∪
(𝐹 “ 𝑡)))) |
| 41 | 40 | imdistani 568 |
1
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝐶((toInc‘𝑠) ∈ Dirset → ∪ 𝑠
∈ 𝐶)) → (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑡 ∈ 𝒫 𝒫
𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) =
∪ (𝐹 “ 𝑡)))) |