Theorem eqsupd

Description: Sufficient condition for an element to be equal to the supremum. (Contributed by Mario Carneiro, 21-Apr-2015)

	Ref	Expression
Hypotheses	supmo.1	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
	eqsupd.2	⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
	eqsupd.3	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ¬ 𝐶 𝑅 𝑦 )
	eqsupd.4	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝐶 ) ) → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 )
Assertion	eqsupd	⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , 𝑅 ) = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		supmo.1	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
2		eqsupd.2	⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
3		eqsupd.3	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ¬ 𝐶 𝑅 𝑦 )
4		eqsupd.4	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝐶 ) ) → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 )
5	3	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 𝑅 𝑦 )
6	4	expr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) )
7	6	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) )
8	1	eqsup	⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) → sup ( 𝐵 , 𝐴 , 𝑅 ) = 𝐶 ) )
9	2 5 7 8	mp3and	⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , 𝑅 ) = 𝐶 )