Theorem sup0riota

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

	Ref	Expression
Assertion	sup0riota	⊢ ( 𝑅 Or 𝐴 → sup ( ∅ , 𝐴 , 𝑅 ) = ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝑅 Or 𝐴 → 𝑅 Or 𝐴 )
2	1	supval2	⊢ ( 𝑅 Or 𝐴 → sup ( ∅ , 𝐴 , 𝑅 ) = ( ℩ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ ∅ ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ ∅ 𝑦 𝑅 𝑧 ) ) ) )
3		ral0	⊢ ∀ 𝑦 ∈ ∅ ¬ 𝑥 𝑅 𝑦
4	3	biantrur	⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ ∅ 𝑦 𝑅 𝑧 ) ↔ ( ∀ 𝑦 ∈ ∅ ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ ∅ 𝑦 𝑅 𝑧 ) ) )
5		rex0	⊢ ¬ ∃ 𝑧 ∈ ∅ 𝑦 𝑅 𝑧
6		imnot	⊢ ( ¬ ∃ 𝑧 ∈ ∅ 𝑦 𝑅 𝑧 → ( ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ ∅ 𝑦 𝑅 𝑧 ) ↔ ¬ 𝑦 𝑅 𝑥 ) )
7	5 6	ax-mp	⊢ ( ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ ∅ 𝑦 𝑅 𝑧 ) ↔ ¬ 𝑦 𝑅 𝑥 )
8	7	ralbii	⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ ∅ 𝑦 𝑅 𝑧 ) ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 )
9	4 8	bitr3i	⊢ ( ( ∀ 𝑦 ∈ ∅ ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ ∅ 𝑦 𝑅 𝑧 ) ) ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 )
10	9	a1i	⊢ ( 𝑅 Or 𝐴 → ( ( ∀ 𝑦 ∈ ∅ ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ ∅ 𝑦 𝑅 𝑧 ) ) ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ) )
11	10	riotabidv	⊢ ( 𝑅 Or 𝐴 → ( ℩ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ ∅ ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ ∅ 𝑦 𝑅 𝑧 ) ) ) = ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ) )
12	2 11	eqtrd	⊢ ( 𝑅 Or 𝐴 → sup ( ∅ , 𝐴 , 𝑅 ) = ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ) )