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

Metamath Proof Explorer

Theorem isdrs

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

Ref Expression
Hypotheses isdrs.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
isdrs.l ⊢ ≤ = ( le ‘ 𝐾 )
Assertion isdrs ( 𝐾 ∈ Dirset ↔ ( 𝐾 ∈ Proset ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 isdrs.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 isdrs.l ⊢ ≤ = ( le ‘ 𝐾 )
3 fveq2 ⊢ ( 𝑓 = 𝐾 → ( Base ‘ 𝑓 ) = ( Base ‘ 𝐾 ) )
4 3 1 eqtr4di ⊢ ( 𝑓 = 𝐾 → ( Base ‘ 𝑓 ) = 𝐵 )
5 fveq2 ⊢ ( 𝑓 = 𝐾 → ( le ‘ 𝑓 ) = ( le ‘ 𝐾 ) )
6 5 2 eqtr4di ⊢ ( 𝑓 = 𝐾 → ( le ‘ 𝑓 ) = ≤ )
7 6 sbceq1d ⊢ ( 𝑓 = 𝐾 → ( [ ( le ‘ 𝑓 ) / 𝑟 ] ( 𝑏 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ) ↔ [ ≤ / 𝑟 ] ( 𝑏 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ) ) )
8 4 7 sbceqbid ⊢ ( 𝑓 = 𝐾 → ( [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ( 𝑏 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ) ↔ [ 𝐵 / 𝑏 ] [ ≤ / 𝑟 ] ( 𝑏 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ) ) )
9 1 fvexi ⊢ 𝐵 ∈ V
10 2 fvexi ⊢ ≤ ∈ V
11 neeq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 ≠ ∅ ↔ 𝐵 ≠ ∅ ) )
12 11 adantr ⊢ ( ( 𝑏 = 𝐵 ∧ 𝑟 = ≤ ) → ( 𝑏 ≠ ∅ ↔ 𝐵 ≠ ∅ ) )
13 rexeq ⊢ ( 𝑏 = 𝐵 → ( ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ↔ ∃ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ) )
14 13 raleqbi1dv ⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ↔ ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ) )
15 14 raleqbi1dv ⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ) )
16 breq ⊢ ( 𝑟 = ≤ → ( 𝑥 𝑟 𝑧 ↔ 𝑥 ≤ 𝑧 ) )
17 breq ⊢ ( 𝑟 = ≤ → ( 𝑦 𝑟 𝑧 ↔ 𝑦 ≤ 𝑧 ) )
18 16 17 anbi12d ⊢ ( 𝑟 = ≤ → ( ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ↔ ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ) )
19 18 rexbidv ⊢ ( 𝑟 = ≤ → ( ∃ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ↔ ∃ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ) )
20 19 2ralbidv ⊢ ( 𝑟 = ≤ → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ) )
21 15 20 sylan9bb ⊢ ( ( 𝑏 = 𝐵 ∧ 𝑟 = ≤ ) → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ) )
22 12 21 anbi12d ⊢ ( ( 𝑏 = 𝐵 ∧ 𝑟 = ≤ ) → ( ( 𝑏 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ) ↔ ( 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ) ) )
23 9 10 22 sbc2ie ⊢ ( [ 𝐵 / 𝑏 ] [ ≤ / 𝑟 ] ( 𝑏 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ) ↔ ( 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ) )
24 8 23 bitrdi ⊢ ( 𝑓 = 𝐾 → ( [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ( 𝑏 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ) ↔ ( 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ) ) )
25 df-drs ⊢ Dirset = { 𝑓 ∈ Proset ∣ [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ( 𝑏 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ) }
26 24 25 elrab2 ⊢ ( 𝐾 ∈ Dirset ↔ ( 𝐾 ∈ Proset ∧ ( 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ) ) )
27 3anass ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ) ↔ ( 𝐾 ∈ Proset ∧ ( 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ) ) )
28 26 27 bitr4i ⊢ ( 𝐾 ∈ Dirset ↔ ( 𝐾 ∈ Proset ∧ 𝐵 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧 ) ) )