| Step | Hyp | Ref
| Expression |
| 1 | | inss2 4238 |
. . 3
⊢ (𝐶 ∩ 𝒫 𝐴) ⊆ 𝒫 𝐴 |
| 2 | 1 | a1i 11 |
. 2
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐴 ∈ 𝐶) → (𝐶 ∩ 𝒫 𝐴) ⊆ 𝒫 𝐴) |
| 3 | | simpr 484 |
. . 3
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ 𝐶) |
| 4 | | pwidg 4620 |
. . . 4
⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ 𝒫 𝐴) |
| 5 | 4 | adantl 481 |
. . 3
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ 𝒫 𝐴) |
| 6 | 3, 5 | elind 4200 |
. 2
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐴 ∈ 𝐶) → 𝐴 ∈ (𝐶 ∩ 𝒫 𝐴)) |
| 7 | | simp1l 1198 |
. . . 4
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ 𝐴 ∈ 𝐶) ∧ 𝑥 ⊆ (𝐶 ∩ 𝒫 𝐴) ∧ 𝑥 ≠ ∅) → 𝐶 ∈ (Moore‘𝑋)) |
| 8 | | inss1 4237 |
. . . . . 6
⊢ (𝐶 ∩ 𝒫 𝐴) ⊆ 𝐶 |
| 9 | | sstr 3992 |
. . . . . 6
⊢ ((𝑥 ⊆ (𝐶 ∩ 𝒫 𝐴) ∧ (𝐶 ∩ 𝒫 𝐴) ⊆ 𝐶) → 𝑥 ⊆ 𝐶) |
| 10 | 8, 9 | mpan2 691 |
. . . . 5
⊢ (𝑥 ⊆ (𝐶 ∩ 𝒫 𝐴) → 𝑥 ⊆ 𝐶) |
| 11 | 10 | 3ad2ant2 1135 |
. . . 4
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ 𝐴 ∈ 𝐶) ∧ 𝑥 ⊆ (𝐶 ∩ 𝒫 𝐴) ∧ 𝑥 ≠ ∅) → 𝑥 ⊆ 𝐶) |
| 12 | | simp3 1139 |
. . . 4
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ 𝐴 ∈ 𝐶) ∧ 𝑥 ⊆ (𝐶 ∩ 𝒫 𝐴) ∧ 𝑥 ≠ ∅) → 𝑥 ≠ ∅) |
| 13 | | mreintcl 17638 |
. . . 4
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅) → ∩ 𝑥
∈ 𝐶) |
| 14 | 7, 11, 12, 13 | syl3anc 1373 |
. . 3
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ 𝐴 ∈ 𝐶) ∧ 𝑥 ⊆ (𝐶 ∩ 𝒫 𝐴) ∧ 𝑥 ≠ ∅) → ∩ 𝑥
∈ 𝐶) |
| 15 | | sstr 3992 |
. . . . . . . 8
⊢ ((𝑥 ⊆ (𝐶 ∩ 𝒫 𝐴) ∧ (𝐶 ∩ 𝒫 𝐴) ⊆ 𝒫 𝐴) → 𝑥 ⊆ 𝒫 𝐴) |
| 16 | 1, 15 | mpan2 691 |
. . . . . . 7
⊢ (𝑥 ⊆ (𝐶 ∩ 𝒫 𝐴) → 𝑥 ⊆ 𝒫 𝐴) |
| 17 | 16 | 3ad2ant2 1135 |
. . . . . 6
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ 𝐴 ∈ 𝐶) ∧ 𝑥 ⊆ (𝐶 ∩ 𝒫 𝐴) ∧ 𝑥 ≠ ∅) → 𝑥 ⊆ 𝒫 𝐴) |
| 18 | | intssuni2 4973 |
. . . . . 6
⊢ ((𝑥 ⊆ 𝒫 𝐴 ∧ 𝑥 ≠ ∅) → ∩ 𝑥
⊆ ∪ 𝒫 𝐴) |
| 19 | 17, 12, 18 | syl2anc 584 |
. . . . 5
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ 𝐴 ∈ 𝐶) ∧ 𝑥 ⊆ (𝐶 ∩ 𝒫 𝐴) ∧ 𝑥 ≠ ∅) → ∩ 𝑥
⊆ ∪ 𝒫 𝐴) |
| 20 | | unipw 5455 |
. . . . 5
⊢ ∪ 𝒫 𝐴 = 𝐴 |
| 21 | 19, 20 | sseqtrdi 4024 |
. . . 4
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ 𝐴 ∈ 𝐶) ∧ 𝑥 ⊆ (𝐶 ∩ 𝒫 𝐴) ∧ 𝑥 ≠ ∅) → ∩ 𝑥
⊆ 𝐴) |
| 22 | | elpw2g 5333 |
. . . . . 6
⊢ (𝐴 ∈ 𝐶 → (∩ 𝑥 ∈ 𝒫 𝐴 ↔ ∩ 𝑥
⊆ 𝐴)) |
| 23 | 22 | adantl 481 |
. . . . 5
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐴 ∈ 𝐶) → (∩ 𝑥 ∈ 𝒫 𝐴 ↔ ∩ 𝑥
⊆ 𝐴)) |
| 24 | 23 | 3ad2ant1 1134 |
. . . 4
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ 𝐴 ∈ 𝐶) ∧ 𝑥 ⊆ (𝐶 ∩ 𝒫 𝐴) ∧ 𝑥 ≠ ∅) → (∩ 𝑥
∈ 𝒫 𝐴 ↔
∩ 𝑥 ⊆ 𝐴)) |
| 25 | 21, 24 | mpbird 257 |
. . 3
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ 𝐴 ∈ 𝐶) ∧ 𝑥 ⊆ (𝐶 ∩ 𝒫 𝐴) ∧ 𝑥 ≠ ∅) → ∩ 𝑥
∈ 𝒫 𝐴) |
| 26 | 14, 25 | elind 4200 |
. 2
⊢ (((𝐶 ∈ (Moore‘𝑋) ∧ 𝐴 ∈ 𝐶) ∧ 𝑥 ⊆ (𝐶 ∩ 𝒫 𝐴) ∧ 𝑥 ≠ ∅) → ∩ 𝑥
∈ (𝐶 ∩ 𝒫
𝐴)) |
| 27 | 2, 6, 26 | ismred 17645 |
1
⊢ ((𝐶 ∈ (Moore‘𝑋) ∧ 𝐴 ∈ 𝐶) → (𝐶 ∩ 𝒫 𝐴) ∈ (Moore‘𝐴)) |