Metamath Proof Explorer

Theorem isoini

Description: Isomorphisms preserve initial segments. Proposition 6.31(2) of TakeutiZaring p. 33. (Contributed by NM, 20-Apr-2004)

Ref Expression
Assertion isoini ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐷 ∈ 𝐴 ) → ( 𝐻 “ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) ) = ( 𝐵 ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) )

Proof

Step Hyp Ref Expression
1 dfima2 ⊢ ( 𝐻 “ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) ) = { 𝑦 ∣ ∃ 𝑥 ∈ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) 𝑥 𝐻 𝑦 }
2 elin ⊢ ( 𝑦 ∈ ( 𝐵 ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) )
3 isof1o ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐻 : 𝐴 –1-1-onto→ 𝐵 )
4 f1ofo ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → 𝐻 : 𝐴 –onto→ 𝐵 )
5 forn ⊢ ( 𝐻 : 𝐴 –onto→ 𝐵 → ran 𝐻 = 𝐵 )
6 5 eleq2d ⊢ ( 𝐻 : 𝐴 –onto→ 𝐵 → ( 𝑦 ∈ ran 𝐻 ↔ 𝑦 ∈ 𝐵 ) )
7 3 4 6 3syl ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝑦 ∈ ran 𝐻 ↔ 𝑦 ∈ 𝐵 ) )
8 f1ofn ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → 𝐻 Fn 𝐴 )
9 fvelrnb ⊢ ( 𝐻 Fn 𝐴 → ( 𝑦 ∈ ran 𝐻 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = 𝑦 ) )
10 3 8 9 3syl ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝑦 ∈ ran 𝐻 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = 𝑦 ) )
11 7 10 bitr3d ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝑦 ∈ 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = 𝑦 ) )
12 fvex ⊢ ( 𝐻 ‘ 𝐷 ) ∈ V
13 vex ⊢ 𝑦 ∈ V
14 13 eliniseg ⊢ ( ( 𝐻 ‘ 𝐷 ) ∈ V → ( 𝑦 ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ↔ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) )
15 12 14 mp1i ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝑦 ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ↔ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) )
16 11 15 anbi12d ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) ↔ ( ∃ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) ) )
17 16 adantr ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐷 ∈ 𝐴 ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) ↔ ( ∃ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) ) )
18 elin ⊢ ( 𝑥 ∈ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) ) )
19 vex ⊢ 𝑥 ∈ V
20 19 eliniseg ⊢ ( 𝐷 ∈ 𝐴 → ( 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) ↔ 𝑥 𝑅 𝐷 ) )
21 20 anbi2d ⊢ ( 𝐷 ∈ 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( ◡ 𝑅 “ { 𝐷 } ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝐷 ) ) )
22 18 21 syl5bb ⊢ ( 𝐷 ∈ 𝐴 → ( 𝑥 ∈ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝐷 ) ) )
23 22 anbi1d ⊢ ( 𝐷 ∈ 𝐴 → ( ( 𝑥 ∈ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) ∧ 𝑥 𝐻 𝑦 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝐷 ) ∧ 𝑥 𝐻 𝑦 ) ) )
24 anass ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝐷 ) ∧ 𝑥 𝐻 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 𝑅 𝐷 ∧ 𝑥 𝐻 𝑦 ) ) )
25 23 24 bitrdi ⊢ ( 𝐷 ∈ 𝐴 → ( ( 𝑥 ∈ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) ∧ 𝑥 𝐻 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 𝑅 𝐷 ∧ 𝑥 𝐻 𝑦 ) ) ) )
26 25 adantl ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐷 ∈ 𝐴 ) → ( ( 𝑥 ∈ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) ∧ 𝑥 𝐻 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 𝑅 𝐷 ∧ 𝑥 𝐻 𝑦 ) ) ) )
27 isorel ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝑥 𝑅 𝐷 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝐷 ) ) )
28 3 8 syl ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐻 Fn 𝐴 )
29 fnbrfvb ⊢ ( ( 𝐻 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑥 ) = 𝑦 ↔ 𝑥 𝐻 𝑦 ) )
30 29 bicomd ⊢ ( ( 𝐻 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 𝐻 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) = 𝑦 ) )
31 28 30 sylan ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 𝐻 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) = 𝑦 ) )
32 31 adantrr ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝑥 𝐻 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) = 𝑦 ) )
33 27 32 anbi12d ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( 𝑥 𝑅 𝐷 ∧ 𝑥 𝐻 𝑦 ) ↔ ( ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝐷 ) ∧ ( 𝐻 ‘ 𝑥 ) = 𝑦 ) ) )
34 ancom ⊢ ( ( ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝐷 ) ∧ ( 𝐻 ‘ 𝑥 ) = 𝑦 ) ↔ ( ( 𝐻 ‘ 𝑥 ) = 𝑦 ∧ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝐷 ) ) )
35 breq1 ⊢ ( ( 𝐻 ‘ 𝑥 ) = 𝑦 → ( ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝐷 ) ↔ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) )
36 35 pm5.32i ⊢ ( ( ( 𝐻 ‘ 𝑥 ) = 𝑦 ∧ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝐷 ) ) ↔ ( ( 𝐻 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) )
37 34 36 bitri ⊢ ( ( ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝐷 ) ∧ ( 𝐻 ‘ 𝑥 ) = 𝑦 ) ↔ ( ( 𝐻 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) )
38 33 37 bitrdi ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( 𝑥 𝑅 𝐷 ∧ 𝑥 𝐻 𝑦 ) ↔ ( ( 𝐻 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) ) )
39 38 exp32 ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝑥 ∈ 𝐴 → ( 𝐷 ∈ 𝐴 → ( ( 𝑥 𝑅 𝐷 ∧ 𝑥 𝐻 𝑦 ) ↔ ( ( 𝐻 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) ) ) ) )
40 39 com23 ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝐷 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → ( ( 𝑥 𝑅 𝐷 ∧ 𝑥 𝐻 𝑦 ) ↔ ( ( 𝐻 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) ) ) ) )
41 40 imp ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐷 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐴 → ( ( 𝑥 𝑅 𝐷 ∧ 𝑥 𝐻 𝑦 ) ↔ ( ( 𝐻 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) ) ) )
42 41 pm5.32d ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐷 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 𝑅 𝐷 ∧ 𝑥 𝐻 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝐻 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) ) ) )
43 26 42 bitrd ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐷 ∈ 𝐴 ) → ( ( 𝑥 ∈ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) ∧ 𝑥 𝐻 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝐻 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) ) ) )
44 43 rexbidv2 ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐷 ∈ 𝐴 ) → ( ∃ 𝑥 ∈ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) 𝑥 𝐻 𝑦 ↔ ∃ 𝑥 ∈ 𝐴 ( ( 𝐻 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) ) )
45 r19.41v ⊢ ( ∃ 𝑥 ∈ 𝐴 ( ( 𝐻 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) ↔ ( ∃ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) )
46 44 45 bitrdi ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐷 ∈ 𝐴 ) → ( ∃ 𝑥 ∈ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) 𝑥 𝐻 𝑦 ↔ ( ∃ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = 𝑦 ∧ 𝑦 𝑆 ( 𝐻 ‘ 𝐷 ) ) ) )
47 17 46 bitr4d ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐷 ∈ 𝐴 ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) ↔ ∃ 𝑥 ∈ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) 𝑥 𝐻 𝑦 ) )
48 2 47 syl5bb ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐷 ∈ 𝐴 ) → ( 𝑦 ∈ ( 𝐵 ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) ↔ ∃ 𝑥 ∈ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) 𝑥 𝐻 𝑦 ) )
49 48 abbi2dv ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐷 ∈ 𝐴 ) → ( 𝐵 ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) = { 𝑦 ∣ ∃ 𝑥 ∈ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) 𝑥 𝐻 𝑦 } )
50 1 49 eqtr4id ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐷 ∈ 𝐴 ) → ( 𝐻 “ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝐷 } ) ) ) = ( 𝐵 ∩ ( ◡ 𝑆 “ { ( 𝐻 ‘ 𝐷 ) } ) ) )