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 
|- F/_ x H
nfiso.2 
|- F/_ x R
nfiso.3 
|- F/_ x S
nfiso.4 
|- F/_ x A
nfiso.5 
|- F/_ x B
Assertion nfiso 
|- F/ x H Isom R , S ( A , B )

Proof

Step Hyp Ref Expression
1 nfiso.1 
 |-  F/_ x H
2 nfiso.2 
 |-  F/_ x R
3 nfiso.3 
 |-  F/_ x S
4 nfiso.4 
 |-  F/_ x A
5 nfiso.5 
 |-  F/_ x B
6 df-isom 
 |-  ( H Isom R , S ( A , B ) <-> ( H : A -1-1-onto-> B /\ A. y e. A A. z e. A ( y R z <-> ( H ` y ) S ( H ` z ) ) ) )
7 1 4 5 nff1o 
 |-  F/ x H : A -1-1-onto-> B
8 nfcv 
 |-  F/_ x y
9 nfcv 
 |-  F/_ x z
10 8 2 9 nfbr 
 |-  F/ x y R z
11 1 8 nffv 
 |-  F/_ x ( H ` y )
12 1 9 nffv 
 |-  F/_ x ( H ` z )
13 11 3 12 nfbr 
 |-  F/ x ( H ` y ) S ( H ` z )
14 10 13 nfbi 
 |-  F/ x ( y R z <-> ( H ` y ) S ( H ` z ) )
15 4 14 nfralw 
 |-  F/ x A. z e. A ( y R z <-> ( H ` y ) S ( H ` z ) )
16 4 15 nfralw 
 |-  F/ x A. y e. A A. z e. A ( y R z <-> ( H ` y ) S ( H ` z ) )
17 7 16 nfan 
 |-  F/ x ( H : A -1-1-onto-> B /\ A. y e. A A. z e. A ( y R z <-> ( H ` y ) S ( H ` z ) ) )
18 6 17 nfxfr 
 |-  F/ x H Isom R , S ( A , B )