polcon2N

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

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

Step	Hyp	Ref	Expression
1		2polss.a	$⊢ A = Atoms (K)$
2		2polss.p	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
3	1 2	2polssN	$⊢ (K \in HL \land Y \subseteq A) \to Y \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (Y))$
4	3	3adant3	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \to Y \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (Y))$
5	1 2	polssatN	$⊢ (K \in HL \land Y \subseteq A) \to \underset{˙}{⊥} (Y) \subseteq A$
6	5	3adant3	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \to \underset{˙}{⊥} (Y) \subseteq A$
7	1 2	polcon3N	$⊢ (K \in HL \land \underset{˙}{⊥} (Y) \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) \subseteq \underset{˙}{⊥} (X)$
8	6 7	syld3an2	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) \subseteq \underset{˙}{⊥} (X)$
9	4 8	sstrd	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \to Y \subseteq \underset{˙}{⊥} (X)$

Metamath Proof Explorer