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 
|- ( ph -> H Isom R , S ( A , B ) )
isoun.2 
|- ( ph -> G Isom R , S ( C , D ) )
isoun.3 
|- ( ( ph /\ x e. A /\ y e. C ) -> x R y )
isoun.4 
|- ( ( ph /\ z e. B /\ w e. D ) -> z S w )
isoun.5 
|- ( ( ph /\ x e. C /\ y e. A ) -> -. x R y )
isoun.6 
|- ( ( ph /\ z e. D /\ w e. B ) -> -. z S w )
isoun.7 
|- ( ph -> ( A i^i C ) = (/) )
isoun.8 
|- ( ph -> ( B i^i D ) = (/) )
Assertion isoun 
|- ( ph -> ( H u. G ) Isom R , S ( ( A u. C ) , ( B u. D ) ) )

Proof

Step Hyp Ref Expression
1 isoun.1 
 |-  ( ph -> H Isom R , S ( A , B ) )
2 isoun.2 
 |-  ( ph -> G Isom R , S ( C , D ) )
3 isoun.3 
 |-  ( ( ph /\ x e. A /\ y e. C ) -> x R y )
4 isoun.4 
 |-  ( ( ph /\ z e. B /\ w e. D ) -> z S w )
5 isoun.5 
 |-  ( ( ph /\ x e. C /\ y e. A ) -> -. x R y )
6 isoun.6 
 |-  ( ( ph /\ z e. D /\ w e. B ) -> -. z S w )
7 isoun.7 
 |-  ( ph -> ( A i^i C ) = (/) )
8 isoun.8 
 |-  ( ph -> ( B i^i D ) = (/) )
9 isof1o 
 |-  ( H Isom R , S ( A , B ) -> H : A -1-1-onto-> B )
10 1 9 syl 
 |-  ( ph -> H : A -1-1-onto-> B )
11 isof1o 
 |-  ( G Isom R , S ( C , D ) -> G : C -1-1-onto-> D )
12 2 11 syl 
 |-  ( ph -> G : C -1-1-onto-> D )
13 f1oun 
 |-  ( ( ( H : A -1-1-onto-> B /\ G : C -1-1-onto-> D ) /\ ( ( A i^i C ) = (/) /\ ( B i^i D ) = (/) ) ) -> ( H u. G ) : ( A u. C ) -1-1-onto-> ( B u. D ) )
14 10 12 7 8 13 syl22anc 
 |-  ( ph -> ( H u. G ) : ( A u. C ) -1-1-onto-> ( B u. D ) )
15 elun 
 |-  ( x e. ( A u. C ) <-> ( x e. A \/ x e. C ) )
16 elun 
 |-  ( y e. ( A u. C ) <-> ( y e. A \/ y e. C ) )
17 isorel 
 |-  ( ( H Isom R , S ( A , B ) /\ ( x e. A /\ y e. A ) ) -> ( x R y <-> ( H ` x ) S ( H ` y ) ) )
18 1 17 sylan 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( x R y <-> ( H ` x ) S ( H ` y ) ) )
19 f1ofn 
 |-  ( H : A -1-1-onto-> B -> H Fn A )
20 10 19 syl 
 |-  ( ph -> H Fn A )
21 20 adantr 
 |-  ( ( ph /\ x e. A ) -> H Fn A )
22 f1ofn 
 |-  ( G : C -1-1-onto-> D -> G Fn C )
23 12 22 syl 
 |-  ( ph -> G Fn C )
24 23 adantr 
 |-  ( ( ph /\ x e. A ) -> G Fn C )
25 7 anim1i 
 |-  ( ( ph /\ x e. A ) -> ( ( A i^i C ) = (/) /\ x e. A ) )
26 fvun1 
 |-  ( ( H Fn A /\ G Fn C /\ ( ( A i^i C ) = (/) /\ x e. A ) ) -> ( ( H u. G ) ` x ) = ( H ` x ) )
27 21 24 25 26 syl3anc 
 |-  ( ( ph /\ x e. A ) -> ( ( H u. G ) ` x ) = ( H ` x ) )
28 27 adantrr 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( ( H u. G ) ` x ) = ( H ` x ) )
29 20 adantr 
 |-  ( ( ph /\ y e. A ) -> H Fn A )
30 23 adantr 
 |-  ( ( ph /\ y e. A ) -> G Fn C )
31 7 anim1i 
 |-  ( ( ph /\ y e. A ) -> ( ( A i^i C ) = (/) /\ y e. A ) )
