Metamath Proof Explorer

Theorem f1oiso2

Description: Any one-to-one onto function determines an isomorphism with an induced relation S . (Contributed by Mario Carneiro, 9-Mar-2013)

Ref Expression
Hypothesis f1oiso2.1 ⊢ 𝑆 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ◡ 𝐻 ‘ 𝑥 ) 𝑅 ( ◡ 𝐻 ‘ 𝑦 ) ) }
Assertion f1oiso2 ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )

Proof

Step Hyp Ref Expression
1 f1oiso2.1 ⊢ 𝑆 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ◡ 𝐻 ‘ 𝑥 ) 𝑅 ( ◡ 𝐻 ‘ 𝑦 ) ) }
2 f1ocnvdm ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( ◡ 𝐻 ‘ 𝑥 ) ∈ 𝐴 )
3 2 adantrr ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ◡ 𝐻 ‘ 𝑥 ) ∈ 𝐴 )
4 3 3adant3 ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ◡ 𝐻 ‘ 𝑥 ) 𝑅 ( ◡ 𝐻 ‘ 𝑦 ) ) → ( ◡ 𝐻 ‘ 𝑥 ) ∈ 𝐴 )
5 f1ocnvdm ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ◡ 𝐻 ‘ 𝑦 ) ∈ 𝐴 )
6 5 adantrl ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ◡ 𝐻 ‘ 𝑦 ) ∈ 𝐴 )
7 6 3adant3 ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ◡ 𝐻 ‘ 𝑥 ) 𝑅 ( ◡ 𝐻 ‘ 𝑦 ) ) → ( ◡ 𝐻 ‘ 𝑦 ) ∈ 𝐴 )
8 f1ocnvfv2 ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑥 ) ) = 𝑥 )
9 8 eqcomd ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 = ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑥 ) ) )
10 f1ocnvfv2 ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑦 ) ) = 𝑦 )
11 10 eqcomd ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 = ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑦 ) ) )
12 9 11 anim12dan ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 = ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑥 ) ) ∧ 𝑦 = ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑦 ) ) ) )
13 12 3adant3 ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ◡ 𝐻 ‘ 𝑥 ) 𝑅 ( ◡ 𝐻 ‘ 𝑦 ) ) → ( 𝑥 = ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑥 ) ) ∧ 𝑦 = ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑦 ) ) ) )
14 simp3 ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ◡ 𝐻 ‘ 𝑥 ) 𝑅 ( ◡ 𝐻 ‘ 𝑦 ) ) → ( ◡ 𝐻 ‘ 𝑥 ) 𝑅 ( ◡ 𝐻 ‘ 𝑦 ) )
15 fveq2 ⊢ ( 𝑤 = ( ◡ 𝐻 ‘ 𝑦 ) → ( 𝐻 ‘ 𝑤 ) = ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑦 ) ) )
16 15 eqeq2d ⊢ ( 𝑤 = ( ◡ 𝐻 ‘ 𝑦 ) → ( 𝑦 = ( 𝐻 ‘ 𝑤 ) ↔ 𝑦 = ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑦 ) ) ) )
17 16 anbi2d ⊢ ( 𝑤 = ( ◡ 𝐻 ‘ 𝑦 ) → ( ( 𝑥 = ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑥 ) ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ↔ ( 𝑥 = ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑥 ) ) ∧ 𝑦 = ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑦 ) ) ) ) )
18 breq2 ⊢ ( 𝑤 = ( ◡ 𝐻 ‘ 𝑦 ) → ( ( ◡ 𝐻 ‘ 𝑥 ) 𝑅 𝑤 ↔ ( ◡ 𝐻 ‘ 𝑥 ) 𝑅 ( ◡ 𝐻 ‘ 𝑦 ) ) )
19 17 18 anbi12d ⊢ ( 𝑤 = ( ◡ 𝐻 ‘ 𝑦 ) → ( ( ( 𝑥 = ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑥 ) ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ ( ◡ 𝐻 ‘ 𝑥 ) 𝑅 𝑤 ) ↔ ( ( 𝑥 = ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑥 ) ) ∧ 𝑦 = ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑦 ) ) ) ∧ ( ◡ 𝐻 ‘ 𝑥 ) 𝑅 ( ◡ 𝐻 ‘ 𝑦 ) ) ) )
20 19 rspcev ⊢ ( ( ( ◡ 𝐻 ‘ 𝑦 ) ∈ 𝐴 ∧ ( ( 𝑥 = ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑥 ) ) ∧ 𝑦 = ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑦 ) ) ) ∧ ( ◡ 𝐻 ‘ 𝑥 ) 𝑅 ( ◡ 𝐻 ‘ 𝑦 ) ) ) → ∃ 𝑤 ∈ 𝐴 ( ( 𝑥 = ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑥 ) ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ ( ◡ 𝐻 ‘ 𝑥 ) 𝑅 𝑤 ) )
21 7 13 14 20 syl12anc ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ◡ 𝐻 ‘ 𝑥 ) 𝑅 ( ◡ 𝐻 ‘ 𝑦 ) ) → ∃ 𝑤 ∈ 𝐴 ( ( 𝑥 = ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑥 ) ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ ( ◡ 𝐻 ‘ 𝑥 ) 𝑅 𝑤 ) )
22 fveq2 ⊢ ( 𝑧 = ( ◡ 𝐻 ‘ 𝑥 ) → ( 𝐻 ‘ 𝑧 ) = ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑥 ) ) )
23 22 eqeq2d ⊢ ( 𝑧 = ( ◡ 𝐻 ‘ 𝑥 ) → ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ↔ 𝑥 = ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑥 ) ) ) )
24 23 anbi1d ⊢ ( 𝑧 = ( ◡ 𝐻 ‘ 𝑥 ) → ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ↔ ( 𝑥 = ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑥 ) ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ) )
25 breq1 ⊢ ( 𝑧 = ( ◡ 𝐻 ‘ 𝑥 ) → ( 𝑧 𝑅 𝑤 ↔ ( ◡ 𝐻 ‘ 𝑥 ) 𝑅 𝑤 ) )
26 24 25 anbi12d ⊢ ( 𝑧 = ( ◡ 𝐻 ‘ 𝑥 ) → ( ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) ↔ ( ( 𝑥 = ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑥 ) ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ ( ◡ 𝐻 ‘ 𝑥 ) 𝑅 𝑤 ) ) )
27 26 rexbidv ⊢ ( 𝑧 = ( ◡ 𝐻 ‘ 𝑥 ) → ( ∃ 𝑤 ∈ 𝐴 ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) ↔ ∃ 𝑤 ∈ 𝐴 ( ( 𝑥 = ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑥 ) ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ ( ◡ 𝐻 ‘ 𝑥 ) 𝑅 𝑤 ) ) )
28 27 rspcev ⊢ ( ( ( ◡ 𝐻 ‘ 𝑥 ) ∈ 𝐴 ∧ ∃ 𝑤 ∈ 𝐴 ( ( 𝑥 = ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑥 ) ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ ( ◡ 𝐻 ‘ 𝑥 ) 𝑅 𝑤 ) ) → ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) )
29 4 21 28 syl2anc ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ◡ 𝐻 ‘ 𝑥 ) 𝑅 ( ◡ 𝐻 ‘ 𝑦 ) ) → ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) )
30 29 3expib ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ◡ 𝐻 ‘ 𝑥 ) 𝑅 ( ◡ 𝐻 ‘ 𝑦 ) ) → ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) ) )
31 simp3ll ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) ) → 𝑥 = ( 𝐻 ‘ 𝑧 ) )
32 simp1 ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) ) → 𝐻 : 𝐴 –1-1-onto→ 𝐵 )
33 simp2l ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) ) → 𝑧 ∈ 𝐴 )
34 f1of ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → 𝐻 : 𝐴 ⟶ 𝐵 )
35 34 ffvelcdmda ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑧 ) ∈ 𝐵 )
36 32 33 35 syl2anc ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) ) → ( 𝐻 ‘ 𝑧 ) ∈ 𝐵 )
37 31 36 eqeltrd ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) ) → 𝑥 ∈ 𝐵 )
38 simp3lr ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) ) → 𝑦 = ( 𝐻 ‘ 𝑤 ) )
39 simp2r ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) ) → 𝑤 ∈ 𝐴 )
40 34 ffvelcdmda ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑤 ) ∈ 𝐵 )
41 32 39 40 syl2anc ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) ) → ( 𝐻 ‘ 𝑤 ) ∈ 𝐵 )
42 38 41 eqeltrd ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) ) → 𝑦 ∈ 𝐵 )
43 simp3r ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) ) → 𝑧 𝑅 𝑤 )
44 31 eqcomd ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) ) → ( 𝐻 ‘ 𝑧 ) = 𝑥 )
45 f1ocnvfv ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑧 ) = 𝑥 → ( ◡ 𝐻 ‘ 𝑥 ) = 𝑧 ) )
46 32 33 45 syl2anc ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) ) → ( ( 𝐻 ‘ 𝑧 ) = 𝑥 → ( ◡ 𝐻 ‘ 𝑥 ) = 𝑧 ) )
47 44 46 mpd ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) ) → ( ◡ 𝐻 ‘ 𝑥 ) = 𝑧 )
48 38 eqcomd ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) ) → ( 𝐻 ‘ 𝑤 ) = 𝑦 )
49 f1ocnvfv ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑤 ) = 𝑦 → ( ◡ 𝐻 ‘ 𝑦 ) = 𝑤 ) )
50 32 39 49 syl2anc ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) ) → ( ( 𝐻 ‘ 𝑤 ) = 𝑦 → ( ◡ 𝐻 ‘ 𝑦 ) = 𝑤 ) )
51 48 50 mpd ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) ) → ( ◡ 𝐻 ‘ 𝑦 ) = 𝑤 )
52 43 47 51 3brtr4d ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) ) → ( ◡ 𝐻 ‘ 𝑥 ) 𝑅 ( ◡ 𝐻 ‘ 𝑦 ) )
53 37 42 52 jca31 ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ◡ 𝐻 ‘ 𝑥 ) 𝑅 ( ◡ 𝐻 ‘ 𝑦 ) ) )
54 53 3exp ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ◡ 𝐻 ‘ 𝑥 ) 𝑅 ( ◡ 𝐻 ‘ 𝑦 ) ) ) ) )
55 54 rexlimdvv ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → ( ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ◡ 𝐻 ‘ 𝑥 ) 𝑅 ( ◡ 𝐻 ‘ 𝑦 ) ) ) )
56 30 55 impbid ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ◡ 𝐻 ‘ 𝑥 ) 𝑅 ( ◡ 𝐻 ‘ 𝑦 ) ) ↔ ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) ) )
57 56 opabbidv ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ◡ 𝐻 ‘ 𝑥 ) 𝑅 ( ◡ 𝐻 ‘ 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) } )
58 1 57 eqtrid ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → 𝑆 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) } )
59 f1oiso ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑆 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( ( 𝑥 = ( 𝐻 ‘ 𝑧 ) ∧ 𝑦 = ( 𝐻 ‘ 𝑤 ) ) ∧ 𝑧 𝑅 𝑤 ) } ) → 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
60 58 59 mpdan ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )