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 ) e. Dirset <-> ( A e. _V /\ A =/= (/) /\ A. x e. A A. y e. A E. z e. A ( x u. y ) C_ z ) )

Proof

Step Hyp Ref Expression
1 eqid
 |-  ( Base ` ( toInc ` A ) ) = ( Base ` ( toInc ` A ) )
2 1 drsbn0
 |-  ( ( toInc ` A ) e. Dirset -> ( Base ` ( toInc ` A ) ) =/= (/) )
3 2 neneqd
 |-  ( ( toInc ` A ) e. Dirset -> -. ( Base ` ( toInc ` A ) ) = (/) )
4 fvprc
 |-  ( -. A e. _V -> ( toInc ` A ) = (/) )
5 4 fveq2d
 |-  ( -. A e. _V -> ( Base ` ( toInc ` A ) ) = ( Base ` (/) ) )
6 base0
 |-  (/) = ( Base ` (/) )
7 5 6 eqtr4di
 |-  ( -. A e. _V -> ( Base ` ( toInc ` A ) ) = (/) )
8 3 7 nsyl2
 |-  ( ( toInc ` A ) e. Dirset -> A e. _V )
9 simp1
 |-  ( ( A e. _V /\ A =/= (/) /\ A. x e. A A. y e. A E. z e. A ( x u. y ) C_ z ) -> A e. _V )
10 eqid
 |-  ( le ` ( toInc ` A ) ) = ( le ` ( toInc ` A ) )
11 1 10 isdrs
 |-  ( ( toInc ` A ) e. Dirset <-> ( ( toInc ` A ) e. Proset /\ ( Base ` ( toInc ` A ) ) =/= (/) /\ A. x e. ( Base ` ( toInc ` A ) ) A. y e. ( Base ` ( toInc ` A ) ) E. z e. ( Base ` ( toInc ` A ) ) ( x ( le ` ( toInc ` A ) ) z /\ y ( le ` ( toInc ` A ) ) z ) ) )
12 eqid
 |-  ( toInc ` A ) = ( toInc ` A )
13 12 ipopos
 |-  ( toInc ` A ) e. Poset
14 posprs
 |-  ( ( toInc ` A ) e. Poset -> ( toInc ` A ) e. Proset )
15 13 14 mp1i
 |-  ( A e. _V -> ( toInc ` A ) e. Proset )
16 id
 |-  ( A e. _V -> A e. _V )
