Metamath Proof Explorer

Theorem isores3

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

Ref Expression
Assertion isores3 ⊢HIsomR,SAB∧K⊆A∧X=HK→H↾KIsomR,SKX

Proof

Step Hyp Ref Expression
1 f1of1 ⊢H:A⟶1-1 ontoB→H:A⟶1-1B
2 f1ores ⊢H:A⟶1-1B∧K⊆A→H↾K:K⟶1-1 ontoHK
3 2 expcom ⊢K⊆A→H:A⟶1-1B→H↾K:K⟶1-1 ontoHK
4 1 3 syl5 ⊢K⊆A→H:A⟶1-1 ontoB→H↾K:K⟶1-1 ontoHK
5 ssralv ⊢K⊆A→∀a∈A∀b∈AaRb↔H⁡aSH⁡b→∀a∈K∀b∈AaRb↔H⁡aSH⁡b
6 ssralv ⊢K⊆A→∀b∈AaRb↔H⁡aSH⁡b→∀b∈KaRb↔H⁡aSH⁡b
7 6 adantr ⊢K⊆A∧a∈K→∀b∈AaRb↔H⁡aSH⁡b→∀b∈KaRb↔H⁡aSH⁡b
8 fvres ⊢a∈K→H↾K⁡a=H⁡a
9 fvres ⊢b∈K→H↾K⁡b=H⁡b
10 8 9 breqan12d ⊢a∈K∧b∈K→H↾K⁡aSH↾K⁡b↔H⁡aSH⁡b
11 10 adantll ⊢K⊆A∧a∈K∧b∈K→H↾K⁡aSH↾K⁡b↔H⁡aSH⁡b
12 11 bibi2d ⊢K⊆A∧a∈K∧b∈K→aRb↔H↾K⁡aSH↾K⁡b↔aRb↔H⁡aSH⁡b
13 12 biimprd ⊢K⊆A∧a∈K∧b∈K→aRb↔H⁡aSH⁡b→aRb↔H↾K⁡aSH↾K⁡b
14 13 ralimdva ⊢K⊆A∧a∈K→∀b∈KaRb↔H⁡aSH⁡b→∀b∈KaRb↔H↾K⁡aSH↾K⁡b
15 7 14 syld ⊢K⊆A∧a∈K→∀b∈AaRb↔H⁡aSH⁡b→∀b∈KaRb↔H↾K⁡aSH↾K⁡b
16 15 ralimdva ⊢K⊆A→∀a∈K∀b∈AaRb↔H⁡aSH⁡b→∀a∈K∀b∈KaRb↔H↾K⁡aSH↾K⁡b
17 5 16 syld ⊢K⊆A→∀a∈A∀b∈AaRb↔H⁡aSH⁡b→∀a∈K∀b∈KaRb↔H↾K⁡aSH↾K⁡b
18 4 17 anim12d ⊢K⊆A→H:A⟶1-1 ontoB∧∀a∈A∀b∈AaRb↔H⁡aSH⁡b→H↾K:K⟶1-1 ontoHK∧∀a∈K∀b∈KaRb↔H↾K⁡aSH↾K⁡b
19 df-isom ⊢HIsomR,SAB↔H:A⟶1-1 ontoB∧∀a∈A∀b∈AaRb↔H⁡aSH⁡b
20 df-isom ⊢H↾KIsomR,SKHK↔H↾K:K⟶1-1 ontoHK∧∀a∈K∀b∈KaRb↔H↾K⁡aSH↾K⁡b
21 18 19 20 3imtr4g ⊢K⊆A→HIsomR,SAB→H↾KIsomR,SKHK
22 21 impcom ⊢HIsomR,SAB∧K⊆A→H↾KIsomR,SKHK
23 isoeq5 ⊢X=HK→H↾KIsomR,SKX↔H↾KIsomR,SKHK
24 22 23 syl5ibrcom ⊢HIsomR,SAB∧K⊆A→X=HK→H↾KIsomR,SKX
25 24 3impia ⊢HIsomR,SAB∧K⊆A∧X=HK→H↾KIsomR,SKX