Metamath Proof Explorer

Theorem polcon3N

Description: Contraposition law for polarity. Remark in Holland95 p. 223. (Contributed by NM, 23-Mar-2012) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	2polss.a	$⊢ A = Atoms (K)$
		2polss.p	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
	Assertion	polcon3N	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq Y) \to \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)$

Proof

Step	Hyp	Ref	Expression
1		2polss.a	$⊢ A = Atoms (K)$
2		2polss.p	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
3		simp3	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq Y) \to X \subseteq Y$
4		iinss1	$⊢ X \subseteq Y \to ⋂_{p \in Y} pmap (K) (oc (K) (p)) \subseteq ⋂_{p \in X} pmap (K) (oc (K) (p))$
5		sslin	$⊢ ⋂_{p \in Y} pmap (K) (oc (K) (p)) \subseteq ⋂_{p \in X} pmap (K) (oc (K) (p)) \to A \cap ⋂_{p \in Y} pmap (K) (oc (K) (p)) \subseteq A \cap ⋂_{p \in X} pmap (K) (oc (K) (p))$
6	3 4 5	3syl	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq Y) \to A \cap ⋂_{p \in Y} pmap (K) (oc (K) (p)) \subseteq A \cap ⋂_{p \in X} pmap (K) (oc (K) (p))$
7		eqid	$⊢ oc (K) = oc (K)$
8		eqid	$⊢ pmap (K) = pmap (K)$
9	7 1 8 2	polvalN	$⊢ (K \in HL \land Y \subseteq A) \to \underset{˙}{⊥} (Y) = A \cap ⋂_{p \in Y} pmap (K) (oc (K) (p))$
10	9	3adant3	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq Y) \to \underset{˙}{⊥} (Y) = A \cap ⋂_{p \in Y} pmap (K) (oc (K) (p))$
11		simp1	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq Y) \to K \in HL$
12		simp2	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq Y) \to Y \subseteq A$
13	3 12	sstrd	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq Y) \to X \subseteq A$
14	7 1 8 2	polvalN	$⊢ (K \in HL \land X \subseteq A) \to \underset{˙}{⊥} (X) = A \cap ⋂_{p \in X} pmap (K) (oc (K) (p))$
15	11 13 14	syl2anc	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq Y) \to \underset{˙}{⊥} (X) = A \cap ⋂_{p \in X} pmap (K) (oc (K) (p))$
16	6 10 15	3sstr4d	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq Y) \to \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)$