Theorem sup0

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

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

Proof

Step	Hyp	Ref	Expression
1		sup0riota	⊢ ( 𝑅 Or 𝐴 → sup ( ∅ , 𝐴 , 𝑅 ) = ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ) )
2	1	3ad2ant1	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑋 ) ∧ ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ) → sup ( ∅ , 𝐴 , 𝑅 ) = ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ) )
3		simp2r	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑋 ) ∧ ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ) → ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑋 )
4		simpl	⊢ ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑋 ) → 𝑋 ∈ 𝐴 )
5	4	anim1i	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑋 ) ∧ ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ) → ( 𝑋 ∈ 𝐴 ∧ ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ) )
6	5	3adant1	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑋 ) ∧ ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ) → ( 𝑋 ∈ 𝐴 ∧ ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ) )
7		breq2	⊢ ( 𝑥 = 𝑋 → ( 𝑦 𝑅 𝑥 ↔ 𝑦 𝑅 𝑋 ) )
8	7	notbid	⊢ ( 𝑥 = 𝑋 → ( ¬ 𝑦 𝑅 𝑥 ↔ ¬ 𝑦 𝑅 𝑋 ) )
9	8	ralbidv	⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑋 ) )
10	9	riota2	⊢ ( ( 𝑋 ∈ 𝐴 ∧ ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ) → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑋 ↔ ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ) = 𝑋 ) )
11	6 10	syl	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑋 ) ∧ ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ) → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑋 ↔ ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ) = 𝑋 ) )
12	3 11	mpbid	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑋 ) ∧ ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ) → ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ) = 𝑋 )
13	2 12	eqtrd	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑋 ) ∧ ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ) → sup ( ∅ , 𝐴 , 𝑅 ) = 𝑋 )