lpolconN

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

	Ref	Expression
Hypotheses	lpolcon.v	$⊢ V = {Base}_{W}$
	lpolcon.p	$⊢ P = LPol (W)$
	lpolcon.w	$⊢ φ \to W \in X$
	lpolcon.o	$⊢ φ \to \underset{˙}{⊥} \in P$
	lpolcon.x	$⊢ φ \to X \subseteq V$
	lpolcon.y	$⊢ φ \to Y \subseteq V$
	lpolcon.c	$⊢ φ \to X \subseteq Y$
Assertion	lpolconN	$⊢ φ \to \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)$

Proof

Step	Hyp	Ref	Expression
1		lpolcon.v	$⊢ V = {Base}_{W}$
2		lpolcon.p	$⊢ P = LPol (W)$
3		lpolcon.w	$⊢ φ \to W \in X$
4		lpolcon.o	$⊢ φ \to \underset{˙}{⊥} \in P$
5		lpolcon.x	$⊢ φ \to X \subseteq V$
6		lpolcon.y	$⊢ φ \to Y \subseteq V$
7		lpolcon.c	$⊢ φ \to X \subseteq Y$
8		eqid	$⊢ LSubSp (W) = LSubSp (W)$
9		eqid	$⊢ 0_{W} = 0_{W}$
10		eqid	$⊢ LSAtoms (W) = LSAtoms (W)$
11		eqid	$⊢ LSHyp (W) = LSHyp (W)$
12	1 8 9 10 11 2	islpolN	$⊢ W \in X \to (\underset{˙}{⊥} \in P \leftrightarrow (\underset{˙}{⊥} : 𝒫 V ⟶ LSubSp (W) \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))))$
13	3 12	syl	$⊢ φ \to (\underset{˙}{⊥} \in P \leftrightarrow (\underset{˙}{⊥} : 𝒫 V ⟶ LSubSp (W) \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))))$
14	4 13	mpbid	$⊢ φ \to (\underset{˙}{⊥} : 𝒫 V ⟶ LSubSp (W) \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)))$
15		simpr2	$⊢ (\underset{˙}{⊥} : 𝒫 V ⟶ LSubSp (W) \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))) \to \forall x \forall y ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x))$
16	5 6 7	3jca	$⊢ φ \to (X \subseteq V \land Y \subseteq V \land X \subseteq Y)$
17	1	fvexi	$⊢ V \in V$
18	17	elpw2	$⊢ X \in 𝒫 V \leftrightarrow X \subseteq V$
19	5 18	sylibr	$⊢ φ \to X \in 𝒫 V$
20	17	elpw2	$⊢ Y \in 𝒫 V \leftrightarrow Y \subseteq V$
21	6 20	sylibr	$⊢ φ \to Y \in 𝒫 V$
22		sseq1	$⊢ x = X \to (x \subseteq V \leftrightarrow X \subseteq V)$
23		biidd	$⊢ x = X \to (y \subseteq V \leftrightarrow y \subseteq V)$
24		sseq1	$⊢ x = X \to (x \subseteq y \leftrightarrow X \subseteq y)$
25	22 23 24	3anbi123d	$⊢ x = X \to ((x \subseteq V \land y \subseteq V \land x \subseteq y) \leftrightarrow (X \subseteq V \land y \subseteq V \land X \subseteq y))$
26		fveq2	$⊢ x = X \to \underset{˙}{⊥} (x) = \underset{˙}{⊥} (X)$
27	26	sseq2d	$⊢ x = X \to (\underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x) \leftrightarrow \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (X))$
28	25 27	imbi12d	$⊢ x = X \to (((x \subseteq V \land y \subseteq V \land x \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x)) \leftrightarrow ((X \subseteq V \land y \subseteq V \land X \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (X)))$
29		biidd	$⊢ y = Y \to (X \subseteq V \leftrightarrow X \subseteq V)$
30		sseq1	$⊢ y = Y \to (y \subseteq V \leftrightarrow Y \subseteq V)$
31		sseq2	$⊢ y = Y \to (X \subseteq y \leftrightarrow X \subseteq Y)$
32	29 30 31	3anbi123d	$⊢ y = Y \to ((X \subseteq V \land y \subseteq V \land X \subseteq y) \leftrightarrow (X \subseteq V \land Y \subseteq V \land X \subseteq Y))$
33		fveq2	$⊢ y = Y \to \underset{˙}{⊥} (y) = \underset{˙}{⊥} (Y)$
34	33	sseq1d	$⊢ y = Y \to (\underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (X) \leftrightarrow \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X))$
35	32 34	imbi12d	$⊢ y = Y \to (((X \subseteq V \land y \subseteq V \land X \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (X)) \leftrightarrow ((X \subseteq V \land Y \subseteq V \land X \subseteq Y) \to \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)))$
36	28 35	sylan9bb	$⊢ (x = X \land y = Y) \to (((x \subseteq V \land y \subseteq V \land x \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x)) \leftrightarrow ((X \subseteq V \land Y \subseteq V \land X \subseteq Y) \to \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)))$
37	36	spc2gv	$⊢ (X \in 𝒫 V \land Y \in 𝒫 V) \to (\forall x \forall y ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x)) \to ((X \subseteq V \land Y \subseteq V \land X \subseteq Y) \to \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)))$
38	19 21 37	syl2anc	$⊢ φ \to (\forall x \forall y ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x)) \to ((X \subseteq V \land Y \subseteq V \land X \subseteq Y) \to \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)))$
39	16 38	mpid	$⊢ φ \to (\forall x \forall y ((x \subseteq V \land y \subseteq V \land x \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x)) \to \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X))$
40	15 39	syl5	$⊢ φ \to ((\underset{˙}{⊥} : 𝒫 V ⟶ LSubSp (W) \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))) \to \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X))$
41	14 40	mpd	$⊢ φ \to \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)$

Metamath Proof Explorer

Theorem lpolconN

Proof