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

Metamath Proof Explorer

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 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ∃ 𝑧 ∈ 𝐵 ( 𝑋 ≤ 𝑧 ∧ 𝑌 ≤ 𝑧 ) )