Metamath Proof Explorer


Theorem infexd

Description: An infimum is a set. (Contributed by AV, 2-Sep-2020)

Ref Expression
Hypothesis infexd.1
|- ( ph -> R Or A )
Assertion infexd
|- ( ph -> inf ( B , A , R ) e. _V )

Proof

Step Hyp Ref Expression
1 infexd.1
 |-  ( ph -> R Or A )
2 df-inf
 |-  inf ( B , A , R ) = sup ( B , A , `' R )
3 cnvso
 |-  ( R Or A <-> `' R Or A )
4 1 3 sylib
 |-  ( ph -> `' R Or A )
5 4 supexd
 |-  ( ph -> sup ( B , A , `' R ) e. _V )
6 2 5 eqeltrid
 |-  ( ph -> inf ( B , A , R ) e. _V )