Proof of Theorem isacs5lem
Step | Hyp | Ref
| Expression |
1 | | unifpw 9122 |
. . . . . 6
⊢ ∪ (𝒫 𝑠 ∩ Fin) = 𝑠 |
2 | 1 | fveq2i 6777 |
. . . . 5
⊢ (𝐹‘∪ (𝒫 𝑠 ∩ Fin)) = (𝐹‘𝑠) |
3 | | vex 3436 |
. . . . . . 7
⊢ 𝑠 ∈ V |
4 | | fpwipodrs 18258 |
. . . . . . 7
⊢ (𝑠 ∈ V →
(toInc‘(𝒫 𝑠
∩ Fin)) ∈ Dirset) |
5 | 3, 4 | mp1i 13 |
. . . . . 6
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑡 ∈ 𝒫 𝒫
𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) =
∪ (𝐹 “ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) → (toInc‘(𝒫 𝑠 ∩ Fin)) ∈
Dirset) |
6 | | fveq2 6774 |
. . . . . . . . 9
⊢ (𝑡 = (𝒫 𝑠 ∩ Fin) → (toInc‘𝑡) = (toInc‘(𝒫
𝑠 ∩
Fin))) |
7 | 6 | eleq1d 2823 |
. . . . . . . 8
⊢ (𝑡 = (𝒫 𝑠 ∩ Fin) → ((toInc‘𝑡) ∈ Dirset ↔
(toInc‘(𝒫 𝑠
∩ Fin)) ∈ Dirset)) |
8 | | unieq 4850 |
. . . . . . . . . 10
⊢ (𝑡 = (𝒫 𝑠 ∩ Fin) → ∪ 𝑡 =
∪ (𝒫 𝑠 ∩ Fin)) |
9 | 8 | fveq2d 6778 |
. . . . . . . . 9
⊢ (𝑡 = (𝒫 𝑠 ∩ Fin) → (𝐹‘∪ 𝑡) = (𝐹‘∪
(𝒫 𝑠 ∩
Fin))) |
10 | | imaeq2 5965 |
. . . . . . . . . 10
⊢ (𝑡 = (𝒫 𝑠 ∩ Fin) → (𝐹 “ 𝑡) = (𝐹 “ (𝒫 𝑠 ∩ Fin))) |
11 | 10 | unieqd 4853 |
. . . . . . . . 9
⊢ (𝑡 = (𝒫 𝑠 ∩ Fin) → ∪ (𝐹
“ 𝑡) = ∪ (𝐹
“ (𝒫 𝑠 ∩
Fin))) |
12 | 9, 11 | eqeq12d 2754 |
. . . . . . . 8
⊢ (𝑡 = (𝒫 𝑠 ∩ Fin) → ((𝐹‘∪ 𝑡) = ∪
(𝐹 “ 𝑡) ↔ (𝐹‘∪
(𝒫 𝑠 ∩ Fin)) =
∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)))) |
13 | 7, 12 | imbi12d 345 |
. . . . . . 7
⊢ (𝑡 = (𝒫 𝑠 ∩ Fin) → (((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) =
∪ (𝐹 “ 𝑡)) ↔ ((toInc‘(𝒫 𝑠 ∩ Fin)) ∈ Dirset
→ (𝐹‘∪ (𝒫 𝑠 ∩ Fin)) = ∪
(𝐹 “ (𝒫 𝑠 ∩ Fin))))) |
14 | | simplr 766 |
. . . . . . 7
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑡 ∈ 𝒫 𝒫
𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) =
∪ (𝐹 “ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) → ∀𝑡 ∈ 𝒫 𝒫 𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) = ∪
(𝐹 “ 𝑡))) |
15 | | inss1 4162 |
. . . . . . . . . 10
⊢
(𝒫 𝑠 ∩
Fin) ⊆ 𝒫 𝑠 |
16 | | elpwi 4542 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ 𝒫 𝑋 → 𝑠 ⊆ 𝑋) |
17 | 16 | sspwd 4548 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ 𝒫 𝑋 → 𝒫 𝑠 ⊆ 𝒫 𝑋) |
18 | 17 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠 ∈ 𝒫 𝑋) → 𝒫 𝑠 ⊆ 𝒫 𝑋) |
19 | 15, 18 | sstrid 3932 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠 ∈ 𝒫 𝑋) → (𝒫 𝑠 ∩ Fin) ⊆ 𝒫 𝑋) |
20 | | vpwex 5300 |
. . . . . . . . . . 11
⊢ 𝒫
𝑠 ∈ V |
21 | 20 | inex1 5241 |
. . . . . . . . . 10
⊢
(𝒫 𝑠 ∩
Fin) ∈ V |
22 | 21 | elpw 4537 |
. . . . . . . . 9
⊢
((𝒫 𝑠 ∩
Fin) ∈ 𝒫 𝒫 𝑋 ↔ (𝒫 𝑠 ∩ Fin) ⊆ 𝒫 𝑋) |
23 | 19, 22 | sylibr 233 |
. . . . . . . 8
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠 ∈ 𝒫 𝑋) → (𝒫 𝑠 ∩ Fin) ∈ 𝒫 𝒫 𝑋) |
24 | 23 | adantlr 712 |
. . . . . . 7
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑡 ∈ 𝒫 𝒫
𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) =
∪ (𝐹 “ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) → (𝒫 𝑠 ∩ Fin) ∈ 𝒫 𝒫 𝑋) |
25 | 13, 14, 24 | rspcdva 3562 |
. . . . . 6
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑡 ∈ 𝒫 𝒫
𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) =
∪ (𝐹 “ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) → ((toInc‘(𝒫 𝑠 ∩ Fin)) ∈ Dirset
→ (𝐹‘∪ (𝒫 𝑠 ∩ Fin)) = ∪
(𝐹 “ (𝒫 𝑠 ∩ Fin)))) |
26 | 5, 25 | mpd 15 |
. . . . 5
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑡 ∈ 𝒫 𝒫
𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) =
∪ (𝐹 “ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) → (𝐹‘∪
(𝒫 𝑠 ∩ Fin)) =
∪ (𝐹 “ (𝒫 𝑠 ∩ Fin))) |
27 | 2, 26 | eqtr3id 2792 |
. . . 4
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑡 ∈ 𝒫 𝒫
𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) =
∪ (𝐹 “ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) → (𝐹‘𝑠) = ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin))) |
28 | 27 | ralrimiva 3103 |
. . 3
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑡 ∈ 𝒫 𝒫
𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) =
∪ (𝐹 “ 𝑡))) → ∀𝑠 ∈ 𝒫 𝑋(𝐹‘𝑠) = ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin))) |
29 | 28 | ex 413 |
. 2
⊢ (𝐶 ∈ (Moore‘𝑋) → (∀𝑡 ∈ 𝒫 𝒫
𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) =
∪ (𝐹 “ 𝑡)) → ∀𝑠 ∈ 𝒫 𝑋(𝐹‘𝑠) = ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)))) |
30 | 29 | imdistani 569 |
1
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑡 ∈ 𝒫 𝒫
𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) =
∪ (𝐹 “ 𝑡))) → (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋(𝐹‘𝑠) = ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)))) |