Metamath Proof Explorer

Theorem lpolconN

Description: Contraposition property of a polarity. (Contributed by NM, 26-Nov-2014) (New usage is discouraged.)

Ref Expression
Hypotheses lpolcon.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lpolcon.p ⊢ 𝑃 = ( LPol ‘ 𝑊 )
lpolcon.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
lpolcon.o ⊢ ( 𝜑 → ⊥ ∈ 𝑃 )
lpolcon.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
lpolcon.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝑉 )
lpolcon.c ⊢ ( 𝜑 → 𝑋 ⊆ 𝑌 )
Assertion lpolconN ( 𝜑 → ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 lpolcon.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lpolcon.p ⊢ 𝑃 = ( LPol ‘ 𝑊 )
3 lpolcon.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
4 lpolcon.o ⊢ ( 𝜑 → ⊥ ∈ 𝑃 )
5 lpolcon.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
6 lpolcon.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝑉 )
7 lpolcon.c ⊢ ( 𝜑 → 𝑋 ⊆ 𝑌 )
8 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
9 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
10 eqid ⊢ ( LSAtoms ‘ 𝑊 ) = ( LSAtoms ‘ 𝑊 )
11 eqid ⊢ ( LSHyp ‘ 𝑊 ) = ( LSHyp ‘ 𝑊 )
12 1 8 9 10 11 2 islpolN ⊢ ( 𝑊 ∈ 𝑋 → ( ⊥ ∈ 𝑃 ↔ ( ⊥ : 𝒫 𝑉 ⟶ ( LSubSp ‘ 𝑊 ) ∧ ( ( ⊥ ‘ 𝑉 ) = { ( 0g ‘ 𝑊 ) } ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) → ( ⊥ ‘ 𝑦 ) ⊆ ( ⊥ ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ ( LSAtoms ‘ 𝑊 ) ( ( ⊥ ‘ 𝑥 ) ∈ ( LSHyp ‘ 𝑊 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ) ) ) ) )
13 3 12 syl ⊢ ( 𝜑 → ( ⊥ ∈ 𝑃 ↔ ( ⊥ : 𝒫 𝑉 ⟶ ( LSubSp ‘ 𝑊 ) ∧ ( ( ⊥ ‘ 𝑉 ) = { ( 0g ‘ 𝑊 ) } ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) → ( ⊥ ‘ 𝑦 ) ⊆ ( ⊥ ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ ( LSAtoms ‘ 𝑊 ) ( ( ⊥ ‘ 𝑥 ) ∈ ( LSHyp ‘ 𝑊 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ) ) ) ) )
14 4 13 mpbid ⊢ ( 𝜑 → ( ⊥ : 𝒫 𝑉 ⟶ ( LSubSp ‘ 𝑊 ) ∧ ( ( ⊥ ‘ 𝑉 ) = { ( 0g ‘ 𝑊 ) } ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) → ( ⊥ ‘ 𝑦 ) ⊆ ( ⊥ ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ ( LSAtoms ‘ 𝑊 ) ( ( ⊥ ‘ 𝑥 ) ∈ ( LSHyp ‘ 𝑊 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ) ) ) )
15 simpr2 ⊢ ( ( ⊥ : 𝒫 𝑉 ⟶ ( LSubSp ‘ 𝑊 ) ∧ ( ( ⊥ ‘ 𝑉 ) = { ( 0g ‘ 𝑊 ) } ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) → ( ⊥ ‘ 𝑦 ) ⊆ ( ⊥ ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ ( LSAtoms ‘ 𝑊 ) ( ( ⊥ ‘ 𝑥 ) ∈ ( LSHyp ‘ 𝑊 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ) ) ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) → ( ⊥ ‘ 𝑦 ) ⊆ ( ⊥ ‘ 𝑥 ) ) )
16 5 6 7 3jca ⊢ ( 𝜑 → ( 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ∧ 𝑋 ⊆ 𝑌 ) )
17 1 fvexi ⊢ 𝑉 ∈ V
18 17 elpw2 ⊢ ( 𝑋 ∈ 𝒫 𝑉 ↔ 𝑋 ⊆ 𝑉 )
19 5 18 sylibr ⊢ ( 𝜑 → 𝑋 ∈ 𝒫 𝑉 )
20 17 elpw2 ⊢ ( 𝑌 ∈ 𝒫 𝑉 ↔ 𝑌 ⊆ 𝑉 )
21 6 20 sylibr ⊢ ( 𝜑 → 𝑌 ∈ 𝒫 𝑉 )
22 sseq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ⊆ 𝑉 ↔ 𝑋 ⊆ 𝑉 ) )
23 biidd ⊢ ( 𝑥 = 𝑋 → ( 𝑦 ⊆ 𝑉 ↔ 𝑦 ⊆ 𝑉 ) )
24 sseq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ⊆ 𝑦 ↔ 𝑋 ⊆ 𝑦 ) )
25 22 23 24 3anbi123d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) ↔ ( 𝑋 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑋 ⊆ 𝑦 ) ) )
26 fveq2 ⊢ ( 𝑥 = 𝑋 → ( ⊥ ‘ 𝑥 ) = ( ⊥ ‘ 𝑋 ) )
27 26 sseq2d ⊢ ( 𝑥 = 𝑋 → ( ( ⊥ ‘ 𝑦 ) ⊆ ( ⊥ ‘ 𝑥 ) ↔ ( ⊥ ‘ 𝑦 ) ⊆ ( ⊥ ‘ 𝑋 ) ) )
28 25 27 imbi12d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) → ( ⊥ ‘ 𝑦 ) ⊆ ( ⊥ ‘ 𝑥 ) ) ↔ ( ( 𝑋 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑋 ⊆ 𝑦 ) → ( ⊥ ‘ 𝑦 ) ⊆ ( ⊥ ‘ 𝑋 ) ) ) )
29 biidd ⊢ ( 𝑦 = 𝑌 → ( 𝑋 ⊆ 𝑉 ↔ 𝑋 ⊆ 𝑉 ) )
30 sseq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 ⊆ 𝑉 ↔ 𝑌 ⊆ 𝑉 ) )
31 sseq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 ⊆ 𝑦 ↔ 𝑋 ⊆ 𝑌 ) )
32 29 30 31 3anbi123d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑋 ⊆ 𝑦 ) ↔ ( 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ∧ 𝑋 ⊆ 𝑌 ) ) )
33 fveq2 ⊢ ( 𝑦 = 𝑌 → ( ⊥ ‘ 𝑦 ) = ( ⊥ ‘ 𝑌 ) )
34 33 sseq1d ⊢ ( 𝑦 = 𝑌 → ( ( ⊥ ‘ 𝑦 ) ⊆ ( ⊥ ‘ 𝑋 ) ↔ ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) ) )
35 32 34 imbi12d ⊢ ( 𝑦 = 𝑌 → ( ( ( 𝑋 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑋 ⊆ 𝑦 ) → ( ⊥ ‘ 𝑦 ) ⊆ ( ⊥ ‘ 𝑋 ) ) ↔ ( ( 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ∧ 𝑋 ⊆ 𝑌 ) → ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) ) ) )
36 28 35 sylan9bb ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) → ( ⊥ ‘ 𝑦 ) ⊆ ( ⊥ ‘ 𝑥 ) ) ↔ ( ( 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ∧ 𝑋 ⊆ 𝑌 ) → ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) ) ) )
37 36 spc2gv ⊢ ( ( 𝑋 ∈ 𝒫 𝑉 ∧ 𝑌 ∈ 𝒫 𝑉 ) → ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) → ( ⊥ ‘ 𝑦 ) ⊆ ( ⊥ ‘ 𝑥 ) ) → ( ( 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ∧ 𝑋 ⊆ 𝑌 ) → ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) ) ) )
38 19 21 37 syl2anc ⊢ ( 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) → ( ⊥ ‘ 𝑦 ) ⊆ ( ⊥ ‘ 𝑥 ) ) → ( ( 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ∧ 𝑋 ⊆ 𝑌 ) → ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) ) ) )
39 16 38 mpid ⊢ ( 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) → ( ⊥ ‘ 𝑦 ) ⊆ ( ⊥ ‘ 𝑥 ) ) → ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) ) )
40 15 39 syl5 ⊢ ( 𝜑 → ( ( ⊥ : 𝒫 𝑉 ⟶ ( LSubSp ‘ 𝑊 ) ∧ ( ( ⊥ ‘ 𝑉 ) = { ( 0g ‘ 𝑊 ) } ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) → ( ⊥ ‘ 𝑦 ) ⊆ ( ⊥ ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ ( LSAtoms ‘ 𝑊 ) ( ( ⊥ ‘ 𝑥 ) ∈ ( LSHyp ‘ 𝑊 ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ) ) ) → ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) ) )
41 14 40 mpd ⊢ ( 𝜑 → ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) )