Step | Hyp | Ref
| Expression |
1 | | f1ocnv 5299 |
. . . 4
⊢ (H:A–1-1-onto→B →
◡H:B–1-1-onto→A) |
2 | 1 | adantr 451 |
. . 3
⊢ ((H:A–1-1-onto→B ∧ ∀x ∈ A ∀y ∈ A (xRy ↔
(H ‘x)S(H ‘y)))
→ ◡H:B–1-1-onto→A) |
3 | | f1ocnvfv2 5477 |
. . . . . . . 8
⊢ ((H:A–1-1-onto→B ∧ z ∈ B) →
(H ‘(◡H
‘z)) = z) |
4 | 3 | adantrr 697 |
. . . . . . 7
⊢ ((H:A–1-1-onto→B ∧ (z ∈ B ∧ w ∈ B)) →
(H ‘(◡H
‘z)) = z) |
5 | | f1ocnvfv2 5477 |
. . . . . . . 8
⊢ ((H:A–1-1-onto→B ∧ w ∈ B) →
(H ‘(◡H
‘w)) = w) |
6 | 5 | adantrl 696 |
. . . . . . 7
⊢ ((H:A–1-1-onto→B ∧ (z ∈ B ∧ w ∈ B)) →
(H ‘(◡H
‘w)) = w) |
7 | 4, 6 | breq12d 4652 |
. . . . . 6
⊢ ((H:A–1-1-onto→B ∧ (z ∈ B ∧ w ∈ B)) →
((H ‘(◡H
‘z))S(H
‘(◡H ‘w))
↔ zSw)) |
8 | 7 | adantlr 695 |
. . . . 5
⊢ (((H:A–1-1-onto→B ∧ ∀x ∈ A ∀y ∈ A (xRy ↔
(H ‘x)S(H ‘y)))
∧ (z ∈ B ∧ w ∈ B)) →
((H ‘(◡H
‘z))S(H
‘(◡H ‘w))
↔ zSw)) |
9 | | f1of 5287 |
. . . . . . 7
⊢ (◡H:B–1-1-onto→A →
◡H:B–→A) |
10 | 1, 9 | syl 15 |
. . . . . 6
⊢ (H:A–1-1-onto→B →
◡H:B–→A) |
11 | | ffvelrn 5415 |
. . . . . . . . 9
⊢ ((◡H:B–→A
∧ z ∈ B) →
(◡H
‘z) ∈ A) |
12 | | ffvelrn 5415 |
. . . . . . . . 9
⊢ ((◡H:B–→A
∧ w ∈ B) →
(◡H
‘w) ∈ A) |
13 | 11, 12 | anim12dan 810 |
. . . . . . . 8
⊢ ((◡H:B–→A
∧ (z ∈ B ∧ w ∈ B)) →
((◡H ‘z)
∈ A ∧ (◡H ‘w)
∈ A)) |
14 | | breq1 4642 |
. . . . . . . . . . 11
⊢ (x = (◡H
‘z) → (xRy ↔ (◡H
‘z)Ry)) |
15 | | fveq2 5328 |
. . . . . . . . . . . 12
⊢ (x = (◡H
‘z) → (H ‘x) =
(H ‘(◡H
‘z))) |
16 | 15 | breq1d 4649 |
. . . . . . . . . . 11
⊢ (x = (◡H
‘z) → ((H ‘x)S(H ‘y)
↔ (H ‘(◡H
‘z))S(H
‘y))) |
17 | 14, 16 | bibi12d 312 |
. . . . . . . . . 10
⊢ (x = (◡H
‘z) → ((xRy ↔ (H
‘x)S(H
‘y)) ↔ ((◡H
‘z)Ry ↔
(H ‘(◡H
‘z))S(H
‘y)))) |
18 | | bicom 191 |
. . . . . . . . . 10
⊢ (((◡H
‘z)Ry ↔
(H ‘(◡H
‘z))S(H
‘y)) ↔ ((H ‘(◡H
‘z))S(H
‘y) ↔ (◡H
‘z)Ry)) |
19 | 17, 18 | syl6bb 252 |
. . . . . . . . 9
⊢ (x = (◡H
‘z) → ((xRy ↔ (H
‘x)S(H
‘y)) ↔ ((H ‘(◡H
‘z))S(H
‘y) ↔ (◡H
‘z)Ry))) |
20 | | fveq2 5328 |
. . . . . . . . . . 11
⊢ (y = (◡H
‘w) → (H ‘y) =
(H ‘(◡H
‘w))) |
21 | 20 | breq2d 4651 |
. . . . . . . . . 10
⊢ (y = (◡H
‘w) → ((H ‘(◡H
‘z))S(H
‘y) ↔ (H ‘(◡H
‘z))S(H
‘(◡H ‘w)))) |
22 | | breq2 4643 |
. . . . . . . . . 10
⊢ (y = (◡H
‘w) → ((◡H
‘z)Ry ↔ (◡H
‘z)R(◡H ‘w))) |
23 | 21, 22 | bibi12d 312 |
. . . . . . . . 9
⊢ (y = (◡H
‘w) → (((H ‘(◡H
‘z))S(H
‘y) ↔ (◡H
‘z)Ry) ↔
((H ‘(◡H
‘z))S(H
‘(◡H ‘w))
↔ (◡H ‘z)R(◡H
‘w)))) |
24 | 19, 23 | rspc2va 2962 |
. . . . . . . 8
⊢ ((((◡H
‘z) ∈ A ∧ (◡H ‘w)
∈ A)
∧ ∀x ∈ A ∀y ∈ A (xRy ↔ (H
‘x)S(H
‘y))) → ((H ‘(◡H
‘z))S(H
‘(◡H ‘w))
↔ (◡H ‘z)R(◡H
‘w))) |
25 | 13, 24 | sylan 457 |
. . . . . . 7
⊢ (((◡H:B–→A
∧ (z ∈ B ∧ w ∈ B)) ∧ ∀x ∈ A ∀y ∈ A (xRy ↔
(H ‘x)S(H ‘y)))
→ ((H ‘(◡H
‘z))S(H
‘(◡H ‘w))
↔ (◡H ‘z)R(◡H
‘w))) |
26 | 25 | an32s 779 |
. . . . . 6
⊢ (((◡H:B–→A
∧ ∀x ∈ A ∀y ∈ A (xRy ↔ (H
‘x)S(H
‘y))) ∧ (z ∈ B ∧ w ∈ B)) →
((H ‘(◡H
‘z))S(H
‘(◡H ‘w))
↔ (◡H ‘z)R(◡H
‘w))) |
27 | 10, 26 | sylanl1 631 |
. . . . 5
⊢ (((H:A–1-1-onto→B ∧ ∀x ∈ A ∀y ∈ A (xRy ↔
(H ‘x)S(H ‘y)))
∧ (z ∈ B ∧ w ∈ B)) →
((H ‘(◡H
‘z))S(H
‘(◡H ‘w))
↔ (◡H ‘z)R(◡H
‘w))) |
28 | 8, 27 | bitr3d 246 |
. . . 4
⊢ (((H:A–1-1-onto→B ∧ ∀x ∈ A ∀y ∈ A (xRy ↔
(H ‘x)S(H ‘y)))
∧ (z ∈ B ∧ w ∈ B)) →
(zSw ↔ (◡H
‘z)R(◡H ‘w))) |
29 | 28 | ralrimivva 2706 |
. . 3
⊢ ((H:A–1-1-onto→B ∧ ∀x ∈ A ∀y ∈ A (xRy ↔
(H ‘x)S(H ‘y)))
→ ∀z ∈ B ∀w ∈ B (zSw ↔ (◡H
‘z)R(◡H ‘w))) |
30 | 2, 29 | jca 518 |
. 2
⊢ ((H:A–1-1-onto→B ∧ ∀x ∈ A ∀y ∈ A (xRy ↔
(H ‘x)S(H ‘y)))
→ (◡H:B–1-1-onto→A ∧ ∀z ∈ B ∀w ∈ B (zSw ↔ (◡H
‘z)R(◡H ‘w)))) |
31 | | df-iso 4796 |
. 2
⊢ (H Isom R,
S (A,
B) ↔ (H:A–1-1-onto→B ∧ ∀x ∈ A ∀y ∈ A (xRy ↔
(H ‘x)S(H ‘y)))) |
32 | | df-iso 4796 |
. 2
⊢ (◡H Isom
S, R
(B, A)
↔ (◡H:B–1-1-onto→A ∧ ∀z ∈ B ∀w ∈ B (zSw ↔ (◡H
‘z)R(◡H ‘w)))) |
33 | 30, 31, 32 | 3imtr4i 257 |
1
⊢ (H Isom R,
S (A,
B) → ◡H Isom
S, R
(B, A)) |