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	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	2polss.p	⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
Assertion	polcon3N	⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝑌 ) → ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		2polss.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2		2polss.p	⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
3		simp3	⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝑌 ) → 𝑋 ⊆ 𝑌 )
4		iinss1	⊢ ( 𝑋 ⊆ 𝑌 → ∩ 𝑝 ∈ 𝑌 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ⊆ ∩ 𝑝 ∈ 𝑋 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) )
5		sslin	⊢ ( ∩ 𝑝 ∈ 𝑌 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ⊆ ∩ 𝑝 ∈ 𝑋 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) → ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑌 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) ⊆ ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑋 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) )
6	3 4 5	3syl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝑌 ) → ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑌 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) ⊆ ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑋 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) )
7		eqid	⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
8		eqid	⊢ ( pmap ‘ 𝐾 ) = ( pmap ‘ 𝐾 )
9	7 1 8 2	polvalN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ) → ( ⊥ ‘ 𝑌 ) = ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑌 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) )
10	9	3adant3	⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝑌 ) → ( ⊥ ‘ 𝑌 ) = ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑌 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) )
11		simp1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝑌 ) → 𝐾 ∈ HL )
12		simp2	⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝑌 ) → 𝑌 ⊆ 𝐴 )
13	3 12	sstrd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝑌 ) → 𝑋 ⊆ 𝐴 )
14	7 1 8 2	polvalN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( ⊥ ‘ 𝑋 ) = ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑋 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) )
15	11 13 14	syl2anc	⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝑌 ) → ( ⊥ ‘ 𝑋 ) = ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑋 ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) )
16	6 10 15	3sstr4d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝑌 ) → ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) )