islpoldN

Description: Properties that determine a polarity. (Contributed by NM, 26-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)$
	islpold.w	$⊢ φ \to W \in X$
	islpold.1	$⊢ φ \to \underset{˙}{⊥} : 𝒫 V ⟶ S$
	islpold.2	$⊢ φ \to \underset{˙}{⊥} (V) = \{\underset{˙}{0}\}$
	islpold.3	$⊢ (φ \land (x \subseteq V \land y \subseteq V \land x \subseteq y)) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x)$
	islpold.4	$⊢ (φ \land x \in A) \to \underset{˙}{⊥} (x) \in H$
	islpold.5	$⊢ (φ \land x \in A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x$
Assertion	islpoldN	$⊢ φ \to \underset{˙}{⊥} \in P$

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		islpold.w	$⊢ φ \to W \in X$
8		islpold.1	$⊢ φ \to \underset{˙}{⊥} : 𝒫 V ⟶ S$
9		islpold.2	$⊢ φ \to \underset{˙}{⊥} (V) = \{\underset{˙}{0}\}$
10		islpold.3	$⊢ (φ \land (x \subseteq V \land y \subseteq V \land x \subseteq y)) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x)$
11		islpold.4	$⊢ (φ \land x \in A) \to \underset{˙}{⊥} (x) \in H$
12		islpold.5	$⊢ (φ \land x \in A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x$
13	10	ex	$⊢ φ \to ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x))$
14	13	alrimivv	$⊢ φ \to \forall x \forall y ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x))$
15	11 12	jca	$⊢ (φ \land x \in A) \to (\underset{˙}{⊥} (x) \in H \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x)$
16	15	ralrimiva	$⊢ φ \to \forall x \in A (\underset{˙}{⊥} (x) \in H \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x)$
17	9 14 16	3jca	$⊢ φ \to (\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))$
18	1 2 3 4 5 6	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))))$
19	7 18	syl	$⊢ φ \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))))$
20	8 17 19	mpbir2and	$⊢ φ \to \underset{˙}{⊥} \in P$

Metamath Proof Explorer

Theorem islpoldN

Proof