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

Metamath Proof Explorer

Theorem polcon2N

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

Ref Expression
Hypotheses 2polss.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2polss.p ⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
Assertion polcon2N ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → 𝑌 ⊆ ( ⊥ ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 2polss.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 2polss.p ⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
3 1 2 2polssN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ) → 𝑌 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) )
4 3 3adant3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → 𝑌 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) )
5 1 2 polssatN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ) → ( ⊥ ‘ 𝑌 ) ⊆ 𝐴 )
6 5 3adant3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → ( ⊥ ‘ 𝑌 ) ⊆ 𝐴 )
7 1 2 polcon3N ⊢ ( ( 𝐾 ∈ HL ∧ ( ⊥ ‘ 𝑌 ) ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) ⊆ ( ⊥ ‘ 𝑋 ) )
8 6 7 syld3an2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) ⊆ ( ⊥ ‘ 𝑋 ) )
9 4 8 sstrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → 𝑌 ⊆ ( ⊥ ‘ 𝑋 ) )