Theorem nffr

Description: Bound-variable hypothesis builder for well-founded relations. (Contributed by Stefan O'Rear, 20-Jan-2015) (Revised by Mario Carneiro, 14-Oct-2016)

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

Proof

Step	Hyp	Ref	Expression
1		nffr.r	$$⊢\underset{\_}{Ⅎ}xR$$
2		nffr.a	$$⊢\underset{\_}{Ⅎ}xA$$
3		df-fr	$$⊢R\mathrm{Fr}A\leftrightarrow \forall a\left(\left(a\subseteq A\wedge a\ne \varnothing \right)\to \exists b\in a\forall c\in a\neg cRb\right)$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}xa$$
5	4 2	nfss	$$⊢Ⅎxa\subseteq A$$
6		nfv	$$⊢Ⅎxa\ne \varnothing$$
7	5 6	nfan	$$⊢Ⅎx\left(a\subseteq A\wedge a\ne \varnothing \right)$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}xc$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}xb$$
10	8 1 9	nfbr	$$⊢ℲxcRb$$
11	10	nfn	$$⊢Ⅎx\neg cRb$$
12	4 11	nfralw	$$⊢Ⅎx\forall c\in a\neg cRb$$
13	4 12	nfrex	$$⊢Ⅎx\exists b\in a\forall c\in a\neg cRb$$
14	7 13	nfim	$$⊢Ⅎx\left(\left(a\subseteq A\wedge a\ne \varnothing \right)\to \exists b\in a\forall c\in a\neg cRb\right)$$
15	14	nfal	$$⊢Ⅎx\forall a\left(\left(a\subseteq A\wedge a\ne \varnothing \right)\to \exists b\in a\forall c\in a\neg cRb\right)$$
16	3 15	nfxfr	$$⊢ℲxR\mathrm{Fr}A$$