Theorem islpoldN

Description: Properties that determine a polarity. (Contributed by NM, 26-Nov-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lpolset.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lpolset.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	lpolset.z	⊢ 0 = ( 0g ‘ 𝑊 )
	lpolset.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
	lpolset.h	⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
	lpolset.p	⊢ 𝑃 = ( LPol ‘ 𝑊 )
	islpold.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
	islpold.1	⊢ ( 𝜑 → ⊥ : 𝒫 𝑉 ⟶ 𝑆 )
	islpold.2	⊢ ( 𝜑 → ( ⊥ ‘ 𝑉 ) = { 0 } )
	islpold.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) ) → ( ⊥ ‘ 𝑦 ) ⊆ ( ⊥ ‘ 𝑥 ) )
	islpold.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ⊥ ‘ 𝑥 ) ∈ 𝐻 )
	islpold.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 )
Assertion	islpoldN	⊢ ( 𝜑 → ⊥ ∈ 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		lpolset.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lpolset.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3		lpolset.z	⊢ 0 = ( 0g ‘ 𝑊 )
4		lpolset.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
5		lpolset.h	⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
6		lpolset.p	⊢ 𝑃 = ( LPol ‘ 𝑊 )
7		islpold.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
8		islpold.1	⊢ ( 𝜑 → ⊥ : 𝒫 𝑉 ⟶ 𝑆 )
9		islpold.2	⊢ ( 𝜑 → ( ⊥ ‘ 𝑉 ) = { 0 } )
10		islpold.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) ) → ( ⊥ ‘ 𝑦 ) ⊆ ( ⊥ ‘ 𝑥 ) )
11		islpold.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ⊥ ‘ 𝑥 ) ∈ 𝐻 )
12		islpold.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 )
13	10	ex	⊢ ( 𝜑 → ( ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) → ( ⊥ ‘ 𝑦 ) ⊆ ( ⊥ ‘ 𝑥 ) ) )
14	13	alrimivv	⊢ ( 𝜑 → ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) → ( ⊥ ‘ 𝑦 ) ⊆ ( ⊥ ‘ 𝑥 ) ) )
15	11 12	jca	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ⊥ ‘ 𝑥 ) ∈ 𝐻 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ) )
16	15	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( ( ⊥ ‘ 𝑥 ) ∈ 𝐻 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ) )
17	9 14 16	3jca	⊢ ( 𝜑 → ( ( ⊥ ‘ 𝑉 ) = { 0 } ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) → ( ⊥ ‘ 𝑦 ) ⊆ ( ⊥ ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( ( ⊥ ‘ 𝑥 ) ∈ 𝐻 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ) ) )
18	1 2 3 4 5 6	islpolN	⊢ ( 𝑊 ∈ 𝑋 → ( ⊥ ∈ 𝑃 ↔ ( ⊥ : 𝒫 𝑉 ⟶ 𝑆 ∧ ( ( ⊥ ‘ 𝑉 ) = { 0 } ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) → ( ⊥ ‘ 𝑦 ) ⊆ ( ⊥ ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( ( ⊥ ‘ 𝑥 ) ∈ 𝐻 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ) ) ) ) )
19	7 18	syl	⊢ ( 𝜑 → ( ⊥ ∈ 𝑃 ↔ ( ⊥ : 𝒫 𝑉 ⟶ 𝑆 ∧ ( ( ⊥ ‘ 𝑉 ) = { 0 } ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦 ) → ( ⊥ ‘ 𝑦 ) ⊆ ( ⊥ ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( ( ⊥ ‘ 𝑥 ) ∈ 𝐻 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑥 ) ) = 𝑥 ) ) ) ) )
20	8 17 19	mpbir2and	⊢ ( 𝜑 → ⊥ ∈ 𝑃 )