Theorem infsn

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

	Ref	Expression
Assertion	infsn	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ) → inf ( { 𝐵 } , 𝐴 , 𝑅 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		dfsn2	⊢ { 𝐵 } = { 𝐵 , 𝐵 }
2	1	infeq1i	⊢ inf ( { 𝐵 } , 𝐴 , 𝑅 ) = inf ( { 𝐵 , 𝐵 } , 𝐴 , 𝑅 )
3		infpr	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴 ) → inf ( { 𝐵 , 𝐵 } , 𝐴 , 𝑅 ) = if ( 𝐵 𝑅 𝐵 , 𝐵 , 𝐵 ) )
4	3	3anidm23	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ) → inf ( { 𝐵 , 𝐵 } , 𝐴 , 𝑅 ) = if ( 𝐵 𝑅 𝐵 , 𝐵 , 𝐵 ) )
5	2 4	syl5eq	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ) → inf ( { 𝐵 } , 𝐴 , 𝑅 ) = if ( 𝐵 𝑅 𝐵 , 𝐵 , 𝐵 ) )
6		ifid	⊢ if ( 𝐵 𝑅 𝐵 , 𝐵 , 𝐵 ) = 𝐵
7	5 6	eqtrdi	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ) → inf ( { 𝐵 } , 𝐴 , 𝑅 ) = 𝐵 )