Step | Hyp | Ref
| Expression |
1 | | mresspw 16252 |
. . . . 5
⊢ (𝑎 ∈ (Moore‘𝑋) → 𝑎 ⊆ 𝒫 𝑋) |
2 | | selpw 4165 |
. . . . 5
⊢ (𝑎 ∈ 𝒫 𝒫
𝑋 ↔ 𝑎 ⊆ 𝒫 𝑋) |
3 | 1, 2 | sylibr 224 |
. . . 4
⊢ (𝑎 ∈ (Moore‘𝑋) → 𝑎 ∈ 𝒫 𝒫 𝑋) |
4 | 3 | ssriv 3607 |
. . 3
⊢
(Moore‘𝑋)
⊆ 𝒫 𝒫 𝑋 |
5 | 4 | a1i 11 |
. 2
⊢ (𝑋 ∈ 𝑉 → (Moore‘𝑋) ⊆ 𝒫 𝒫 𝑋) |
6 | | ssid 3624 |
. . . 4
⊢ 𝒫
𝑋 ⊆ 𝒫 𝑋 |
7 | 6 | a1i 11 |
. . 3
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ⊆ 𝒫 𝑋) |
8 | | pwidg 4173 |
. . 3
⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ 𝒫 𝑋) |
9 | | intssuni2 4502 |
. . . . . 6
⊢ ((𝑎 ⊆ 𝒫 𝑋 ∧ 𝑎 ≠ ∅) → ∩ 𝑎
⊆ ∪ 𝒫 𝑋) |
10 | 9 | 3adant1 1079 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ 𝒫 𝑋 ∧ 𝑎 ≠ ∅) → ∩ 𝑎
⊆ ∪ 𝒫 𝑋) |
11 | | unipw 4918 |
. . . . 5
⊢ ∪ 𝒫 𝑋 = 𝑋 |
12 | 10, 11 | syl6sseq 3651 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ 𝒫 𝑋 ∧ 𝑎 ≠ ∅) → ∩ 𝑎
⊆ 𝑋) |
13 | | elpw2g 4827 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → (∩ 𝑎 ∈ 𝒫 𝑋 ↔ ∩ 𝑎
⊆ 𝑋)) |
14 | 13 | 3ad2ant1 1082 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ 𝒫 𝑋 ∧ 𝑎 ≠ ∅) → (∩ 𝑎
∈ 𝒫 𝑋 ↔
∩ 𝑎 ⊆ 𝑋)) |
15 | 12, 14 | mpbird 247 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ 𝒫 𝑋 ∧ 𝑎 ≠ ∅) → ∩ 𝑎
∈ 𝒫 𝑋) |
16 | 7, 8, 15 | ismred 16262 |
. 2
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ (Moore‘𝑋)) |
17 | | n0 3931 |
. . . . 5
⊢ (𝑎 ≠ ∅ ↔
∃𝑏 𝑏 ∈ 𝑎) |
18 | | intss1 4492 |
. . . . . . . . 9
⊢ (𝑏 ∈ 𝑎 → ∩ 𝑎 ⊆ 𝑏) |
19 | 18 | adantl 482 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋)) ∧ 𝑏 ∈ 𝑎) → ∩ 𝑎 ⊆ 𝑏) |
20 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋)) → 𝑎 ⊆ (Moore‘𝑋)) |
21 | 20 | sselda 3603 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋)) ∧ 𝑏 ∈ 𝑎) → 𝑏 ∈ (Moore‘𝑋)) |
22 | | mresspw 16252 |
. . . . . . . . 9
⊢ (𝑏 ∈ (Moore‘𝑋) → 𝑏 ⊆ 𝒫 𝑋) |
23 | 21, 22 | syl 17 |
. . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋)) ∧ 𝑏 ∈ 𝑎) → 𝑏 ⊆ 𝒫 𝑋) |
24 | 19, 23 | sstrd 3613 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋)) ∧ 𝑏 ∈ 𝑎) → ∩ 𝑎 ⊆ 𝒫 𝑋) |
25 | 24 | ex 450 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋)) → (𝑏 ∈ 𝑎 → ∩ 𝑎 ⊆ 𝒫 𝑋)) |
26 | 25 | exlimdv 1861 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋)) → (∃𝑏 𝑏 ∈ 𝑎 → ∩ 𝑎 ⊆ 𝒫 𝑋)) |
27 | 17, 26 | syl5bi 232 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋)) → (𝑎 ≠ ∅ → ∩ 𝑎
⊆ 𝒫 𝑋)) |
28 | 27 | 3impia 1261 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) → ∩ 𝑎
⊆ 𝒫 𝑋) |
29 | | simp2 1062 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) → 𝑎 ⊆ (Moore‘𝑋)) |
30 | 29 | sselda 3603 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) ∧ 𝑏 ∈ 𝑎) → 𝑏 ∈ (Moore‘𝑋)) |
31 | | mre1cl 16254 |
. . . . . 6
⊢ (𝑏 ∈ (Moore‘𝑋) → 𝑋 ∈ 𝑏) |
32 | 30, 31 | syl 17 |
. . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) ∧ 𝑏 ∈ 𝑎) → 𝑋 ∈ 𝑏) |
33 | 32 | ralrimiva 2966 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) → ∀𝑏 ∈ 𝑎 𝑋 ∈ 𝑏) |
34 | | elintg 4483 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ ∩ 𝑎 ↔ ∀𝑏 ∈ 𝑎 𝑋 ∈ 𝑏)) |
35 | 34 | 3ad2ant1 1082 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) → (𝑋 ∈ ∩ 𝑎 ↔ ∀𝑏 ∈ 𝑎 𝑋 ∈ 𝑏)) |
36 | 33, 35 | mpbird 247 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) → 𝑋 ∈ ∩ 𝑎) |
37 | | simp12 1092 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) ∧ 𝑏 ⊆ ∩ 𝑎 ∧ 𝑏 ≠ ∅) → 𝑎 ⊆ (Moore‘𝑋)) |
38 | 37 | sselda 3603 |
. . . . . 6
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) ∧ 𝑏 ⊆ ∩ 𝑎 ∧ 𝑏 ≠ ∅) ∧ 𝑐 ∈ 𝑎) → 𝑐 ∈ (Moore‘𝑋)) |
39 | | simpl2 1065 |
. . . . . . 7
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) ∧ 𝑏 ⊆ ∩ 𝑎 ∧ 𝑏 ≠ ∅) ∧ 𝑐 ∈ 𝑎) → 𝑏 ⊆ ∩ 𝑎) |
40 | | intss1 4492 |
. . . . . . . 8
⊢ (𝑐 ∈ 𝑎 → ∩ 𝑎 ⊆ 𝑐) |
41 | 40 | adantl 482 |
. . . . . . 7
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) ∧ 𝑏 ⊆ ∩ 𝑎 ∧ 𝑏 ≠ ∅) ∧ 𝑐 ∈ 𝑎) → ∩ 𝑎 ⊆ 𝑐) |
42 | 39, 41 | sstrd 3613 |
. . . . . 6
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) ∧ 𝑏 ⊆ ∩ 𝑎 ∧ 𝑏 ≠ ∅) ∧ 𝑐 ∈ 𝑎) → 𝑏 ⊆ 𝑐) |
43 | | simpl3 1066 |
. . . . . 6
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) ∧ 𝑏 ⊆ ∩ 𝑎 ∧ 𝑏 ≠ ∅) ∧ 𝑐 ∈ 𝑎) → 𝑏 ≠ ∅) |
44 | | mreintcl 16255 |
. . . . . 6
⊢ ((𝑐 ∈ (Moore‘𝑋) ∧ 𝑏 ⊆ 𝑐 ∧ 𝑏 ≠ ∅) → ∩ 𝑏
∈ 𝑐) |
45 | 38, 42, 43, 44 | syl3anc 1326 |
. . . . 5
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) ∧ 𝑏 ⊆ ∩ 𝑎 ∧ 𝑏 ≠ ∅) ∧ 𝑐 ∈ 𝑎) → ∩ 𝑏 ∈ 𝑐) |
46 | 45 | ralrimiva 2966 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) ∧ 𝑏 ⊆ ∩ 𝑎 ∧ 𝑏 ≠ ∅) → ∀𝑐 ∈ 𝑎 ∩ 𝑏 ∈ 𝑐) |
47 | | intex 4820 |
. . . . . 6
⊢ (𝑏 ≠ ∅ ↔ ∩ 𝑏
∈ V) |
48 | | elintg 4483 |
. . . . . 6
⊢ (∩ 𝑏
∈ V → (∩ 𝑏 ∈ ∩ 𝑎 ↔ ∀𝑐 ∈ 𝑎 ∩ 𝑏 ∈ 𝑐)) |
49 | 47, 48 | sylbi 207 |
. . . . 5
⊢ (𝑏 ≠ ∅ → (∩ 𝑏
∈ ∩ 𝑎 ↔ ∀𝑐 ∈ 𝑎 ∩ 𝑏 ∈ 𝑐)) |
50 | 49 | 3ad2ant3 1084 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) ∧ 𝑏 ⊆ ∩ 𝑎 ∧ 𝑏 ≠ ∅) → (∩ 𝑏
∈ ∩ 𝑎 ↔ ∀𝑐 ∈ 𝑎 ∩ 𝑏 ∈ 𝑐)) |
51 | 46, 50 | mpbird 247 |
. . 3
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) ∧ 𝑏 ⊆ ∩ 𝑎 ∧ 𝑏 ≠ ∅) → ∩ 𝑏
∈ ∩ 𝑎) |
52 | 28, 36, 51 | ismred 16262 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) → ∩ 𝑎
∈ (Moore‘𝑋)) |
53 | 5, 16, 52 | ismred 16262 |
1
⊢ (𝑋 ∈ 𝑉 → (Moore‘𝑋) ∈ (Moore‘𝒫 𝑋)) |