32 fvun1 
 |-  ( ( H Fn A /\ G Fn C /\ ( ( A i^i C ) = (/) /\ y e. A ) ) -> ( ( H u. G ) ` y ) = ( H ` y ) )
33 29 30 31 32 syl3anc 
 |-  ( ( ph /\ y e. A ) -> ( ( H u. G ) ` y ) = ( H ` y ) )
34 33 adantrl 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( ( H u. G ) ` y ) = ( H ` y ) )
35 28 34 breq12d 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( ( ( H u. G ) ` x ) S ( ( H u. G ) ` y ) <-> ( H ` x ) S ( H ` y ) ) )
36 18 35 bitr4d 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( x R y <-> ( ( H u. G ) ` x ) S ( ( H u. G ) ` y ) ) )
37 36 anassrs 
 |-  ( ( ( ph /\ x e. A ) /\ y e. A ) -> ( x R y <-> ( ( H u. G ) ` x ) S ( ( H u. G ) ` y ) ) )
38 3 3expb 
 |-  ( ( ph /\ ( x e. A /\ y e. C ) ) -> x R y )
39 4 3expia 
 |-  ( ( ph /\ z e. B ) -> ( w e. D -> z S w ) )
40 39 ralrimiv 
 |-  ( ( ph /\ z e. B ) -> A. w e. D z S w )
41 40 ralrimiva 
 |-  ( ph -> A. z e. B A. w e. D z S w )
42 41 adantr 
 |-  ( ( ph /\ ( x e. A /\ y e. C ) ) -> A. z e. B A. w e. D z S w )
43 f1of 
 |-  ( H : A -1-1-onto-> B -> H : A --> B )
44 10 43 syl 
 |-  ( ph -> H : A --> B )
45 44 ffvelrnda 
 |-  ( ( ph /\ x e. A ) -> ( H ` x ) e. B )
46 45 adantrr 
 |-  ( ( ph /\ ( x e. A /\ y e. C ) ) -> ( H ` x ) e. B )
47 f1of 
 |-  ( G : C -1-1-onto-> D -> G : C --> D )
48 12 47 syl 
 |-  ( ph -> G : C --> D )
49 48 ffvelrnda 
 |-  ( ( ph /\ y e. C ) -> ( G ` y ) e. D )
50 49 adantrl 
 |-  ( ( ph /\ ( x e. A /\ y e. C ) ) -> ( G ` y ) e. D )
51 breq1 
 |-  ( z = ( H ` x ) -> ( z S w <-> ( H ` x ) S w ) )
52 breq2 
 |-  ( w = ( G ` y ) -> ( ( H ` x ) S w <-> ( H ` x ) S ( G ` y ) ) )
53 51 52 rspc2v 
 |-  ( ( ( H ` x ) e. B /\ ( G ` y ) e. D ) -> ( A. z e. B A. w e. D z S w -> ( H ` x ) S ( G ` y ) ) )
54 46 50 53 syl2anc 
 |-  ( ( ph /\ ( x e. A /\ y e. C ) ) -> ( A. z e. B A. w e. D z S w -> ( H ` x ) S ( G ` y ) ) )
55 42 54 mpd 
 |-  ( ( ph /\ ( x e. A /\ y e. C ) ) -> ( H ` x ) S ( G ` y ) )
56 27 adantrr 
 |-  ( ( ph /\ ( x e. A /\ y e. C ) ) -> ( ( H u. G ) ` x ) = ( H ` x ) )
57 20 adantr 
 |-  ( ( ph /\ y e. C ) -> H Fn A )
58 23 adantr 
 |-  ( ( ph /\ y e. C ) -> G Fn C )
59 7 anim1i 
 |-  ( ( ph /\ y e. C ) -> ( ( A i^i C ) = (/) /\ y e. C ) )
60 fvun2 
 |-  ( ( H Fn A /\ G Fn C /\ ( ( A i^i C ) = (/) /\ y e. C ) ) -> ( ( H u. G ) ` y ) = ( G ` y ) )
61 57 58 59 60 syl3anc 
 |-  ( ( ph /\ y e. C ) -> ( ( H u. G ) ` y ) = ( G ` y ) )
62 61 adantrl 
 |-  ( ( ph /\ ( x e. A /\ y e. C ) ) -> ( ( H u. G ) ` y ) = ( G ` y ) )
