infssd

Description: Inequality deduction for infimum of a subset. (Contributed by AV, 4-Oct-2020)

	Ref	Expression
Hypotheses	infssd.0	$⊢ φ \to R Or A$
	infssd.1	$⊢ φ \to C \subseteq B$
	infssd.3	$⊢ φ \to \exists x \in A (\forall y \in C \neg y R x \land \forall y \in A (x R y \to \exists z \in C z R y))$
	infssd.4	$⊢ φ \to \exists x \in A (\forall y \in B \neg y R x \land \forall y \in A (x R y \to \exists z \in B z R y))$
Assertion	infssd	$⊢ φ \to \neg inf (C, A, R) R inf (B, A, R)$

Step	Hyp	Ref	Expression
1		infssd.0	$⊢ φ \to R Or A$
2		infssd.1	$⊢ φ \to C \subseteq B$
3		infssd.3	$⊢ φ \to \exists x \in A (\forall y \in C \neg y R x \land \forall y \in A (x R y \to \exists z \in C z R y))$
4		infssd.4	$⊢ φ \to \exists x \in A (\forall y \in B \neg y R x \land \forall y \in A (x R y \to \exists z \in B z R y))$
5	1 4	infcl	$⊢ φ \to inf (B, A, R) \in A$
6	2	sseld	$⊢ φ \to (z \in C \to z \in B)$
7	1 4	inflb	$⊢ φ \to (z \in B \to \neg z R inf (B, A, R))$
8	6 7	syld	$⊢ φ \to (z \in C \to \neg z R inf (B, A, R))$
9	8	ralrimiv	$⊢ φ \to \forall z \in C \neg z R inf (B, A, R)$
10	1 3	infnlb	$⊢ φ \to ((inf (B, A, R) \in A \land \forall z \in C \neg z R inf (B, A, R)) \to \neg inf (C, A, R) R inf (B, A, R))$
11	5 9 10	mp2and	$⊢ φ \to \neg inf (C, A, R) R inf (B, A, R)$

Metamath Proof Explorer