Step | Hyp | Ref
| Expression |
1 | | f1of1 5068 |
. . . . . . 7
⊢ (𝐻:A–1-1-onto→B →
𝐻:A–1-1→B) |
2 | | f1ores 5084 |
. . . . . . . 8
⊢ ((𝐻:A–1-1→B ∧ 𝐾 ⊆ A) → (𝐻 ↾ 𝐾):𝐾–1-1-onto→(𝐻 “ 𝐾)) |
3 | 2 | expcom 109 |
. . . . . . 7
⊢ (𝐾 ⊆ A → (𝐻:A–1-1→B →
(𝐻 ↾ 𝐾):𝐾–1-1-onto→(𝐻 “ 𝐾))) |
4 | 1, 3 | syl5 28 |
. . . . . 6
⊢ (𝐾 ⊆ A → (𝐻:A–1-1-onto→B →
(𝐻 ↾ 𝐾):𝐾–1-1-onto→(𝐻 “ 𝐾))) |
5 | | ssralv 2998 |
. . . . . . 7
⊢ (𝐾 ⊆ A → (∀𝑎 ∈ A ∀𝑏 ∈ A (𝑎𝑅𝑏 ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏)) → ∀𝑎 ∈ 𝐾 ∀𝑏 ∈ A (𝑎𝑅𝑏 ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))) |
6 | | ssralv 2998 |
. . . . . . . . . 10
⊢ (𝐾 ⊆ A → (∀𝑏 ∈ A (𝑎𝑅𝑏 ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏)) → ∀𝑏 ∈ 𝐾 (𝑎𝑅𝑏 ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))) |
7 | 6 | adantr 261 |
. . . . . . . . 9
⊢ ((𝐾 ⊆ A ∧ 𝑎 ∈ 𝐾) → (∀𝑏 ∈ A (𝑎𝑅𝑏 ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏)) → ∀𝑏 ∈ 𝐾 (𝑎𝑅𝑏 ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))) |
8 | | fvres 5141 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ 𝐾 → ((𝐻 ↾ 𝐾)‘𝑎) = (𝐻‘𝑎)) |
9 | | fvres 5141 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ 𝐾 → ((𝐻 ↾ 𝐾)‘𝑏) = (𝐻‘𝑏)) |
10 | 8, 9 | breqan12d 3770 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) → (((𝐻 ↾ 𝐾)‘𝑎)𝑆((𝐻 ↾ 𝐾)‘𝑏) ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏))) |
11 | 10 | adantll 445 |
. . . . . . . . . . . 12
⊢ (((𝐾 ⊆ A ∧ 𝑎 ∈ 𝐾) ∧ 𝑏
∈ 𝐾) → (((𝐻 ↾ 𝐾)‘𝑎)𝑆((𝐻 ↾ 𝐾)‘𝑏) ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏))) |
12 | 11 | bibi2d 221 |
. . . . . . . . . . 11
⊢ (((𝐾 ⊆ A ∧ 𝑎 ∈ 𝐾) ∧ 𝑏
∈ 𝐾) → ((𝑎𝑅𝑏 ↔ ((𝐻 ↾ 𝐾)‘𝑎)𝑆((𝐻 ↾ 𝐾)‘𝑏)) ↔ (𝑎𝑅𝑏 ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))) |
13 | 12 | biimprd 147 |
. . . . . . . . . 10
⊢ (((𝐾 ⊆ A ∧ 𝑎 ∈ 𝐾) ∧ 𝑏
∈ 𝐾) → ((𝑎𝑅𝑏 ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏)) → (𝑎𝑅𝑏 ↔ ((𝐻 ↾ 𝐾)‘𝑎)𝑆((𝐻 ↾ 𝐾)‘𝑏)))) |
14 | 13 | ralimdva 2381 |
. . . . . . . . 9
⊢ ((𝐾 ⊆ A ∧ 𝑎 ∈ 𝐾) → (∀𝑏 ∈ 𝐾 (𝑎𝑅𝑏 ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏)) → ∀𝑏 ∈ 𝐾 (𝑎𝑅𝑏 ↔ ((𝐻 ↾ 𝐾)‘𝑎)𝑆((𝐻 ↾ 𝐾)‘𝑏)))) |
15 | 7, 14 | syld 40 |
. . . . . . . 8
⊢ ((𝐾 ⊆ A ∧ 𝑎 ∈ 𝐾) → (∀𝑏 ∈ A (𝑎𝑅𝑏 ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏)) → ∀𝑏 ∈ 𝐾 (𝑎𝑅𝑏 ↔ ((𝐻 ↾ 𝐾)‘𝑎)𝑆((𝐻 ↾ 𝐾)‘𝑏)))) |
16 | 15 | ralimdva 2381 |
. . . . . . 7
⊢ (𝐾 ⊆ A → (∀𝑎 ∈ 𝐾 ∀𝑏 ∈ A (𝑎𝑅𝑏 ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏)) → ∀𝑎 ∈ 𝐾 ∀𝑏 ∈ 𝐾 (𝑎𝑅𝑏 ↔ ((𝐻 ↾ 𝐾)‘𝑎)𝑆((𝐻 ↾ 𝐾)‘𝑏)))) |
17 | 5, 16 | syld 40 |
. . . . . 6
⊢ (𝐾 ⊆ A → (∀𝑎 ∈ A ∀𝑏 ∈ A (𝑎𝑅𝑏 ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏)) → ∀𝑎 ∈ 𝐾 ∀𝑏 ∈ 𝐾 (𝑎𝑅𝑏 ↔ ((𝐻 ↾ 𝐾)‘𝑎)𝑆((𝐻 ↾ 𝐾)‘𝑏)))) |
18 | 4, 17 | anim12d 318 |
. . . . 5
⊢ (𝐾 ⊆ A → ((𝐻:A–1-1-onto→B ∧ ∀𝑎 ∈ A ∀𝑏 ∈ A (𝑎𝑅𝑏 ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏))) → ((𝐻 ↾ 𝐾):𝐾–1-1-onto→(𝐻 “ 𝐾) ∧ ∀𝑎 ∈ 𝐾 ∀𝑏 ∈ 𝐾 (𝑎𝑅𝑏 ↔ ((𝐻 ↾ 𝐾)‘𝑎)𝑆((𝐻 ↾ 𝐾)‘𝑏))))) |
19 | | df-isom 4854 |
. . . . 5
⊢ (𝐻 Isom 𝑅, 𝑆 (A,
B) ↔ (𝐻:A–1-1-onto→B ∧ ∀𝑎 ∈ A ∀𝑏 ∈ A (𝑎𝑅𝑏 ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))) |
20 | | df-isom 4854 |
. . . . 5
⊢ ((𝐻 ↾ 𝐾) Isom 𝑅, 𝑆 (𝐾, (𝐻 “ 𝐾)) ↔ ((𝐻 ↾ 𝐾):𝐾–1-1-onto→(𝐻 “ 𝐾) ∧ ∀𝑎 ∈ 𝐾 ∀𝑏 ∈ 𝐾 (𝑎𝑅𝑏 ↔ ((𝐻 ↾ 𝐾)‘𝑎)𝑆((𝐻 ↾ 𝐾)‘𝑏)))) |
21 | 18, 19, 20 | 3imtr4g 194 |
. . . 4
⊢ (𝐾 ⊆ A → (𝐻 Isom 𝑅, 𝑆 (A,
B) → (𝐻 ↾ 𝐾) Isom 𝑅, 𝑆 (𝐾, (𝐻 “ 𝐾)))) |
22 | 21 | impcom 116 |
. . 3
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧ 𝐾 ⊆ A) → (𝐻 ↾ 𝐾) Isom 𝑅, 𝑆 (𝐾, (𝐻 “ 𝐾))) |
23 | | isoeq5 5388 |
. . 3
⊢ (𝑋 = (𝐻 “ 𝐾) → ((𝐻 ↾ 𝐾) Isom 𝑅, 𝑆 (𝐾, 𝑋) ↔ (𝐻 ↾ 𝐾) Isom 𝑅, 𝑆 (𝐾, (𝐻 “ 𝐾)))) |
24 | 22, 23 | syl5ibrcom 146 |
. 2
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧ 𝐾 ⊆ A) → (𝑋 = (𝐻 “ 𝐾) → (𝐻 ↾ 𝐾) Isom 𝑅, 𝑆 (𝐾, 𝑋))) |
25 | 24 | 3impia 1100 |
1
⊢ ((𝐻 Isom 𝑅, 𝑆 (A,
B) ∧ 𝐾 ⊆ A ∧ 𝑋 = (𝐻 “ 𝐾)) → (𝐻 ↾ 𝐾) Isom 𝑅, 𝑆 (𝐾, 𝑋)) |