Theorem nfiso

Description: Bound-variable hypothesis builder for an isomorphism. (Contributed by NM, 17-May-2004) (Proof shortened by Andrew Salmon, 22-Oct-2011)

	Ref	Expression
Hypotheses	nfiso.1	$$⊢\underset{\_}{Ⅎ}xH$$
	nfiso.2	$$⊢\underset{\_}{Ⅎ}xR$$
	nfiso.3	$$⊢\underset{\_}{Ⅎ}xS$$
	nfiso.4	$$⊢\underset{\_}{Ⅎ}xA$$
	nfiso.5	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	nfiso	$$⊢ℲxH{Isom}_{R,S}\left(A,B\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfiso.1	$$⊢\underset{\_}{Ⅎ}xH$$
2		nfiso.2	$$⊢\underset{\_}{Ⅎ}xR$$
3		nfiso.3	$$⊢\underset{\_}{Ⅎ}xS$$
4		nfiso.4	$$⊢\underset{\_}{Ⅎ}xA$$
5		nfiso.5	$$⊢\underset{\_}{Ⅎ}xB$$
6		df-isom	$$⊢H{Isom}_{R,S}\left(A,B\right)\leftrightarrow \left(H:A\underset{1-1\; onto}{⟶}B\wedge \forall y\in A\forall z\in A\left(yRz\leftrightarrow H\left(y\right)SH\left(z\right)\right)\right)$$
7	1 4 5	nff1o	$$⊢ℲxH:A\underset{1-1\; onto}{⟶}B$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}xz$$
10	8 2 9	nfbr	$$⊢ℲxyRz$$
11	1 8	nffv	$$⊢\underset{\_}{Ⅎ}xH\left(y\right)$$
12	1 9	nffv	$$⊢\underset{\_}{Ⅎ}xH\left(z\right)$$
13	11 3 12	nfbr	$$⊢ℲxH\left(y\right)SH\left(z\right)$$
14	10 13	nfbi	$$⊢Ⅎx\left(yRz\leftrightarrow H\left(y\right)SH\left(z\right)\right)$$
15	4 14	nfralw	$$⊢Ⅎx\forall z\in A\left(yRz\leftrightarrow H\left(y\right)SH\left(z\right)\right)$$
16	4 15	nfralw	$$⊢Ⅎx\forall y\in A\forall z\in A\left(yRz\leftrightarrow H\left(y\right)SH\left(z\right)\right)$$
17	7 16	nfan	$$⊢Ⅎx\left(H:A\underset{1-1\; onto}{⟶}B\wedge \forall y\in A\forall z\in A\left(yRz\leftrightarrow H\left(y\right)SH\left(z\right)\right)\right)$$
18	6 17	nfxfr	$$⊢ℲxH{Isom}_{R,S}\left(A,B\right)$$