| Step | Hyp | Ref
| Expression |
| 1 | | unisng 4925 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} = 𝐴) |
| 2 | | snidg 4660 |
. . 3
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴}) |
| 3 | 1, 2 | eqeltrd 2841 |
. 2
⊢ (𝐴 ∈ 𝑉 → ∪ {𝐴} ∈ {𝐴}) |
| 4 | | df-ne 2941 |
. . . . . 6
⊢ (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅) |
| 5 | | sssn 4826 |
. . . . . 6
⊢ (𝑥 ⊆ {𝐴} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐴})) |
| 6 | | biorf 937 |
. . . . . . 7
⊢ (¬
𝑥 = ∅ → (𝑥 = {𝐴} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐴}))) |
| 7 | 6 | biimpar 477 |
. . . . . 6
⊢ ((¬
𝑥 = ∅ ∧ (𝑥 = ∅ ∨ 𝑥 = {𝐴})) → 𝑥 = {𝐴}) |
| 8 | 4, 5, 7 | syl2anb 598 |
. . . . 5
⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ {𝐴}) → 𝑥 = {𝐴}) |
| 9 | | inteq 4949 |
. . . . . . 7
⊢ (𝑥 = {𝐴} → ∩ 𝑥 = ∩
{𝐴}) |
| 10 | | intsng 4983 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → ∩ {𝐴} = 𝐴) |
| 11 | | eqtr 2760 |
. . . . . . . 8
⊢ ((∩ 𝑥 =
∩ {𝐴} ∧ ∩ {𝐴} = 𝐴) → ∩ 𝑥 = 𝐴) |
| 12 | 11 | ex 412 |
. . . . . . 7
⊢ (∩ 𝑥 =
∩ {𝐴} → (∩
{𝐴} = 𝐴 → ∩ 𝑥 = 𝐴)) |
| 13 | 9, 10, 12 | syl2im 40 |
. . . . . 6
⊢ (𝑥 = {𝐴} → (𝐴 ∈ 𝑉 → ∩ 𝑥 = 𝐴)) |
| 14 | | intex 5344 |
. . . . . . . 8
⊢ (𝑥 ≠ ∅ ↔ ∩ 𝑥
∈ V) |
| 15 | | elsng 4640 |
. . . . . . . 8
⊢ (∩ 𝑥
∈ V → (∩ 𝑥 ∈ {𝐴} ↔ ∩ 𝑥 = 𝐴)) |
| 16 | 14, 15 | sylbi 217 |
. . . . . . 7
⊢ (𝑥 ≠ ∅ → (∩ 𝑥
∈ {𝐴} ↔ ∩ 𝑥 =
𝐴)) |
| 17 | 16 | biimprd 248 |
. . . . . 6
⊢ (𝑥 ≠ ∅ → (∩ 𝑥 =
𝐴 → ∩ 𝑥
∈ {𝐴})) |
| 18 | 13, 17 | sylan9r 508 |
. . . . 5
⊢ ((𝑥 ≠ ∅ ∧ 𝑥 = {𝐴}) → (𝐴 ∈ 𝑉 → ∩ 𝑥 ∈ {𝐴})) |
| 19 | 8, 18 | syldan 591 |
. . . 4
⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ {𝐴}) → (𝐴 ∈ 𝑉 → ∩ 𝑥 ∈ {𝐴})) |
| 20 | 19 | ancoms 458 |
. . 3
⊢ ((𝑥 ⊆ {𝐴} ∧ 𝑥 ≠ ∅) → (𝐴 ∈ 𝑉 → ∩ 𝑥 ∈ {𝐴})) |
| 21 | 20 | impcom 407 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ⊆ {𝐴} ∧ 𝑥 ≠ ∅)) → ∩ 𝑥
∈ {𝐴}) |
| 22 | 3, 21 | bj-ismooredr2 37111 |
1
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ Moore) |