Metamath Proof Explorer

Theorem fin23lem7

Description: Lemma for isfin2-2 . The componentwise complement of a nonempty collection of sets is nonempty. (Contributed by Stefan O'Rear, 31-Oct-2014) (Revised by Mario Carneiro, 16-May-2015)

Ref Expression
Assertion fin23lem7 ⊢ A ∈ V ∧ B ⊆ 𝒫 A ∧ B ≠ ∅ → x ∈ 𝒫 A | A ∖ x ∈ B ≠ ∅

Proof

Step Hyp Ref Expression
1 n0 ⊢ B ≠ ∅ ↔ ∃ y y ∈ B
2 difss ⊢ A ∖ y ⊆ A
3 elpw2g ⊢ A ∈ V → A ∖ y ∈ 𝒫 A ↔ A ∖ y ⊆ A
4 3 ad2antrr ⊢ A ∈ V ∧ B ⊆ 𝒫 A ∧ y ∈ B → A ∖ y ∈ 𝒫 A ↔ A ∖ y ⊆ A
5 2 4 mpbiri ⊢ A ∈ V ∧ B ⊆ 𝒫 A ∧ y ∈ B → A ∖ y ∈ 𝒫 A
6 simpr ⊢ A ∈ V ∧ B ⊆ 𝒫 A → B ⊆ 𝒫 A
7 6 sselda ⊢ A ∈ V ∧ B ⊆ 𝒫 A ∧ y ∈ B → y ∈ 𝒫 A
8 7 elpwid ⊢ A ∈ V ∧ B ⊆ 𝒫 A ∧ y ∈ B → y ⊆ A
9 dfss4 ⊢ y ⊆ A ↔ A ∖ A ∖ y = y
10 8 9 sylib ⊢ A ∈ V ∧ B ⊆ 𝒫 A ∧ y ∈ B → A ∖ A ∖ y = y
11 simpr ⊢ A ∈ V ∧ B ⊆ 𝒫 A ∧ y ∈ B → y ∈ B
12 10 11 eqeltrd ⊢ A ∈ V ∧ B ⊆ 𝒫 A ∧ y ∈ B → A ∖ A ∖ y ∈ B
13 difeq2 ⊢ x = A ∖ y → A ∖ x = A ∖ A ∖ y
14 13 eleq1d ⊢ x = A ∖ y → A ∖ x ∈ B ↔ A ∖ A ∖ y ∈ B
15 14 rspcev ⊢ A ∖ y ∈ 𝒫 A ∧ A ∖ A ∖ y ∈ B → ∃ x ∈ 𝒫 A A ∖ x ∈ B
16 5 12 15 syl2anc ⊢ A ∈ V ∧ B ⊆ 𝒫 A ∧ y ∈ B → ∃ x ∈ 𝒫 A A ∖ x ∈ B
17 16 ex ⊢ A ∈ V ∧ B ⊆ 𝒫 A → y ∈ B → ∃ x ∈ 𝒫 A A ∖ x ∈ B
18 17 exlimdv ⊢ A ∈ V ∧ B ⊆ 𝒫 A → ∃ y y ∈ B → ∃ x ∈ 𝒫 A A ∖ x ∈ B
19 1 18 syl5bi ⊢ A ∈ V ∧ B ⊆ 𝒫 A → B ≠ ∅ → ∃ x ∈ 𝒫 A A ∖ x ∈ B
20 19 3impia ⊢ A ∈ V ∧ B ⊆ 𝒫 A ∧ B ≠ ∅ → ∃ x ∈ 𝒫 A A ∖ x ∈ B
21 rabn0 ⊢ x ∈ 𝒫 A | A ∖ x ∈ B ≠ ∅ ↔ ∃ x ∈ 𝒫 A A ∖ x ∈ B
22 20 21 sylibr ⊢ A ∈ V ∧ B ⊆ 𝒫 A ∧ B ≠ ∅ → x ∈ 𝒫 A | A ∖ x ∈ B ≠ ∅