lpolpolsatN

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

	Ref	Expression
Hypotheses	lpolpolsat.a	$⊢ A = LSAtoms (W)$
	lpolpolsat.p	$⊢ P = LPol (W)$
	lpolpolsat.w	$⊢ φ \to W \in X$
	lpolpolsat.o	$⊢ φ \to \underset{˙}{⊥} \in P$
	lpolpolsat.q	$⊢ φ \to Q \in A$
Assertion	lpolpolsatN	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) = Q$

Proof

Step	Hyp	Ref	Expression
1		lpolpolsat.a	$⊢ A = LSAtoms (W)$
2		lpolpolsat.p	$⊢ P = LPol (W)$
3		lpolpolsat.w	$⊢ φ \to W \in X$
4		lpolpolsat.o	$⊢ φ \to \underset{˙}{⊥} \in P$
5		lpolpolsat.q	$⊢ φ \to Q \in A$
6		eqid	$⊢ {Base}_{W} = {Base}_{W}$
7		eqid	$⊢ LSubSp (W) = LSubSp (W)$
8		eqid	$⊢ 0_{W} = 0_{W}$
9		eqid	$⊢ LSHyp (W) = LSHyp (W)$
10	6 7 8 1 9 2	islpolN	$⊢ W \in X \to (\underset{˙}{⊥} \in P \leftrightarrow (\underset{˙}{⊥} : 𝒫 {Base}_{W} ⟶ LSubSp (W) \land (\underset{˙}{⊥} ({Base}_{W}) = \{0_{W}\} \land \forall x \forall y ((x \subseteq {Base}_{W} \land y \subseteq {Base}_{W} \land x \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x)) \land \forall x \in A (\underset{˙}{⊥} (x) \in LSHyp (W) \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x))))$
11	3 10	syl	$⊢ φ \to (\underset{˙}{⊥} \in P \leftrightarrow (\underset{˙}{⊥} : 𝒫 {Base}_{W} ⟶ LSubSp (W) \land (\underset{˙}{⊥} ({Base}_{W}) = \{0_{W}\} \land \forall x \forall y ((x \subseteq {Base}_{W} \land y \subseteq {Base}_{W} \land x \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x)) \land \forall x \in A (\underset{˙}{⊥} (x) \in LSHyp (W) \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x))))$
12	4 11	mpbid	$⊢ φ \to (\underset{˙}{⊥} : 𝒫 {Base}_{W} ⟶ LSubSp (W) \land (\underset{˙}{⊥} ({Base}_{W}) = \{0_{W}\} \land \forall x \forall y ((x \subseteq {Base}_{W} \land y \subseteq {Base}_{W} \land x \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x)) \land \forall x \in A (\underset{˙}{⊥} (x) \in LSHyp (W) \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x)))$
13		simpr3	$⊢ (\underset{˙}{⊥} : 𝒫 {Base}_{W} ⟶ LSubSp (W) \land (\underset{˙}{⊥} ({Base}_{W}) = \{0_{W}\} \land \forall x \forall y ((x \subseteq {Base}_{W} \land y \subseteq {Base}_{W} \land x \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x)) \land \forall x \in A (\underset{˙}{⊥} (x) \in LSHyp (W) \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x))) \to \forall x \in A (\underset{˙}{⊥} (x) \in LSHyp (W) \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x)$
14		fveq2	$⊢ x = Q \to \underset{˙}{⊥} (x) = \underset{˙}{⊥} (Q)$
15	14	eleq1d	$⊢ x = Q \to (\underset{˙}{⊥} (x) \in LSHyp (W) \leftrightarrow \underset{˙}{⊥} (Q) \in LSHyp (W))$
16		2fveq3	$⊢ x = Q \to \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = \underset{˙}{⊥} (\underset{˙}{⊥} (Q))$
17		id	$⊢ x = Q \to x = Q$
18	16 17	eqeq12d	$⊢ x = Q \to (\underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) = Q)$
19	15 18	anbi12d	$⊢ x = Q \to ((\underset{˙}{⊥} (x) \in LSHyp (W) \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x) \leftrightarrow (\underset{˙}{⊥} (Q) \in LSHyp (W) \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) = Q))$
20	19	rspcv	$⊢ Q \in A \to (\forall x \in A (\underset{˙}{⊥} (x) \in LSHyp (W) \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x) \to (\underset{˙}{⊥} (Q) \in LSHyp (W) \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) = Q))$
21	5 20	syl	$⊢ φ \to (\forall x \in A (\underset{˙}{⊥} (x) \in LSHyp (W) \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x) \to (\underset{˙}{⊥} (Q) \in LSHyp (W) \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) = Q))$
22		simpr	$⊢ (\underset{˙}{⊥} (Q) \in LSHyp (W) \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) = Q) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) = Q$
23	13 21 22	syl56	$⊢ φ \to ((\underset{˙}{⊥} : 𝒫 {Base}_{W} ⟶ LSubSp (W) \land (\underset{˙}{⊥} ({Base}_{W}) = \{0_{W}\} \land \forall x \forall y ((x \subseteq {Base}_{W} \land y \subseteq {Base}_{W} \land x \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x)) \land \forall x \in A (\underset{˙}{⊥} (x) \in LSHyp (W) \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x))) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) = Q)$
24	12 23	mpd	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) = Q$

Metamath Proof Explorer

Theorem lpolpolsatN

Proof