islpolN

Description: The predicate "is a polarity". (Contributed by NM, 24-Nov-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lpolset.v	$⊢ V = {Base}_{W}$
	lpolset.s	$⊢ S = LSubSp (W)$
	lpolset.z	$⊢ \underset{˙}{0} = 0_{W}$
	lpolset.a	$⊢ A = LSAtoms (W)$
	lpolset.h	$⊢ H = LSHyp (W)$
	lpolset.p	$⊢ P = LPol (W)$
Assertion	islpolN	$⊢ W \in X \to (\underset{˙}{⊥} \in P \leftrightarrow (\underset{˙}{⊥} : 𝒫 V ⟶ S \land (\underset{˙}{⊥} (V) = \{\underset{˙}{0}\} \land \forall x \forall y ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x)) \land \forall x \in A (\underset{˙}{⊥} (x) \in H \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x))))$

Proof

Step	Hyp	Ref	Expression
1		lpolset.v	$⊢ V = {Base}_{W}$
2		lpolset.s	$⊢ S = LSubSp (W)$
3		lpolset.z	$⊢ \underset{˙}{0} = 0_{W}$
4		lpolset.a	$⊢ A = LSAtoms (W)$
5		lpolset.h	$⊢ H = LSHyp (W)$
6		lpolset.p	$⊢ P = LPol (W)$
7	1 2 3 4 5 6	lpolsetN	$⊢ W \in X \to P = \{o \in (S^{𝒫 V}) \| (o (V) = \{\underset{˙}{0}\} \land \forall x \forall y ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to o (y) \subseteq o (x)) \land \forall x \in A (o (x) \in H \land o (o (x)) = x))\}$
8	7	eleq2d	$⊢ W \in X \to (\underset{˙}{⊥} \in P \leftrightarrow \underset{˙}{⊥} \in \{o \in (S^{𝒫 V}) \| (o (V) = \{\underset{˙}{0}\} \land \forall x \forall y ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to o (y) \subseteq o (x)) \land \forall x \in A (o (x) \in H \land o (o (x)) = x))\})$
9		fveq1	$⊢ o = \underset{˙}{⊥} \to o (V) = \underset{˙}{⊥} (V)$
10	9	eqeq1d	$⊢ o = \underset{˙}{⊥} \to (o (V) = \{\underset{˙}{0}\} \leftrightarrow \underset{˙}{⊥} (V) = \{\underset{˙}{0}\})$
11		fveq1	$⊢ o = \underset{˙}{⊥} \to o (y) = \underset{˙}{⊥} (y)$
12		fveq1	$⊢ o = \underset{˙}{⊥} \to o (x) = \underset{˙}{⊥} (x)$
13	11 12	sseq12d	$⊢ o = \underset{˙}{⊥} \to (o (y) \subseteq o (x) \leftrightarrow \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x))$
14	13	imbi2d	$⊢ o = \underset{˙}{⊥} \to (((x \subseteq V \land y \subseteq V \land x \subseteq y) \to o (y) \subseteq o (x)) \leftrightarrow ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x)))$
15	14	2albidv	$⊢ o = \underset{˙}{⊥} \to (\forall x \forall y ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to o (y) \subseteq o (x)) \leftrightarrow \forall x \forall y ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x)))$
16	12	eleq1d	$⊢ o = \underset{˙}{⊥} \to (o (x) \in H \leftrightarrow \underset{˙}{⊥} (x) \in H)$
17		id	$⊢ o = \underset{˙}{⊥} \to o = \underset{˙}{⊥}$
18	17 12	fveq12d	$⊢ o = \underset{˙}{⊥} \to o (o (x)) = \underset{˙}{⊥} (\underset{˙}{⊥} (x))$
19	18	eqeq1d	$⊢ o = \underset{˙}{⊥} \to (o (o (x)) = x \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x)$
20	16 19	anbi12d	$⊢ o = \underset{˙}{⊥} \to ((o (x) \in H \land o (o (x)) = x) \leftrightarrow (\underset{˙}{⊥} (x) \in H \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x))$
21	20	ralbidv	$⊢ o = \underset{˙}{⊥} \to (\forall x \in A (o (x) \in H \land o (o (x)) = x) \leftrightarrow \forall x \in A (\underset{˙}{⊥} (x) \in H \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x))$
22	10 15 21	3anbi123d	$⊢ o = \underset{˙}{⊥} \to ((o (V) = \{\underset{˙}{0}\} \land \forall x \forall y ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to o (y) \subseteq o (x)) \land \forall x \in A (o (x) \in H \land o (o (x)) = x)) \leftrightarrow (\underset{˙}{⊥} (V) = \{\underset{˙}{0}\} \land \forall x \forall y ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x)) \land \forall x \in A (\underset{˙}{⊥} (x) \in H \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x)))$
23	22	elrab	$⊢ \underset{˙}{⊥} \in \{o \in (S^{𝒫 V}) \| (o (V) = \{\underset{˙}{0}\} \land \forall x \forall y ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to o (y) \subseteq o (x)) \land \forall x \in A (o (x) \in H \land o (o (x)) = x))\} \leftrightarrow (\underset{˙}{⊥} \in (S^{𝒫 V}) \land (\underset{˙}{⊥} (V) = \{\underset{˙}{0}\} \land \forall x \forall y ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x)) \land \forall x \in A (\underset{˙}{⊥} (x) \in H \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x)))$
24	2	fvexi	$⊢ S \in V$
25	1	fvexi	$⊢ V \in V$
26	25	pwex	$⊢ 𝒫 V \in V$
27	24 26	elmap	$⊢ \underset{˙}{⊥} \in (S^{𝒫 V}) \leftrightarrow \underset{˙}{⊥} : 𝒫 V ⟶ S$
28	27	anbi1i	$⊢ (\underset{˙}{⊥} \in (S^{𝒫 V}) \land (\underset{˙}{⊥} (V) = \{\underset{˙}{0}\} \land \forall x \forall y ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x)) \land \forall x \in A (\underset{˙}{⊥} (x) \in H \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x))) \leftrightarrow (\underset{˙}{⊥} : 𝒫 V ⟶ S \land (\underset{˙}{⊥} (V) = \{\underset{˙}{0}\} \land \forall x \forall y ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x)) \land \forall x \in A (\underset{˙}{⊥} (x) \in H \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x)))$
29	23 28	bitri	$⊢ \underset{˙}{⊥} \in \{o \in (S^{𝒫 V}) \| (o (V) = \{\underset{˙}{0}\} \land \forall x \forall y ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to o (y) \subseteq o (x)) \land \forall x \in A (o (x) \in H \land o (o (x)) = x))\} \leftrightarrow (\underset{˙}{⊥} : 𝒫 V ⟶ S \land (\underset{˙}{⊥} (V) = \{\underset{˙}{0}\} \land \forall x \forall y ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x)) \land \forall x \in A (\underset{˙}{⊥} (x) \in H \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x)))$
30	8 29	bitrdi	$⊢ W \in X \to (\underset{˙}{⊥} \in P \leftrightarrow (\underset{˙}{⊥} : 𝒫 V ⟶ S \land (\underset{˙}{⊥} (V) = \{\underset{˙}{0}\} \land \forall x \forall y ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x)) \land \forall x \in A (\underset{˙}{⊥} (x) \in H \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x))))$

Metamath Proof Explorer

Theorem islpolN

Proof