# Metamath Proof Explorer

## Theorem isf34lem4

Description: Lemma for isfin3-4 . (Contributed by Stefan O'Rear, 7-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Hypothesis compss.a ${⊢}{F}=\left({x}\in 𝒫{A}⟼{A}\setminus {x}\right)$
Assertion isf34lem4 ${⊢}\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\to {F}\left(\bigcup {X}\right)=\bigcap {F}\left[{X}\right]$

### Proof

Step Hyp Ref Expression
1 compss.a ${⊢}{F}=\left({x}\in 𝒫{A}⟼{A}\setminus {x}\right)$
2 sspwuni ${⊢}{X}\subseteq 𝒫{A}↔\bigcup {X}\subseteq {A}$
3 1 isf34lem1 ${⊢}\left({A}\in {V}\wedge \bigcup {X}\subseteq {A}\right)\to {F}\left(\bigcup {X}\right)={A}\setminus \bigcup {X}$
4 2 3 sylan2b ${⊢}\left({A}\in {V}\wedge {X}\subseteq 𝒫{A}\right)\to {F}\left(\bigcup {X}\right)={A}\setminus \bigcup {X}$
5 4 adantrr ${⊢}\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\to {F}\left(\bigcup {X}\right)={A}\setminus \bigcup {X}$
6 simplrr ${⊢}\left(\left(\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\wedge \left({b}\in {A}\wedge ¬{b}\in \bigcup {X}\right)\right)\wedge \left({a}\in 𝒫{A}\wedge {A}\setminus {a}\in {X}\right)\right)\to ¬{b}\in \bigcup {X}$
7 simprl ${⊢}\left(\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\wedge \left({b}\in {A}\wedge ¬{b}\in \bigcup {X}\right)\right)\to {b}\in {A}$
8 7 ad2antrr ${⊢}\left(\left(\left(\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\wedge \left({b}\in {A}\wedge ¬{b}\in \bigcup {X}\right)\right)\wedge \left({a}\in 𝒫{A}\wedge {A}\setminus {a}\in {X}\right)\right)\wedge ¬{b}\in {a}\right)\to {b}\in {A}$
9 simpr ${⊢}\left(\left(\left(\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\wedge \left({b}\in {A}\wedge ¬{b}\in \bigcup {X}\right)\right)\wedge \left({a}\in 𝒫{A}\wedge {A}\setminus {a}\in {X}\right)\right)\wedge ¬{b}\in {a}\right)\to ¬{b}\in {a}$
10 8 9 eldifd ${⊢}\left(\left(\left(\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\wedge \left({b}\in {A}\wedge ¬{b}\in \bigcup {X}\right)\right)\wedge \left({a}\in 𝒫{A}\wedge {A}\setminus {a}\in {X}\right)\right)\wedge ¬{b}\in {a}\right)\to {b}\in \left({A}\setminus {a}\right)$
11 simplrr ${⊢}\left(\left(\left(\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\wedge \left({b}\in {A}\wedge ¬{b}\in \bigcup {X}\right)\right)\wedge \left({a}\in 𝒫{A}\wedge {A}\setminus {a}\in {X}\right)\right)\wedge ¬{b}\in {a}\right)\to {A}\setminus {a}\in {X}$
12 elunii ${⊢}\left({b}\in \left({A}\setminus {a}\right)\wedge {A}\setminus {a}\in {X}\right)\to {b}\in \bigcup {X}$
13 10 11 12 syl2anc ${⊢}\left(\left(\left(\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\wedge \left({b}\in {A}\wedge ¬{b}\in \bigcup {X}\right)\right)\wedge \left({a}\in 𝒫{A}\wedge {A}\setminus {a}\in {X}\right)\right)\wedge ¬{b}\in {a}\right)\to {b}\in \bigcup {X}$
14 13 ex ${⊢}\left(\left(\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\wedge \left({b}\in {A}\wedge ¬{b}\in \bigcup {X}\right)\right)\wedge \left({a}\in 𝒫{A}\wedge {A}\setminus {a}\in {X}\right)\right)\to \left(¬{b}\in {a}\to {b}\in \bigcup {X}\right)$
15 6 14 mt3d ${⊢}\left(\left(\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\wedge \left({b}\in {A}\wedge ¬{b}\in \bigcup {X}\right)\right)\wedge \left({a}\in 𝒫{A}\wedge {A}\setminus {a}\in {X}\right)\right)\to {b}\in {a}$
16 15 expr ${⊢}\left(\left(\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\wedge \left({b}\in {A}\wedge ¬{b}\in \bigcup {X}\right)\right)\wedge {a}\in 𝒫{A}\right)\to \left({A}\setminus {a}\in {X}\to {b}\in {a}\right)$
17 16 ralrimiva ${⊢}\left(\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\wedge \left({b}\in {A}\wedge ¬{b}\in \bigcup {X}\right)\right)\to \forall {a}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\left({A}\setminus {a}\in {X}\to {b}\in {a}\right)$
18 17 ex ${⊢}\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\to \left(\left({b}\in {A}\wedge ¬{b}\in \bigcup {X}\right)\to \forall {a}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\left({A}\setminus {a}\in {X}\to {b}\in {a}\right)\right)$
19 n0 ${⊢}{X}\ne \varnothing ↔\exists {c}\phantom{\rule{.4em}{0ex}}{c}\in {X}$
20 simpr ${⊢}\left({A}\in {V}\wedge {X}\subseteq 𝒫{A}\right)\to {X}\subseteq 𝒫{A}$
21 20 sselda ${⊢}\left(\left({A}\in {V}\wedge {X}\subseteq 𝒫{A}\right)\wedge {c}\in {X}\right)\to {c}\in 𝒫{A}$
22 21 elpwid ${⊢}\left(\left({A}\in {V}\wedge {X}\subseteq 𝒫{A}\right)\wedge {c}\in {X}\right)\to {c}\subseteq {A}$
23 dfss4 ${⊢}{c}\subseteq {A}↔{A}\setminus \left({A}\setminus {c}\right)={c}$
24 22 23 sylib ${⊢}\left(\left({A}\in {V}\wedge {X}\subseteq 𝒫{A}\right)\wedge {c}\in {X}\right)\to {A}\setminus \left({A}\setminus {c}\right)={c}$
25 simpr ${⊢}\left(\left({A}\in {V}\wedge {X}\subseteq 𝒫{A}\right)\wedge {c}\in {X}\right)\to {c}\in {X}$
26 24 25 eqeltrd ${⊢}\left(\left({A}\in {V}\wedge {X}\subseteq 𝒫{A}\right)\wedge {c}\in {X}\right)\to {A}\setminus \left({A}\setminus {c}\right)\in {X}$
27 difss ${⊢}{A}\setminus {c}\subseteq {A}$
28 elpw2g ${⊢}{A}\in {V}\to \left({A}\setminus {c}\in 𝒫{A}↔{A}\setminus {c}\subseteq {A}\right)$
29 27 28 mpbiri ${⊢}{A}\in {V}\to {A}\setminus {c}\in 𝒫{A}$
30 29 ad2antrr ${⊢}\left(\left({A}\in {V}\wedge {X}\subseteq 𝒫{A}\right)\wedge {c}\in {X}\right)\to {A}\setminus {c}\in 𝒫{A}$
31 difeq2 ${⊢}{a}={A}\setminus {c}\to {A}\setminus {a}={A}\setminus \left({A}\setminus {c}\right)$
32 31 eleq1d ${⊢}{a}={A}\setminus {c}\to \left({A}\setminus {a}\in {X}↔{A}\setminus \left({A}\setminus {c}\right)\in {X}\right)$
33 eleq2 ${⊢}{a}={A}\setminus {c}\to \left({b}\in {a}↔{b}\in \left({A}\setminus {c}\right)\right)$
34 32 33 imbi12d ${⊢}{a}={A}\setminus {c}\to \left(\left({A}\setminus {a}\in {X}\to {b}\in {a}\right)↔\left({A}\setminus \left({A}\setminus {c}\right)\in {X}\to {b}\in \left({A}\setminus {c}\right)\right)\right)$
35 34 rspcv ${⊢}{A}\setminus {c}\in 𝒫{A}\to \left(\forall {a}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\left({A}\setminus {a}\in {X}\to {b}\in {a}\right)\to \left({A}\setminus \left({A}\setminus {c}\right)\in {X}\to {b}\in \left({A}\setminus {c}\right)\right)\right)$
36 30 35 syl ${⊢}\left(\left({A}\in {V}\wedge {X}\subseteq 𝒫{A}\right)\wedge {c}\in {X}\right)\to \left(\forall {a}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\left({A}\setminus {a}\in {X}\to {b}\in {a}\right)\to \left({A}\setminus \left({A}\setminus {c}\right)\in {X}\to {b}\in \left({A}\setminus {c}\right)\right)\right)$
37 26 36 mpid ${⊢}\left(\left({A}\in {V}\wedge {X}\subseteq 𝒫{A}\right)\wedge {c}\in {X}\right)\to \left(\forall {a}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\left({A}\setminus {a}\in {X}\to {b}\in {a}\right)\to {b}\in \left({A}\setminus {c}\right)\right)$
38 eldifi ${⊢}{b}\in \left({A}\setminus {c}\right)\to {b}\in {A}$
39 37 38 syl6 ${⊢}\left(\left({A}\in {V}\wedge {X}\subseteq 𝒫{A}\right)\wedge {c}\in {X}\right)\to \left(\forall {a}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\left({A}\setminus {a}\in {X}\to {b}\in {a}\right)\to {b}\in {A}\right)$
40 39 ex ${⊢}\left({A}\in {V}\wedge {X}\subseteq 𝒫{A}\right)\to \left({c}\in {X}\to \left(\forall {a}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\left({A}\setminus {a}\in {X}\to {b}\in {a}\right)\to {b}\in {A}\right)\right)$
41 40 exlimdv ${⊢}\left({A}\in {V}\wedge {X}\subseteq 𝒫{A}\right)\to \left(\exists {c}\phantom{\rule{.4em}{0ex}}{c}\in {X}\to \left(\forall {a}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\left({A}\setminus {a}\in {X}\to {b}\in {a}\right)\to {b}\in {A}\right)\right)$
42 19 41 syl5bi ${⊢}\left({A}\in {V}\wedge {X}\subseteq 𝒫{A}\right)\to \left({X}\ne \varnothing \to \left(\forall {a}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\left({A}\setminus {a}\in {X}\to {b}\in {a}\right)\to {b}\in {A}\right)\right)$
43 42 impr ${⊢}\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\to \left(\forall {a}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\left({A}\setminus {a}\in {X}\to {b}\in {a}\right)\to {b}\in {A}\right)$
44 eluni ${⊢}{b}\in \bigcup {X}↔\exists {c}\phantom{\rule{.4em}{0ex}}\left({b}\in {c}\wedge {c}\in {X}\right)$
45 29 ad2antrr ${⊢}\left(\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\wedge \left({b}\in {c}\wedge {c}\in {X}\right)\right)\to {A}\setminus {c}\in 𝒫{A}$
46 26 adantlrr ${⊢}\left(\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\wedge {c}\in {X}\right)\to {A}\setminus \left({A}\setminus {c}\right)\in {X}$
47 46 adantrl ${⊢}\left(\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\wedge \left({b}\in {c}\wedge {c}\in {X}\right)\right)\to {A}\setminus \left({A}\setminus {c}\right)\in {X}$
48 elndif ${⊢}{b}\in {c}\to ¬{b}\in \left({A}\setminus {c}\right)$
49 48 ad2antrl ${⊢}\left(\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\wedge \left({b}\in {c}\wedge {c}\in {X}\right)\right)\to ¬{b}\in \left({A}\setminus {c}\right)$
50 47 49 jcn ${⊢}\left(\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\wedge \left({b}\in {c}\wedge {c}\in {X}\right)\right)\to ¬\left({A}\setminus \left({A}\setminus {c}\right)\in {X}\to {b}\in \left({A}\setminus {c}\right)\right)$
51 34 notbid ${⊢}{a}={A}\setminus {c}\to \left(¬\left({A}\setminus {a}\in {X}\to {b}\in {a}\right)↔¬\left({A}\setminus \left({A}\setminus {c}\right)\in {X}\to {b}\in \left({A}\setminus {c}\right)\right)\right)$
52 51 rspcev ${⊢}\left({A}\setminus {c}\in 𝒫{A}\wedge ¬\left({A}\setminus \left({A}\setminus {c}\right)\in {X}\to {b}\in \left({A}\setminus {c}\right)\right)\right)\to \exists {a}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}¬\left({A}\setminus {a}\in {X}\to {b}\in {a}\right)$
53 45 50 52 syl2anc ${⊢}\left(\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\wedge \left({b}\in {c}\wedge {c}\in {X}\right)\right)\to \exists {a}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}¬\left({A}\setminus {a}\in {X}\to {b}\in {a}\right)$
54 rexnal ${⊢}\exists {a}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}¬\left({A}\setminus {a}\in {X}\to {b}\in {a}\right)↔¬\forall {a}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\left({A}\setminus {a}\in {X}\to {b}\in {a}\right)$
55 53 54 sylib ${⊢}\left(\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\wedge \left({b}\in {c}\wedge {c}\in {X}\right)\right)\to ¬\forall {a}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\left({A}\setminus {a}\in {X}\to {b}\in {a}\right)$
56 55 ex ${⊢}\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\to \left(\left({b}\in {c}\wedge {c}\in {X}\right)\to ¬\forall {a}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\left({A}\setminus {a}\in {X}\to {b}\in {a}\right)\right)$
57 56 exlimdv ${⊢}\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\to \left(\exists {c}\phantom{\rule{.4em}{0ex}}\left({b}\in {c}\wedge {c}\in {X}\right)\to ¬\forall {a}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\left({A}\setminus {a}\in {X}\to {b}\in {a}\right)\right)$
58 44 57 syl5bi ${⊢}\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\to \left({b}\in \bigcup {X}\to ¬\forall {a}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\left({A}\setminus {a}\in {X}\to {b}\in {a}\right)\right)$
59 58 con2d ${⊢}\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\to \left(\forall {a}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\left({A}\setminus {a}\in {X}\to {b}\in {a}\right)\to ¬{b}\in \bigcup {X}\right)$
60 43 59 jcad ${⊢}\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\to \left(\forall {a}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\left({A}\setminus {a}\in {X}\to {b}\in {a}\right)\to \left({b}\in {A}\wedge ¬{b}\in \bigcup {X}\right)\right)$
61 18 60 impbid ${⊢}\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\to \left(\left({b}\in {A}\wedge ¬{b}\in \bigcup {X}\right)↔\forall {a}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\left({A}\setminus {a}\in {X}\to {b}\in {a}\right)\right)$
62 eldif ${⊢}{b}\in \left({A}\setminus \bigcup {X}\right)↔\left({b}\in {A}\wedge ¬{b}\in \bigcup {X}\right)$
63 vex ${⊢}{b}\in \mathrm{V}$
64 63 elintrab ${⊢}{b}\in \bigcap \left\{{a}\in 𝒫{A}|{A}\setminus {a}\in {X}\right\}↔\forall {a}\in 𝒫{A}\phantom{\rule{.4em}{0ex}}\left({A}\setminus {a}\in {X}\to {b}\in {a}\right)$
65 61 62 64 3bitr4g ${⊢}\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\to \left({b}\in \left({A}\setminus \bigcup {X}\right)↔{b}\in \bigcap \left\{{a}\in 𝒫{A}|{A}\setminus {a}\in {X}\right\}\right)$
66 65 eqrdv ${⊢}\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\to {A}\setminus \bigcup {X}=\bigcap \left\{{a}\in 𝒫{A}|{A}\setminus {a}\in {X}\right\}$
67 5 66 eqtrd ${⊢}\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\to {F}\left(\bigcup {X}\right)=\bigcap \left\{{a}\in 𝒫{A}|{A}\setminus {a}\in {X}\right\}$
68 1 compss ${⊢}{F}\left[{X}\right]=\left\{{a}\in 𝒫{A}|{A}\setminus {a}\in {X}\right\}$
69 68 inteqi ${⊢}\bigcap {F}\left[{X}\right]=\bigcap \left\{{a}\in 𝒫{A}|{A}\setminus {a}\in {X}\right\}$
70 67 69 syl6eqr ${⊢}\left({A}\in {V}\wedge \left({X}\subseteq 𝒫{A}\wedge {X}\ne \varnothing \right)\right)\to {F}\left(\bigcup {X}\right)=\bigcap {F}\left[{X}\right]$