This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ⊥ ˙ = ⊥ 𝑃 ⁡ K
Assertion polcon3N ⊢ K ∈ HL ∧ Y ⊆ A ∧ X ⊆ Y → ⊥ ˙ ⁡ Y ⊆ ⊥ ˙ ⁡ X

Proof

Step Hyp Ref Expression
1 2polss.a ⊢ A = Atoms ⁡ K
2 2polss.p ⊢ ⊥ ˙ = ⊥ 𝑃 ⁡ K
3 simp3 ⊢ K ∈ HL ∧ Y ⊆ A ∧ X ⊆ Y → X ⊆ Y
4 iinss1 ⊢ X ⊆ Y → ⋂ p ∈ Y pmap ⁡ K ⁡ oc ⁡ K ⁡ p ⊆ ⋂ p ∈ X pmap ⁡ K ⁡ oc ⁡ K ⁡ p
5 sslin ⊢ ⋂ p ∈ Y pmap ⁡ K ⁡ oc ⁡ K ⁡ p ⊆ ⋂ p ∈ X pmap ⁡ K ⁡ oc ⁡ K ⁡ p → A ∩ ⋂ p ∈ Y pmap ⁡ K ⁡ oc ⁡ K ⁡ p ⊆ A ∩ ⋂ p ∈ X pmap ⁡ K ⁡ oc ⁡ K ⁡ p
6 3 4 5 3syl ⊢ K ∈ HL ∧ Y ⊆ A ∧ X ⊆ Y → A ∩ ⋂ p ∈ Y pmap ⁡ K ⁡ oc ⁡ K ⁡ p ⊆ A ∩ ⋂ p ∈ 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 ∈ HL ∧ Y ⊆ A → ⊥ ˙ ⁡ Y = A ∩ ⋂ p ∈ Y pmap ⁡ K ⁡ oc ⁡ K ⁡ p
10 9 3adant3 ⊢ K ∈ HL ∧ Y ⊆ A ∧ X ⊆ Y → ⊥ ˙ ⁡ Y = A ∩ ⋂ p ∈ Y pmap ⁡ K ⁡ oc ⁡ K ⁡ p
11 simp1 ⊢ K ∈ HL ∧ Y ⊆ A ∧ X ⊆ Y → K ∈ HL
12 simp2 ⊢ K ∈ HL ∧ Y ⊆ A ∧ X ⊆ Y → Y ⊆ A
13 3 12 sstrd ⊢ K ∈ HL ∧ Y ⊆ A ∧ X ⊆ Y → X ⊆ A
14 7 1 8 2 polvalN ⊢ K ∈ HL ∧ X ⊆ A → ⊥ ˙ ⁡ X = A ∩ ⋂ p ∈ X pmap ⁡ K ⁡ oc ⁡ K ⁡ p
15 11 13 14 syl2anc ⊢ K ∈ HL ∧ Y ⊆ A ∧ X ⊆ Y → ⊥ ˙ ⁡ X = A ∩ ⋂ p ∈ X pmap ⁡ K ⁡ oc ⁡ K ⁡ p
16 6 10 15 3sstr4d ⊢ K ∈ HL ∧ Y ⊆ A ∧ X ⊆ Y → ⊥ ˙ ⁡ Y ⊆ ⊥ ˙ ⁡ X