Metamath Proof Explorer


Theorem isoun

Description: Infer an isomorphism from a union of two isomorphisms. (Contributed by Thierry Arnoux, 30-Mar-2017)

Ref Expression
Hypotheses isoun.1 ( 𝜑𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
isoun.2 ( 𝜑𝐺 Isom 𝑅 , 𝑆 ( 𝐶 , 𝐷 ) )
isoun.3 ( ( 𝜑𝑥𝐴𝑦𝐶 ) → 𝑥 𝑅 𝑦 )
isoun.4 ( ( 𝜑𝑧𝐵𝑤𝐷 ) → 𝑧 𝑆 𝑤 )
isoun.5 ( ( 𝜑𝑥𝐶𝑦𝐴 ) → ¬ 𝑥 𝑅 𝑦 )
isoun.6 ( ( 𝜑𝑧𝐷𝑤𝐵 ) → ¬ 𝑧 𝑆 𝑤 )
isoun.7 ( 𝜑 → ( 𝐴𝐶 ) = ∅ )
isoun.8 ( 𝜑 → ( 𝐵𝐷 ) = ∅ )
Assertion isoun ( 𝜑 → ( 𝐻𝐺 ) Isom 𝑅 , 𝑆 ( ( 𝐴𝐶 ) , ( 𝐵𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 isoun.1 ( 𝜑𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
2 isoun.2 ( 𝜑𝐺 Isom 𝑅 , 𝑆 ( 𝐶 , 𝐷 ) )
3 isoun.3 ( ( 𝜑𝑥𝐴𝑦𝐶 ) → 𝑥 𝑅 𝑦 )
4 isoun.4 ( ( 𝜑𝑧𝐵𝑤𝐷 ) → 𝑧 𝑆 𝑤 )
5 isoun.5 ( ( 𝜑𝑥𝐶𝑦𝐴 ) → ¬ 𝑥 𝑅 𝑦 )
6 isoun.6 ( ( 𝜑𝑧𝐷𝑤𝐵 ) → ¬ 𝑧 𝑆 𝑤 )
7 isoun.7 ( 𝜑 → ( 𝐴𝐶 ) = ∅ )
8 isoun.8 ( 𝜑 → ( 𝐵𝐷 ) = ∅ )
9 isof1o ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐻 : 𝐴1-1-onto𝐵 )
10 1 9 syl ( 𝜑𝐻 : 𝐴1-1-onto𝐵 )
11 isof1o ( 𝐺 Isom 𝑅 , 𝑆 ( 𝐶 , 𝐷 ) → 𝐺 : 𝐶1-1-onto𝐷 )
12 2 11 syl ( 𝜑𝐺 : 𝐶1-1-onto𝐷 )
13 f1oun ( ( ( 𝐻 : 𝐴1-1-onto𝐵𝐺 : 𝐶1-1-onto𝐷 ) ∧ ( ( 𝐴𝐶 ) = ∅ ∧ ( 𝐵𝐷 ) = ∅ ) ) → ( 𝐻𝐺 ) : ( 𝐴𝐶 ) –1-1-onto→ ( 𝐵𝐷 ) )
14 10 12 7 8 13 syl22anc ( 𝜑 → ( 𝐻𝐺 ) : ( 𝐴𝐶 ) –1-1-onto→ ( 𝐵𝐷 ) )
15 elun ( 𝑥 ∈ ( 𝐴𝐶 ) ↔ ( 𝑥𝐴𝑥𝐶 ) )
16 elun ( 𝑦 ∈ ( 𝐴𝐶 ) ↔ ( 𝑦𝐴𝑦𝐶 ) )
17 isorel ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( 𝐻𝑥 ) 𝑆 ( 𝐻𝑦 ) ) )
18 1 17 sylan ( ( 𝜑 ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( 𝐻𝑥 ) 𝑆 ( 𝐻𝑦 ) ) )
19 f1ofn ( 𝐻 : 𝐴1-1-onto𝐵𝐻 Fn 𝐴 )
20 10 19 syl ( 𝜑𝐻 Fn 𝐴 )
21 20 adantr ( ( 𝜑𝑥𝐴 ) → 𝐻 Fn 𝐴 )
22 f1ofn ( 𝐺 : 𝐶1-1-onto𝐷𝐺 Fn 𝐶 )
23 12 22 syl ( 𝜑𝐺 Fn 𝐶 )
24 23 adantr ( ( 𝜑𝑥𝐴 ) → 𝐺 Fn 𝐶 )
25 7 anim1i ( ( 𝜑𝑥𝐴 ) → ( ( 𝐴𝐶 ) = ∅ ∧ 𝑥𝐴 ) )
26 fvun1 ( ( 𝐻 Fn 𝐴𝐺 Fn 𝐶 ∧ ( ( 𝐴𝐶 ) = ∅ ∧ 𝑥𝐴 ) ) → ( ( 𝐻𝐺 ) ‘ 𝑥 ) = ( 𝐻𝑥 ) )
27 21 24 25 26 syl3anc ( ( 𝜑𝑥𝐴 ) → ( ( 𝐻𝐺 ) ‘ 𝑥 ) = ( 𝐻𝑥 ) )
28 27 adantrr ( ( 𝜑 ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( ( 𝐻𝐺 ) ‘ 𝑥 ) = ( 𝐻𝑥 ) )
29 20 adantr ( ( 𝜑𝑦𝐴 ) → 𝐻 Fn 𝐴 )
30 23 adantr ( ( 𝜑𝑦𝐴 ) → 𝐺 Fn 𝐶 )
31 7 anim1i ( ( 𝜑𝑦𝐴 ) → ( ( 𝐴𝐶 ) = ∅ ∧ 𝑦𝐴 ) )
32 fvun1 ( ( 𝐻 Fn 𝐴𝐺 Fn 𝐶 ∧ ( ( 𝐴𝐶 ) = ∅ ∧ 𝑦𝐴 ) ) → ( ( 𝐻𝐺 ) ‘ 𝑦 ) = ( 𝐻𝑦 ) )
33 29 30 31 32 syl3anc ( ( 𝜑𝑦𝐴 ) → ( ( 𝐻𝐺 ) ‘ 𝑦 ) = ( 𝐻𝑦 ) )
34 33 adantrl ( ( 𝜑 ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( ( 𝐻𝐺 ) ‘ 𝑦 ) = ( 𝐻𝑦 ) )
35 28 34 breq12d ( ( 𝜑 ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( ( ( 𝐻𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻𝐺 ) ‘ 𝑦 ) ↔ ( 𝐻𝑥 ) 𝑆 ( 𝐻𝑦 ) ) )
36 18 35 bitr4d ( ( 𝜑 ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻𝐺 ) ‘ 𝑦 ) ) )
37 36 anassrs ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑦𝐴 ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻𝐺 ) ‘ 𝑦 ) ) )
38 3 3expb ( ( 𝜑 ∧ ( 𝑥𝐴𝑦𝐶 ) ) → 𝑥 𝑅 𝑦 )
39 4 3expia ( ( 𝜑𝑧𝐵 ) → ( 𝑤𝐷𝑧 𝑆 𝑤 ) )
40 39 ralrimiv ( ( 𝜑𝑧𝐵 ) → ∀ 𝑤𝐷 𝑧 𝑆 𝑤 )
41 40 ralrimiva ( 𝜑 → ∀ 𝑧𝐵𝑤𝐷 𝑧 𝑆 𝑤 )
42 41 adantr ( ( 𝜑 ∧ ( 𝑥𝐴𝑦𝐶 ) ) → ∀ 𝑧𝐵𝑤𝐷 𝑧 𝑆 𝑤 )
43 f1of ( 𝐻 : 𝐴1-1-onto𝐵𝐻 : 𝐴𝐵 )
44 10 43 syl ( 𝜑𝐻 : 𝐴𝐵 )
45 44 ffvelrnda ( ( 𝜑𝑥𝐴 ) → ( 𝐻𝑥 ) ∈ 𝐵 )
46 45 adantrr ( ( 𝜑 ∧ ( 𝑥𝐴𝑦𝐶 ) ) → ( 𝐻𝑥 ) ∈ 𝐵 )
47 f1of ( 𝐺 : 𝐶1-1-onto𝐷𝐺 : 𝐶𝐷 )
48 12 47 syl ( 𝜑𝐺 : 𝐶𝐷 )
49 48 ffvelrnda ( ( 𝜑𝑦𝐶 ) → ( 𝐺𝑦 ) ∈ 𝐷 )
50 49 adantrl ( ( 𝜑 ∧ ( 𝑥𝐴𝑦𝐶 ) ) → ( 𝐺𝑦 ) ∈ 𝐷 )
51 breq1 ( 𝑧 = ( 𝐻𝑥 ) → ( 𝑧 𝑆 𝑤 ↔ ( 𝐻𝑥 ) 𝑆 𝑤 ) )
52 breq2 ( 𝑤 = ( 𝐺𝑦 ) → ( ( 𝐻𝑥 ) 𝑆 𝑤 ↔ ( 𝐻𝑥 ) 𝑆 ( 𝐺𝑦 ) ) )
53 51 52 rspc2v ( ( ( 𝐻𝑥 ) ∈ 𝐵 ∧ ( 𝐺𝑦 ) ∈ 𝐷 ) → ( ∀ 𝑧𝐵𝑤𝐷 𝑧 𝑆 𝑤 → ( 𝐻𝑥 ) 𝑆 ( 𝐺𝑦 ) ) )
54 46 50 53 syl2anc ( ( 𝜑 ∧ ( 𝑥𝐴𝑦𝐶 ) ) → ( ∀ 𝑧𝐵𝑤𝐷 𝑧 𝑆 𝑤 → ( 𝐻𝑥 ) 𝑆 ( 𝐺𝑦 ) ) )
55 42 54 mpd ( ( 𝜑 ∧ ( 𝑥𝐴𝑦𝐶 ) ) → ( 𝐻𝑥 ) 𝑆 ( 𝐺𝑦 ) )
56 27 adantrr ( ( 𝜑 ∧ ( 𝑥𝐴𝑦𝐶 ) ) → ( ( 𝐻𝐺 ) ‘ 𝑥 ) = ( 𝐻𝑥 ) )
57 20 adantr ( ( 𝜑𝑦𝐶 ) → 𝐻 Fn 𝐴 )
58 23 adantr ( ( 𝜑𝑦𝐶 ) → 𝐺 Fn 𝐶 )
59 7 anim1i ( ( 𝜑𝑦𝐶 ) → ( ( 𝐴𝐶 ) = ∅ ∧ 𝑦𝐶 ) )
60 fvun2 ( ( 𝐻 Fn 𝐴𝐺 Fn 𝐶 ∧ ( ( 𝐴𝐶 ) = ∅ ∧ 𝑦𝐶 ) ) → ( ( 𝐻𝐺 ) ‘ 𝑦 ) = ( 𝐺𝑦 ) )
61 57 58 59 60 syl3anc ( ( 𝜑𝑦𝐶 ) → ( ( 𝐻𝐺 ) ‘ 𝑦 ) = ( 𝐺𝑦 ) )
62 61 adantrl ( ( 𝜑 ∧ ( 𝑥𝐴𝑦𝐶 ) ) → ( ( 𝐻𝐺 ) ‘ 𝑦 ) = ( 𝐺𝑦 ) )
63 55 56 62 3brtr4d ( ( 𝜑 ∧ ( 𝑥𝐴𝑦𝐶 ) ) → ( ( 𝐻𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻𝐺 ) ‘ 𝑦 ) )
64 38 63 2thd ( ( 𝜑 ∧ ( 𝑥𝐴𝑦𝐶 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻𝐺 ) ‘ 𝑦 ) ) )
65 64 anassrs ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑦𝐶 ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻𝐺 ) ‘ 𝑦 ) ) )
66 37 65 jaodan ( ( ( 𝜑𝑥𝐴 ) ∧ ( 𝑦𝐴𝑦𝐶 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻𝐺 ) ‘ 𝑦 ) ) )
67 16 66 sylan2b ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑦 ∈ ( 𝐴𝐶 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻𝐺 ) ‘ 𝑦 ) ) )
68 67 ex ( ( 𝜑𝑥𝐴 ) → ( 𝑦 ∈ ( 𝐴𝐶 ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻𝐺 ) ‘ 𝑦 ) ) ) )
69 5 3expb ( ( 𝜑 ∧ ( 𝑥𝐶𝑦𝐴 ) ) → ¬ 𝑥 𝑅 𝑦 )
70 6 3expia ( ( 𝜑𝑧𝐷 ) → ( 𝑤𝐵 → ¬ 𝑧 𝑆 𝑤 ) )
71 70 ralrimiv ( ( 𝜑𝑧𝐷 ) → ∀ 𝑤𝐵 ¬ 𝑧 𝑆 𝑤 )
72 71 ralrimiva ( 𝜑 → ∀ 𝑧𝐷𝑤𝐵 ¬ 𝑧 𝑆 𝑤 )
73 72 adantr ( ( 𝜑 ∧ ( 𝑥𝐶𝑦𝐴 ) ) → ∀ 𝑧𝐷𝑤𝐵 ¬ 𝑧 𝑆 𝑤 )
74 48 ffvelrnda ( ( 𝜑𝑥𝐶 ) → ( 𝐺𝑥 ) ∈ 𝐷 )
75 74 adantrr ( ( 𝜑 ∧ ( 𝑥𝐶𝑦𝐴 ) ) → ( 𝐺𝑥 ) ∈ 𝐷 )
76 44 ffvelrnda ( ( 𝜑𝑦𝐴 ) → ( 𝐻𝑦 ) ∈ 𝐵 )
77 76 adantrl ( ( 𝜑 ∧ ( 𝑥𝐶𝑦𝐴 ) ) → ( 𝐻𝑦 ) ∈ 𝐵 )
78 breq1 ( 𝑧 = ( 𝐺𝑥 ) → ( 𝑧 𝑆 𝑤 ↔ ( 𝐺𝑥 ) 𝑆 𝑤 ) )
79 78 notbid ( 𝑧 = ( 𝐺𝑥 ) → ( ¬ 𝑧 𝑆 𝑤 ↔ ¬ ( 𝐺𝑥 ) 𝑆 𝑤 ) )
80 breq2 ( 𝑤 = ( 𝐻𝑦 ) → ( ( 𝐺𝑥 ) 𝑆 𝑤 ↔ ( 𝐺𝑥 ) 𝑆 ( 𝐻𝑦 ) ) )
81 80 notbid ( 𝑤 = ( 𝐻𝑦 ) → ( ¬ ( 𝐺𝑥 ) 𝑆 𝑤 ↔ ¬ ( 𝐺𝑥 ) 𝑆 ( 𝐻𝑦 ) ) )
82 79 81 rspc2v ( ( ( 𝐺𝑥 ) ∈ 𝐷 ∧ ( 𝐻𝑦 ) ∈ 𝐵 ) → ( ∀ 𝑧𝐷𝑤𝐵 ¬ 𝑧 𝑆 𝑤 → ¬ ( 𝐺𝑥 ) 𝑆 ( 𝐻𝑦 ) ) )
83 75 77 82 syl2anc ( ( 𝜑 ∧ ( 𝑥𝐶𝑦𝐴 ) ) → ( ∀ 𝑧𝐷𝑤𝐵 ¬ 𝑧 𝑆 𝑤 → ¬ ( 𝐺𝑥 ) 𝑆 ( 𝐻𝑦 ) ) )
84 73 83 mpd ( ( 𝜑 ∧ ( 𝑥𝐶𝑦𝐴 ) ) → ¬ ( 𝐺𝑥 ) 𝑆 ( 𝐻𝑦 ) )
85 20 adantr ( ( 𝜑𝑥𝐶 ) → 𝐻 Fn 𝐴 )
86 23 adantr ( ( 𝜑𝑥𝐶 ) → 𝐺 Fn 𝐶 )
87 7 anim1i ( ( 𝜑𝑥𝐶 ) → ( ( 𝐴𝐶 ) = ∅ ∧ 𝑥𝐶 ) )
88 fvun2 ( ( 𝐻 Fn 𝐴𝐺 Fn 𝐶 ∧ ( ( 𝐴𝐶 ) = ∅ ∧ 𝑥𝐶 ) ) → ( ( 𝐻𝐺 ) ‘ 𝑥 ) = ( 𝐺𝑥 ) )
89 85 86 87 88 syl3anc ( ( 𝜑𝑥𝐶 ) → ( ( 𝐻𝐺 ) ‘ 𝑥 ) = ( 𝐺𝑥 ) )
90 89 adantrr ( ( 𝜑 ∧ ( 𝑥𝐶𝑦𝐴 ) ) → ( ( 𝐻𝐺 ) ‘ 𝑥 ) = ( 𝐺𝑥 ) )
91 33 adantrl ( ( 𝜑 ∧ ( 𝑥𝐶𝑦𝐴 ) ) → ( ( 𝐻𝐺 ) ‘ 𝑦 ) = ( 𝐻𝑦 ) )
92 90 91 breq12d ( ( 𝜑 ∧ ( 𝑥𝐶𝑦𝐴 ) ) → ( ( ( 𝐻𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻𝐺 ) ‘ 𝑦 ) ↔ ( 𝐺𝑥 ) 𝑆 ( 𝐻𝑦 ) ) )
93 84 92 mtbird ( ( 𝜑 ∧ ( 𝑥𝐶𝑦𝐴 ) ) → ¬ ( ( 𝐻𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻𝐺 ) ‘ 𝑦 ) )
94 69 93 2falsed ( ( 𝜑 ∧ ( 𝑥𝐶𝑦𝐴 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻𝐺 ) ‘ 𝑦 ) ) )
95 94 anassrs ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑦𝐴 ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻𝐺 ) ‘ 𝑦 ) ) )
96 isorel ( ( 𝐺 Isom 𝑅 , 𝑆 ( 𝐶 , 𝐷 ) ∧ ( 𝑥𝐶𝑦𝐶 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( 𝐺𝑥 ) 𝑆 ( 𝐺𝑦 ) ) )
97 2 96 sylan ( ( 𝜑 ∧ ( 𝑥𝐶𝑦𝐶 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( 𝐺𝑥 ) 𝑆 ( 𝐺𝑦 ) ) )
98 89 adantrr ( ( 𝜑 ∧ ( 𝑥𝐶𝑦𝐶 ) ) → ( ( 𝐻𝐺 ) ‘ 𝑥 ) = ( 𝐺𝑥 ) )
99 61 adantrl ( ( 𝜑 ∧ ( 𝑥𝐶𝑦𝐶 ) ) → ( ( 𝐻𝐺 ) ‘ 𝑦 ) = ( 𝐺𝑦 ) )
100 98 99 breq12d ( ( 𝜑 ∧ ( 𝑥𝐶𝑦𝐶 ) ) → ( ( ( 𝐻𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻𝐺 ) ‘ 𝑦 ) ↔ ( 𝐺𝑥 ) 𝑆 ( 𝐺𝑦 ) ) )
101 97 100 bitr4d ( ( 𝜑 ∧ ( 𝑥𝐶𝑦𝐶 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻𝐺 ) ‘ 𝑦 ) ) )
102 101 anassrs ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑦𝐶 ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻𝐺 ) ‘ 𝑦 ) ) )
103 95 102 jaodan ( ( ( 𝜑𝑥𝐶 ) ∧ ( 𝑦𝐴𝑦𝐶 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻𝐺 ) ‘ 𝑦 ) ) )
104 16 103 sylan2b ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑦 ∈ ( 𝐴𝐶 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻𝐺 ) ‘ 𝑦 ) ) )
105 104 ex ( ( 𝜑𝑥𝐶 ) → ( 𝑦 ∈ ( 𝐴𝐶 ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻𝐺 ) ‘ 𝑦 ) ) ) )
106 68 105 jaodan ( ( 𝜑 ∧ ( 𝑥𝐴𝑥𝐶 ) ) → ( 𝑦 ∈ ( 𝐴𝐶 ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻𝐺 ) ‘ 𝑦 ) ) ) )
107 15 106 sylan2b ( ( 𝜑𝑥 ∈ ( 𝐴𝐶 ) ) → ( 𝑦 ∈ ( 𝐴𝐶 ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻𝐺 ) ‘ 𝑦 ) ) ) )
108 107 ralrimiv ( ( 𝜑𝑥 ∈ ( 𝐴𝐶 ) ) → ∀ 𝑦 ∈ ( 𝐴𝐶 ) ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻𝐺 ) ‘ 𝑦 ) ) )
109 108 ralrimiva ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴𝐶 ) ∀ 𝑦 ∈ ( 𝐴𝐶 ) ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻𝐺 ) ‘ 𝑦 ) ) )
110 df-isom ( ( 𝐻𝐺 ) Isom 𝑅 , 𝑆 ( ( 𝐴𝐶 ) , ( 𝐵𝐷 ) ) ↔ ( ( 𝐻𝐺 ) : ( 𝐴𝐶 ) –1-1-onto→ ( 𝐵𝐷 ) ∧ ∀ 𝑥 ∈ ( 𝐴𝐶 ) ∀ 𝑦 ∈ ( 𝐴𝐶 ) ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐻𝐺 ) ‘ 𝑥 ) 𝑆 ( ( 𝐻𝐺 ) ‘ 𝑦 ) ) ) )
111 14 109 110 sylanbrc ( 𝜑 → ( 𝐻𝐺 ) Isom 𝑅 , 𝑆 ( ( 𝐴𝐶 ) , ( 𝐵𝐷 ) ) )