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

Metamath Proof Explorer

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 ( ∅ , 𝐴 , 𝑅 ) = 𝑋 )