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=x∈𝒫A⟼A∖x
Assertion isf34lem4 ⊢A∈V∧X⊆𝒫A∧X≠∅→F⁡⋃X=⋂FX

Proof

Step Hyp Ref Expression
1 compss.a ⊢F=x∈𝒫A⟼A∖x
2 sspwuni ⊢X⊆𝒫A↔⋃X⊆A
3 1 isf34lem1 ⊢A∈V∧⋃X⊆A→F⁡⋃X=A∖⋃X
4 2 3 sylan2b ⊢A∈V∧X⊆𝒫A→F⁡⋃X=A∖⋃X
5 4 adantrr ⊢A∈V∧X⊆𝒫A∧X≠∅→F⁡⋃X=A∖⋃X
6 simplrr ⊢A∈V∧X⊆𝒫A∧X≠∅∧b∈A∧¬b∈⋃X∧a∈𝒫A∧A∖a∈X→¬b∈⋃X
7 simprl ⊢A∈V∧X⊆𝒫A∧X≠∅∧b∈A∧¬b∈⋃X→b∈A
8 7 ad2antrr ⊢A∈V∧X⊆𝒫A∧X≠∅∧b∈A∧¬b∈⋃X∧a∈𝒫A∧A∖a∈X∧¬b∈a→b∈A
9 simpr ⊢A∈V∧X⊆𝒫A∧X≠∅∧b∈A∧¬b∈⋃X∧a∈𝒫A∧A∖a∈X∧¬b∈a→¬b∈a
10 8 9 eldifd ⊢A∈V∧X⊆𝒫A∧X≠∅∧b∈A∧¬b∈⋃X∧a∈𝒫A∧A∖a∈X∧¬b∈a→b∈A∖a
11 simplrr ⊢A∈V∧X⊆𝒫A∧X≠∅∧b∈A∧¬b∈⋃X∧a∈𝒫A∧A∖a∈X∧¬b∈a→A∖a∈X
12 elunii ⊢b∈A∖a∧A∖a∈X→b∈⋃X
13 10 11 12 syl2anc ⊢A∈V∧X⊆𝒫A∧X≠∅∧b∈A∧¬b∈⋃X∧a∈𝒫A∧A∖a∈X∧¬b∈a→b∈⋃X
14 13 ex ⊢A∈V∧X⊆𝒫A∧X≠∅∧b∈A∧¬b∈⋃X∧a∈𝒫A∧A∖a∈X→¬b∈a→b∈⋃X
15 6 14 mt3d ⊢A∈V∧X⊆𝒫A∧X≠∅∧b∈A∧¬b∈⋃X∧a∈𝒫A∧A∖a∈X→b∈a
16 15 expr ⊢A∈V∧X⊆𝒫A∧X≠∅∧b∈A∧¬b∈⋃X∧a∈𝒫A→A∖a∈X→b∈a
17 16 ralrimiva ⊢A∈V∧X⊆𝒫A∧X≠∅∧b∈A∧¬b∈⋃X→∀a∈𝒫AA∖a∈X→b∈a
18 17 ex ⊢A∈V∧X⊆𝒫A∧X≠∅→b∈A∧¬b∈⋃X→∀a∈𝒫AA∖a∈X→b∈a
19 n0 ⊢X≠∅↔∃cc∈X
20 simpr ⊢A∈V∧X⊆𝒫A→X⊆𝒫A
21 20 sselda ⊢A∈V∧X⊆𝒫A∧c∈X→c∈𝒫A
22 21 elpwid ⊢A∈V∧X⊆𝒫A∧c∈X→c⊆A
23 dfss4 ⊢c⊆A↔A∖A∖c=c
24 22 23 sylib ⊢A∈V∧X⊆𝒫A∧c∈X→A∖A∖c=c
25 simpr ⊢A∈V∧X⊆𝒫A∧c∈X→c∈X
26 24 25 eqeltrd ⊢A∈V∧X⊆𝒫A∧c∈X→A∖A∖c∈X
27 difss ⊢A∖c⊆A
28 elpw2g ⊢A∈V→A∖c∈𝒫A↔A∖c⊆A
29 27 28 mpbiri ⊢A∈V→A∖c∈𝒫A
30 29 ad2antrr ⊢A∈V∧X⊆𝒫A∧c∈X→A∖c∈𝒫A
31 difeq2 ⊢a=A∖c→A∖a=A∖A∖c
32 31 eleq1d ⊢a=A∖c→A∖a∈X↔A∖A∖c∈X
33 eleq2 ⊢a=A∖c→b∈a↔b∈A∖c
34 32 33 imbi12d ⊢a=A∖c→A∖a∈X→b∈a↔A∖A∖c∈X→b∈A∖c
35 34 rspcv ⊢A∖c∈𝒫A→∀a∈𝒫AA∖a∈X→b∈a→A∖A∖c∈X→b∈A∖c
36 30 35 syl ⊢A∈V∧X⊆𝒫A∧c∈X→∀a∈𝒫AA∖a∈X→b∈a→A∖A∖c∈X→b∈A∖c
37 26 36 mpid ⊢A∈V∧X⊆𝒫A∧c∈X→∀a∈𝒫AA∖a∈X→b∈a→b∈A∖c
38 eldifi ⊢b∈A∖c→b∈A
39 37 38 syl6 ⊢A∈V∧X⊆𝒫A∧c∈X→∀a∈𝒫AA∖a∈X→b∈a→b∈A
40 39 ex ⊢A∈V∧X⊆𝒫A→c∈X→∀a∈𝒫AA∖a∈X→b∈a→b∈A
41 40 exlimdv ⊢A∈V∧X⊆𝒫A→∃cc∈X→∀a∈𝒫AA∖a∈X→b∈a→b∈A
42 19 41 biimtrid ⊢A∈V∧X⊆𝒫A→X≠∅→∀a∈𝒫AA∖a∈X→b∈a→b∈A
43 42 impr ⊢A∈V∧X⊆𝒫A∧X≠∅→∀a∈𝒫AA∖a∈X→b∈a→b∈A
44 eluni ⊢b∈⋃X↔∃cb∈c∧c∈X
45 29 ad2antrr ⊢A∈V∧X⊆𝒫A∧X≠∅∧b∈c∧c∈X→A∖c∈𝒫A
46 26 adantlrr ⊢A∈V∧X⊆𝒫A∧X≠∅∧c∈X→A∖A∖c∈X
47 46 adantrl ⊢A∈V∧X⊆𝒫A∧X≠∅∧b∈c∧c∈X→A∖A∖c∈X
48 elndif ⊢b∈c→¬b∈A∖c
49 48 ad2antrl ⊢A∈V∧X⊆𝒫A∧X≠∅∧b∈c∧c∈X→¬b∈A∖c
50 47 49 jcnd ⊢A∈V∧X⊆𝒫A∧X≠∅∧b∈c∧c∈X→¬A∖A∖c∈X→b∈A∖c
51 34 notbid ⊢a=A∖c→¬A∖a∈X→b∈a↔¬A∖A∖c∈X→b∈A∖c
52 51 rspcev ⊢A∖c∈𝒫A∧¬A∖A∖c∈X→b∈A∖c→∃a∈𝒫A¬A∖a∈X→b∈a
53 45 50 52 syl2anc ⊢A∈V∧X⊆𝒫A∧X≠∅∧b∈c∧c∈X→∃a∈𝒫A¬A∖a∈X→b∈a
54 rexnal ⊢∃a∈𝒫A¬A∖a∈X→b∈a↔¬∀a∈𝒫AA∖a∈X→b∈a
55 53 54 sylib ⊢A∈V∧X⊆𝒫A∧X≠∅∧b∈c∧c∈X→¬∀a∈𝒫AA∖a∈X→b∈a
56 55 ex ⊢A∈V∧X⊆𝒫A∧X≠∅→b∈c∧c∈X→¬∀a∈𝒫AA∖a∈X→b∈a
57 56 exlimdv ⊢A∈V∧X⊆𝒫A∧X≠∅→∃cb∈c∧c∈X→¬∀a∈𝒫AA∖a∈X→b∈a
58 44 57 biimtrid ⊢A∈V∧X⊆𝒫A∧X≠∅→b∈⋃X→¬∀a∈𝒫AA∖a∈X→b∈a
59 58 con2d ⊢A∈V∧X⊆𝒫A∧X≠∅→∀a∈𝒫AA∖a∈X→b∈a→¬b∈⋃X
60 43 59 jcad ⊢A∈V∧X⊆𝒫A∧X≠∅→∀a∈𝒫AA∖a∈X→b∈a→b∈A∧¬b∈⋃X
61 18 60 impbid ⊢A∈V∧X⊆𝒫A∧X≠∅→b∈A∧¬b∈⋃X↔∀a∈𝒫AA∖a∈X→b∈a
62 eldif ⊢b∈A∖⋃X↔b∈A∧¬b∈⋃X
63 vex ⊢b∈V
64 63 elintrab ⊢b∈⋂a∈𝒫A|A∖a∈X↔∀a∈𝒫AA∖a∈X→b∈a
65 61 62 64 3bitr4g ⊢A∈V∧X⊆𝒫A∧X≠∅→b∈A∖⋃X↔b∈⋂a∈𝒫A|A∖a∈X
66 65 eqrdv ⊢A∈V∧X⊆𝒫A∧X≠∅→A∖⋃X=⋂a∈𝒫A|A∖a∈X
67 5 66 eqtrd ⊢A∈V∧X⊆𝒫A∧X≠∅→F⁡⋃X=⋂a∈𝒫A|A∖a∈X
68 1 compss ⊢FX=a∈𝒫A|A∖a∈X
69 68 inteqi ⊢⋂FX=⋂a∈𝒫A|A∖a∈X
70 67 69 eqtr4di ⊢A∈V∧X⊆𝒫A∧X≠∅→F⁡⋃X=⋂FX