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 ) )