Theorem infsn

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

	Ref	Expression
Assertion	infsn	$$⊢\left(R\mathrm{Or}A\wedge B\in A\right)\to inf\left(\left\{B\right\},A,R\right)=B$$

Proof

Step	Hyp	Ref	Expression
1		dfsn2	$$⊢\left\{B\right\}=\left\{B,B\right\}$$
2	1	infeq1i	$$⊢inf\left(\left\{B\right\},A,R\right)=inf\left(\left\{B,B\right\},A,R\right)$$
3		infpr	$$⊢\left(R\mathrm{Or}A\wedge B\in A\wedge B\in A\right)\to inf\left(\left\{B,B\right\},A,R\right)=if\left(BRB,B,B\right)$$
4	3	3anidm23	$$⊢\left(R\mathrm{Or}A\wedge B\in A\right)\to inf\left(\left\{B,B\right\},A,R\right)=if\left(BRB,B,B\right)$$
5	2 4	eqtrid	$$⊢\left(R\mathrm{Or}A\wedge B\in A\right)\to inf\left(\left\{B\right\},A,R\right)=if\left(BRB,B,B\right)$$
6		ifid	$$⊢if\left(BRB,B,B\right)=B$$
7	5 6	eqtrdi	$$⊢\left(R\mathrm{Or}A\wedge B\in A\right)\to inf\left(\left\{B\right\},A,R\right)=B$$