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 \in Moore (X) \leftrightarrow (C \subseteq 𝒫 X \land X \in C \land \forall s \in 𝒫 C (s \neq \emptyset \to ⋂ s \in C))$

Proof

Step	Hyp	Ref	Expression
1		elfvex	$⊢ C \in Moore (X) \to X \in V$
2		elex	$⊢ X \in C \to X \in V$
3	2	3ad2ant2	$⊢ (C \subseteq 𝒫 X \land X \in C \land \forall s \in 𝒫 C (s \neq \emptyset \to ⋂ s \in C)) \to X \in V$
4		pweq	$⊢ x = X \to 𝒫 x = 𝒫 X$
5	4	pweqd	$⊢ x = X \to 𝒫 𝒫 x = 𝒫 𝒫 X$
6		eleq1	$⊢ x = X \to (x \in c \leftrightarrow X \in c)$
7	6	anbi1d	$⊢ x = X \to ((x \in c \land \forall s \in 𝒫 c (s \neq \emptyset \to ⋂ s \in c)) \leftrightarrow (X \in c \land \forall s \in 𝒫 c (s \neq \emptyset \to ⋂ s \in c)))$
8	5 7	rabeqbidv	$⊢ x = X \to \{c \in 𝒫 𝒫 x \| (x \in c \land \forall s \in 𝒫 c (s \neq \emptyset \to ⋂ s \in c))\} = \{c \in 𝒫 𝒫 X \| (X \in c \land \forall s \in 𝒫 c (s \neq \emptyset \to ⋂ s \in c))\}$
9		df-mre	$⊢ Moore = (x \in V ⟼ \{c \in 𝒫 𝒫 x \| (x \in c \land \forall s \in 𝒫 c (s \neq \emptyset \to ⋂ s \in c))\})$
10		vpwex	$⊢ 𝒫 x \in V$
11	10	pwex	$⊢ 𝒫 𝒫 x \in V$
12	11	rabex	$⊢ \{c \in 𝒫 𝒫 x \| (x \in c \land \forall s \in 𝒫 c (s \neq \emptyset \to ⋂ s \in c))\} \in V$
13	8 9 12	fvmpt3i	$⊢ X \in V \to Moore (X) = \{c \in 𝒫 𝒫 X \| (X \in c \land \forall s \in 𝒫 c (s \neq \emptyset \to ⋂ s \in c))\}$
14	13	eleq2d	$⊢ X \in V \to (C \in Moore (X) \leftrightarrow C \in \{c \in 𝒫 𝒫 X \| (X \in c \land \forall s \in 𝒫 c (s \neq \emptyset \to ⋂ s \in c))\})$
15		eleq2	$⊢ c = C \to (X \in c \leftrightarrow X \in C)$
16		pweq	$⊢ c = C \to 𝒫 c = 𝒫 C$
17		eleq2	$⊢ c = C \to (⋂ s \in c \leftrightarrow ⋂ s \in C)$
18	17	imbi2d	$⊢ c = C \to ((s \neq \emptyset \to ⋂ s \in c) \leftrightarrow (s \neq \emptyset \to ⋂ s \in C))$
19	16 18	raleqbidv	$⊢ c = C \to (\forall s \in 𝒫 c (s \neq \emptyset \to ⋂ s \in c) \leftrightarrow \forall s \in 𝒫 C (s \neq \emptyset \to ⋂ s \in C))$
20	15 19	anbi12d	$⊢ c = C \to ((X \in c \land \forall s \in 𝒫 c (s \neq \emptyset \to ⋂ s \in c)) \leftrightarrow (X \in C \land \forall s \in 𝒫 C (s \neq \emptyset \to ⋂ s \in C)))$
21	20	elrab	$⊢ C \in \{c \in 𝒫 𝒫 X \| (X \in c \land \forall s \in 𝒫 c (s \neq \emptyset \to ⋂ s \in c))\} \leftrightarrow (C \in 𝒫 𝒫 X \land (X \in C \land \forall s \in 𝒫 C (s \neq \emptyset \to ⋂ s \in C)))$
22	21	a1i	$⊢ X \in V \to (C \in \{c \in 𝒫 𝒫 X \| (X \in c \land \forall s \in 𝒫 c (s \neq \emptyset \to ⋂ s \in c))\} \leftrightarrow (C \in 𝒫 𝒫 X \land (X \in C \land \forall s \in 𝒫 C (s \neq \emptyset \to ⋂ s \in C))))$
23		pwexg	$⊢ X \in V \to 𝒫 X \in V$
24		elpw2g	$⊢ 𝒫 X \in V \to (C \in 𝒫 𝒫 X \leftrightarrow C \subseteq 𝒫 X)$
25	23 24	syl	$⊢ X \in V \to (C \in 𝒫 𝒫 X \leftrightarrow C \subseteq 𝒫 X)$
26	25	anbi1d	$⊢ X \in V \to ((C \in 𝒫 𝒫 X \land (X \in C \land \forall s \in 𝒫 C (s \neq \emptyset \to ⋂ s \in C))) \leftrightarrow (C \subseteq 𝒫 X \land (X \in C \land \forall s \in 𝒫 C (s \neq \emptyset \to ⋂ s \in C))))$
27		3anass	$⊢ (C \subseteq 𝒫 X \land X \in C \land \forall s \in 𝒫 C (s \neq \emptyset \to ⋂ s \in C)) \leftrightarrow (C \subseteq 𝒫 X \land (X \in C \land \forall s \in 𝒫 C (s \neq \emptyset \to ⋂ s \in C)))$
28	26 27	bitr4di	$⊢ X \in V \to ((C \in 𝒫 𝒫 X \land (X \in C \land \forall s \in 𝒫 C (s \neq \emptyset \to ⋂ s \in C))) \leftrightarrow (C \subseteq 𝒫 X \land X \in C \land \forall s \in 𝒫 C (s \neq \emptyset \to ⋂ s \in C)))$
29	14 22 28	3bitrd	$⊢ X \in V \to (C \in Moore (X) \leftrightarrow (C \subseteq 𝒫 X \land X \in C \land \forall s \in 𝒫 C (s \neq \emptyset \to ⋂ s \in C)))$
30	1 3 29	pm5.21nii	$⊢ C \in Moore (X) \leftrightarrow (C \subseteq 𝒫 X \land X \in C \land \forall s \in 𝒫 C (s \neq \emptyset \to ⋂ s \in C))$

Metamath Proof Explorer

Theorem ismre

Proof