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