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

Metamath Proof Explorer

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 ( ∅ , 𝐴 , 𝑅 ) = ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ) )