Step |
Hyp |
Ref |
Expression |
1 |
|
drsbn0.b |
|- B = ( Base ` K ) |
2 |
|
drsdirfi.l |
|- .<_ = ( le ` K ) |
3 |
|
drsprs |
|- ( K e. Dirset -> K e. Proset ) |
4 |
|
simpl |
|- ( ( K e. Dirset /\ x e. ( ~P B i^i Fin ) ) -> K e. Dirset ) |
5 |
|
elinel1 |
|- ( x e. ( ~P B i^i Fin ) -> x e. ~P B ) |
6 |
5
|
elpwid |
|- ( x e. ( ~P B i^i Fin ) -> x C_ B ) |
7 |
6
|
adantl |
|- ( ( K e. Dirset /\ x e. ( ~P B i^i Fin ) ) -> x C_ B ) |
8 |
|
elinel2 |
|- ( x e. ( ~P B i^i Fin ) -> x e. Fin ) |
9 |
8
|
adantl |
|- ( ( K e. Dirset /\ x e. ( ~P B i^i Fin ) ) -> x e. Fin ) |
10 |
1 2
|
drsdirfi |
|- ( ( K e. Dirset /\ x C_ B /\ x e. Fin ) -> E. y e. B A. z e. x z .<_ y ) |
11 |
4 7 9 10
|
syl3anc |
|- ( ( K e. Dirset /\ x e. ( ~P B i^i Fin ) ) -> E. y e. B A. z e. x z .<_ y ) |
12 |
11
|
ralrimiva |
|- ( K e. Dirset -> A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y ) |
13 |
3 12
|
jca |
|- ( K e. Dirset -> ( K e. Proset /\ A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y ) ) |
14 |
|
simpl |
|- ( ( K e. Proset /\ A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y ) -> K e. Proset ) |
15 |
|
0elpw |
|- (/) e. ~P B |
16 |
|
0fin |
|- (/) e. Fin |
17 |
15 16
|
elini |
|- (/) e. ( ~P B i^i Fin ) |
18 |
|
raleq |
|- ( x = (/) -> ( A. z e. x z .<_ y <-> A. z e. (/) z .<_ y ) ) |
19 |
18
|
rexbidv |
|- ( x = (/) -> ( E. y e. B A. z e. x z .<_ y <-> E. y e. B A. z e. (/) z .<_ y ) ) |
20 |
19
|
rspcv |
|- ( (/) e. ( ~P B i^i Fin ) -> ( A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y -> E. y e. B A. z e. (/) z .<_ y ) ) |
21 |
17 20
|
ax-mp |
|- ( A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y -> E. y e. B A. z e. (/) z .<_ y ) |
22 |
|
rexn0 |
|- ( E. y e. B A. z e. (/) z .<_ y -> B =/= (/) ) |
23 |
21 22
|
syl |
|- ( A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y -> B =/= (/) ) |
24 |
23
|
adantl |
|- ( ( K e. Proset /\ A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y ) -> B =/= (/) ) |
25 |
|
raleq |
|- ( x = { a , b } -> ( A. z e. x z .<_ y <-> A. z e. { a , b } z .<_ y ) ) |
26 |
25
|
rexbidv |
|- ( x = { a , b } -> ( E. y e. B A. z e. x z .<_ y <-> E. y e. B A. z e. { a , b } z .<_ y ) ) |
27 |
|
simplr |
|- ( ( ( K e. Proset /\ A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y ) /\ ( a e. B /\ b e. B ) ) -> A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y ) |
28 |
|
prelpwi |
|- ( ( a e. B /\ b e. B ) -> { a , b } e. ~P B ) |
29 |
|
prfi |
|- { a , b } e. Fin |
30 |
29
|
a1i |
|- ( ( a e. B /\ b e. B ) -> { a , b } e. Fin ) |
31 |
28 30
|
elind |
|- ( ( a e. B /\ b e. B ) -> { a , b } e. ( ~P B i^i Fin ) ) |
32 |
31
|
adantl |
|- ( ( ( K e. Proset /\ A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y ) /\ ( a e. B /\ b e. B ) ) -> { a , b } e. ( ~P B i^i Fin ) ) |
33 |
26 27 32
|
rspcdva |
|- ( ( ( K e. Proset /\ A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y ) /\ ( a e. B /\ b e. B ) ) -> E. y e. B A. z e. { a , b } z .<_ y ) |
34 |
|
vex |
|- a e. _V |
35 |
|
vex |
|- b e. _V |
36 |
|
breq1 |
|- ( z = a -> ( z .<_ y <-> a .<_ y ) ) |
37 |
|
breq1 |
|- ( z = b -> ( z .<_ y <-> b .<_ y ) ) |
38 |
34 35 36 37
|
ralpr |
|- ( A. z e. { a , b } z .<_ y <-> ( a .<_ y /\ b .<_ y ) ) |
39 |
38
|
rexbii |
|- ( E. y e. B A. z e. { a , b } z .<_ y <-> E. y e. B ( a .<_ y /\ b .<_ y ) ) |
40 |
33 39
|
sylib |
|- ( ( ( K e. Proset /\ A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y ) /\ ( a e. B /\ b e. B ) ) -> E. y e. B ( a .<_ y /\ b .<_ y ) ) |
41 |
40
|
ralrimivva |
|- ( ( K e. Proset /\ A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y ) -> A. a e. B A. b e. B E. y e. B ( a .<_ y /\ b .<_ y ) ) |
42 |
1 2
|
isdrs |
|- ( K e. Dirset <-> ( K e. Proset /\ B =/= (/) /\ A. a e. B A. b e. B E. y e. B ( a .<_ y /\ b .<_ y ) ) ) |
43 |
14 24 41 42
|
syl3anbrc |
|- ( ( K e. Proset /\ A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y ) -> K e. Dirset ) |
44 |
13 43
|
impbii |
|- ( K e. Dirset <-> ( K e. Proset /\ A. x e. ( ~P B i^i Fin ) E. y e. B A. z e. x z .<_ y ) ) |