Theorem supnub

Description: An upper bound is not less than the supremum. (Contributed by NM, 13-Oct-2004)

	Ref	Expression
Hypotheses	supmo.1	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
	supcl.2	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) )
Assertion	supnub	⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐵 ¬ 𝐶 𝑅 𝑧 ) → ¬ 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		supmo.1	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
2		supcl.2	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) )
3	1 2	suplub	⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐴 ∧ 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) → ∃ 𝑧 ∈ 𝐵 𝐶 𝑅 𝑧 ) )
4	3	expdimp	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝐶 𝑅 𝑧 ) )
5		dfrex2	⊢ ( ∃ 𝑧 ∈ 𝐵 𝐶 𝑅 𝑧 ↔ ¬ ∀ 𝑧 ∈ 𝐵 ¬ 𝐶 𝑅 𝑧 )
6	4 5	imbitrdi	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ¬ ∀ 𝑧 ∈ 𝐵 ¬ 𝐶 𝑅 𝑧 ) )
7	6	con2d	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( ∀ 𝑧 ∈ 𝐵 ¬ 𝐶 𝑅 𝑧 → ¬ 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
8	7	expimpd	⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐵 ¬ 𝐶 𝑅 𝑧 ) → ¬ 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )