Metamath Proof Explorer

Theorem ismre

Description: Property of being a Moore collection on some base set. (Contributed by Stefan O'Rear, 30-Jan-2015)

Ref Expression
Assertion ismre ⊢C∈Moore⁡X↔C⊆𝒫X∧X∈C∧∀s∈𝒫Cs≠∅→⋂s∈C

Proof

Step Hyp Ref Expression
1 elfvex ⊢C∈Moore⁡X→X∈V
2 elex ⊢X∈C→X∈V
3 2 3ad2ant2 ⊢C⊆𝒫X∧X∈C∧∀s∈𝒫Cs≠∅→⋂s∈C→X∈V
4 pweq ⊢x=X→𝒫x=𝒫X
5 4 pweqd ⊢x=X→𝒫𝒫x=𝒫𝒫X
6 eleq1 ⊢x=X→x∈c↔X∈c
7 6 anbi1d ⊢x=X→x∈c∧∀s∈𝒫cs≠∅→⋂s∈c↔X∈c∧∀s∈𝒫cs≠∅→⋂s∈c
8 5 7 rabeqbidv ⊢x=X→c∈𝒫𝒫x|x∈c∧∀s∈𝒫cs≠∅→⋂s∈c=c∈𝒫𝒫X|X∈c∧∀s∈𝒫cs≠∅→⋂s∈c
9 df-mre ⊢Moore=x∈V⟼c∈𝒫𝒫x|x∈c∧∀s∈𝒫cs≠∅→⋂s∈c
10 vpwex ⊢𝒫x∈V
11 10 pwex ⊢𝒫𝒫x∈V
12 11 rabex ⊢c∈𝒫𝒫x|x∈c∧∀s∈𝒫cs≠∅→⋂s∈c∈V
13 8 9 12 fvmpt3i ⊢X∈V→Moore⁡X=c∈𝒫𝒫X|X∈c∧∀s∈𝒫cs≠∅→⋂s∈c
14 13 eleq2d ⊢X∈V→C∈Moore⁡X↔C∈c∈𝒫𝒫X|X∈c∧∀s∈𝒫cs≠∅→⋂s∈c
15 eleq2 ⊢c=C→X∈c↔X∈C
16 pweq ⊢c=C→𝒫c=𝒫C
17 eleq2 ⊢c=C→⋂s∈c↔⋂s∈C
18 17 imbi2d ⊢c=C→s≠∅→⋂s∈c↔s≠∅→⋂s∈C
19 16 18 raleqbidv ⊢c=C→∀s∈𝒫cs≠∅→⋂s∈c↔∀s∈𝒫Cs≠∅→⋂s∈C
20 15 19 anbi12d ⊢c=C→X∈c∧∀s∈𝒫cs≠∅→⋂s∈c↔X∈C∧∀s∈𝒫Cs≠∅→⋂s∈C
21 20 elrab ⊢C∈c∈𝒫𝒫X|X∈c∧∀s∈𝒫cs≠∅→⋂s∈c↔C∈𝒫𝒫X∧X∈C∧∀s∈𝒫Cs≠∅→⋂s∈C
22 21 a1i ⊢X∈V→C∈c∈𝒫𝒫X|X∈c∧∀s∈𝒫cs≠∅→⋂s∈c↔C∈𝒫𝒫X∧X∈C∧∀s∈𝒫Cs≠∅→⋂s∈C
23 pwexg ⊢X∈V→𝒫X∈V
24 elpw2g ⊢𝒫X∈V→C∈𝒫𝒫X↔C⊆𝒫X
25 23 24 syl ⊢X∈V→C∈𝒫𝒫X↔C⊆𝒫X
26 25 anbi1d ⊢X∈V→C∈𝒫𝒫X∧X∈C∧∀s∈𝒫Cs≠∅→⋂s∈C↔C⊆𝒫X∧X∈C∧∀s∈𝒫Cs≠∅→⋂s∈C
27 3anass ⊢C⊆𝒫X∧X∈C∧∀s∈𝒫Cs≠∅→⋂s∈C↔C⊆𝒫X∧X∈C∧∀s∈𝒫Cs≠∅→⋂s∈C
28 26 27 bitr4di ⊢X∈V→C∈𝒫𝒫X∧X∈C∧∀s∈𝒫Cs≠∅→⋂s∈C↔C⊆𝒫X∧X∈C∧∀s∈𝒫Cs≠∅→⋂s∈C
29 14 22 28 3bitrd ⊢X∈V→C∈Moore⁡X↔C⊆𝒫X∧X∈C∧∀s∈𝒫Cs≠∅→⋂s∈C
30 1 3 29 pm5.21nii ⊢C∈Moore⁡X↔C⊆𝒫X∧X∈C∧∀s∈𝒫Cs≠∅→⋂s∈C