Theorem nfso

Description: Bound-variable hypothesis builder for total orders. (Contributed by Stefan O'Rear, 20-Jan-2015)

	Ref	Expression
Hypotheses	nfpo.r	$$⊢\underset{\_}{Ⅎ}xR$$
	nfpo.a	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	nfso	$$⊢ℲxR\mathrm{Or}A$$

Proof

Step	Hyp	Ref	Expression
1		nfpo.r	$$⊢\underset{\_}{Ⅎ}xR$$
2		nfpo.a	$$⊢\underset{\_}{Ⅎ}xA$$
3		df-so	$$⊢R\mathrm{Or}A\leftrightarrow \left(R\mathrm{Po}A\wedge \forall a\in A\forall b\in A\left(aRb\vee a=b\vee bRa\right)\right)$$
4	1 2	nfpo	$$⊢ℲxR\mathrm{Po}A$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}xa$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}xb$$
7	5 1 6	nfbr	$$⊢ℲxaRb$$
8		nfv	$$⊢Ⅎxa=b$$
9	6 1 5	nfbr	$$⊢ℲxbRa$$
10	7 8 9	nf3or	$$⊢Ⅎx\left(aRb\vee a=b\vee bRa\right)$$
11	2 10	nfralw	$$⊢Ⅎx\forall b\in A\left(aRb\vee a=b\vee bRa\right)$$
12	2 11	nfralw	$$⊢Ⅎx\forall a\in A\forall b\in A\left(aRb\vee a=b\vee bRa\right)$$
13	4 12	nfan	$$⊢Ⅎx\left(R\mathrm{Po}A\wedge \forall a\in A\forall b\in A\left(aRb\vee a=b\vee bRa\right)\right)$$
14	3 13	nfxfr	$$⊢ℲxR\mathrm{Or}A$$