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 ⊢B=BaseK
isdrs.l ⊢≤˙=≤K
Assertion isdrs ⊢K∈Dirset↔K∈Proset∧B≠∅∧∀x∈B∀y∈B∃z∈Bx≤˙z∧y≤˙z

Proof

Step Hyp Ref Expression
1 isdrs.b ⊢B=BaseK
2 isdrs.l ⊢≤˙=≤K
3 fveq2 ⊢f=K→Basef=BaseK
4 3 1 eqtr4di ⊢f=K→Basef=B
5 fveq2 ⊢f=K→≤f=≤K
6 5 2 eqtr4di ⊢f=K→≤f=≤˙
7 6 sbceq1d ⊢f=K→[˙≤f/r]˙b≠∅∧∀x∈b∀y∈b∃z∈bxrz∧yrz↔[˙≤˙/r]˙b≠∅∧∀x∈b∀y∈b∃z∈bxrz∧yrz
8 4 7 sbceqbid ⊢f=K→[˙Basef/b]˙[˙≤f/r]˙b≠∅∧∀x∈b∀y∈b∃z∈bxrz∧yrz↔[˙B/b]˙[˙≤˙/r]˙b≠∅∧∀x∈b∀y∈b∃z∈bxrz∧yrz
9 1 fvexi ⊢B∈V
10 2 fvexi ⊢≤˙∈V
11 neeq1 ⊢b=B→b≠∅↔B≠∅
12 11 adantr ⊢b=B∧r=≤˙→b≠∅↔B≠∅
13 rexeq ⊢b=B→∃z∈bxrz∧yrz↔∃z∈Bxrz∧yrz
14 13 raleqbi1dv ⊢b=B→∀y∈b∃z∈bxrz∧yrz↔∀y∈B∃z∈Bxrz∧yrz
15 14 raleqbi1dv ⊢b=B→∀x∈b∀y∈b∃z∈bxrz∧yrz↔∀x∈B∀y∈B∃z∈Bxrz∧yrz
16 breq ⊢r=≤˙→xrz↔x≤˙z
17 breq ⊢r=≤˙→yrz↔y≤˙z
18 16 17 anbi12d ⊢r=≤˙→xrz∧yrz↔x≤˙z∧y≤˙z
19 18 rexbidv ⊢r=≤˙→∃z∈Bxrz∧yrz↔∃z∈Bx≤˙z∧y≤˙z
20 19 2ralbidv ⊢r=≤˙→∀x∈B∀y∈B∃z∈Bxrz∧yrz↔∀x∈B∀y∈B∃z∈Bx≤˙z∧y≤˙z
21 15 20 sylan9bb ⊢b=B∧r=≤˙→∀x∈b∀y∈b∃z∈bxrz∧yrz↔∀x∈B∀y∈B∃z∈Bx≤˙z∧y≤˙z
22 12 21 anbi12d ⊢b=B∧r=≤˙→b≠∅∧∀x∈b∀y∈b∃z∈bxrz∧yrz↔B≠∅∧∀x∈B∀y∈B∃z∈Bx≤˙z∧y≤˙z
23 9 10 22 sbc2ie ⊢[˙B/b]˙[˙≤˙/r]˙b≠∅∧∀x∈b∀y∈b∃z∈bxrz∧yrz↔B≠∅∧∀x∈B∀y∈B∃z∈Bx≤˙z∧y≤˙z
24 8 23 bitrdi ⊢f=K→[˙Basef/b]˙[˙≤f/r]˙b≠∅∧∀x∈b∀y∈b∃z∈bxrz∧yrz↔B≠∅∧∀x∈B∀y∈B∃z∈Bx≤˙z∧y≤˙z
25 df-drs ⊢Dirset=f∈Proset|[˙Basef/b]˙[˙≤f/r]˙b≠∅∧∀x∈b∀y∈b∃z∈bxrz∧yrz
26 24 25 elrab2 ⊢K∈Dirset↔K∈Proset∧B≠∅∧∀x∈B∀y∈B∃z∈Bx≤˙z∧y≤˙z
27 3anass ⊢K∈Proset∧B≠∅∧∀x∈B∀y∈B∃z∈Bx≤˙z∧y≤˙z↔K∈Proset∧B≠∅∧∀x∈B∀y∈B∃z∈Bx≤˙z∧y≤˙z
28 26 27 bitr4i ⊢K∈Dirset↔K∈Proset∧B≠∅∧∀x∈B∀y∈B∃z∈Bx≤˙z∧y≤˙z