Theorem safesnsupfiub

Description: If B is a finite subset of ordered class A , we can safely create a small subset with the same largest element and upper bound, if any. (Contributed by RP, 1-Sep-2024)

	Ref	Expression
Hypotheses	safesnsupfiub.small	$$⊢\phi \to \left(O=\varnothing \vee O=1_{𝑜}\right)$$
	safesnsupfiub.finite	$$⊢\phi \to B\in \mathrm{Fin}$$
	safesnsupfiub.subset	$$⊢\phi \to B\subseteq A$$
	safesnsupfiub.ordered	$$⊢\phi \to R\mathrm{Or}A$$
	safesnsupfiub.ub	$$⊢\phi \to \forall x\in B\forall y\in CxRy$$
Assertion	safesnsupfiub	$$⊢\phi \to \forall x\in if\left(O\prec B,\left\{sup\left(B,A,R\right)\right\},B\right)\forall y\in CxRy$$

Proof

Step	Hyp	Ref	Expression
1		safesnsupfiub.small	$$⊢\phi \to \left(O=\varnothing \vee O=1_{𝑜}\right)$$
2		safesnsupfiub.finite	$$⊢\phi \to B\in \mathrm{Fin}$$
3		safesnsupfiub.subset	$$⊢\phi \to B\subseteq A$$
4		safesnsupfiub.ordered	$$⊢\phi \to R\mathrm{Or}A$$
5		safesnsupfiub.ub	$$⊢\phi \to \forall x\in B\forall y\in CxRy$$
6	1 2 3 4	safesnsupfiss	$$⊢\phi \to if\left(O\prec B,\left\{sup\left(B,A,R\right)\right\},B\right)\subseteq B$$
7	6	sseld	$$⊢\phi \to \left(x\in if\left(O\prec B,\left\{sup\left(B,A,R\right)\right\},B\right)\to x\in B\right)$$
8	7	imim1d	$$⊢\phi \to \left(\left(x\in B\to \forall y\in CxRy\right)\to \left(x\in if\left(O\prec B,\left\{sup\left(B,A,R\right)\right\},B\right)\to \forall y\in CxRy\right)\right)$$
9	8	ralimdv2	$$⊢\phi \to \left(\forall x\in B\forall y\in CxRy\to \forall x\in if\left(O\prec B,\left\{sup\left(B,A,R\right)\right\},B\right)\forall y\in CxRy\right)$$
10	5 9	mpd	$$⊢\phi \to \forall x\in if\left(O\prec B,\left\{sup\left(B,A,R\right)\right\},B\right)\forall y\in CxRy$$