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

Proof

Step Hyp Ref Expression
1 nfiso.1 ⊢ Ⅎ _ x H
2 nfiso.2 ⊢ Ⅎ _ x R
3 nfiso.3 ⊢ Ⅎ _ x S
4 nfiso.4 ⊢ Ⅎ _ x A
5 nfiso.5 ⊢ Ⅎ _ x B
6 df-isom ⊢ H Isom R , S A B ↔ H : A ⟶ 1-1 onto B ∧ ∀ y ∈ A ∀ z ∈ A y R z ↔ H ⁡ y S H ⁡ z
7 1 4 5 nff1o ⊢ Ⅎ x H : A ⟶ 1-1 onto B
8 nfcv ⊢ Ⅎ _ x y
9 nfcv ⊢ Ⅎ _ x z
10 8 2 9 nfbr ⊢ Ⅎ x y R z
11 1 8 nffv ⊢ Ⅎ _ x H ⁡ y
12 1 9 nffv ⊢ Ⅎ _ x H ⁡ z
13 11 3 12 nfbr ⊢ Ⅎ x H ⁡ y S H ⁡ z
14 10 13 nfbi ⊢ Ⅎ x y R z ↔ H ⁡ y S H ⁡ z
15 4 14 nfralw ⊢ Ⅎ x ∀ z ∈ A y R z ↔ H ⁡ y S H ⁡ z
16 4 15 nfralw ⊢ Ⅎ x ∀ y ∈ A ∀ z ∈ A y R z ↔ H ⁡ y S H ⁡ z
17 7 16 nfan ⊢ Ⅎ x H : A ⟶ 1-1 onto B ∧ ∀ y ∈ A ∀ z ∈ A y R z ↔ H ⁡ y S H ⁡ z
18 6 17 nfxfr ⊢ Ⅎ x H Isom R , S A B