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

Metamath Proof Explorer

Theorem op1le

Description: If the orthoposet unity is less than or equal to an element, the element equals the unit. ( chle0 analog.) (Contributed by NM, 5-Dec-2011)

		Ref	Expression
	Hypotheses	ople1.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
		ople1.l	⊢ ≤ = ( le ‘ 𝐾 )
		ople1.u	⊢ 1 = ( 1. ‘ 𝐾 )
	Assertion	op1le	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( 1 ≤ 𝑋 ↔ 𝑋 = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		ople1.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		ople1.l	⊢ ≤ = ( le ‘ 𝐾 )
3		ople1.u	⊢ 1 = ( 1. ‘ 𝐾 )
4	1 2 3	ople1	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ≤ 1 )
5	4	biantrurd	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( 1 ≤ 𝑋 ↔ ( 𝑋 ≤ 1 ∧ 1 ≤ 𝑋 ) ) )
6		opposet	⊢ ( 𝐾 ∈ OP → 𝐾 ∈ Poset )
7	6	adantr	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → 𝐾 ∈ Poset )
8		simpr	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
9	1 3	op1cl	⊢ ( 𝐾 ∈ OP → 1 ∈ 𝐵 )
10	9	adantr	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → 1 ∈ 𝐵 )
11	1 2	posasymb	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 1 ∈ 𝐵 ) → ( ( 𝑋 ≤ 1 ∧ 1 ≤ 𝑋 ) ↔ 𝑋 = 1 ) )
12	7 8 10 11	syl3anc	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑋 ≤ 1 ∧ 1 ≤ 𝑋 ) ↔ 𝑋 = 1 ) )
13	5 12	bitrd	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( 1 ≤ 𝑋 ↔ 𝑋 = 1 ) )