Step | Hyp | Ref
| Expression |
1 | | simpl 102 |
. 2
⊢ ((𝐻:A–1-1-onto→B ∧ 𝑆 = {〈z, w〉
∣ ∃x ∈ A ∃y ∈ A ((z = (𝐻‘x) ∧ w = (𝐻‘y)) ∧ x𝑅y)})
→ 𝐻:A–1-1-onto→B) |
2 | | f1of1 5068 |
. . 3
⊢ (𝐻:A–1-1-onto→B →
𝐻:A–1-1→B) |
3 | | df-br 3756 |
. . . . 5
⊢ ((𝐻‘v)𝑆(𝐻‘u) ↔ 〈(𝐻‘v), (𝐻‘u)〉 ∈ 𝑆) |
4 | | eleq2 2098 |
. . . . . . 7
⊢ (𝑆 = {〈z, w〉
∣ ∃x ∈ A ∃y ∈ A ((z = (𝐻‘x) ∧ w = (𝐻‘y)) ∧ x𝑅y)}
→ (〈(𝐻‘v), (𝐻‘u)〉 ∈ 𝑆 ↔ 〈(𝐻‘v), (𝐻‘u)〉 ∈
{〈z, w〉 ∣ ∃x ∈ A ∃y ∈ A ((z = (𝐻‘x) ∧ w = (𝐻‘y)) ∧ x𝑅y)})) |
5 | | f1fn 5036 |
. . . . . . . . 9
⊢ (𝐻:A–1-1→B →
𝐻 Fn A) |
6 | | funfvex 5135 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐻 ∧ v ∈ dom 𝐻) → (𝐻‘v) ∈
V) |
7 | 6 | funfni 4942 |
. . . . . . . . . . 11
⊢ ((𝐻 Fn A ∧ v ∈ A) → (𝐻‘v) ∈
V) |
8 | | funfvex 5135 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐻 ∧ u ∈ dom 𝐻) → (𝐻‘u) ∈
V) |
9 | 8 | funfni 4942 |
. . . . . . . . . . 11
⊢ ((𝐻 Fn A ∧ u ∈ A) → (𝐻‘u) ∈
V) |
10 | 7, 9 | anim12dan 532 |
. . . . . . . . . 10
⊢ ((𝐻 Fn A ∧ (v ∈ A ∧ u ∈ A)) → ((𝐻‘v) ∈ V ∧ (𝐻‘u) ∈
V)) |
11 | | eqeq1 2043 |
. . . . . . . . . . . . . 14
⊢ (z = (𝐻‘v) → (z =
(𝐻‘x) ↔ (𝐻‘v) = (𝐻‘x))) |
12 | 11 | anbi1d 438 |
. . . . . . . . . . . . 13
⊢ (z = (𝐻‘v) → ((z =
(𝐻‘x) ∧ w = (𝐻‘y)) ↔ ((𝐻‘v) = (𝐻‘x) ∧ w = (𝐻‘y)))) |
13 | 12 | anbi1d 438 |
. . . . . . . . . . . 12
⊢ (z = (𝐻‘v) → (((z =
(𝐻‘x) ∧ w = (𝐻‘y)) ∧ x𝑅y)
↔ (((𝐻‘v) = (𝐻‘x) ∧ w = (𝐻‘y)) ∧ x𝑅y))) |
14 | 13 | 2rexbidv 2343 |
. . . . . . . . . . 11
⊢ (z = (𝐻‘v) → (∃x ∈ A ∃y ∈ A ((z = (𝐻‘x) ∧ w = (𝐻‘y)) ∧ x𝑅y)
↔ ∃x ∈ A ∃y ∈ A (((𝐻‘v) = (𝐻‘x) ∧ w = (𝐻‘y)) ∧ x𝑅y))) |
15 | | eqeq1 2043 |
. . . . . . . . . . . . . 14
⊢ (w = (𝐻‘u) → (w =
(𝐻‘y) ↔ (𝐻‘u) = (𝐻‘y))) |
16 | 15 | anbi2d 437 |
. . . . . . . . . . . . 13
⊢ (w = (𝐻‘u) → (((𝐻‘v) = (𝐻‘x) ∧ w = (𝐻‘y)) ↔ ((𝐻‘v) = (𝐻‘x) ∧ (𝐻‘u) = (𝐻‘y)))) |
17 | 16 | anbi1d 438 |
. . . . . . . . . . . 12
⊢ (w = (𝐻‘u) → ((((𝐻‘v) = (𝐻‘x) ∧ w = (𝐻‘y)) ∧ x𝑅y)
↔ (((𝐻‘v) = (𝐻‘x) ∧ (𝐻‘u) = (𝐻‘y)) ∧ x𝑅y))) |
18 | 17 | 2rexbidv 2343 |
. . . . . . . . . . 11
⊢ (w = (𝐻‘u) → (∃x ∈ A ∃y ∈ A (((𝐻‘v) = (𝐻‘x) ∧ w = (𝐻‘y)) ∧ x𝑅y)
↔ ∃x ∈ A ∃y ∈ A (((𝐻‘v) = (𝐻‘x) ∧ (𝐻‘u) = (𝐻‘y)) ∧ x𝑅y))) |
19 | 14, 18 | opelopabg 3996 |
. . . . . . . . . 10
⊢ (((𝐻‘v) ∈ V ∧ (𝐻‘u) ∈ V) →
(〈(𝐻‘v), (𝐻‘u)〉 ∈
{〈z, w〉 ∣ ∃x ∈ A ∃y ∈ A ((z = (𝐻‘x) ∧ w = (𝐻‘y)) ∧ x𝑅y)}
↔ ∃x ∈ A ∃y ∈ A (((𝐻‘v) = (𝐻‘x) ∧ (𝐻‘u) = (𝐻‘y)) ∧ x𝑅y))) |
20 | 10, 19 | syl 14 |
. . . . . . . . 9
⊢ ((𝐻 Fn A ∧ (v ∈ A ∧ u ∈ A)) → (〈(𝐻‘v), (𝐻‘u)〉 ∈
{〈z, w〉 ∣ ∃x ∈ A ∃y ∈ A ((z = (𝐻‘x) ∧ w = (𝐻‘y)) ∧ x𝑅y)}
↔ ∃x ∈ A ∃y ∈ A (((𝐻‘v) = (𝐻‘x) ∧ (𝐻‘u) = (𝐻‘y)) ∧ x𝑅y))) |
21 | 5, 20 | sylan 267 |
. . . . . . . 8
⊢ ((𝐻:A–1-1→B ∧ (v ∈ A ∧ u ∈ A)) →
(〈(𝐻‘v), (𝐻‘u)〉 ∈
{〈z, w〉 ∣ ∃x ∈ A ∃y ∈ A ((z = (𝐻‘x) ∧ w = (𝐻‘y)) ∧ x𝑅y)}
↔ ∃x ∈ A ∃y ∈ A (((𝐻‘v) = (𝐻‘x) ∧ (𝐻‘u) = (𝐻‘y)) ∧ x𝑅y))) |
22 | | anass 381 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐻‘v) = (𝐻‘x) ∧ (𝐻‘u) = (𝐻‘y)) ∧ x𝑅y)
↔ ((𝐻‘v) = (𝐻‘x) ∧ ((𝐻‘u) = (𝐻‘y) ∧ x𝑅y))) |
23 | | f1fveq 5354 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐻:A–1-1→B ∧ (v ∈ A ∧ x ∈ A)) →
((𝐻‘v) = (𝐻‘x) ↔ v =
x)) |
24 | | equcom 1590 |
. . . . . . . . . . . . . . . . . 18
⊢ (v = x ↔
x = v) |
25 | 23, 24 | syl6bb 185 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐻:A–1-1→B ∧ (v ∈ A ∧ x ∈ A)) →
((𝐻‘v) = (𝐻‘x) ↔ x =
v)) |
26 | 25 | anassrs 380 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐻:A–1-1→B ∧ v ∈ A) ∧ x ∈ A) →
((𝐻‘v) = (𝐻‘x) ↔ x =
v)) |
27 | 26 | anbi1d 438 |
. . . . . . . . . . . . . . 15
⊢ (((𝐻:A–1-1→B ∧ v ∈ A) ∧ x ∈ A) →
(((𝐻‘v) = (𝐻‘x) ∧ ((𝐻‘u) = (𝐻‘y) ∧ x𝑅y))
↔ (x = v ∧ ((𝐻‘u) = (𝐻‘y) ∧ x𝑅y)))) |
28 | 22, 27 | syl5bb 181 |
. . . . . . . . . . . . . 14
⊢ (((𝐻:A–1-1→B ∧ v ∈ A) ∧ x ∈ A) →
((((𝐻‘v) = (𝐻‘x) ∧ (𝐻‘u) = (𝐻‘y)) ∧ x𝑅y)
↔ (x = v ∧ ((𝐻‘u) = (𝐻‘y) ∧ x𝑅y)))) |
29 | 28 | rexbidv 2321 |
. . . . . . . . . . . . 13
⊢ (((𝐻:A–1-1→B ∧ v ∈ A) ∧ x ∈ A) →
(∃y
∈ A
(((𝐻‘v) = (𝐻‘x) ∧ (𝐻‘u) = (𝐻‘y)) ∧ x𝑅y)
↔ ∃y ∈ A (x = v ∧ ((𝐻‘u) = (𝐻‘y) ∧ x𝑅y)))) |
30 | | r19.42v 2461 |
. . . . . . . . . . . . 13
⊢ (∃y ∈ A (x = v ∧ ((𝐻‘u) = (𝐻‘y) ∧ x𝑅y))
↔ (x = v ∧ ∃y ∈ A ((𝐻‘u) = (𝐻‘y) ∧ x𝑅y))) |
31 | 29, 30 | syl6bb 185 |
. . . . . . . . . . . 12
⊢ (((𝐻:A–1-1→B ∧ v ∈ A) ∧ x ∈ A) →
(∃y
∈ A
(((𝐻‘v) = (𝐻‘x) ∧ (𝐻‘u) = (𝐻‘y)) ∧ x𝑅y)
↔ (x = v ∧ ∃y ∈ A ((𝐻‘u) = (𝐻‘y) ∧ x𝑅y)))) |
32 | 31 | rexbidva 2317 |
. . . . . . . . . . 11
⊢ ((𝐻:A–1-1→B ∧ v ∈ A) →
(∃x
∈ A ∃y ∈ A (((𝐻‘v) = (𝐻‘x) ∧ (𝐻‘u) = (𝐻‘y)) ∧ x𝑅y)
↔ ∃x ∈ A (x = v ∧ ∃y ∈ A ((𝐻‘u) = (𝐻‘y) ∧ x𝑅y)))) |
33 | | breq1 3758 |
. . . . . . . . . . . . . . 15
⊢ (x = v →
(x𝑅y ↔
v𝑅y)) |
34 | 33 | anbi2d 437 |
. . . . . . . . . . . . . 14
⊢ (x = v →
(((𝐻‘u) = (𝐻‘y) ∧ x𝑅y)
↔ ((𝐻‘u) = (𝐻‘y) ∧ v𝑅y))) |
35 | 34 | rexbidv 2321 |
. . . . . . . . . . . . 13
⊢ (x = v →
(∃y
∈ A
((𝐻‘u) = (𝐻‘y) ∧ x𝑅y)
↔ ∃y ∈ A ((𝐻‘u) = (𝐻‘y) ∧ v𝑅y))) |
36 | 35 | ceqsrexv 2668 |
. . . . . . . . . . . 12
⊢ (v ∈ A → (∃x ∈ A (x = v ∧ ∃y ∈ A ((𝐻‘u) = (𝐻‘y) ∧ x𝑅y))
↔ ∃y ∈ A ((𝐻‘u) = (𝐻‘y) ∧ v𝑅y))) |
37 | 36 | adantl 262 |
. . . . . . . . . . 11
⊢ ((𝐻:A–1-1→B ∧ v ∈ A) →
(∃x
∈ A
(x = v
∧ ∃y ∈ A ((𝐻‘u) = (𝐻‘y) ∧ x𝑅y))
↔ ∃y ∈ A ((𝐻‘u) = (𝐻‘y) ∧ v𝑅y))) |
38 | 32, 37 | bitrd 177 |
. . . . . . . . . 10
⊢ ((𝐻:A–1-1→B ∧ v ∈ A) →
(∃x
∈ A ∃y ∈ A (((𝐻‘v) = (𝐻‘x) ∧ (𝐻‘u) = (𝐻‘y)) ∧ x𝑅y)
↔ ∃y ∈ A ((𝐻‘u) = (𝐻‘y) ∧ v𝑅y))) |
39 | | f1fveq 5354 |
. . . . . . . . . . . . . . 15
⊢ ((𝐻:A–1-1→B ∧ (u ∈ A ∧ y ∈ A)) →
((𝐻‘u) = (𝐻‘y) ↔ u =
y)) |
40 | | equcom 1590 |
. . . . . . . . . . . . . . 15
⊢ (u = y ↔
y = u) |
41 | 39, 40 | syl6bb 185 |
. . . . . . . . . . . . . 14
⊢ ((𝐻:A–1-1→B ∧ (u ∈ A ∧ y ∈ A)) →
((𝐻‘u) = (𝐻‘y) ↔ y =
u)) |
42 | 41 | anassrs 380 |
. . . . . . . . . . . . 13
⊢ (((𝐻:A–1-1→B ∧ u ∈ A) ∧ y ∈ A) →
((𝐻‘u) = (𝐻‘y) ↔ y =
u)) |
43 | 42 | anbi1d 438 |
. . . . . . . . . . . 12
⊢ (((𝐻:A–1-1→B ∧ u ∈ A) ∧ y ∈ A) →
(((𝐻‘u) = (𝐻‘y) ∧ v𝑅y)
↔ (y = u ∧ v𝑅y))) |
44 | 43 | rexbidva 2317 |
. . . . . . . . . . 11
⊢ ((𝐻:A–1-1→B ∧ u ∈ A) →
(∃y
∈ A
((𝐻‘u) = (𝐻‘y) ∧ v𝑅y)
↔ ∃y ∈ A (y = u ∧ v𝑅y))) |
45 | | breq2 3759 |
. . . . . . . . . . . . 13
⊢ (y = u →
(v𝑅y ↔
v𝑅u)) |
46 | 45 | ceqsrexv 2668 |
. . . . . . . . . . . 12
⊢ (u ∈ A → (∃y ∈ A (y = u ∧ v𝑅y) ↔ v𝑅u)) |
47 | 46 | adantl 262 |
. . . . . . . . . . 11
⊢ ((𝐻:A–1-1→B ∧ u ∈ A) →
(∃y
∈ A
(y = u
∧ v𝑅y) ↔ v𝑅u)) |
48 | 44, 47 | bitrd 177 |
. . . . . . . . . 10
⊢ ((𝐻:A–1-1→B ∧ u ∈ A) →
(∃y
∈ A
((𝐻‘u) = (𝐻‘y) ∧ v𝑅y)
↔ v𝑅u)) |
49 | 38, 48 | sylan9bb 435 |
. . . . . . . . 9
⊢ (((𝐻:A–1-1→B ∧ v ∈ A) ∧ (𝐻:A–1-1→B ∧ u ∈ A)) →
(∃x
∈ A ∃y ∈ A (((𝐻‘v) = (𝐻‘x) ∧ (𝐻‘u) = (𝐻‘y)) ∧ x𝑅y)
↔ v𝑅u)) |
50 | 49 | anandis 526 |
. . . . . . . 8
⊢ ((𝐻:A–1-1→B ∧ (v ∈ A ∧ u ∈ A)) →
(∃x
∈ A ∃y ∈ A (((𝐻‘v) = (𝐻‘x) ∧ (𝐻‘u) = (𝐻‘y)) ∧ x𝑅y)
↔ v𝑅u)) |
51 | 21, 50 | bitrd 177 |
. . . . . . 7
⊢ ((𝐻:A–1-1→B ∧ (v ∈ A ∧ u ∈ A)) →
(〈(𝐻‘v), (𝐻‘u)〉 ∈
{〈z, w〉 ∣ ∃x ∈ A ∃y ∈ A ((z = (𝐻‘x) ∧ w = (𝐻‘y)) ∧ x𝑅y)}
↔ v𝑅u)) |
52 | 4, 51 | sylan9bbr 436 |
. . . . . 6
⊢ (((𝐻:A–1-1→B ∧ (v ∈ A ∧ u ∈ A)) ∧ 𝑆 = {〈z, w〉
∣ ∃x ∈ A ∃y ∈ A ((z = (𝐻‘x) ∧ w = (𝐻‘y)) ∧ x𝑅y)})
→ (〈(𝐻‘v), (𝐻‘u)〉 ∈ 𝑆 ↔ v𝑅u)) |
53 | 52 | an32s 502 |
. . . . 5
⊢ (((𝐻:A–1-1→B ∧ 𝑆 = {〈z, w〉
∣ ∃x ∈ A ∃y ∈ A ((z = (𝐻‘x) ∧ w = (𝐻‘y)) ∧ x𝑅y)})
∧ (v ∈ A ∧ u ∈ A)) →
(〈(𝐻‘v), (𝐻‘u)〉 ∈ 𝑆 ↔ v𝑅u)) |
54 | 3, 53 | syl5rbb 182 |
. . . 4
⊢ (((𝐻:A–1-1→B ∧ 𝑆 = {〈z, w〉
∣ ∃x ∈ A ∃y ∈ A ((z = (𝐻‘x) ∧ w = (𝐻‘y)) ∧ x𝑅y)})
∧ (v ∈ A ∧ u ∈ A)) →
(v𝑅u ↔
(𝐻‘v)𝑆(𝐻‘u))) |
55 | 54 | ralrimivva 2395 |
. . 3
⊢ ((𝐻:A–1-1→B ∧ 𝑆 = {〈z, w〉
∣ ∃x ∈ A ∃y ∈ A ((z = (𝐻‘x) ∧ w = (𝐻‘y)) ∧ x𝑅y)})
→ ∀v ∈ A ∀u ∈ A (v𝑅u ↔ (𝐻‘v)𝑆(𝐻‘u))) |
56 | 2, 55 | sylan 267 |
. 2
⊢ ((𝐻:A–1-1-onto→B ∧ 𝑆 = {〈z, w〉
∣ ∃x ∈ A ∃y ∈ A ((z = (𝐻‘x) ∧ w = (𝐻‘y)) ∧ x𝑅y)})
→ ∀v ∈ A ∀u ∈ A (v𝑅u ↔ (𝐻‘v)𝑆(𝐻‘u))) |
57 | | df-isom 4854 |
. 2
⊢ (𝐻 Isom 𝑅, 𝑆 (A,
B) ↔ (𝐻:A–1-1-onto→B ∧ ∀v ∈ A ∀u ∈ A (v𝑅u ↔ (𝐻‘v)𝑆(𝐻‘u)))) |
58 | 1, 56, 57 | sylanbrc 394 |
1
⊢ ((𝐻:A–1-1-onto→B ∧ 𝑆 = {〈z, w〉
∣ ∃x ∈ A ∃y ∈ A ((z = (𝐻‘x) ∧ w = (𝐻‘y)) ∧ x𝑅y)})
→ 𝐻 Isom 𝑅, 𝑆 (A,
B)) |