Theorem drsdir

Description: Direction of a directed set. (Contributed by Stefan O'Rear, 1-Feb-2015)

	Ref	Expression
Hypotheses	isdrs.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	isdrs.l	⊢ ≤ = ( le ‘ 𝐾 )
Assertion	drsdir	⊢ ( ( 𝐾 ∈ Dirset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ∃ 𝑧 ∈ 𝐵 ( 𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		isdrs.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		isdrs.l	⊢ ≤ = ( le ‘ 𝐾 )
3	1 2	isdrs	⊢ ( 𝐾 ∈ Dirset ↔ ( 𝐾 ∈ Proset ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ) )
4	3	simp3bi	⊢ ( 𝐾 ∈ Dirset → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) )
5		breq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ≤ 𝑧 ↔ 𝑋 ≤ 𝑧 ) )
6	5	anbi1d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ↔ ( 𝑋 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ) )
7	6	rexbidv	⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ↔ ∃ 𝑧 ∈ 𝐵 ( 𝑋 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ) )
8		breq1	⊢ ( 𝑦 = 𝑌 → ( 𝑦 ≤ 𝑧 ↔ 𝑌 ≤ 𝑧 ) )
9	8	anbi2d	⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ↔ ( 𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧 ) ) )
10	9	rexbidv	⊢ ( 𝑦 = 𝑌 → ( ∃ 𝑧 ∈ 𝐵 ( 𝑋 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ↔ ∃ 𝑧 ∈ 𝐵 ( 𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧 ) ) )
11	7 10	rspc2v	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) → ∃ 𝑧 ∈ 𝐵 ( 𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧 ) ) )
12	4 11	syl5com	⊢ ( 𝐾 ∈ Dirset → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ∃ 𝑧 ∈ 𝐵 ( 𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧 ) ) )
13	12	3impib	⊢ ( ( 𝐾 ∈ Dirset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ∃ 𝑧 ∈ 𝐵 ( 𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧 ) )