This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑅 , 𝑆 ( 𝐴 , 𝐵 )