Theorem nfpo

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

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

Proof

Step	Hyp	Ref	Expression
1		nfpo.r	$$⊢\underset{\_}{Ⅎ}xR$$
2		nfpo.a	$$⊢\underset{\_}{Ⅎ}xA$$
3		df-po	$$⊢R\mathrm{Po}A\leftrightarrow \forall a\in A\forall b\in A\forall c\in A\left(\neg aRa\wedge \left(\left(aRb\wedge bRc\right)\to aRc\right)\right)$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}xa$$
5	4 1 4	nfbr	$$⊢ℲxaRa$$
6	5	nfn	$$⊢Ⅎx\neg aRa$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}xb$$
8	4 1 7	nfbr	$$⊢ℲxaRb$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}xc$$
10	7 1 9	nfbr	$$⊢ℲxbRc$$
11	8 10	nfan	$$⊢Ⅎx\left(aRb\wedge bRc\right)$$
12	4 1 9	nfbr	$$⊢ℲxaRc$$
13	11 12	nfim	$$⊢Ⅎx\left(\left(aRb\wedge bRc\right)\to aRc\right)$$
14	6 13	nfan	$$⊢Ⅎx\left(\neg aRa\wedge \left(\left(aRb\wedge bRc\right)\to aRc\right)\right)$$
15	2 14	nfralw	$$⊢Ⅎx\forall c\in A\left(\neg aRa\wedge \left(\left(aRb\wedge bRc\right)\to aRc\right)\right)$$
16	2 15	nfralw	$$⊢Ⅎx\forall b\in A\forall c\in A\left(\neg aRa\wedge \left(\left(aRb\wedge bRc\right)\to aRc\right)\right)$$
17	2 16	nfralw	$$⊢Ⅎx\forall a\in A\forall b\in A\forall c\in A\left(\neg aRa\wedge \left(\left(aRb\wedge bRc\right)\to aRc\right)\right)$$
18	3 17	nfxfr	$$⊢ℲxR\mathrm{Po}A$$