Step | Hyp | Ref
| Expression |
1 | | elin 3120 |
. . . 4
⊢ (y ∈ (B ∩ (◡𝑆 “ {(𝐻‘𝐷)})) ↔ (y ∈ B ∧ y ∈ (◡𝑆 “ {(𝐻‘𝐷)}))) |
2 | | isof1o 5390 |
. . . . . . . . 9
⊢ (𝐻 Isom 𝑅, 𝑆 (A,
B) → 𝐻:A–1-1-onto→B) |
3 | | f1ofo 5076 |
. . . . . . . . 9
⊢ (𝐻:A–1-1-onto→B →
𝐻:A–onto→B) |
4 | | forn 5052 |
. . . . . . . . . 10
⊢ (𝐻:A–onto→B →
ran 𝐻 = B) |
5 | 4 | eleq2d 2104 |
. . . . . . . . 9
⊢ (𝐻:A–onto→B →
(y ∈ ran
𝐻 ↔ y ∈ B)) |
6 | 2, 3, 5 | 3syl 17 |
. . . . . . . 8
⊢ (𝐻 Isom 𝑅, 𝑆 (A,
B) → (y ∈ ran 𝐻 ↔ y ∈ B)) |
7 | | f1ofn 5070 |
. . . . . . . . 9
⊢ (𝐻:A–1-1-onto→B →
𝐻 Fn A) |
8 | | fvelrnb 5164 |
. . . . . . . . 9
⊢ (𝐻 Fn A → (y
∈ ran 𝐻 ↔ ∃x ∈ A (𝐻‘x) = y)) |
9 | 2, 7, 8 | 3syl 17 |
. . . . . . . 8
⊢ (𝐻 Isom 𝑅, 𝑆 (A,
B) → (y ∈ ran 𝐻 ↔ ∃x ∈ A (𝐻‘x) = y)) |
10 | 6, 9 | bitr3d 179 |
. . . . . . 7
⊢ (𝐻 Isom 𝑅, 𝑆 (A,
B) → (y ∈ B ↔ ∃x ∈ A (𝐻‘x) = y)) |
11 | 10 | adantr 261 |
. . . . . 6
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧ 𝐷 ∈ A) →
(y ∈
B ↔ ∃x ∈ A (𝐻‘x) = y)) |
12 | 2, 7 | syl 14 |
. . . . . . . 8
⊢ (𝐻 Isom 𝑅, 𝑆 (A,
B) → 𝐻 Fn A) |
13 | 12 | anim1i 323 |
. . . . . . 7
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧ 𝐷 ∈ A) →
(𝐻 Fn A ∧ 𝐷 ∈ A)) |
14 | | funfvex 5135 |
. . . . . . . 8
⊢ ((Fun
𝐻 ∧ 𝐷 ∈ dom
𝐻) → (𝐻‘𝐷) ∈
V) |
15 | 14 | funfni 4942 |
. . . . . . 7
⊢ ((𝐻 Fn A ∧ 𝐷 ∈ A) →
(𝐻‘𝐷) ∈
V) |
16 | | vex 2554 |
. . . . . . . 8
⊢ y ∈
V |
17 | 16 | eliniseg 4638 |
. . . . . . 7
⊢ ((𝐻‘𝐷) ∈ V
→ (y ∈ (◡𝑆 “ {(𝐻‘𝐷)}) ↔ y𝑆(𝐻‘𝐷))) |
18 | 13, 15, 17 | 3syl 17 |
. . . . . 6
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧ 𝐷 ∈ A) →
(y ∈
(◡𝑆 “ {(𝐻‘𝐷)}) ↔ y𝑆(𝐻‘𝐷))) |
19 | 11, 18 | anbi12d 442 |
. . . . 5
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧ 𝐷 ∈ A) →
((y ∈
B ∧
y ∈
(◡𝑆 “ {(𝐻‘𝐷)})) ↔ (∃x ∈ A (𝐻‘x) = y ∧ y𝑆(𝐻‘𝐷)))) |
20 | | elin 3120 |
. . . . . . . . . . . 12
⊢ (x ∈ (A ∩ (◡𝑅 “ {𝐷})) ↔ (x ∈ A ∧ x ∈ (◡𝑅 “ {𝐷}))) |
21 | | vex 2554 |
. . . . . . . . . . . . . 14
⊢ x ∈
V |
22 | 21 | eliniseg 4638 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∈ A →
(x ∈
(◡𝑅 “ {𝐷}) ↔ x𝑅𝐷)) |
23 | 22 | anbi2d 437 |
. . . . . . . . . . . 12
⊢ (𝐷 ∈ A →
((x ∈
A ∧
x ∈
(◡𝑅 “ {𝐷})) ↔ (x ∈ A ∧ x𝑅𝐷))) |
24 | 20, 23 | syl5bb 181 |
. . . . . . . . . . 11
⊢ (𝐷 ∈ A →
(x ∈
(A ∩ (◡𝑅 “ {𝐷})) ↔ (x ∈ A ∧ x𝑅𝐷))) |
25 | 24 | anbi1d 438 |
. . . . . . . . . 10
⊢ (𝐷 ∈ A →
((x ∈
(A ∩ (◡𝑅 “ {𝐷})) ∧
x𝐻y)
↔ ((x ∈ A ∧ x𝑅𝐷) ∧
x𝐻y))) |
26 | | anass 381 |
. . . . . . . . . 10
⊢
(((x ∈ A ∧ x𝑅𝐷) ∧
x𝐻y)
↔ (x ∈ A ∧ (x𝑅𝐷 ∧ x𝐻y))) |
27 | 25, 26 | syl6bb 185 |
. . . . . . . . 9
⊢ (𝐷 ∈ A →
((x ∈
(A ∩ (◡𝑅 “ {𝐷})) ∧
x𝐻y)
↔ (x ∈ A ∧ (x𝑅𝐷 ∧ x𝐻y)))) |
28 | 27 | adantl 262 |
. . . . . . . 8
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧ 𝐷 ∈ A) →
((x ∈
(A ∩ (◡𝑅 “ {𝐷})) ∧
x𝐻y)
↔ (x ∈ A ∧ (x𝑅𝐷 ∧ x𝐻y)))) |
29 | | isorel 5391 |
. . . . . . . . . . . . . 14
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧
(x ∈
A ∧ 𝐷 ∈ A)) →
(x𝑅𝐷 ↔ (𝐻‘x)𝑆(𝐻‘𝐷))) |
30 | | fnbrfvb 5157 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐻 Fn A ∧ x ∈ A) → ((𝐻‘x) = y ↔
x𝐻y)) |
31 | 30 | bicomd 129 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐻 Fn A ∧ x ∈ A) → (x𝐻y ↔
(𝐻‘x) = y)) |
32 | 12, 31 | sylan 267 |
. . . . . . . . . . . . . . 15
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧
x ∈
A) → (x𝐻y ↔
(𝐻‘x) = y)) |
33 | 32 | adantrr 448 |
. . . . . . . . . . . . . 14
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧
(x ∈
A ∧ 𝐷 ∈ A)) →
(x𝐻y ↔
(𝐻‘x) = y)) |
34 | 29, 33 | anbi12d 442 |
. . . . . . . . . . . . 13
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧
(x ∈
A ∧ 𝐷 ∈ A)) →
((x𝑅𝐷 ∧ x𝐻y)
↔ ((𝐻‘x)𝑆(𝐻‘𝐷) ∧ (𝐻‘x) = y))) |
35 | | ancom 253 |
. . . . . . . . . . . . . 14
⊢ (((𝐻‘x)𝑆(𝐻‘𝐷) ∧ (𝐻‘x) = y) ↔
((𝐻‘x) = y ∧ (𝐻‘x)𝑆(𝐻‘𝐷))) |
36 | | breq1 3758 |
. . . . . . . . . . . . . . 15
⊢ ((𝐻‘x) = y →
((𝐻‘x)𝑆(𝐻‘𝐷) ↔ y𝑆(𝐻‘𝐷))) |
37 | 36 | pm5.32i 427 |
. . . . . . . . . . . . . 14
⊢ (((𝐻‘x) = y ∧ (𝐻‘x)𝑆(𝐻‘𝐷)) ↔ ((𝐻‘x) = y ∧ y𝑆(𝐻‘𝐷))) |
38 | 35, 37 | bitri 173 |
. . . . . . . . . . . . 13
⊢ (((𝐻‘x)𝑆(𝐻‘𝐷) ∧ (𝐻‘x) = y) ↔
((𝐻‘x) = y ∧ y𝑆(𝐻‘𝐷))) |
39 | 34, 38 | syl6bb 185 |
. . . . . . . . . . . 12
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧
(x ∈
A ∧ 𝐷 ∈ A)) →
((x𝑅𝐷 ∧ x𝐻y)
↔ ((𝐻‘x) = y ∧ y𝑆(𝐻‘𝐷)))) |
40 | 39 | exp32 347 |
. . . . . . . . . . 11
⊢ (𝐻 Isom 𝑅, 𝑆 (A,
B) → (x ∈ A → (𝐷 ∈
A → ((x𝑅𝐷 ∧ x𝐻y)
↔ ((𝐻‘x) = y ∧ y𝑆(𝐻‘𝐷)))))) |
41 | 40 | com23 72 |
. . . . . . . . . 10
⊢ (𝐻 Isom 𝑅, 𝑆 (A,
B) → (𝐷 ∈
A → (x ∈ A → ((x𝑅𝐷 ∧ x𝐻y)
↔ ((𝐻‘x) = y ∧ y𝑆(𝐻‘𝐷)))))) |
42 | 41 | imp 115 |
. . . . . . . . 9
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧ 𝐷 ∈ A) →
(x ∈
A → ((x𝑅𝐷 ∧ x𝐻y)
↔ ((𝐻‘x) = y ∧ y𝑆(𝐻‘𝐷))))) |
43 | 42 | pm5.32d 423 |
. . . . . . . 8
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧ 𝐷 ∈ A) →
((x ∈
A ∧
(x𝑅𝐷 ∧ x𝐻y))
↔ (x ∈ A ∧ ((𝐻‘x) = y ∧ y𝑆(𝐻‘𝐷))))) |
44 | 28, 43 | bitrd 177 |
. . . . . . 7
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧ 𝐷 ∈ A) →
((x ∈
(A ∩ (◡𝑅 “ {𝐷})) ∧
x𝐻y)
↔ (x ∈ A ∧ ((𝐻‘x) = y ∧ y𝑆(𝐻‘𝐷))))) |
45 | 44 | rexbidv2 2323 |
. . . . . 6
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧ 𝐷 ∈ A) →
(∃x
∈ (A
∩ (◡𝑅 “ {𝐷}))x𝐻y ↔
∃x ∈ A ((𝐻‘x) = y ∧ y𝑆(𝐻‘𝐷)))) |
46 | | r19.41v 2460 |
. . . . . 6
⊢ (∃x ∈ A ((𝐻‘x) = y ∧ y𝑆(𝐻‘𝐷)) ↔ (∃x ∈ A (𝐻‘x) = y ∧ y𝑆(𝐻‘𝐷))) |
47 | 45, 46 | syl6bb 185 |
. . . . 5
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧ 𝐷 ∈ A) →
(∃x
∈ (A
∩ (◡𝑅 “ {𝐷}))x𝐻y ↔
(∃x
∈ A
(𝐻‘x) = y ∧ y𝑆(𝐻‘𝐷)))) |
48 | 19, 47 | bitr4d 180 |
. . . 4
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧ 𝐷 ∈ A) →
((y ∈
B ∧
y ∈
(◡𝑆 “ {(𝐻‘𝐷)})) ↔ ∃x ∈ (A ∩
(◡𝑅 “ {𝐷}))x𝐻y)) |
49 | 1, 48 | syl5bb 181 |
. . 3
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧ 𝐷 ∈ A) →
(y ∈
(B ∩ (◡𝑆 “ {(𝐻‘𝐷)})) ↔ ∃x ∈ (A ∩
(◡𝑅 “ {𝐷}))x𝐻y)) |
50 | 49 | abbi2dv 2153 |
. 2
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧ 𝐷 ∈ A) →
(B ∩ (◡𝑆 “ {(𝐻‘𝐷)})) = {y ∣ ∃x ∈ (A ∩
(◡𝑅 “ {𝐷}))x𝐻y}) |
51 | | dfima2 4613 |
. 2
⊢ (𝐻 “ (A ∩ (◡𝑅 “ {𝐷}))) = {y ∣ ∃x ∈ (A ∩
(◡𝑅 “ {𝐷}))x𝐻y} |
52 | 50, 51 | syl6reqr 2088 |
1
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧ 𝐷 ∈ A) →
(𝐻 “ (A ∩ (◡𝑅 “ {𝐷}))) = (B ∩ (◡𝑆 “ {(𝐻‘𝐷)}))) |