Metamath Proof Explorer

Theorem polcon2bN

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	polcon2bN	$⊢ (K \in HL \land X \subseteq A \land Y \subseteq A) \to (X \subseteq \underset{˙}{⊥} (Y) \leftrightarrow Y \subseteq \underset{˙}{⊥} (X))$

Proof

Step	Hyp	Ref	Expression
1		2polss.a	$⊢ A = Atoms (K)$
2		2polss.p	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
3		simpl1	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land X \subseteq \underset{˙}{⊥} (Y)) \to K \in HL$
4		simpl3	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land X \subseteq \underset{˙}{⊥} (Y)) \to Y \subseteq A$
5		simpr	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land X \subseteq \underset{˙}{⊥} (Y)) \to X \subseteq \underset{˙}{⊥} (Y)$
6	1 2	polcon2N	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq \underset{˙}{⊥} (Y)) \to Y \subseteq \underset{˙}{⊥} (X)$
7	3 4 5 6	syl3anc	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land X \subseteq \underset{˙}{⊥} (Y)) \to Y \subseteq \underset{˙}{⊥} (X)$
8		simpl1	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land Y \subseteq \underset{˙}{⊥} (X)) \to K \in HL$
9		simpl2	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land Y \subseteq \underset{˙}{⊥} (X)) \to X \subseteq A$
10		simpr	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land Y \subseteq \underset{˙}{⊥} (X)) \to Y \subseteq \underset{˙}{⊥} (X)$
11	1 2	polcon2N	$⊢ (K \in HL \land X \subseteq A \land Y \subseteq \underset{˙}{⊥} (X)) \to X \subseteq \underset{˙}{⊥} (Y)$
12	8 9 10 11	syl3anc	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land Y \subseteq \underset{˙}{⊥} (X)) \to X \subseteq \underset{˙}{⊥} (Y)$
13	7 12	impbida	$⊢ (K \in HL \land X \subseteq A \land Y \subseteq A) \to (X \subseteq \underset{˙}{⊥} (Y) \leftrightarrow Y \subseteq \underset{˙}{⊥} (X))$