supnub

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

	Ref	Expression
Hypotheses	supmo.1	$⊢ φ \to R Or A$
	supcl.2	$⊢ φ \to \exists x \in A (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z))$
Assertion	supnub	$⊢ φ \to ((C \in A \land \forall z \in B \neg C R z) \to \neg C R sup (B, A, R))$

Step	Hyp	Ref	Expression
1		supmo.1	$⊢ φ \to R Or A$
2		supcl.2	$⊢ φ \to \exists x \in A (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z))$
3	1 2	suplub	$⊢ φ \to ((C \in A \land C R sup (B, A, R)) \to \exists z \in B C R z)$
4	3	expdimp	$⊢ (φ \land C \in A) \to (C R sup (B, A, R) \to \exists z \in B C R z)$
5		dfrex2	$⊢ \exists z \in B C R z \leftrightarrow \neg \forall z \in B \neg C R z$
6	4 5	imbitrdi	$⊢ (φ \land C \in A) \to (C R sup (B, A, R) \to \neg \forall z \in B \neg C R z)$
7	6	con2d	$⊢ (φ \land C \in A) \to (\forall z \in B \neg C R z \to \neg C R sup (B, A, R))$
8	7	expimpd	$⊢ φ \to ((C \in A \land \forall z \in B \neg C R z) \to \neg C R sup (B, A, R))$

Metamath Proof Explorer