Metamath Proof Explorer

Theorem isores3

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

Ref Expression
Assertion isores3 ⊢ H Isom R , S A B ∧ K ⊆ A ∧ X = H K → H ↾ K Isom R , S K X

Proof

Step Hyp Ref Expression
1 f1of1 ⊢ H : A ⟶ 1-1 onto B → H : A ⟶ 1-1 B
2 f1ores ⊢ H : A ⟶ 1-1 B ∧ K ⊆ A → H ↾ K : K ⟶ 1-1 onto H K
3 2 expcom ⊢ K ⊆ A → H : A ⟶ 1-1 B → H ↾ K : K ⟶ 1-1 onto H K
4 1 3 syl5 ⊢ K ⊆ A → H : A ⟶ 1-1 onto B → H ↾ K : K ⟶ 1-1 onto H K
5 ssralv ⊢ K ⊆ A → ∀ a ∈ A ∀ b ∈ A a R b ↔ H ⁡ a S H ⁡ b → ∀ a ∈ K ∀ b ∈ A a R b ↔ H ⁡ a S H ⁡ b
6 ssralv ⊢ K ⊆ A → ∀ b ∈ A a R b ↔ H ⁡ a S H ⁡ b → ∀ b ∈ K a R b ↔ H ⁡ a S H ⁡ b
7 6 adantr ⊢ K ⊆ A ∧ a ∈ K → ∀ b ∈ A a R b ↔ H ⁡ a S H ⁡ b → ∀ b ∈ K a R b ↔ H ⁡ a S H ⁡ 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 ⁡ a S H ↾ K ⁡ b ↔ H ⁡ a S H ⁡ b
11 10 adantll ⊢ K ⊆ A ∧ a ∈ K ∧ b ∈ K → H ↾ K ⁡ a S H ↾ K ⁡ b ↔ H ⁡ a S H ⁡ b
12 11 bibi2d ⊢ K ⊆ A ∧ a ∈ K ∧ b ∈ K → a R b ↔ H ↾ K ⁡ a S H ↾ K ⁡ b ↔ a R b ↔ H ⁡ a S H ⁡ b
13 12 biimprd ⊢ K ⊆ A ∧ a ∈ K ∧ b ∈ K → a R b ↔ H ⁡ a S H ⁡ b → a R b ↔ H ↾ K ⁡ a S H ↾ K ⁡ b
14 13 ralimdva ⊢ K ⊆ A ∧ a ∈ K → ∀ b ∈ K a R b ↔ H ⁡ a S H ⁡ b → ∀ b ∈ K a R b ↔ H ↾ K ⁡ a S H ↾ K ⁡ b
15 7 14 syld ⊢ K ⊆ A ∧ a ∈ K → ∀ b ∈ A a R b ↔ H ⁡ a S H ⁡ b → ∀ b ∈ K a R b ↔ H ↾ K ⁡ a S H ↾ K ⁡ b
16 15 ralimdva ⊢ K ⊆ A → ∀ a ∈ K ∀ b ∈ A a R b ↔ H ⁡ a S H ⁡ b → ∀ a ∈ K ∀ b ∈ K a R b ↔ H ↾ K ⁡ a S H ↾ K ⁡ b
17 5 16 syld ⊢ K ⊆ A → ∀ a ∈ A ∀ b ∈ A a R b ↔ H ⁡ a S H ⁡ b → ∀ a ∈ K ∀ b ∈ K a R b ↔ H ↾ K ⁡ a S H ↾ K ⁡ b
18 4 17 anim12d ⊢ K ⊆ A → H : A ⟶ 1-1 onto B ∧ ∀ a ∈ A ∀ b ∈ A a R b ↔ H ⁡ a S H ⁡ b → H ↾ K : K ⟶ 1-1 onto H K ∧ ∀ a ∈ K ∀ b ∈ K a R b ↔ H ↾ K ⁡ a S H ↾ K ⁡ b
19 df-isom ⊢ H Isom R , S A B ↔ H : A ⟶ 1-1 onto B ∧ ∀ a ∈ A ∀ b ∈ A a R b ↔ H ⁡ a S H ⁡ b
20 df-isom ⊢ H ↾ K Isom R , S K H K ↔ H ↾ K : K ⟶ 1-1 onto H K ∧ ∀ a ∈ K ∀ b ∈ K a R b ↔ H ↾ K ⁡ a S H ↾ K ⁡ b
21 18 19 20 3imtr4g ⊢ K ⊆ A → H Isom R , S A B → H ↾ K Isom R , S K H K
22 21 impcom ⊢ H Isom R , S A B ∧ K ⊆ A → H ↾ K Isom R , S K H K
23 isoeq5 ⊢ X = H K → H ↾ K Isom R , S K X ↔ H ↾ K Isom R , S K H K
24 22 23 syl5ibrcom ⊢ H Isom R , S A B ∧ K ⊆ A → X = H K → H ↾ K Isom R , S K X
25 24 3impia ⊢ H Isom R , S A B ∧ K ⊆ A ∧ X = H K → H ↾ K Isom R , S K X