This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem infsn

Description: The infimum of a singleton. (Contributed by NM, 2-Oct-2007)

Ref Expression
Assertion infsn 
|- ( ( R Or A /\ B e. A ) -> inf ( { B } , A , R ) = B )

Proof

Step Hyp Ref Expression
1 dfsn2 
 |-  { B } = { B , B }
2 1 infeq1i 
 |-  inf ( { B } , A , R ) = inf ( { B , B } , A , R )
3 infpr 
 |-  ( ( R Or A /\ B e. A /\ B e. A ) -> inf ( { B , B } , A , R ) = if ( B R B , B , B ) )
4 3 3anidm23 
 |-  ( ( R Or A /\ B e. A ) -> inf ( { B , B } , A , R ) = if ( B R B , B , B ) )
5 2 4 eqtrid 
 |-  ( ( R Or A /\ B e. A ) -> inf ( { B } , A , R ) = if ( B R B , B , B ) )
6 ifid 
 |-  if ( B R B , B , B ) = B
7 5 6 eqtrdi 
 |-  ( ( R Or A /\ B e. A ) -> inf ( { B } , A , R ) = B )