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 bitrdi ( ( 𝐻 : 𝐴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 bitrdi ( ( ( 𝐻 : 𝐴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 bitrdi ( ( 𝐻 : 𝐴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 bitr2id ( ( ( 𝐻 : 𝐴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 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )