Description: An infimum belongs to its base class (closure law). See also inflb and infglb . (Contributed by AV, 3-Sep-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | infcl.1 | |- ( ph -> R Or A ) |
|
infcl.2 | |- ( ph -> E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) ) |
||
Assertion | infcl | |- ( ph -> inf ( B , A , R ) e. A ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | infcl.1 | |- ( ph -> R Or A ) |
|
2 | infcl.2 | |- ( ph -> E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) ) |
|
3 | df-inf | |- inf ( B , A , R ) = sup ( B , A , `' R ) |
|
4 | cnvso | |- ( R Or A <-> `' R Or A ) |
|
5 | 1 4 | sylib | |- ( ph -> `' R Or A ) |
6 | 1 2 | infcllem | |- ( ph -> E. x e. A ( A. y e. B -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) ) |
7 | 5 6 | supcl | |- ( ph -> sup ( B , A , `' R ) e. A ) |
8 | 3 7 | eqeltrid | |- ( ph -> inf ( B , A , R ) e. A ) |