63 55 56 62 3brtr4d 
 |-  ( ( ph /\ ( x e. A /\ y e. C ) ) -> ( ( H u. G ) ` x ) S ( ( H u. G ) ` y ) )
64 38 63 2thd 
 |-  ( ( ph /\ ( x e. A /\ y e. C ) ) -> ( x R y <-> ( ( H u. G ) ` x ) S ( ( H u. G ) ` y ) ) )
65 64 anassrs 
 |-  ( ( ( ph /\ x e. A ) /\ y e. C ) -> ( x R y <-> ( ( H u. G ) ` x ) S ( ( H u. G ) ` y ) ) )
66 37 65 jaodan 
 |-  ( ( ( ph /\ x e. A ) /\ ( y e. A \/ y e. C ) ) -> ( x R y <-> ( ( H u. G ) ` x ) S ( ( H u. G ) ` y ) ) )
67 16 66 sylan2b 
 |-  ( ( ( ph /\ x e. A ) /\ y e. ( A u. C ) ) -> ( x R y <-> ( ( H u. G ) ` x ) S ( ( H u. G ) ` y ) ) )
68 67 ex 
 |-  ( ( ph /\ x e. A ) -> ( y e. ( A u. C ) -> ( x R y <-> ( ( H u. G ) ` x ) S ( ( H u. G ) ` y ) ) ) )
69 5 3expb 
 |-  ( ( ph /\ ( x e. C /\ y e. A ) ) -> -. x R y )
70 6 3expia 
 |-  ( ( ph /\ z e. D ) -> ( w e. B -> -. z S w ) )
71 70 ralrimiv 
 |-  ( ( ph /\ z e. D ) -> A. w e. B -. z S w )
72 71 ralrimiva 
 |-  ( ph -> A. z e. D A. w e. B -. z S w )
73 72 adantr 
 |-  ( ( ph /\ ( x e. C /\ y e. A ) ) -> A. z e. D A. w e. B -. z S w )
74 48 ffvelrnda 
 |-  ( ( ph /\ x e. C ) -> ( G ` x ) e. D )
75 74 adantrr 
 |-  ( ( ph /\ ( x e. C /\ y e. A ) ) -> ( G ` x ) e. D )
76 44 ffvelrnda 
 |-  ( ( ph /\ y e. A ) -> ( H ` y ) e. B )
77 76 adantrl 
 |-  ( ( ph /\ ( x e. C /\ y e. A ) ) -> ( H ` y ) e. B )
78 breq1 
 |-  ( z = ( G ` x ) -> ( z S w <-> ( G ` x ) S w ) )
79 78 notbid 
 |-  ( z = ( G ` x ) -> ( -. z S w <-> -. ( G ` x ) S w ) )
80 breq2 
 |-  ( w = ( H ` y ) -> ( ( G ` x ) S w <-> ( G ` x ) S ( H ` y ) ) )
81 80 notbid 
 |-  ( w = ( H ` y ) -> ( -. ( G ` x ) S w <-> -. ( G ` x ) S ( H ` y ) ) )
82 79 81 rspc2v 
 |-  ( ( ( G ` x ) e. D /\ ( H ` y ) e. B ) -> ( A. z e. D A. w e. B -. z S w -> -. ( G ` x ) S ( H ` y ) ) )
83 75 77 82 syl2anc 
 |-  ( ( ph /\ ( x e. C /\ y e. A ) ) -> ( A. z e. D A. w e. B -. z S w -> -. ( G ` x ) S ( H ` y ) ) )
84 73 83 mpd 
 |-  ( ( ph /\ ( x e. C /\ y e. A ) ) -> -. ( G ` x ) S ( H ` y ) )
85 20 adantr 
 |-  ( ( ph /\ x e. C ) -> H Fn A )
86 23 adantr 
 |-  ( ( ph /\ x e. C ) -> G Fn C )
87 7 anim1i 
 |-  ( ( ph /\ x e. C ) -> ( ( A i^i C ) = (/) /\ x e. C ) )
88 fvun2 
 |-  ( ( H Fn A /\ G Fn C /\ ( ( A i^i C ) = (/) /\ x e. C ) ) -> ( ( H u. G ) ` x ) = ( G ` x ) )
89 85 86 87 88 syl3anc 
 |-  ( ( ph /\ x e. C ) -> ( ( H u. G ) ` x ) = ( G ` x ) )
90 89 adantrr 
 |-  ( ( ph /\ ( x e. C /\ y e. A ) ) -> ( ( H u. G ) ` x ) = ( G ` x ) )
