| Step | Hyp | Ref
| Expression |
| 1 | | sspwuni 5100 |
. . . . 5
⊢ (𝑋 ⊆ 𝒫 𝐴 ↔ ∪ 𝑋
⊆ 𝐴) |
| 2 | | compss.a |
. . . . . 6
⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥)) |
| 3 | 2 | isf34lem1 10412 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ ∪ 𝑋 ⊆ 𝐴) → (𝐹‘∪ 𝑋) = (𝐴 ∖ ∪ 𝑋)) |
| 4 | 1, 3 | sylan2b 594 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) → (𝐹‘∪ 𝑋) = (𝐴 ∖ ∪ 𝑋)) |
| 5 | 4 | adantrr 717 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (𝐹‘∪ 𝑋) = (𝐴 ∖ ∪ 𝑋)) |
| 6 | | simplrr 778 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑎) ∈ 𝑋)) → ¬ 𝑏 ∈ ∪ 𝑋) |
| 7 | | simprl 771 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋)) → 𝑏 ∈ 𝐴) |
| 8 | 7 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑎) ∈ 𝑋)) ∧ ¬ 𝑏 ∈ 𝑎) → 𝑏 ∈ 𝐴) |
| 9 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑎) ∈ 𝑋)) ∧ ¬ 𝑏 ∈ 𝑎) → ¬ 𝑏 ∈ 𝑎) |
| 10 | 8, 9 | eldifd 3962 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑎) ∈ 𝑋)) ∧ ¬ 𝑏 ∈ 𝑎) → 𝑏 ∈ (𝐴 ∖ 𝑎)) |
| 11 | | simplrr 778 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑎) ∈ 𝑋)) ∧ ¬ 𝑏 ∈ 𝑎) → (𝐴 ∖ 𝑎) ∈ 𝑋) |
| 12 | | elunii 4912 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ (𝐴 ∖ 𝑎) ∧ (𝐴 ∖ 𝑎) ∈ 𝑋) → 𝑏 ∈ ∪ 𝑋) |
| 13 | 10, 11, 12 | syl2anc 584 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑎) ∈ 𝑋)) ∧ ¬ 𝑏 ∈ 𝑎) → 𝑏 ∈ ∪ 𝑋) |
| 14 | 13 | ex 412 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑎) ∈ 𝑋)) → (¬ 𝑏 ∈ 𝑎 → 𝑏 ∈ ∪ 𝑋)) |
| 15 | 6, 14 | mt3d 148 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋)) ∧ (𝑎 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑎) ∈ 𝑋)) → 𝑏 ∈ 𝑎) |
| 16 | 15 | expr 456 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋)) ∧ 𝑎 ∈ 𝒫 𝐴) → ((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎)) |
| 17 | 16 | ralrimiva 3146 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋)) → ∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎)) |
| 18 | 17 | ex 412 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → ((𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋) → ∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎))) |
| 19 | | n0 4353 |
. . . . . . . . 9
⊢ (𝑋 ≠ ∅ ↔
∃𝑐 𝑐 ∈ 𝑋) |
| 20 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) → 𝑋 ⊆ 𝒫 𝐴) |
| 21 | 20 | sselda 3983 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) ∧ 𝑐 ∈ 𝑋) → 𝑐 ∈ 𝒫 𝐴) |
| 22 | 21 | elpwid 4609 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) ∧ 𝑐 ∈ 𝑋) → 𝑐 ⊆ 𝐴) |
| 23 | | dfss4 4269 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ 𝑐)) = 𝑐) |
| 24 | 22, 23 | sylib 218 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) ∧ 𝑐 ∈ 𝑋) → (𝐴 ∖ (𝐴 ∖ 𝑐)) = 𝑐) |
| 25 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) ∧ 𝑐 ∈ 𝑋) → 𝑐 ∈ 𝑋) |
| 26 | 24, 25 | eqeltrd 2841 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) ∧ 𝑐 ∈ 𝑋) → (𝐴 ∖ (𝐴 ∖ 𝑐)) ∈ 𝑋) |
| 27 | | difss 4136 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∖ 𝑐) ⊆ 𝐴 |
| 28 | | elpw2g 5333 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ 𝑉 → ((𝐴 ∖ 𝑐) ∈ 𝒫 𝐴 ↔ (𝐴 ∖ 𝑐) ⊆ 𝐴)) |
| 29 | 27, 28 | mpbiri 258 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∖ 𝑐) ∈ 𝒫 𝐴) |
| 30 | 29 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) ∧ 𝑐 ∈ 𝑋) → (𝐴 ∖ 𝑐) ∈ 𝒫 𝐴) |
| 31 | | difeq2 4120 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝐴 ∖ 𝑐) → (𝐴 ∖ 𝑎) = (𝐴 ∖ (𝐴 ∖ 𝑐))) |
| 32 | 31 | eleq1d 2826 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝐴 ∖ 𝑐) → ((𝐴 ∖ 𝑎) ∈ 𝑋 ↔ (𝐴 ∖ (𝐴 ∖ 𝑐)) ∈ 𝑋)) |
| 33 | | eleq2 2830 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝐴 ∖ 𝑐) → (𝑏 ∈ 𝑎 ↔ 𝑏 ∈ (𝐴 ∖ 𝑐))) |
| 34 | 32, 33 | imbi12d 344 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = (𝐴 ∖ 𝑐) → (((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎) ↔ ((𝐴 ∖ (𝐴 ∖ 𝑐)) ∈ 𝑋 → 𝑏 ∈ (𝐴 ∖ 𝑐)))) |
| 35 | 34 | rspcv 3618 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∖ 𝑐) ∈ 𝒫 𝐴 → (∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎) → ((𝐴 ∖ (𝐴 ∖ 𝑐)) ∈ 𝑋 → 𝑏 ∈ (𝐴 ∖ 𝑐)))) |
| 36 | 30, 35 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) ∧ 𝑐 ∈ 𝑋) → (∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎) → ((𝐴 ∖ (𝐴 ∖ 𝑐)) ∈ 𝑋 → 𝑏 ∈ (𝐴 ∖ 𝑐)))) |
| 37 | 26, 36 | mpid 44 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) ∧ 𝑐 ∈ 𝑋) → (∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎) → 𝑏 ∈ (𝐴 ∖ 𝑐))) |
| 38 | | eldifi 4131 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ (𝐴 ∖ 𝑐) → 𝑏 ∈ 𝐴) |
| 39 | 37, 38 | syl6 35 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) ∧ 𝑐 ∈ 𝑋) → (∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎) → 𝑏 ∈ 𝐴)) |
| 40 | 39 | ex 412 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) → (𝑐 ∈ 𝑋 → (∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎) → 𝑏 ∈ 𝐴))) |
| 41 | 40 | exlimdv 1933 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) → (∃𝑐 𝑐 ∈ 𝑋 → (∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎) → 𝑏 ∈ 𝐴))) |
| 42 | 19, 41 | biimtrid 242 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴) → (𝑋 ≠ ∅ → (∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎) → 𝑏 ∈ 𝐴))) |
| 43 | 42 | impr 454 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎) → 𝑏 ∈ 𝐴)) |
| 44 | | eluni 4910 |
. . . . . . . . 9
⊢ (𝑏 ∈ ∪ 𝑋
↔ ∃𝑐(𝑏 ∈ 𝑐 ∧ 𝑐 ∈ 𝑋)) |
| 45 | 29 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝑐 ∧ 𝑐 ∈ 𝑋)) → (𝐴 ∖ 𝑐) ∈ 𝒫 𝐴) |
| 46 | 26 | adantlrr 721 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ 𝑐 ∈ 𝑋) → (𝐴 ∖ (𝐴 ∖ 𝑐)) ∈ 𝑋) |
| 47 | 46 | adantrl 716 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝑐 ∧ 𝑐 ∈ 𝑋)) → (𝐴 ∖ (𝐴 ∖ 𝑐)) ∈ 𝑋) |
| 48 | | elndif 4133 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ 𝑐 → ¬ 𝑏 ∈ (𝐴 ∖ 𝑐)) |
| 49 | 48 | ad2antrl 728 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝑐 ∧ 𝑐 ∈ 𝑋)) → ¬ 𝑏 ∈ (𝐴 ∖ 𝑐)) |
| 50 | 47, 49 | jcnd 163 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝑐 ∧ 𝑐 ∈ 𝑋)) → ¬ ((𝐴 ∖ (𝐴 ∖ 𝑐)) ∈ 𝑋 → 𝑏 ∈ (𝐴 ∖ 𝑐))) |
| 51 | 34 | notbid 318 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = (𝐴 ∖ 𝑐) → (¬ ((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎) ↔ ¬ ((𝐴 ∖ (𝐴 ∖ 𝑐)) ∈ 𝑋 → 𝑏 ∈ (𝐴 ∖ 𝑐)))) |
| 52 | 51 | rspcev 3622 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∖ 𝑐) ∈ 𝒫 𝐴 ∧ ¬ ((𝐴 ∖ (𝐴 ∖ 𝑐)) ∈ 𝑋 → 𝑏 ∈ (𝐴 ∖ 𝑐))) → ∃𝑎 ∈ 𝒫 𝐴 ¬ ((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎)) |
| 53 | 45, 50, 52 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝑐 ∧ 𝑐 ∈ 𝑋)) → ∃𝑎 ∈ 𝒫 𝐴 ¬ ((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎)) |
| 54 | | rexnal 3100 |
. . . . . . . . . . . 12
⊢
(∃𝑎 ∈
𝒫 𝐴 ¬ ((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎) ↔ ¬ ∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎)) |
| 55 | 53, 54 | sylib 218 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) ∧ (𝑏 ∈ 𝑐 ∧ 𝑐 ∈ 𝑋)) → ¬ ∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎)) |
| 56 | 55 | ex 412 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → ((𝑏 ∈ 𝑐 ∧ 𝑐 ∈ 𝑋) → ¬ ∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎))) |
| 57 | 56 | exlimdv 1933 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (∃𝑐(𝑏 ∈ 𝑐 ∧ 𝑐 ∈ 𝑋) → ¬ ∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎))) |
| 58 | 44, 57 | biimtrid 242 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (𝑏 ∈ ∪ 𝑋 → ¬ ∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎))) |
| 59 | 58 | con2d 134 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎) → ¬ 𝑏 ∈ ∪ 𝑋)) |
| 60 | 43, 59 | jcad 512 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎) → (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋))) |
| 61 | 18, 60 | impbid 212 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → ((𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋) ↔ ∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎))) |
| 62 | | eldif 3961 |
. . . . 5
⊢ (𝑏 ∈ (𝐴 ∖ ∪ 𝑋) ↔ (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋)) |
| 63 | | vex 3484 |
. . . . . 6
⊢ 𝑏 ∈ V |
| 64 | 63 | elintrab 4960 |
. . . . 5
⊢ (𝑏 ∈ ∩ {𝑎
∈ 𝒫 𝐴 ∣
(𝐴 ∖ 𝑎) ∈ 𝑋} ↔ ∀𝑎 ∈ 𝒫 𝐴((𝐴 ∖ 𝑎) ∈ 𝑋 → 𝑏 ∈ 𝑎)) |
| 65 | 61, 62, 64 | 3bitr4g 314 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (𝑏 ∈ (𝐴 ∖ ∪ 𝑋) ↔ 𝑏 ∈ ∩ {𝑎 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑎) ∈ 𝑋})) |
| 66 | 65 | eqrdv 2735 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (𝐴 ∖ ∪ 𝑋) = ∩
{𝑎 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑎) ∈ 𝑋}) |
| 67 | 5, 66 | eqtrd 2777 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (𝐹‘∪ 𝑋) = ∩
{𝑎 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑎) ∈ 𝑋}) |
| 68 | 2 | compss 10416 |
. . 3
⊢ (𝐹 “ 𝑋) = {𝑎 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑎) ∈ 𝑋} |
| 69 | 68 | inteqi 4950 |
. 2
⊢ ∩ (𝐹
“ 𝑋) = ∩ {𝑎
∈ 𝒫 𝐴 ∣
(𝐴 ∖ 𝑎) ∈ 𝑋} |
| 70 | 67, 69 | eqtr4di 2795 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅)) → (𝐹‘∪ 𝑋) = ∩
(𝐹 “ 𝑋)) |