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

Metamath Proof Explorer

Theorem infempty

Description: The infimum of an empty set under a base set which has a unique greatest element is the greatest element of the base set. (Contributed by AV, 4-Sep-2020)

		Ref	Expression
	Assertion	infempty	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑋 𝑅 𝑦 ) ∧ ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ) → inf ( ∅ , 𝐴 , 𝑅 ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		df-inf	⊢ inf ( ∅ , 𝐴 , 𝑅 ) = sup ( ∅ , 𝐴 , ^◡ 𝑅 )
2		cnvso	⊢ ( 𝑅 Or 𝐴 ↔ ^◡ 𝑅 Or 𝐴 )
3		brcnvg	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑦 ^◡ 𝑅 𝑋 ↔ 𝑋 𝑅 𝑦 ) )
4	3	ancoms	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ^◡ 𝑅 𝑋 ↔ 𝑋 𝑅 𝑦 ) )
5	4	bicomd	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑋 𝑅 𝑦 ↔ 𝑦 ^◡ 𝑅 𝑋 ) )
6	5	notbid	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ¬ 𝑋 𝑅 𝑦 ↔ ¬ 𝑦 ^◡ 𝑅 𝑋 ) )
7	6	ralbidva	⊢ ( 𝑋 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑋 𝑅 𝑦 ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 ^◡ 𝑅 𝑋 ) )
8	7	pm5.32i	⊢ ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑋 𝑅 𝑦 ) ↔ ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 ^◡ 𝑅 𝑋 ) )
9		brcnvg	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ^◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 ) )
10	9	ancoms	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ^◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 ) )
11	10	bicomd	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑦 ↔ 𝑦 ^◡ 𝑅 𝑥 ) )
12	11	notbid	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ¬ 𝑥 𝑅 𝑦 ↔ ¬ 𝑦 ^◡ 𝑅 𝑥 ) )
13	12	ralbidva	⊢ ( 𝑥 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 ^◡ 𝑅 𝑥 ) )
14	13	reubiia	⊢ ( ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ↔ ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 ^◡ 𝑅 𝑥 )
15		sup0	⊢ ( ( ^◡ 𝑅 Or 𝐴 ∧ ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 ^◡ 𝑅 𝑋 ) ∧ ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 ^◡ 𝑅 𝑥 ) → sup ( ∅ , 𝐴 , ^◡ 𝑅 ) = 𝑋 )
16	2 8 14 15	syl3anb	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑋 𝑅 𝑦 ) ∧ ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ) → sup ( ∅ , 𝐴 , ^◡ 𝑅 ) = 𝑋 )
17	1 16	eqtrid	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑋 𝑅 𝑦 ) ∧ ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ) → inf ( ∅ , 𝐴 , 𝑅 ) = 𝑋 )