Proof of Theorem isacs5lem
Step | Hyp | Ref
| Expression |
1 | | unifpw 8821 |
. . . . . 6
⊢ ∪ (𝒫 𝑠 ∩ Fin) = 𝑠 |
2 | 1 | fveq2i 6667 |
. . . . 5
⊢ (𝐹‘∪ (𝒫 𝑠 ∩ Fin)) = (𝐹‘𝑠) |
3 | | vex 3497 |
. . . . . . 7
⊢ 𝑠 ∈ V |
4 | | fpwipodrs 17768 |
. . . . . . 7
⊢ (𝑠 ∈ V →
(toInc‘(𝒫 𝑠
∩ Fin)) ∈ Dirset) |
5 | 3, 4 | mp1i 13 |
. . . . . 6
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑡 ∈ 𝒫 𝒫
𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) =
∪ (𝐹 “ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) → (toInc‘(𝒫 𝑠 ∩ Fin)) ∈
Dirset) |
6 | | fveq2 6664 |
. . . . . . . . 9
⊢ (𝑡 = (𝒫 𝑠 ∩ Fin) → (toInc‘𝑡) = (toInc‘(𝒫
𝑠 ∩
Fin))) |
7 | 6 | eleq1d 2897 |
. . . . . . . 8
⊢ (𝑡 = (𝒫 𝑠 ∩ Fin) → ((toInc‘𝑡) ∈ Dirset ↔
(toInc‘(𝒫 𝑠
∩ Fin)) ∈ Dirset)) |
8 | | unieq 4839 |
. . . . . . . . . 10
⊢ (𝑡 = (𝒫 𝑠 ∩ Fin) → ∪ 𝑡 =
∪ (𝒫 𝑠 ∩ Fin)) |
9 | 8 | fveq2d 6668 |
. . . . . . . . 9
⊢ (𝑡 = (𝒫 𝑠 ∩ Fin) → (𝐹‘∪ 𝑡) = (𝐹‘∪
(𝒫 𝑠 ∩
Fin))) |
10 | | imaeq2 5919 |
. . . . . . . . . 10
⊢ (𝑡 = (𝒫 𝑠 ∩ Fin) → (𝐹 “ 𝑡) = (𝐹 “ (𝒫 𝑠 ∩ Fin))) |
11 | 10 | unieqd 4841 |
. . . . . . . . 9
⊢ (𝑡 = (𝒫 𝑠 ∩ Fin) → ∪ (𝐹
“ 𝑡) = ∪ (𝐹
“ (𝒫 𝑠 ∩
Fin))) |
12 | 9, 11 | eqeq12d 2837 |
. . . . . . . 8
⊢ (𝑡 = (𝒫 𝑠 ∩ Fin) → ((𝐹‘∪ 𝑡) = ∪
(𝐹 “ 𝑡) ↔ (𝐹‘∪
(𝒫 𝑠 ∩ Fin)) =
∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)))) |
13 | 7, 12 | imbi12d 347 |
. . . . . . 7
⊢ (𝑡 = (𝒫 𝑠 ∩ Fin) → (((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) =
∪ (𝐹 “ 𝑡)) ↔ ((toInc‘(𝒫 𝑠 ∩ Fin)) ∈ Dirset
→ (𝐹‘∪ (𝒫 𝑠 ∩ Fin)) = ∪
(𝐹 “ (𝒫 𝑠 ∩ Fin))))) |
14 | | simplr 767 |
. . . . . . 7
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑡 ∈ 𝒫 𝒫
𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) =
∪ (𝐹 “ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) → ∀𝑡 ∈ 𝒫 𝒫 𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) = ∪
(𝐹 “ 𝑡))) |
15 | | inss1 4204 |
. . . . . . . . . 10
⊢
(𝒫 𝑠 ∩
Fin) ⊆ 𝒫 𝑠 |
16 | | elpwi 4550 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ 𝒫 𝑋 → 𝑠 ⊆ 𝑋) |
17 | | sspwb 5333 |
. . . . . . . . . . . 12
⊢ (𝑠 ⊆ 𝑋 ↔ 𝒫 𝑠 ⊆ 𝒫 𝑋) |
18 | 16, 17 | sylib 220 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ 𝒫 𝑋 → 𝒫 𝑠 ⊆ 𝒫 𝑋) |
19 | 18 | adantl 484 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠 ∈ 𝒫 𝑋) → 𝒫 𝑠 ⊆ 𝒫 𝑋) |
20 | 15, 19 | sstrid 3977 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠 ∈ 𝒫 𝑋) → (𝒫 𝑠 ∩ Fin) ⊆ 𝒫 𝑋) |
21 | | vpwex 5270 |
. . . . . . . . . . 11
⊢ 𝒫
𝑠 ∈ V |
22 | 21 | inex1 5213 |
. . . . . . . . . 10
⊢
(𝒫 𝑠 ∩
Fin) ∈ V |
23 | 22 | elpw 4545 |
. . . . . . . . 9
⊢
((𝒫 𝑠 ∩
Fin) ∈ 𝒫 𝒫 𝑋 ↔ (𝒫 𝑠 ∩ Fin) ⊆ 𝒫 𝑋) |
24 | 20, 23 | sylibr 236 |
. . . . . . . 8
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑠 ∈ 𝒫 𝑋) → (𝒫 𝑠 ∩ Fin) ∈ 𝒫 𝒫 𝑋) |
25 | 24 | adantlr 713 |
. . . . . . 7
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑡 ∈ 𝒫 𝒫
𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) =
∪ (𝐹 “ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) → (𝒫 𝑠 ∩ Fin) ∈ 𝒫 𝒫 𝑋) |
26 | 13, 14, 25 | rspcdva 3624 |
. . . . . 6
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑡 ∈ 𝒫 𝒫
𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) =
∪ (𝐹 “ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) → ((toInc‘(𝒫 𝑠 ∩ Fin)) ∈ Dirset
→ (𝐹‘∪ (𝒫 𝑠 ∩ Fin)) = ∪
(𝐹 “ (𝒫 𝑠 ∩ Fin)))) |
27 | 5, 26 | mpd 15 |
. . . . 5
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑡 ∈ 𝒫 𝒫
𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) =
∪ (𝐹 “ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) → (𝐹‘∪
(𝒫 𝑠 ∩ Fin)) =
∪ (𝐹 “ (𝒫 𝑠 ∩ Fin))) |
28 | 2, 27 | syl5eqr 2870 |
. . . 4
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑡 ∈ 𝒫 𝒫
𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) =
∪ (𝐹 “ 𝑡))) ∧ 𝑠 ∈ 𝒫 𝑋) → (𝐹‘𝑠) = ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin))) |
29 | 28 | ralrimiva 3182 |
. . 3
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑡 ∈ 𝒫 𝒫
𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) =
∪ (𝐹 “ 𝑡))) → ∀𝑠 ∈ 𝒫 𝑋(𝐹‘𝑠) = ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin))) |
30 | 29 | ex 415 |
. 2
⊢ (𝐶 ∈ (Moore‘𝑋) → (∀𝑡 ∈ 𝒫 𝒫
𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) =
∪ (𝐹 “ 𝑡)) → ∀𝑠 ∈ 𝒫 𝑋(𝐹‘𝑠) = ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)))) |
31 | 30 | imdistani 571 |
1
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑡 ∈ 𝒫 𝒫
𝑋((toInc‘𝑡) ∈ Dirset → (𝐹‘∪ 𝑡) =
∪ (𝐹 “ 𝑡))) → (𝐶 ∈ (Moore‘𝑋) ∧ ∀𝑠 ∈ 𝒫 𝑋(𝐹‘𝑠) = ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)))) |