Metamath Proof Explorer

Theorem lpolfN

Description: Functionality of a polarity. (Contributed by NM, 26-Nov-2014) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	lpolf.v	$⊢ V = {Base}_{W}$
		lpolf.s	$⊢ S = LSubSp (W)$
		lpolf.p	$⊢ P = LPol (W)$
		lpolf.w	$⊢ φ \to W \in X$
		lpolf.o	$⊢ φ \to \underset{˙}{⊥} \in P$
	Assertion	lpolfN	$⊢ φ \to \underset{˙}{⊥} : 𝒫 V ⟶ S$

Proof

Step	Hyp	Ref	Expression
1		lpolf.v	$⊢ V = {Base}_{W}$
2		lpolf.s	$⊢ S = LSubSp (W)$
3		lpolf.p	$⊢ P = LPol (W)$
4		lpolf.w	$⊢ φ \to W \in X$
5		lpolf.o	$⊢ φ \to \underset{˙}{⊥} \in P$
6		eqid	$⊢ 0_{W} = 0_{W}$
7		eqid	$⊢ LSAtoms (W) = LSAtoms (W)$
8		eqid	$⊢ LSHyp (W) = LSHyp (W)$
9	1 2 6 7 8 3	islpolN	$⊢ W \in X \to (\underset{˙}{⊥} \in P \leftrightarrow (\underset{˙}{⊥} : 𝒫 V ⟶ S \land (\underset{˙}{⊥} (V) = \{0_{W}\} \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 LSAtoms (W) (\underset{˙}{⊥} (x) \in LSHyp (W) \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x))))$
10	4 9	syl	$⊢ φ \to (\underset{˙}{⊥} \in P \leftrightarrow (\underset{˙}{⊥} : 𝒫 V ⟶ S \land (\underset{˙}{⊥} (V) = \{0_{W}\} \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 LSAtoms (W) (\underset{˙}{⊥} (x) \in LSHyp (W) \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x))))$
11	5 10	mpbid	$⊢ φ \to (\underset{˙}{⊥} : 𝒫 V ⟶ S \land (\underset{˙}{⊥} (V) = \{0_{W}\} \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 LSAtoms (W) (\underset{˙}{⊥} (x) \in LSHyp (W) \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x)))$
12	11	simpld	$⊢ φ \to \underset{˙}{⊥} : 𝒫 V ⟶ S$