| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mresspw 17636 | . . . . 5
⊢ (𝑎 ∈ (Moore‘𝑋) → 𝑎 ⊆ 𝒫 𝑋) | 
| 2 |  | velpw 4604 | . . . . 5
⊢ (𝑎 ∈ 𝒫 𝒫
𝑋 ↔ 𝑎 ⊆ 𝒫 𝑋) | 
| 3 | 1, 2 | sylibr 234 | . . . 4
⊢ (𝑎 ∈ (Moore‘𝑋) → 𝑎 ∈ 𝒫 𝒫 𝑋) | 
| 4 | 3 | ssriv 3986 | . . 3
⊢
(Moore‘𝑋)
⊆ 𝒫 𝒫 𝑋 | 
| 5 | 4 | a1i 11 | . 2
⊢ (𝑋 ∈ 𝑉 → (Moore‘𝑋) ⊆ 𝒫 𝒫 𝑋) | 
| 6 |  | ssidd 4006 | . . 3
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ⊆ 𝒫 𝑋) | 
| 7 |  | pwidg 4619 | . . 3
⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ 𝒫 𝑋) | 
| 8 |  | intssuni2 4972 | . . . . . 6
⊢ ((𝑎 ⊆ 𝒫 𝑋 ∧ 𝑎 ≠ ∅) → ∩ 𝑎
⊆ ∪ 𝒫 𝑋) | 
| 9 | 8 | 3adant1 1130 | . . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ 𝒫 𝑋 ∧ 𝑎 ≠ ∅) → ∩ 𝑎
⊆ ∪ 𝒫 𝑋) | 
| 10 |  | unipw 5454 | . . . . 5
⊢ ∪ 𝒫 𝑋 = 𝑋 | 
| 11 | 9, 10 | sseqtrdi 4023 | . . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ 𝒫 𝑋 ∧ 𝑎 ≠ ∅) → ∩ 𝑎
⊆ 𝑋) | 
| 12 |  | elpw2g 5332 | . . . . 5
⊢ (𝑋 ∈ 𝑉 → (∩ 𝑎 ∈ 𝒫 𝑋 ↔ ∩ 𝑎
⊆ 𝑋)) | 
| 13 | 12 | 3ad2ant1 1133 | . . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ 𝒫 𝑋 ∧ 𝑎 ≠ ∅) → (∩ 𝑎
∈ 𝒫 𝑋 ↔
∩ 𝑎 ⊆ 𝑋)) | 
| 14 | 11, 13 | mpbird 257 | . . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ 𝒫 𝑋 ∧ 𝑎 ≠ ∅) → ∩ 𝑎
∈ 𝒫 𝑋) | 
| 15 | 6, 7, 14 | ismred 17646 | . 2
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ (Moore‘𝑋)) | 
| 16 |  | n0 4352 | . . . . 5
⊢ (𝑎 ≠ ∅ ↔
∃𝑏 𝑏 ∈ 𝑎) | 
| 17 |  | intss1 4962 | . . . . . . . . 9
⊢ (𝑏 ∈ 𝑎 → ∩ 𝑎 ⊆ 𝑏) | 
| 18 | 17 | adantl 481 | . . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋)) ∧ 𝑏 ∈ 𝑎) → ∩ 𝑎 ⊆ 𝑏) | 
| 19 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋)) → 𝑎 ⊆ (Moore‘𝑋)) | 
| 20 | 19 | sselda 3982 | . . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋)) ∧ 𝑏 ∈ 𝑎) → 𝑏 ∈ (Moore‘𝑋)) | 
| 21 |  | mresspw 17636 | . . . . . . . . 9
⊢ (𝑏 ∈ (Moore‘𝑋) → 𝑏 ⊆ 𝒫 𝑋) | 
| 22 | 20, 21 | syl 17 | . . . . . . . 8
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋)) ∧ 𝑏 ∈ 𝑎) → 𝑏 ⊆ 𝒫 𝑋) | 
| 23 | 18, 22 | sstrd 3993 | . . . . . . 7
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋)) ∧ 𝑏 ∈ 𝑎) → ∩ 𝑎 ⊆ 𝒫 𝑋) | 
| 24 | 23 | ex 412 | . . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋)) → (𝑏 ∈ 𝑎 → ∩ 𝑎 ⊆ 𝒫 𝑋)) | 
| 25 | 24 | exlimdv 1932 | . . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋)) → (∃𝑏 𝑏 ∈ 𝑎 → ∩ 𝑎 ⊆ 𝒫 𝑋)) | 
| 26 | 16, 25 | biimtrid 242 | . . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋)) → (𝑎 ≠ ∅ → ∩ 𝑎
⊆ 𝒫 𝑋)) | 
| 27 | 26 | 3impia 1117 | . . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) → ∩ 𝑎
⊆ 𝒫 𝑋) | 
| 28 |  | simp2 1137 | . . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) → 𝑎 ⊆ (Moore‘𝑋)) | 
| 29 | 28 | sselda 3982 | . . . . . 6
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) ∧ 𝑏 ∈ 𝑎) → 𝑏 ∈ (Moore‘𝑋)) | 
| 30 |  | mre1cl 17638 | . . . . . 6
⊢ (𝑏 ∈ (Moore‘𝑋) → 𝑋 ∈ 𝑏) | 
| 31 | 29, 30 | syl 17 | . . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) ∧ 𝑏 ∈ 𝑎) → 𝑋 ∈ 𝑏) | 
| 32 | 31 | ralrimiva 3145 | . . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) → ∀𝑏 ∈ 𝑎 𝑋 ∈ 𝑏) | 
| 33 |  | elintg 4953 | . . . . 5
⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ ∩ 𝑎 ↔ ∀𝑏 ∈ 𝑎 𝑋 ∈ 𝑏)) | 
| 34 | 33 | 3ad2ant1 1133 | . . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) → (𝑋 ∈ ∩ 𝑎 ↔ ∀𝑏 ∈ 𝑎 𝑋 ∈ 𝑏)) | 
| 35 | 32, 34 | mpbird 257 | . . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) → 𝑋 ∈ ∩ 𝑎) | 
| 36 |  | simp12 1204 | . . . . . . 7
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) ∧ 𝑏 ⊆ ∩ 𝑎 ∧ 𝑏 ≠ ∅) → 𝑎 ⊆ (Moore‘𝑋)) | 
| 37 | 36 | sselda 3982 | . . . . . 6
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) ∧ 𝑏 ⊆ ∩ 𝑎 ∧ 𝑏 ≠ ∅) ∧ 𝑐 ∈ 𝑎) → 𝑐 ∈ (Moore‘𝑋)) | 
| 38 |  | simpl2 1192 | . . . . . . 7
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) ∧ 𝑏 ⊆ ∩ 𝑎 ∧ 𝑏 ≠ ∅) ∧ 𝑐 ∈ 𝑎) → 𝑏 ⊆ ∩ 𝑎) | 
| 39 |  | intss1 4962 | . . . . . . . 8
⊢ (𝑐 ∈ 𝑎 → ∩ 𝑎 ⊆ 𝑐) | 
| 40 | 39 | adantl 481 | . . . . . . 7
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) ∧ 𝑏 ⊆ ∩ 𝑎 ∧ 𝑏 ≠ ∅) ∧ 𝑐 ∈ 𝑎) → ∩ 𝑎 ⊆ 𝑐) | 
| 41 | 38, 40 | sstrd 3993 | . . . . . 6
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) ∧ 𝑏 ⊆ ∩ 𝑎 ∧ 𝑏 ≠ ∅) ∧ 𝑐 ∈ 𝑎) → 𝑏 ⊆ 𝑐) | 
| 42 |  | simpl3 1193 | . . . . . 6
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) ∧ 𝑏 ⊆ ∩ 𝑎 ∧ 𝑏 ≠ ∅) ∧ 𝑐 ∈ 𝑎) → 𝑏 ≠ ∅) | 
| 43 |  | mreintcl 17639 | . . . . . 6
⊢ ((𝑐 ∈ (Moore‘𝑋) ∧ 𝑏 ⊆ 𝑐 ∧ 𝑏 ≠ ∅) → ∩ 𝑏
∈ 𝑐) | 
| 44 | 37, 41, 42, 43 | syl3anc 1372 | . . . . 5
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) ∧ 𝑏 ⊆ ∩ 𝑎 ∧ 𝑏 ≠ ∅) ∧ 𝑐 ∈ 𝑎) → ∩ 𝑏 ∈ 𝑐) | 
| 45 | 44 | ralrimiva 3145 | . . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) ∧ 𝑏 ⊆ ∩ 𝑎 ∧ 𝑏 ≠ ∅) → ∀𝑐 ∈ 𝑎 ∩ 𝑏 ∈ 𝑐) | 
| 46 |  | intex 5343 | . . . . . 6
⊢ (𝑏 ≠ ∅ ↔ ∩ 𝑏
∈ V) | 
| 47 |  | elintg 4953 | . . . . . 6
⊢ (∩ 𝑏
∈ V → (∩ 𝑏 ∈ ∩ 𝑎 ↔ ∀𝑐 ∈ 𝑎 ∩ 𝑏 ∈ 𝑐)) | 
| 48 | 46, 47 | sylbi 217 | . . . . 5
⊢ (𝑏 ≠ ∅ → (∩ 𝑏
∈ ∩ 𝑎 ↔ ∀𝑐 ∈ 𝑎 ∩ 𝑏 ∈ 𝑐)) | 
| 49 | 48 | 3ad2ant3 1135 | . . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) ∧ 𝑏 ⊆ ∩ 𝑎 ∧ 𝑏 ≠ ∅) → (∩ 𝑏
∈ ∩ 𝑎 ↔ ∀𝑐 ∈ 𝑎 ∩ 𝑏 ∈ 𝑐)) | 
| 50 | 45, 49 | mpbird 257 | . . 3
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) ∧ 𝑏 ⊆ ∩ 𝑎 ∧ 𝑏 ≠ ∅) → ∩ 𝑏
∈ ∩ 𝑎) | 
| 51 | 27, 35, 50 | ismred 17646 | . 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑎 ⊆ (Moore‘𝑋) ∧ 𝑎 ≠ ∅) → ∩ 𝑎
∈ (Moore‘𝑋)) | 
| 52 | 5, 15, 51 | ismred 17646 | 1
⊢ (𝑋 ∈ 𝑉 → (Moore‘𝑋) ∈ (Moore‘𝒫 𝑋)) |