17 15 16 2thd
 |-  ( A e. _V -> ( ( toInc ` A ) e. Proset <-> A e. _V ) )
18 12 ipobas
 |-  ( A e. _V -> A = ( Base ` ( toInc ` A ) ) )
19 neeq1
 |-  ( A = ( Base ` ( toInc ` A ) ) -> ( A =/= (/) <-> ( Base ` ( toInc ` A ) ) =/= (/) ) )
20 rexeq
 |-  ( A = ( Base ` ( toInc ` A ) ) -> ( E. z e. A ( x ( le ` ( toInc ` A ) ) z /\ y ( le ` ( toInc ` A ) ) z ) <-> E. z e. ( Base ` ( toInc ` A ) ) ( x ( le ` ( toInc ` A ) ) z /\ y ( le ` ( toInc ` A ) ) z ) ) )
21 20 raleqbi1dv
 |-  ( A = ( Base ` ( toInc ` A ) ) -> ( A. y e. A E. z e. A ( x ( le ` ( toInc ` A ) ) z /\ y ( le ` ( toInc ` A ) ) z ) <-> A. y e. ( Base ` ( toInc ` A ) ) E. z e. ( Base ` ( toInc ` A ) ) ( x ( le ` ( toInc ` A ) ) z /\ y ( le ` ( toInc ` A ) ) z ) ) )
22 21 raleqbi1dv
 |-  ( A = ( Base ` ( toInc ` A ) ) -> ( A. x e. A A. y e. A E. z e. A ( x ( le ` ( toInc ` A ) ) z /\ y ( le ` ( toInc ` A ) ) z ) <-> A. x e. ( Base ` ( toInc ` A ) ) A. y e. ( Base ` ( toInc ` A ) ) E. z e. ( Base ` ( toInc ` A ) ) ( x ( le ` ( toInc ` A ) ) z /\ y ( le ` ( toInc ` A ) ) z ) ) )
23 19 22 anbi12d
 |-  ( A = ( Base ` ( toInc ` A ) ) -> ( ( A =/= (/) /\ A. x e. A A. y e. A E. z e. A ( x ( le ` ( toInc ` A ) ) z /\ y ( le ` ( toInc ` A ) ) z ) ) <-> ( ( Base ` ( toInc ` A ) ) =/= (/) /\ A. x e. ( Base ` ( toInc ` A ) ) A. y e. ( Base ` ( toInc ` A ) ) E. z e. ( Base ` ( toInc ` A ) ) ( x ( le ` ( toInc ` A ) ) z /\ y ( le ` ( toInc ` A ) ) z ) ) ) )
24 18 23 syl
 |-  ( A e. _V -> ( ( A =/= (/) /\ A. x e. A A. y e. A E. z e. A ( x ( le ` ( toInc ` A ) ) z /\ y ( le ` ( toInc ` A ) ) z ) ) <-> ( ( Base ` ( toInc ` A ) ) =/= (/) /\ A. x e. ( Base ` ( toInc ` A ) ) A. y e. ( Base ` ( toInc ` A ) ) E. z e. ( Base ` ( toInc ` A ) ) ( x ( le ` ( toInc ` A ) ) z /\ y ( le ` ( toInc ` A ) ) z ) ) ) )
25 simpll
 |-  ( ( ( A e. _V /\ ( x e. A /\ y e. A ) ) /\ z e. A ) -> A e. _V )
26 simplrl
 |-  ( ( ( A e. _V /\ ( x e. A /\ y e. A ) ) /\ z e. A ) -> x e. A )
27 simpr
 |-  ( ( ( A e. _V /\ ( x e. A /\ y e. A ) ) /\ z e. A ) -> z e. A )
28 12 10 ipole
 |-  ( ( A e. _V /\ x e. A /\ z e. A ) -> ( x ( le ` ( toInc ` A ) ) z <-> x C_ z ) )
29 25 26 27 28 syl3anc
 |-  ( ( ( A e. _V /\ ( x e. A /\ y e. A ) ) /\ z e. A ) -> ( x ( le ` ( toInc ` A ) ) z <-> x C_ z ) )
30 simplrr
 |-  ( ( ( A e. _V /\ ( x e. A /\ y e. A ) ) /\ z e. A ) -> y e. A )
31 12 10 ipole
 |-  ( ( A e. _V /\ y e. A /\ z e. A ) -> ( y ( le ` ( toInc ` A ) ) z <-> y C_ z ) )
32 25 30 27 31 syl3anc
 |-  ( ( ( A e. _V /\ ( x e. A /\ y e. A ) ) /\ z e. A ) -> ( y ( le ` ( toInc ` A ) ) z <-> y C_ z ) )
33 29 32 anbi12d
 |-  ( ( ( A e. _V /\ ( x e. A /\ y e. A ) ) /\ z e. A ) -> ( ( x ( le ` ( toInc ` A ) ) z /\ y ( le ` ( toInc ` A ) ) z ) <-> ( x C_ z /\ y C_ z ) ) )
34 unss
 |-  ( ( x C_ z /\ y C_ z ) <-> ( x u. y ) C_ z )
35 33 34 bitrdi
 |-  ( ( ( A e. _V /\ ( x e. A /\ y e. A ) ) /\ z e. A ) -> ( ( x ( le ` ( toInc ` A ) ) z /\ y ( le ` ( toInc ` A ) ) z ) <-> ( x u. y ) C_ z ) )
36 35 rexbidva
 |-  ( ( A e. _V /\ ( x e. A /\ y e. A ) ) -> ( E. z e. A ( x ( le ` ( toInc ` A ) ) z /\ y ( le ` ( toInc ` A ) ) z ) <-> E. z e. A ( x u. y ) C_ z ) )
37 36 2ralbidva
 |-  ( A e. _V -> ( A. x e. A A. y e. A E. z e. A ( x ( le ` ( toInc ` A ) ) z /\ y ( le ` ( toInc ` A ) ) z ) <-> A. x e. A A. y e. A E. z e. A ( x u. y ) C_ z ) )
38 37 anbi2d
 |-  ( A e. _V -> ( ( A =/= (/) /\ A. x e. A A. y e. A E. z e. A ( x ( le ` ( toInc ` A ) ) z /\ y ( le ` ( toInc ` A ) ) z ) ) <-> ( A =/= (/) /\ A. x e. A A. y e. A E. z e. A ( x u. y ) C_ z ) ) )
39 24 38 bitr3d
 |-  ( A e. _V -> ( ( ( Base ` ( toInc ` A ) ) =/= (/) /\ A. x e. ( Base ` ( toInc ` A ) ) A. y e. ( Base ` ( toInc ` A ) ) E. z e. ( Base ` ( toInc ` A ) ) ( x ( le ` ( toInc ` A ) ) z /\ y ( le ` ( toInc ` A ) ) z ) ) <-> ( A =/= (/) /\ A. x e. A A. y e. A E. z e. A ( x u. y ) C_ z ) ) )
40 17 39 anbi12d
 |-  ( A e. _V -> ( ( ( toInc ` A ) e. Proset /\ ( ( Base ` ( toInc ` A ) ) =/= (/) /\ A. x e. ( Base ` ( toInc ` A ) ) A. y e. ( Base ` ( toInc ` A ) ) E. z e. ( Base ` ( toInc ` A ) ) ( x ( le ` ( toInc ` A ) ) z /\ y ( le ` ( toInc ` A ) ) z ) ) ) <-> ( A e. _V /\ ( A =/= (/) /\ A. x e. A A. y e. A E. z e. A ( x u. y ) C_ z ) ) ) )
41 3anass
 |-  ( ( ( toInc ` A ) e. Proset /\ ( Base ` ( toInc ` A ) ) =/= (/) /\ A. x e. ( Base ` ( toInc ` A ) ) A. y e. ( Base ` ( toInc ` A ) ) E. z e. ( Base ` ( toInc ` A ) ) ( x ( le ` ( toInc ` A ) ) z /\ y ( le ` ( toInc ` A ) ) z ) ) <-> ( ( toInc ` A ) e. Proset /\ ( ( Base ` ( toInc ` A ) ) =/= (/) /\ A. x e. ( Base ` ( toInc ` A ) ) A. y e. ( Base ` ( toInc ` A ) ) E. z e. ( Base ` ( toInc ` A ) ) ( x ( le ` ( toInc ` A ) ) z /\ y ( le ` ( toInc ` A ) ) z ) ) ) )
42 3anass
 |-  ( ( A e. _V /\ A =/= (/) /\ A. x e. A A. y e. A E. z e. A ( x u. y ) C_ z ) <-> ( A e. _V /\ ( A =/= (/) /\ A. x e. A A. y e. A E. z e. A ( x u. y ) C_ z ) ) )
43 40 41 42 3bitr4g
 |-  ( A e. _V -> ( ( ( toInc ` A ) e. Proset /\ ( Base ` ( toInc ` A ) ) =/= (/) /\ A. x e. ( Base ` ( toInc ` A ) ) A. y e. ( Base ` ( toInc ` A ) ) E. z e. ( Base ` ( toInc ` A ) ) ( x ( le ` ( toInc ` A ) ) z /\ y ( le ` ( toInc ` A ) ) z ) ) <-> ( A e. _V /\ A =/= (/) /\ A. x e. A A. y e. A E. z e. A ( x u. y ) C_ z ) ) )
44 11 43 syl5bb
 |-  ( A e. _V -> ( ( toInc ` A ) e. Dirset <-> ( A e. _V /\ A =/= (/) /\ A. x e. A A. y e. A E. z e. A ( x u. y ) C_ z ) ) )
45 8 9 44 pm5.21nii
 |-  ( ( toInc ` A ) e. Dirset <-> ( A e. _V /\ A =/= (/) /\ A. x e. A A. y e. A E. z e. A ( x u. y ) C_ z ) )