# 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 ${⊢}\left({A}\in {V}\wedge {B}\subseteq 𝒫{A}\wedge {B}\ne \varnothing \right)\to \left\{{x}\in 𝒫{A}|{A}\setminus {x}\in {B}\right\}\ne \varnothing$

### Proof

Step Hyp Ref Expression
1 n0 ${⊢}{B}\ne \varnothing ↔\exists {y}\phantom{\rule{.4em}{0ex}}{y}\in {B}$
2 difss ${⊢}{A}\setminus {y}\subseteq {A}$
3 elpw2g ${⊢}{A}\in {V}\to \left({A}\setminus {y}\in 𝒫{A}↔{A}\setminus {y}\subseteq {A}\right)$
4 3 ad2antrr ${⊢}\left(\left({A}\in {V}\wedge {B}\subseteq 𝒫{A}\right)\wedge {y}\in {B}\right)\to \left({A}\setminus {y}\in 𝒫{A}↔{A}\setminus {y}\subseteq {A}\right)$
5 2 4 mpbiri ${⊢}\left(\left({A}\in {V}\wedge {B}\subseteq 𝒫{A}\right)\wedge {y}\in {B}\right)\to {A}\setminus {y}\in 𝒫{A}$
6 simpr ${⊢}\left({A}\in {V}\wedge {B}\subseteq 𝒫{A}\right)\to {B}\subseteq 𝒫{A}$
7 6 sselda ${⊢}\left(\left({A}\in {V}\wedge {B}\subseteq 𝒫{A}\right)\wedge {y}\in {B}\right)\to {y}\in 𝒫{A}$
8 7 elpwid ${⊢}\left(\left({A}\in {V}\wedge {B}\subseteq 𝒫{A}\right)\wedge {y}\in {B}\right)\to {y}\subseteq {A}$
9 dfss4 ${⊢}{y}\subseteq {A}↔{A}\setminus \left({A}\setminus {y}\right)={y}$
10 8 9 sylib ${⊢}\left(\left({A}\in {V}\wedge {B}\subseteq 𝒫{A}\right)\wedge {y}\in {B}\right)\to {A}\setminus \left({A}\setminus {y}\right)={y}$
11 simpr ${⊢}\left(\left({A}\in {V}\wedge {B}\subseteq 𝒫{A}\right)\wedge {y}\in {B}\right)\to {y}\in {B}$
12 10 11 eqeltrd ${⊢}\left(\left({A}\in {V}\wedge {B}\subseteq 𝒫{A}\right)\wedge {y}\in {B}\right)\to {A}\setminus \left({A}\setminus {y}\right)\in {B}$
13 difeq2 ${⊢}{x}={A}\setminus {y}\to {A}\setminus {x}={A}\setminus \left({A}\setminus {y}\right)$
14 13 eleq1d ${⊢}{x}={A}\setminus {y}\to \left({A}\setminus {x}\in {B}↔{A}\setminus \left({A}\setminus {y}\right)\in {B}\right)$
15 14 rspcev ${⊢}\left({A}\setminus {y}\in 𝒫{A}\wedge {A}\setminus \left({A}\setminus {y}\right)\in {B}\right)\to \exists {x}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}{A}\setminus {x}\in {B}$
16 5 12 15 syl2anc ${⊢}\left(\left({A}\in {V}\wedge {B}\subseteq 𝒫{A}\right)\wedge {y}\in {B}\right)\to \exists {x}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}{A}\setminus {x}\in {B}$
17 16 ex ${⊢}\left({A}\in {V}\wedge {B}\subseteq 𝒫{A}\right)\to \left({y}\in {B}\to \exists {x}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}{A}\setminus {x}\in {B}\right)$
18 17 exlimdv ${⊢}\left({A}\in {V}\wedge {B}\subseteq 𝒫{A}\right)\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}{y}\in {B}\to \exists {x}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}{A}\setminus {x}\in {B}\right)$
19 1 18 syl5bi ${⊢}\left({A}\in {V}\wedge {B}\subseteq 𝒫{A}\right)\to \left({B}\ne \varnothing \to \exists {x}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}{A}\setminus {x}\in {B}\right)$
20 19 3impia ${⊢}\left({A}\in {V}\wedge {B}\subseteq 𝒫{A}\wedge {B}\ne \varnothing \right)\to \exists {x}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}{A}\setminus {x}\in {B}$
21 rabn0 ${⊢}\left\{{x}\in 𝒫{A}|{A}\setminus {x}\in {B}\right\}\ne \varnothing ↔\exists {x}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}{A}\setminus {x}\in {B}$
22 20 21 sylibr ${⊢}\left({A}\in {V}\wedge {B}\subseteq 𝒫{A}\wedge {B}\ne \varnothing \right)\to \left\{{x}\in 𝒫{A}|{A}\setminus {x}\in {B}\right\}\ne \varnothing$