This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isoini2

Description: Isomorphisms are isomorphisms on their initial segments. (Contributed by Mario Carneiro, 29-Mar-2014)

Ref Expression
Hypotheses isoini2.1 ⊢ 𝐶 = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
isoini2.2 ⊢ 𝐷 = ( 𝐵 ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝑋 ) } ) )
Assertion isoini2 ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝐻 ↾ 𝐶 ) Isom 𝑅 , 𝑆 ( 𝐶 , 𝐷 ) )

Proof

Step Hyp Ref Expression
1 isoini2.1 ⊢ 𝐶 = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
2 isoini2.2 ⊢ 𝐷 = ( 𝐵 ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝑋 ) } ) )
3 isof1o ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐻 : 𝐴 –1-1-onto→ 𝐵 )
4 f1of1 ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → 𝐻 : 𝐴 –1-1→ 𝐵 )
5 3 4 syl ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐻 : 𝐴 –1-1→ 𝐵 )
6 5 adantr ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝑋 ∈ 𝐴 ) → 𝐻 : 𝐴 –1-1→ 𝐵 )
7 inss1 ⊢ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ⊆ 𝐴
8 1 7 eqsstri ⊢ 𝐶 ⊆ 𝐴
9 f1ores ⊢ ( ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐻 ↾ 𝐶 ) : 𝐶 –1-1-onto→ ( 𝐻 “ 𝐶 ) )
10 6 8 9 sylancl ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝐻 ↾ 𝐶 ) : 𝐶 –1-1-onto→ ( 𝐻 “ 𝐶 ) )
11 isoini ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝐻 “ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ) = ( 𝐵 ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝑋 ) } ) ) )
12 1 imaeq2i ⊢ ( 𝐻 “ 𝐶 ) = ( 𝐻 “ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) )
13 11 12 2 3eqtr4g ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝐻 “ 𝐶 ) = 𝐷 )
14 13 f1oeq3d ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐻 ↾ 𝐶 ) : 𝐶 –1-1-onto→ ( 𝐻 “ 𝐶 ) ↔ ( 𝐻 ↾ 𝐶 ) : 𝐶 –1-1-onto→ 𝐷 ) )
15 10 14 mpbid ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝐻 ↾ 𝐶 ) : 𝐶 –1-1-onto→ 𝐷 )
16 df-isom ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) )
17 16 simprbi ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) )
18 17 adantr ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) )
19 ssralv ⊢ ( 𝐶 ⊆ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) → ∀ 𝑦 ∈ 𝐶 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) )
20 19 ralimdv ⊢ ( 𝐶 ⊆ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) )
21 8 18 20 mpsyl ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) )
22 ssralv ⊢ ( 𝐶 ⊆ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐶 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) )
23 8 21 22 mpsyl ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐶 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) )
24 fvres ⊢ ( 𝑥 ∈ 𝐶 → ( ( 𝐻 ↾ 𝐶 ) ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) )
25 fvres ⊢ ( 𝑦 ∈ 𝐶 → ( ( 𝐻 ↾ 𝐶 ) ‘ 𝑦 ) = ( 𝐻 ‘ 𝑦 ) )
26 24 25 breqan12d ⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ( ( ( 𝐻 ↾ 𝐶 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ↾ 𝐶 ) ‘ 𝑦 ) ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) )
27 26 bibi2d ⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻 ↾ 𝐶 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ↾ 𝐶 ) ‘ 𝑦 ) ) ↔ ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) )
28 27 ralbidva ⊢ ( 𝑥 ∈ 𝐶 → ( ∀ 𝑦 ∈ 𝐶 ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻 ↾ 𝐶 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ↾ 𝐶 ) ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝐶 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) )
29 28 ralbiia ⊢ ( ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐶 ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻 ↾ 𝐶 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ↾ 𝐶 ) ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐶 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) )
30 23 29 sylibr ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐶 ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻 ↾ 𝐶 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ↾ 𝐶 ) ‘ 𝑦 ) ) )
31 df-isom ⊢ ( ( 𝐻 ↾ 𝐶 ) Isom 𝑅 , 𝑆 ( 𝐶 , 𝐷 ) ↔ ( ( 𝐻 ↾ 𝐶 ) : 𝐶 –1-1-onto→ 𝐷 ∧ ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐶 ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻 ↾ 𝐶 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻 ↾ 𝐶 ) ‘ 𝑦 ) ) ) )
32 15 30 31 sylanbrc ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝐻 ↾ 𝐶 ) Isom 𝑅 , 𝑆 ( 𝐶 , 𝐷 ) )