2polcon4bN

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

	Ref	Expression
Hypotheses	2polss.a	$⊢ A = Atoms (K)$
	2polss.p	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
Assertion	2polcon4bN	$⊢ (K \in HL \land X \subseteq A \land Y \subseteq A) \to (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) \leftrightarrow \underset{˙}{⊥} (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 \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (Y))) \to K \in HL$
4		simp1	$⊢ (K \in HL \land X \subseteq A \land Y \subseteq A) \to K \in HL$
5	1 2	polssatN	$⊢ (K \in HL \land Y \subseteq A) \to \underset{˙}{⊥} (Y) \subseteq A$
6	5	3adant2	$⊢ (K \in HL \land X \subseteq A \land Y \subseteq A) \to \underset{˙}{⊥} (Y) \subseteq A$
7	1 2	polssatN	$⊢ (K \in HL \land \underset{˙}{⊥} (Y) \subseteq A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) \subseteq A$
8	4 6 7	syl2anc	$⊢ (K \in HL \land X \subseteq A \land Y \subseteq A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) \subseteq A$
9	8	adantr	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (Y))) \to \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) \subseteq A$
10		simpr	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (Y))) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (Y))$
11	1 2	polcon3N	$⊢ (K \in HL \land \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) \subseteq A \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (Y))) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (Y))) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X)))$
12	3 9 10 11	syl3anc	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (Y))) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (Y))) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X)))$
13	12	ex	$⊢ (K \in HL \land X \subseteq A \land Y \subseteq A) \to (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (Y))) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))))$
14	1 2	3polN	$⊢ (K \in HL \land Y \subseteq A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (Y))) = \underset{˙}{⊥} (Y)$
15	14	3adant2	$⊢ (K \in HL \land X \subseteq A \land Y \subseteq A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (Y))) = \underset{˙}{⊥} (Y)$
16	1 2	3polN	$⊢ (K \in HL \land X \subseteq A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) = \underset{˙}{⊥} (X)$
17	16	3adant3	$⊢ (K \in HL \land X \subseteq A \land Y \subseteq A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) = \underset{˙}{⊥} (X)$
18	15 17	sseq12d	$⊢ (K \in HL \land X \subseteq A \land Y \subseteq A) \to (\underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (Y))) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (X))) \leftrightarrow \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X))$
19	13 18	sylibd	$⊢ (K \in HL \land X \subseteq A \land Y \subseteq A) \to (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) \to \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X))$
20		simpl1	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)) \to K \in HL$
21	1 2	polssatN	$⊢ (K \in HL \land X \subseteq A) \to \underset{˙}{⊥} (X) \subseteq A$
22	21	3adant3	$⊢ (K \in HL \land X \subseteq A \land Y \subseteq A) \to \underset{˙}{⊥} (X) \subseteq A$
23	22	adantr	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)) \to \underset{˙}{⊥} (X) \subseteq A$
24		simpr	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)) \to \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)$
25	1 2	polcon3N	$⊢ (K \in HL \land \underset{˙}{⊥} (X) \subseteq A \land \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (Y))$
26	20 23 24 25	syl3anc	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (Y))$
27	26	ex	$⊢ (K \in HL \land X \subseteq A \land Y \subseteq A) \to (\underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (Y)))$
28	19 27	impbid	$⊢ (K \in HL \land X \subseteq A \land Y \subseteq A) \to (\underset{˙}{⊥} (\underset{˙}{⊥} (X)) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (Y)) \leftrightarrow \underset{˙}{⊥} (Y) \subseteq \underset{˙}{⊥} (X))$

Metamath Proof Explorer

Theorem 2polcon4bN

Proof