Metamath Proof Explorer

Theorem isipodrs

Description: Condition for a family of sets to be directed by inclusion. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Assertion isipodrs ⊢toInc⁡A∈Dirset↔A∈V∧A≠∅∧∀x∈A∀y∈A∃z∈Ax∪y⊆z

Proof

Step Hyp Ref Expression
1 eqid ⊢BasetoInc⁡A=BasetoInc⁡A
2 1 drsbn0 ⊢toInc⁡A∈Dirset→BasetoInc⁡A≠∅
3 2 neneqd ⊢toInc⁡A∈Dirset→¬BasetoInc⁡A=∅
4 fvprc ⊢¬A∈V→toInc⁡A=∅
5 4 fveq2d ⊢¬A∈V→BasetoInc⁡A=Base∅
6 base0 ⊢∅=Base∅
7 5 6 eqtr4di ⊢¬A∈V→BasetoInc⁡A=∅
8 3 7 nsyl2 ⊢toInc⁡A∈Dirset→A∈V
9 simp1 ⊢A∈V∧A≠∅∧∀x∈A∀y∈A∃z∈Ax∪y⊆z→A∈V
10 eqid ⊢≤toInc⁡A=≤toInc⁡A
11 1 10 isdrs ⊢toInc⁡A∈Dirset↔toInc⁡A∈Proset∧BasetoInc⁡A≠∅∧∀x∈BasetoInc⁡A∀y∈BasetoInc⁡A∃z∈BasetoInc⁡Ax≤toInc⁡Az∧y≤toInc⁡Az
12 eqid ⊢toInc⁡A=toInc⁡A
13 12 ipopos ⊢toInc⁡A∈Poset
14 posprs ⊢toInc⁡A∈Poset→toInc⁡A∈Proset
15 13 14 mp1i ⊢A∈V→toInc⁡A∈Proset
16 id ⊢A∈V→A∈V
17 15 16 2thd ⊢A∈V→toInc⁡A∈Proset↔A∈V
18 12 ipobas ⊢A∈V→A=BasetoInc⁡A
19 neeq1 ⊢A=BasetoInc⁡A→A≠∅↔BasetoInc⁡A≠∅
20 rexeq ⊢A=BasetoInc⁡A→∃z∈Ax≤toInc⁡Az∧y≤toInc⁡Az↔∃z∈BasetoInc⁡Ax≤toInc⁡Az∧y≤toInc⁡Az
21 20 raleqbi1dv ⊢A=BasetoInc⁡A→∀y∈A∃z∈Ax≤toInc⁡Az∧y≤toInc⁡Az↔∀y∈BasetoInc⁡A∃z∈BasetoInc⁡Ax≤toInc⁡Az∧y≤toInc⁡Az
22 21 raleqbi1dv ⊢A=BasetoInc⁡A→∀x∈A∀y∈A∃z∈Ax≤toInc⁡Az∧y≤toInc⁡Az↔∀x∈BasetoInc⁡A∀y∈BasetoInc⁡A∃z∈BasetoInc⁡Ax≤toInc⁡Az∧y≤toInc⁡Az
23 19 22 anbi12d ⊢A=BasetoInc⁡A→A≠∅∧∀x∈A∀y∈A∃z∈Ax≤toInc⁡Az∧y≤toInc⁡Az↔BasetoInc⁡A≠∅∧∀x∈BasetoInc⁡A∀y∈BasetoInc⁡A∃z∈BasetoInc⁡Ax≤toInc⁡Az∧y≤toInc⁡Az
24 18 23 syl ⊢A∈V→A≠∅∧∀x∈A∀y∈A∃z∈Ax≤toInc⁡Az∧y≤toInc⁡Az↔BasetoInc⁡A≠∅∧∀x∈BasetoInc⁡A∀y∈BasetoInc⁡A∃z∈BasetoInc⁡Ax≤toInc⁡Az∧y≤toInc⁡Az
25 simpll ⊢A∈V∧x∈A∧y∈A∧z∈A→A∈V
26 simplrl ⊢A∈V∧x∈A∧y∈A∧z∈A→x∈A
27 simpr ⊢A∈V∧x∈A∧y∈A∧z∈A→z∈A
28 12 10 ipole ⊢A∈V∧x∈A∧z∈A→x≤toInc⁡Az↔x⊆z
29 25 26 27 28 syl3anc ⊢A∈V∧x∈A∧y∈A∧z∈A→x≤toInc⁡Az↔x⊆z
30 simplrr ⊢A∈V∧x∈A∧y∈A∧z∈A→y∈A
31 12 10 ipole ⊢A∈V∧y∈A∧z∈A→y≤toInc⁡Az↔y⊆z
32 25 30 27 31 syl3anc ⊢A∈V∧x∈A∧y∈A∧z∈A→y≤toInc⁡Az↔y⊆z
33 29 32 anbi12d ⊢A∈V∧x∈A∧y∈A∧z∈A→x≤toInc⁡Az∧y≤toInc⁡Az↔x⊆z∧y⊆z
34 unss ⊢x⊆z∧y⊆z↔x∪y⊆z
35 33 34 bitrdi ⊢A∈V∧x∈A∧y∈A∧z∈A→x≤toInc⁡Az∧y≤toInc⁡Az↔x∪y⊆z
36 35 rexbidva ⊢A∈V∧x∈A∧y∈A→∃z∈Ax≤toInc⁡Az∧y≤toInc⁡Az↔∃z∈Ax∪y⊆z
37 36 2ralbidva ⊢A∈V→∀x∈A∀y∈A∃z∈Ax≤toInc⁡Az∧y≤toInc⁡Az↔∀x∈A∀y∈A∃z∈Ax∪y⊆z
38 37 anbi2d ⊢A∈V→A≠∅∧∀x∈A∀y∈A∃z∈Ax≤toInc⁡Az∧y≤toInc⁡Az↔A≠∅∧∀x∈A∀y∈A∃z∈Ax∪y⊆z
39 24 38 bitr3d ⊢A∈V→BasetoInc⁡A≠∅∧∀x∈BasetoInc⁡A∀y∈BasetoInc⁡A∃z∈BasetoInc⁡Ax≤toInc⁡Az∧y≤toInc⁡Az↔A≠∅∧∀x∈A∀y∈A∃z∈Ax∪y⊆z
40 17 39 anbi12d ⊢A∈V→toInc⁡A∈Proset∧BasetoInc⁡A≠∅∧∀x∈BasetoInc⁡A∀y∈BasetoInc⁡A∃z∈BasetoInc⁡Ax≤toInc⁡Az∧y≤toInc⁡Az↔A∈V∧A≠∅∧∀x∈A∀y∈A∃z∈Ax∪y⊆z
41 3anass ⊢toInc⁡A∈Proset∧BasetoInc⁡A≠∅∧∀x∈BasetoInc⁡A∀y∈BasetoInc⁡A∃z∈BasetoInc⁡Ax≤toInc⁡Az∧y≤toInc⁡Az↔toInc⁡A∈Proset∧BasetoInc⁡A≠∅∧∀x∈BasetoInc⁡A∀y∈BasetoInc⁡A∃z∈BasetoInc⁡Ax≤toInc⁡Az∧y≤toInc⁡Az
42 3anass ⊢A∈V∧A≠∅∧∀x∈A∀y∈A∃z∈Ax∪y⊆z↔A∈V∧A≠∅∧∀x∈A∀y∈A∃z∈Ax∪y⊆z
43 40 41 42 3bitr4g ⊢A∈V→toInc⁡A∈Proset∧BasetoInc⁡A≠∅∧∀x∈BasetoInc⁡A∀y∈BasetoInc⁡A∃z∈BasetoInc⁡Ax≤toInc⁡Az∧y≤toInc⁡Az↔A∈V∧A≠∅∧∀x∈A∀y∈A∃z∈Ax∪y⊆z
44 11 43 bitrid ⊢A∈V→toInc⁡A∈Dirset↔A∈V∧A≠∅∧∀x∈A∀y∈A∃z∈Ax∪y⊆z
45 8 9 44 pm5.21nii ⊢toInc⁡A∈Dirset↔A∈V∧A≠∅∧∀x∈A∀y∈A∃z∈Ax∪y⊆z