Step |
Hyp |
Ref |
Expression |
1 |
|
fvex |
⊢ ( 𝐻 ‘ 𝑥 ) ∈ V |
2 |
|
fvex |
⊢ ( 𝐻 ‘ 𝑦 ) ∈ V |
3 |
1 2
|
opelvv |
⊢ 〈 ( 𝐻 ‘ 𝑥 ) , ( 𝐻 ‘ 𝑦 ) 〉 ∈ ( V × V ) |
4 |
|
df-br |
⊢ ( ( 𝐻 ‘ 𝑥 ) ( V × V ) ( 𝐻 ‘ 𝑦 ) ↔ 〈 ( 𝐻 ‘ 𝑥 ) , ( 𝐻 ‘ 𝑦 ) 〉 ∈ ( V × V ) ) |
5 |
3 4
|
mpbir |
⊢ ( 𝐻 ‘ 𝑥 ) ( V × V ) ( 𝐻 ‘ 𝑦 ) |
6 |
5
|
a1i |
⊢ ( 𝑥 ( V × V ) 𝑦 → ( 𝐻 ‘ 𝑥 ) ( V × V ) ( 𝐻 ‘ 𝑦 ) ) |
7 |
|
opelvvg |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → 〈 𝑥 , 𝑦 〉 ∈ ( V × V ) ) |
8 |
|
df-br |
⊢ ( 𝑥 ( V × V ) 𝑦 ↔ 〈 𝑥 , 𝑦 〉 ∈ ( V × V ) ) |
9 |
7 8
|
sylibr |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ( V × V ) 𝑦 ) |
10 |
9
|
a1d |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑥 ) ( V × V ) ( 𝐻 ‘ 𝑦 ) → 𝑥 ( V × V ) 𝑦 ) ) |
11 |
6 10
|
impbid2 |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ( V × V ) 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) ( V × V ) ( 𝐻 ‘ 𝑦 ) ) ) |
12 |
11
|
adantl |
⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 ( V × V ) 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) ( V × V ) ( 𝐻 ‘ 𝑦 ) ) ) |
13 |
12
|
ralrimivva |
⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ( V × V ) 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) ( V × V ) ( 𝐻 ‘ 𝑦 ) ) ) |
14 |
13
|
pm4.71i |
⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ( V × V ) 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) ( V × V ) ( 𝐻 ‘ 𝑦 ) ) ) ) |
15 |
|
df-isom |
⊢ ( 𝐻 Isom ( V × V ) , ( V × V ) ( 𝐴 , 𝐵 ) ↔ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ( V × V ) 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) ( V × V ) ( 𝐻 ‘ 𝑦 ) ) ) ) |
16 |
14 15
|
bitr4i |
⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ↔ 𝐻 Isom ( V × V ) , ( V × V ) ( 𝐴 , 𝐵 ) ) |