91 33 adantrl 
 |-  ( ( ph /\ ( x e. C /\ y e. A ) ) -> ( ( H u. G ) ` y ) = ( H ` y ) )
92 90 91 breq12d 
 |-  ( ( ph /\ ( x e. C /\ y e. A ) ) -> ( ( ( H u. G ) ` x ) S ( ( H u. G ) ` y ) <-> ( G ` x ) S ( H ` y ) ) )
93 84 92 mtbird 
 |-  ( ( ph /\ ( x e. C /\ y e. A ) ) -> -. ( ( H u. G ) ` x ) S ( ( H u. G ) ` y ) )
94 69 93 2falsed 
 |-  ( ( ph /\ ( x e. C /\ y e. A ) ) -> ( x R y <-> ( ( H u. G ) ` x ) S ( ( H u. G ) ` y ) ) )
95 94 anassrs 
 |-  ( ( ( ph /\ x e. C ) /\ y e. A ) -> ( x R y <-> ( ( H u. G ) ` x ) S ( ( H u. G ) ` y ) ) )
96 isorel 
 |-  ( ( G Isom R , S ( C , D ) /\ ( x e. C /\ y e. C ) ) -> ( x R y <-> ( G ` x ) S ( G ` y ) ) )
97 2 96 sylan 
 |-  ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x R y <-> ( G ` x ) S ( G ` y ) ) )
98 89 adantrr 
 |-  ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( ( H u. G ) ` x ) = ( G ` x ) )
99 61 adantrl 
 |-  ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( ( H u. G ) ` y ) = ( G ` y ) )
100 98 99 breq12d 
 |-  ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( ( ( H u. G ) ` x ) S ( ( H u. G ) ` y ) <-> ( G ` x ) S ( G ` y ) ) )
101 97 100 bitr4d 
 |-  ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x R y <-> ( ( H u. G ) ` x ) S ( ( H u. G ) ` y ) ) )
102 101 anassrs 
 |-  ( ( ( ph /\ x e. C ) /\ y e. C ) -> ( x R y <-> ( ( H u. G ) ` x ) S ( ( H u. G ) ` y ) ) )
103 95 102 jaodan 
 |-  ( ( ( ph /\ x e. C ) /\ ( y e. A \/ y e. C ) ) -> ( x R y <-> ( ( H u. G ) ` x ) S ( ( H u. G ) ` y ) ) )
104 16 103 sylan2b 
 |-  ( ( ( ph /\ x e. C ) /\ y e. ( A u. C ) ) -> ( x R y <-> ( ( H u. G ) ` x ) S ( ( H u. G ) ` y ) ) )
105 104 ex 
 |-  ( ( ph /\ x e. C ) -> ( y e. ( A u. C ) -> ( x R y <-> ( ( H u. G ) ` x ) S ( ( H u. G ) ` y ) ) ) )
106 68 105 jaodan 
 |-  ( ( ph /\ ( x e. A \/ x e. C ) ) -> ( y e. ( A u. C ) -> ( x R y <-> ( ( H u. G ) ` x ) S ( ( H u. G ) ` y ) ) ) )
107 15 106 sylan2b 
 |-  ( ( ph /\ x e. ( A u. C ) ) -> ( y e. ( A u. C ) -> ( x R y <-> ( ( H u. G ) ` x ) S ( ( H u. G ) ` y ) ) ) )
108 107 ralrimiv 
 |-  ( ( ph /\ x e. ( A u. C ) ) -> A. y e. ( A u. C ) ( x R y <-> ( ( H u. G ) ` x ) S ( ( H u. G ) ` y ) ) )
109 108 ralrimiva 
 |-  ( ph -> A. x e. ( A u. C ) A. y e. ( A u. C ) ( x R y <-> ( ( H u. G ) ` x ) S ( ( H u. G ) ` y ) ) )
110 df-isom 
 |-  ( ( H u. G ) Isom R , S ( ( A u. C ) , ( B u. D ) ) <-> ( ( H u. G ) : ( A u. C ) -1-1-onto-> ( B u. D ) /\ A. x e. ( A u. C ) A. y e. ( A u. C ) ( x R y <-> ( ( H u. G ) ` x ) S ( ( H u. G ) ` y ) ) ) )
111 14 109 110 sylanbrc 
 |-  ( ph -> ( H u. G ) Isom R , S ( ( A u. C ) , ( B u. D ) ) )