Metamath Proof Explorer

Theorem f1oiso

Description: Any one-to-one onto function determines an isomorphism with an induced relation S . Proposition 6.33 of TakeutiZaring p. 34. (Contributed by NM, 30-Apr-2004)

Ref Expression
Assertion f1oiso ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑆 = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝑧 = ( 𝐻 ‘ 𝑥 ) ∧ 𝑤 = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) } ) → 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑆 = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝑧 = ( 𝐻 ‘ 𝑥 ) ∧ 𝑤 = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) } ) → 𝐻 : 𝐴 –1-1-onto→ 𝐵 )
2 f1of1 ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → 𝐻 : 𝐴 –1-1→ 𝐵 )
3 df-br ⊢ ( ( 𝐻 ‘ 𝑣 ) 𝑆 ( 𝐻 ‘ 𝑢 ) ↔ ⟨ ( 𝐻 ‘ 𝑣 ) , ( 𝐻 ‘ 𝑢 ) ⟩ ∈ 𝑆 )
4 eleq2 ⊢ ( 𝑆 = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝑧 = ( 𝐻 ‘ 𝑥 ) ∧ 𝑤 = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) } → ( ⟨ ( 𝐻 ‘ 𝑣 ) , ( 𝐻 ‘ 𝑢 ) ⟩ ∈ 𝑆 ↔ ⟨ ( 𝐻 ‘ 𝑣 ) , ( 𝐻 ‘ 𝑢 ) ⟩ ∈ { ⟨ 𝑧 , 𝑤 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝑧 = ( 𝐻 ‘ 𝑥 ) ∧ 𝑤 = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) } ) )
5 fvex ⊢ ( 𝐻 ‘ 𝑣 ) ∈ V
6 fvex ⊢ ( 𝐻 ‘ 𝑢 ) ∈ V
7 eqeq1 ⊢ ( 𝑧 = ( 𝐻 ‘ 𝑣 ) → ( 𝑧 = ( 𝐻 ‘ 𝑥 ) ↔ ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑥 ) ) )
8 7 anbi1d ⊢ ( 𝑧 = ( 𝐻 ‘ 𝑣 ) → ( ( 𝑧 = ( 𝐻 ‘ 𝑥 ) ∧ 𝑤 = ( 𝐻 ‘ 𝑦 ) ) ↔ ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑥 ) ∧ 𝑤 = ( 𝐻 ‘ 𝑦 ) ) ) )
9 8 anbi1d ⊢ ( 𝑧 = ( 𝐻 ‘ 𝑣 ) → ( ( ( 𝑧 = ( 𝐻 ‘ 𝑥 ) ∧ 𝑤 = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) ↔ ( ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑥 ) ∧ 𝑤 = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) ) )
10 9 2rexbidv ⊢ ( 𝑧 = ( 𝐻 ‘ 𝑣 ) → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝑧 = ( 𝐻 ‘ 𝑥 ) ∧ 𝑤 = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑥 ) ∧ 𝑤 = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) ) )
11 eqeq1 ⊢ ( 𝑤 = ( 𝐻 ‘ 𝑢 ) → ( 𝑤 = ( 𝐻 ‘ 𝑦 ) ↔ ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ) )
12 11 anbi2d ⊢ ( 𝑤 = ( 𝐻 ‘ 𝑢 ) → ( ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑥 ) ∧ 𝑤 = ( 𝐻 ‘ 𝑦 ) ) ↔ ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑥 ) ∧ ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ) ) )
13 12 anbi1d ⊢ ( 𝑤 = ( 𝐻 ‘ 𝑢 ) → ( ( ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑥 ) ∧ 𝑤 = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) ↔ ( ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑥 ) ∧ ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) ) )
14 13 2rexbidv ⊢ ( 𝑤 = ( 𝐻 ‘ 𝑢 ) → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑥 ) ∧ 𝑤 = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑥 ) ∧ ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) ) )
15 5 6 10 14 opelopab ⊢ ( ⟨ ( 𝐻 ‘ 𝑣 ) , ( 𝐻 ‘ 𝑢 ) ⟩ ∈ { ⟨ 𝑧 , 𝑤 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝑧 = ( 𝐻 ‘ 𝑥 ) ∧ 𝑤 = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) } ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑥 ) ∧ ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) )
16 anass ⊢ ( ( ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑥 ) ∧ ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) ↔ ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑥 ) ∧ ( ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ∧ 𝑥 𝑅 𝑦 ) ) )
17 f1fveq ⊢ ( ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) → ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑥 ) ↔ 𝑣 = 𝑥 ) )
18 equcom ⊢ ( 𝑣 = 𝑥 ↔ 𝑥 = 𝑣 )
19 17 18 syl6bb ⊢ ( ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) → ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑥 ) ↔ 𝑥 = 𝑣 ) )
20 19 anassrs ⊢ ( ( ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑥 ) ↔ 𝑥 = 𝑣 ) )
21 20 anbi1d ⊢ ( ( ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑥 ) ∧ ( ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ∧ 𝑥 𝑅 𝑦 ) ) ↔ ( 𝑥 = 𝑣 ∧ ( ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ∧ 𝑥 𝑅 𝑦 ) ) ) )
22 16 21 syl5bb ⊢ ( ( ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑥 ) ∧ ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) ↔ ( 𝑥 = 𝑣 ∧ ( ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ∧ 𝑥 𝑅 𝑦 ) ) ) )
23 22 rexbidv ⊢ ( ( ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑦 ∈ 𝐴 ( ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑥 ) ∧ ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) ↔ ∃ 𝑦 ∈ 𝐴 ( 𝑥 = 𝑣 ∧ ( ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ∧ 𝑥 𝑅 𝑦 ) ) ) )
24 r19.42v ⊢ ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 = 𝑣 ∧ ( ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ∧ 𝑥 𝑅 𝑦 ) ) ↔ ( 𝑥 = 𝑣 ∧ ∃ 𝑦 ∈ 𝐴 ( ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ∧ 𝑥 𝑅 𝑦 ) ) )
25 23 24 syl6bb ⊢ ( ( ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑦 ∈ 𝐴 ( ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑥 ) ∧ ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) ↔ ( 𝑥 = 𝑣 ∧ ∃ 𝑦 ∈ 𝐴 ( ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ∧ 𝑥 𝑅 𝑦 ) ) ) )
26 25 rexbidva ⊢ ( ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ 𝑣 ∈ 𝐴 ) → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑥 ) ∧ ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑥 = 𝑣 ∧ ∃ 𝑦 ∈ 𝐴 ( ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ∧ 𝑥 𝑅 𝑦 ) ) ) )
27 breq1 ⊢ ( 𝑥 = 𝑣 → ( 𝑥 𝑅 𝑦 ↔ 𝑣 𝑅 𝑦 ) )
28 27 anbi2d ⊢ ( 𝑥 = 𝑣 → ( ( ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ∧ 𝑥 𝑅 𝑦 ) ↔ ( ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ∧ 𝑣 𝑅 𝑦 ) ) )
29 28 rexbidv ⊢ ( 𝑥 = 𝑣 → ( ∃ 𝑦 ∈ 𝐴 ( ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ∧ 𝑥 𝑅 𝑦 ) ↔ ∃ 𝑦 ∈ 𝐴 ( ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ∧ 𝑣 𝑅 𝑦 ) ) )
30 29 ceqsrexv ⊢ ( 𝑣 ∈ 𝐴 → ( ∃ 𝑥 ∈ 𝐴 ( 𝑥 = 𝑣 ∧ ∃ 𝑦 ∈ 𝐴 ( ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ∧ 𝑥 𝑅 𝑦 ) ) ↔ ∃ 𝑦 ∈ 𝐴 ( ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ∧ 𝑣 𝑅 𝑦 ) ) )
31 30 adantl ⊢ ( ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ 𝑣 ∈ 𝐴 ) → ( ∃ 𝑥 ∈ 𝐴 ( 𝑥 = 𝑣 ∧ ∃ 𝑦 ∈ 𝐴 ( ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ∧ 𝑥 𝑅 𝑦 ) ) ↔ ∃ 𝑦 ∈ 𝐴 ( ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ∧ 𝑣 𝑅 𝑦 ) ) )
32 26 31 bitrd ⊢ ( ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ 𝑣 ∈ 𝐴 ) → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑥 ) ∧ ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) ↔ ∃ 𝑦 ∈ 𝐴 ( ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ∧ 𝑣 𝑅 𝑦 ) ) )
33 f1fveq ⊢ ( ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ↔ 𝑢 = 𝑦 ) )
34 equcom ⊢ ( 𝑢 = 𝑦 ↔ 𝑦 = 𝑢 )
35 33 34 syl6bb ⊢ ( ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ↔ 𝑦 = 𝑢 ) )
36 35 anassrs ⊢ ( ( ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ↔ 𝑦 = 𝑢 ) )
37 36 anbi1d ⊢ ( ( ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ( ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ∧ 𝑣 𝑅 𝑦 ) ↔ ( 𝑦 = 𝑢 ∧ 𝑣 𝑅 𝑦 ) ) )
38 37 rexbidva ⊢ ( ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ 𝑢 ∈ 𝐴 ) → ( ∃ 𝑦 ∈ 𝐴 ( ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ∧ 𝑣 𝑅 𝑦 ) ↔ ∃ 𝑦 ∈ 𝐴 ( 𝑦 = 𝑢 ∧ 𝑣 𝑅 𝑦 ) ) )
39 breq2 ⊢ ( 𝑦 = 𝑢 → ( 𝑣 𝑅 𝑦 ↔ 𝑣 𝑅 𝑢 ) )
40 39 ceqsrexv ⊢ ( 𝑢 ∈ 𝐴 → ( ∃ 𝑦 ∈ 𝐴 ( 𝑦 = 𝑢 ∧ 𝑣 𝑅 𝑦 ) ↔ 𝑣 𝑅 𝑢 ) )
41 40 adantl ⊢ ( ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ 𝑢 ∈ 𝐴 ) → ( ∃ 𝑦 ∈ 𝐴 ( 𝑦 = 𝑢 ∧ 𝑣 𝑅 𝑦 ) ↔ 𝑣 𝑅 𝑢 ) )
42 38 41 bitrd ⊢ ( ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ 𝑢 ∈ 𝐴 ) → ( ∃ 𝑦 ∈ 𝐴 ( ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ∧ 𝑣 𝑅 𝑦 ) ↔ 𝑣 𝑅 𝑢 ) )
43 32 42 sylan9bb ⊢ ( ( ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ 𝑣 ∈ 𝐴 ) ∧ ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ 𝑢 ∈ 𝐴 ) ) → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑥 ) ∧ ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) ↔ 𝑣 𝑅 𝑢 ) )
44 43 anandis ⊢ ( ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ) ) → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑥 ) ∧ ( 𝐻 ‘ 𝑢 ) = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) ↔ 𝑣 𝑅 𝑢 ) )
45 15 44 syl5bb ⊢ ( ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ) ) → ( ⟨ ( 𝐻 ‘ 𝑣 ) , ( 𝐻 ‘ 𝑢 ) ⟩ ∈ { ⟨ 𝑧 , 𝑤 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝑧 = ( 𝐻 ‘ 𝑥 ) ∧ 𝑤 = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) } ↔ 𝑣 𝑅 𝑢 ) )
46 4 45 sylan9bbr ⊢ ( ( ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ) ) ∧ 𝑆 = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝑧 = ( 𝐻 ‘ 𝑥 ) ∧ 𝑤 = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) } ) → ( ⟨ ( 𝐻 ‘ 𝑣 ) , ( 𝐻 ‘ 𝑢 ) ⟩ ∈ 𝑆 ↔ 𝑣 𝑅 𝑢 ) )
47 46 an32s ⊢ ( ( ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ 𝑆 = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝑧 = ( 𝐻 ‘ 𝑥 ) ∧ 𝑤 = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) } ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ) ) → ( ⟨ ( 𝐻 ‘ 𝑣 ) , ( 𝐻 ‘ 𝑢 ) ⟩ ∈ 𝑆 ↔ 𝑣 𝑅 𝑢 ) )
48 3 47 syl5rbb ⊢ ( ( ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ 𝑆 = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝑧 = ( 𝐻 ‘ 𝑥 ) ∧ 𝑤 = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) } ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ) ) → ( 𝑣 𝑅 𝑢 ↔ ( 𝐻 ‘ 𝑣 ) 𝑆 ( 𝐻 ‘ 𝑢 ) ) )
49 48 ralrimivva ⊢ ( ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ 𝑆 = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝑧 = ( 𝐻 ‘ 𝑥 ) ∧ 𝑤 = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) } ) → ∀ 𝑣 ∈ 𝐴 ∀ 𝑢 ∈ 𝐴 ( 𝑣 𝑅 𝑢 ↔ ( 𝐻 ‘ 𝑣 ) 𝑆 ( 𝐻 ‘ 𝑢 ) ) )
50 2 49 sylan ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑆 = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝑧 = ( 𝐻 ‘ 𝑥 ) ∧ 𝑤 = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) } ) → ∀ 𝑣 ∈ 𝐴 ∀ 𝑢 ∈ 𝐴 ( 𝑣 𝑅 𝑢 ↔ ( 𝐻 ‘ 𝑣 ) 𝑆 ( 𝐻 ‘ 𝑢 ) ) )
51 df-isom ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑣 ∈ 𝐴 ∀ 𝑢 ∈ 𝐴 ( 𝑣 𝑅 𝑢 ↔ ( 𝐻 ‘ 𝑣 ) 𝑆 ( 𝐻 ‘ 𝑢 ) ) ) )
52 1 50 51 sylanbrc ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑆 = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝑧 = ( 𝐻 ‘ 𝑥 ) ∧ 𝑤 = ( 𝐻 ‘ 𝑦 ) ) ∧ 𝑥 𝑅 𝑦 ) } ) → 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )