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 )