# Metamath Proof Explorer

## Theorem isores3

Description: Induced isomorphism on a subset. (Contributed by Stefan O'Rear, 5-Nov-2014)

Ref Expression
Assertion isores3 ${⊢}\left({H}{Isom}_{{R},{S}}\left({A},{B}\right)\wedge {K}\subseteq {A}\wedge {X}={H}\left[{K}\right]\right)\to \left({{H}↾}_{{K}}\right){Isom}_{{R},{S}}\left({K},{X}\right)$

### Proof

Step Hyp Ref Expression
1 f1of1 ${⊢}{H}:{A}\underset{1-1 onto}{⟶}{B}\to {H}:{A}\underset{1-1}{⟶}{B}$
2 f1ores ${⊢}\left({H}:{A}\underset{1-1}{⟶}{B}\wedge {K}\subseteq {A}\right)\to \left({{H}↾}_{{K}}\right):{K}\underset{1-1 onto}{⟶}{H}\left[{K}\right]$
3 2 expcom ${⊢}{K}\subseteq {A}\to \left({H}:{A}\underset{1-1}{⟶}{B}\to \left({{H}↾}_{{K}}\right):{K}\underset{1-1 onto}{⟶}{H}\left[{K}\right]\right)$
4 1 3 syl5 ${⊢}{K}\subseteq {A}\to \left({H}:{A}\underset{1-1 onto}{⟶}{B}\to \left({{H}↾}_{{K}}\right):{K}\underset{1-1 onto}{⟶}{H}\left[{K}\right]\right)$
5 ssralv ${⊢}{K}\subseteq {A}\to \left(\forall {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}\left({a}{R}{b}↔{H}\left({a}\right){S}{H}\left({b}\right)\right)\to \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}\left({a}{R}{b}↔{H}\left({a}\right){S}{H}\left({b}\right)\right)\right)$
6 ssralv ${⊢}{K}\subseteq {A}\to \left(\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}\left({a}{R}{b}↔{H}\left({a}\right){S}{H}\left({b}\right)\right)\to \forall {b}\in {K}\phantom{\rule{.4em}{0ex}}\left({a}{R}{b}↔{H}\left({a}\right){S}{H}\left({b}\right)\right)\right)$
7 6 adantr ${⊢}\left({K}\subseteq {A}\wedge {a}\in {K}\right)\to \left(\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}\left({a}{R}{b}↔{H}\left({a}\right){S}{H}\left({b}\right)\right)\to \forall {b}\in {K}\phantom{\rule{.4em}{0ex}}\left({a}{R}{b}↔{H}\left({a}\right){S}{H}\left({b}\right)\right)\right)$
8 fvres ${⊢}{a}\in {K}\to \left({{H}↾}_{{K}}\right)\left({a}\right)={H}\left({a}\right)$
9 fvres ${⊢}{b}\in {K}\to \left({{H}↾}_{{K}}\right)\left({b}\right)={H}\left({b}\right)$
10 8 9 breqan12d ${⊢}\left({a}\in {K}\wedge {b}\in {K}\right)\to \left(\left({{H}↾}_{{K}}\right)\left({a}\right){S}\left({{H}↾}_{{K}}\right)\left({b}\right)↔{H}\left({a}\right){S}{H}\left({b}\right)\right)$
11 10 adantll ${⊢}\left(\left({K}\subseteq {A}\wedge {a}\in {K}\right)\wedge {b}\in {K}\right)\to \left(\left({{H}↾}_{{K}}\right)\left({a}\right){S}\left({{H}↾}_{{K}}\right)\left({b}\right)↔{H}\left({a}\right){S}{H}\left({b}\right)\right)$
12 11 bibi2d ${⊢}\left(\left({K}\subseteq {A}\wedge {a}\in {K}\right)\wedge {b}\in {K}\right)\to \left(\left({a}{R}{b}↔\left({{H}↾}_{{K}}\right)\left({a}\right){S}\left({{H}↾}_{{K}}\right)\left({b}\right)\right)↔\left({a}{R}{b}↔{H}\left({a}\right){S}{H}\left({b}\right)\right)\right)$
13 12 biimprd ${⊢}\left(\left({K}\subseteq {A}\wedge {a}\in {K}\right)\wedge {b}\in {K}\right)\to \left(\left({a}{R}{b}↔{H}\left({a}\right){S}{H}\left({b}\right)\right)\to \left({a}{R}{b}↔\left({{H}↾}_{{K}}\right)\left({a}\right){S}\left({{H}↾}_{{K}}\right)\left({b}\right)\right)\right)$
14 13 ralimdva ${⊢}\left({K}\subseteq {A}\wedge {a}\in {K}\right)\to \left(\forall {b}\in {K}\phantom{\rule{.4em}{0ex}}\left({a}{R}{b}↔{H}\left({a}\right){S}{H}\left({b}\right)\right)\to \forall {b}\in {K}\phantom{\rule{.4em}{0ex}}\left({a}{R}{b}↔\left({{H}↾}_{{K}}\right)\left({a}\right){S}\left({{H}↾}_{{K}}\right)\left({b}\right)\right)\right)$
15 7 14 syld ${⊢}\left({K}\subseteq {A}\wedge {a}\in {K}\right)\to \left(\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}\left({a}{R}{b}↔{H}\left({a}\right){S}{H}\left({b}\right)\right)\to \forall {b}\in {K}\phantom{\rule{.4em}{0ex}}\left({a}{R}{b}↔\left({{H}↾}_{{K}}\right)\left({a}\right){S}\left({{H}↾}_{{K}}\right)\left({b}\right)\right)\right)$
16 15 ralimdva ${⊢}{K}\subseteq {A}\to \left(\forall {a}\in {K}\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}\left({a}{R}{b}↔{H}\left({a}\right){S}{H}\left({b}\right)\right)\to \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}\forall {b}\in {K}\phantom{\rule{.4em}{0ex}}\left({a}{R}{b}↔\left({{H}↾}_{{K}}\right)\left({a}\right){S}\left({{H}↾}_{{K}}\right)\left({b}\right)\right)\right)$
17 5 16 syld ${⊢}{K}\subseteq {A}\to \left(\forall {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}\left({a}{R}{b}↔{H}\left({a}\right){S}{H}\left({b}\right)\right)\to \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}\forall {b}\in {K}\phantom{\rule{.4em}{0ex}}\left({a}{R}{b}↔\left({{H}↾}_{{K}}\right)\left({a}\right){S}\left({{H}↾}_{{K}}\right)\left({b}\right)\right)\right)$
18 4 17 anim12d ${⊢}{K}\subseteq {A}\to \left(\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \forall {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}\left({a}{R}{b}↔{H}\left({a}\right){S}{H}\left({b}\right)\right)\right)\to \left(\left({{H}↾}_{{K}}\right):{K}\underset{1-1 onto}{⟶}{H}\left[{K}\right]\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}\forall {b}\in {K}\phantom{\rule{.4em}{0ex}}\left({a}{R}{b}↔\left({{H}↾}_{{K}}\right)\left({a}\right){S}\left({{H}↾}_{{K}}\right)\left({b}\right)\right)\right)\right)$
19 df-isom ${⊢}{H}{Isom}_{{R},{S}}\left({A},{B}\right)↔\left({H}:{A}\underset{1-1 onto}{⟶}{B}\wedge \forall {a}\in {A}\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}\left({a}{R}{b}↔{H}\left({a}\right){S}{H}\left({b}\right)\right)\right)$
20 df-isom ${⊢}\left({{H}↾}_{{K}}\right){Isom}_{{R},{S}}\left({K},{H}\left[{K}\right]\right)↔\left(\left({{H}↾}_{{K}}\right):{K}\underset{1-1 onto}{⟶}{H}\left[{K}\right]\wedge \forall {a}\in {K}\phantom{\rule{.4em}{0ex}}\forall {b}\in {K}\phantom{\rule{.4em}{0ex}}\left({a}{R}{b}↔\left({{H}↾}_{{K}}\right)\left({a}\right){S}\left({{H}↾}_{{K}}\right)\left({b}\right)\right)\right)$
21 18 19 20 3imtr4g ${⊢}{K}\subseteq {A}\to \left({H}{Isom}_{{R},{S}}\left({A},{B}\right)\to \left({{H}↾}_{{K}}\right){Isom}_{{R},{S}}\left({K},{H}\left[{K}\right]\right)\right)$
22 21 impcom ${⊢}\left({H}{Isom}_{{R},{S}}\left({A},{B}\right)\wedge {K}\subseteq {A}\right)\to \left({{H}↾}_{{K}}\right){Isom}_{{R},{S}}\left({K},{H}\left[{K}\right]\right)$
23 isoeq5 ${⊢}{X}={H}\left[{K}\right]\to \left(\left({{H}↾}_{{K}}\right){Isom}_{{R},{S}}\left({K},{X}\right)↔\left({{H}↾}_{{K}}\right){Isom}_{{R},{S}}\left({K},{H}\left[{K}\right]\right)\right)$
24 22 23 syl5ibrcom ${⊢}\left({H}{Isom}_{{R},{S}}\left({A},{B}\right)\wedge {K}\subseteq {A}\right)\to \left({X}={H}\left[{K}\right]\to \left({{H}↾}_{{K}}\right){Isom}_{{R},{S}}\left({K},{X}\right)\right)$
25 24 3impia ${⊢}\left({H}{Isom}_{{R},{S}}\left({A},{B}\right)\wedge {K}\subseteq {A}\wedge {X}={H}\left[{K}\right]\right)\to \left({{H}↾}_{{K}}\right){Isom}_{{R},{S}}\left({K},{X}\right)$