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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) ∈ 𝐵 )
46 45 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝐻 ‘ 𝑥 ) ∈ 𝐵 )
47 f1of ⊢ ( 𝐺 : 𝐶 –1-1-onto→ 𝐷 → 𝐺 : 𝐶 ⟶ 𝐷 )
48 12 47 syl ⊢ ( 𝜑 → 𝐺 : 𝐶 ⟶ 𝐷 )
49 48 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐷 )
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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝐷 )
75 74 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝐷 )
76 44 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑦 ) ∈ 𝐵 )
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 𝑅 , 𝑆 ( ( 𝐴 ∪ 𝐶 ) , ( 𝐵 ∪ 𝐷 ) ) )