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	⊢ Ⅎ 𝑥 𝐻
	nfiso.2	⊢ Ⅎ 𝑥 𝑅
	nfiso.3	⊢ Ⅎ 𝑥 𝑆
	nfiso.4	⊢ Ⅎ 𝑥 𝐴
	nfiso.5	⊢ Ⅎ 𝑥 𝐵
Assertion	nfiso	⊢ Ⅎ 𝑥 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		nfiso.1	⊢ Ⅎ 𝑥 𝐻
2		nfiso.2	⊢ Ⅎ 𝑥 𝑅
3		nfiso.3	⊢ Ⅎ 𝑥 𝑆
4		nfiso.4	⊢ Ⅎ 𝑥 𝐴
5		nfiso.5	⊢ Ⅎ 𝑥 𝐵
6		df-isom	⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑦 𝑅 𝑧 ↔ ( 𝐻 ‘ 𝑦 ) 𝑆 ( 𝐻 ‘ 𝑧 ) ) ) )
7	1 4 5	nff1o	⊢ Ⅎ 𝑥 𝐻 : 𝐴 –1-1-onto→ 𝐵
8		nfcv	⊢ Ⅎ 𝑥 𝑦
9		nfcv	⊢ Ⅎ 𝑥 𝑧
10	8 2 9	nfbr	⊢ Ⅎ 𝑥 𝑦 𝑅 𝑧
11	1 8	nffv	⊢ Ⅎ 𝑥 ( 𝐻 ‘ 𝑦 )
12	1 9	nffv	⊢ Ⅎ 𝑥 ( 𝐻 ‘ 𝑧 )
13	11 3 12	nfbr	⊢ Ⅎ 𝑥 ( 𝐻 ‘ 𝑦 ) 𝑆 ( 𝐻 ‘ 𝑧 )
14	10 13	nfbi	⊢ Ⅎ 𝑥 ( 𝑦 𝑅 𝑧 ↔ ( 𝐻 ‘ 𝑦 ) 𝑆 ( 𝐻 ‘ 𝑧 ) )
15	4 14	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑧 ∈ 𝐴 ( 𝑦 𝑅 𝑧 ↔ ( 𝐻 ‘ 𝑦 ) 𝑆 ( 𝐻 ‘ 𝑧 ) )
16	4 15	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑦 𝑅 𝑧 ↔ ( 𝐻 ‘ 𝑦 ) 𝑆 ( 𝐻 ‘ 𝑧 ) )
17	7 16	nfan	⊢ Ⅎ 𝑥 ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑦 𝑅 𝑧 ↔ ( 𝐻 ‘ 𝑦 ) 𝑆 ( 𝐻 ‘ 𝑧 ) ) )
18	6 17	nfxfr	⊢ Ⅎ 𝑥 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 )