This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ghmqusker

Description: A surjective group homomorphism F from G to H induces an isomorphism J from Q to H , where Q is the factor group of G by F 's kernel K . (Contributed by Thierry Arnoux, 15-Feb-2025)

Ref Expression
Hypotheses ghmqusker.1 
|- .0. = ( 0g ` H )
ghmqusker.f 
|- ( ph -> F e. ( G GrpHom H ) )
ghmqusker.k 
|- K = ( `' F " { .0. } )
ghmqusker.q 
|- Q = ( G /s ( G ~QG K ) )
ghmqusker.j 
|- J = ( q e. ( Base ` Q ) |-> U. ( F " q ) )
ghmqusker.s 
|- ( ph -> ran F = ( Base ` H ) )
Assertion ghmqusker 
|- ( ph -> J e. ( Q GrpIso H ) )

Proof

Step Hyp Ref Expression
1 ghmqusker.1 
 |-  .0. = ( 0g ` H )
2 ghmqusker.f 
 |-  ( ph -> F e. ( G GrpHom H ) )
3 ghmqusker.k 
 |-  K = ( `' F " { .0. } )
4 ghmqusker.q 
 |-  Q = ( G /s ( G ~QG K ) )
5 ghmqusker.j 
 |-  J = ( q e. ( Base ` Q ) |-> U. ( F " q ) )
6 ghmqusker.s 
 |-  ( ph -> ran F = ( Base ` H ) )
7 1 2 3 4 5 ghmquskerlem3 
 |-  ( ph -> J e. ( Q GrpHom H ) )
8 ghmgrp1 
 |-  ( F e. ( G GrpHom H ) -> G e. Grp )
9 2 8 syl 
 |-  ( ph -> G e. Grp )
10 9 ad4antr 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ ( J ` r ) = .0. ) -> G e. Grp )
11 1 ghmker 
 |-  ( F e. ( G GrpHom H ) -> ( `' F " { .0. } ) e. ( NrmSGrp ` G ) )
12 2 11 syl 
 |-  ( ph -> ( `' F " { .0. } ) e. ( NrmSGrp ` G ) )
13 3 12 eqeltrid 
 |-  ( ph -> K e. ( NrmSGrp ` G ) )
14 nsgsubg 
 |-  ( K e. ( NrmSGrp ` G ) -> K e. ( SubGrp ` G ) )
15 13 14 syl 
 |-  ( ph -> K e. ( SubGrp ` G ) )
16 15 ad4antr 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ ( J ` r ) = .0. ) -> K e. ( SubGrp ` G ) )
17 eqid 
 |-  ( Base ` G ) = ( Base ` G )
18 eqid 
 |-  ( Base ` H ) = ( Base ` H )
19 17 18 ghmf 
 |-  ( F e. ( G GrpHom H ) -> F : ( Base ` G ) --> ( Base ` H ) )
20 2 19 syl 
 |-  ( ph -> F : ( Base ` G ) --> ( Base ` H ) )
21 20 ffnd 
 |-  ( ph -> F Fn ( Base ` G ) )
22 21 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> F Fn ( Base ` G ) )
23 22 adantr 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ ( J ` r ) = .0. ) -> F Fn ( Base ` G ) )
24 4 a1i 
 |-  ( ph -> Q = ( G /s ( G ~QG K ) ) )
25 eqidd 
 |-  ( ph -> ( Base ` G ) = ( Base ` G ) )
26 ovexd 
 |-  ( ph -> ( G ~QG K ) e. _V )
27 24 25 26 9 qusbas 
 |-  ( ph -> ( ( Base ` G ) /. ( G ~QG K ) ) = ( Base ` Q ) )
28 eqid 
 |-  ( G ~QG K ) = ( G ~QG K )
29 17 28 eqger 
 |-  ( K e. ( SubGrp ` G ) -> ( G ~QG K ) Er ( Base ` G ) )
30 13 14 29 3syl 
 |-  ( ph -> ( G ~QG K ) Er ( Base ` G ) )
31 30 qsss 
 |-  ( ph -> ( ( Base ` G ) /. ( G ~QG K ) ) C_ ~P ( Base ` G ) )
32 27 31 eqsstrrd 
 |-  ( ph -> ( Base ` Q ) C_ ~P ( Base ` G ) )
33 32 sselda 
 |-  ( ( ph /\ r e. ( Base ` Q ) ) -> r e. ~P ( Base ` G ) )
34 33 elpwid 
 |-  ( ( ph /\ r e. ( Base ` Q ) ) -> r C_ ( Base ` G ) )
35 34 sselda 
 |-  ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) -> x e. ( Base ` G ) )
36 35 adantr 
 |-  ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> x e. ( Base ` G ) )
37 36 adantr 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ ( J ` r ) = .0. ) -> x e. ( Base ` G ) )
38 simpr 
 |-  ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ( J ` r ) = ( F ` x ) )
39 38 eqeq1d 
 |-  ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ( ( J ` r ) = .0. <-> ( F ` x ) = .0. ) )
40 39 biimpa 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ ( J ` r ) = .0. ) -> ( F ` x ) = .0. )
41 fniniseg 
 |-  ( F Fn ( Base ` G ) -> ( x e. ( `' F " { .0. } ) <-> ( x e. ( Base ` G ) /\ ( F ` x ) = .0. ) ) )
42 41 biimpar 
 |-  ( ( F Fn ( Base ` G ) /\ ( x e. ( Base ` G ) /\ ( F ` x ) = .0. ) ) -> x e. ( `' F " { .0. } ) )
43 23 37 40 42 syl12anc 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ ( J ` r ) = .0. ) -> x e. ( `' F " { .0. } ) )
44 43 3 eleqtrrdi 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ ( J ` r ) = .0. ) -> x e. K )
45 28 eqg0el 
 |-  ( ( G e. Grp /\ K e. ( SubGrp ` G ) ) -> ( [ x ] ( G ~QG K ) = K <-> x e. K ) )
46 45 biimpar 
 |-  ( ( ( G e. Grp /\ K e. ( SubGrp ` G ) ) /\ x e. K ) -> [ x ] ( G ~QG K ) = K )
47 10 16 44 46 syl21anc 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ ( J ` r ) = .0. ) -> [ x ] ( G ~QG K ) = K )
48 30 ad4antr 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ ( J ` r ) = .0. ) -> ( G ~QG K ) Er ( Base ` G ) )
49 simpr 
 |-  ( ( ph /\ r e. ( Base ` Q ) ) -> r e. ( Base ` Q ) )
50 27 adantr 
 |-  ( ( ph /\ r e. ( Base ` Q ) ) -> ( ( Base ` G ) /. ( G ~QG K ) ) = ( Base ` Q ) )
51 49 50 eleqtrrd 
 |-  ( ( ph /\ r e. ( Base ` Q ) ) -> r e. ( ( Base ` G ) /. ( G ~QG K ) ) )
52 51 ad3antrrr 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ ( J ` r ) = .0. ) -> r e. ( ( Base ` G ) /. ( G ~QG K ) ) )
53 simpllr 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ ( J ` r ) = .0. ) -> x e. r )
54 qsel 
 |-  ( ( ( G ~QG K ) Er ( Base ` G ) /\ r e. ( ( Base ` G ) /. ( G ~QG K ) ) /\ x e. r ) -> r = [ x ] ( G ~QG K ) )
55 48 52 53 54 syl3anc 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ ( J ` r ) = .0. ) -> r = [ x ] ( G ~QG K ) )
56 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
57 17 28 56 eqgid 
 |-  ( K e. ( SubGrp ` G ) -> [ ( 0g ` G ) ] ( G ~QG K ) = K )
58 15 57 syl 
 |-  ( ph -> [ ( 0g ` G ) ] ( G ~QG K ) = K )
59 58 ad4antr 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ ( J ` r ) = .0. ) -> [ ( 0g ` G ) ] ( G ~QG K ) = K )
60 47 55 59 3eqtr4d 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ ( J ` r ) = .0. ) -> r = [ ( 0g ` G ) ] ( G ~QG K ) )
61 4 56 qus0 
 |-  ( K e. ( NrmSGrp ` G ) -> [ ( 0g ` G ) ] ( G ~QG K ) = ( 0g ` Q ) )
62 13 61 syl 
 |-  ( ph -> [ ( 0g ` G ) ] ( G ~QG K ) = ( 0g ` Q ) )
63 62 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> [ ( 0g ` G ) ] ( G ~QG K ) = ( 0g ` Q ) )
64 63 adantr 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ ( J ` r ) = .0. ) -> [ ( 0g ` G ) ] ( G ~QG K ) = ( 0g ` Q ) )
65 60 64 eqtrd 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ ( J ` r ) = .0. ) -> r = ( 0g ` Q ) )
66 63 eqeq2d 
 |-  ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ( r = [ ( 0g ` G ) ] ( G ~QG K ) <-> r = ( 0g ` Q ) ) )
67 66 biimpar 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ r = ( 0g ` Q ) ) -> r = [ ( 0g ` G ) ] ( G ~QG K ) )
68 67 fveq2d 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ r = ( 0g ` Q ) ) -> ( J ` r ) = ( J ` [ ( 0g ` G ) ] ( G ~QG K ) ) )
69 2 adantr 
 |-  ( ( ph /\ r e. ( Base ` Q ) ) -> F e. ( G GrpHom H ) )
70 69 ad3antrrr 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ r = ( 0g ` Q ) ) -> F e. ( G GrpHom H ) )
71 17 56 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. ( Base ` G ) )
72 9 71 syl 
 |-  ( ph -> ( 0g ` G ) e. ( Base ` G ) )
73 72 ad4antr 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ r = ( 0g ` Q ) ) -> ( 0g ` G ) e. ( Base ` G ) )
74 1 70 3 4 5 73 ghmquskerlem1 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ r = ( 0g ` Q ) ) -> ( J ` [ ( 0g ` G ) ] ( G ~QG K ) ) = ( F ` ( 0g ` G ) ) )
75 56 1 ghmid 
 |-  ( F e. ( G GrpHom H ) -> ( F ` ( 0g ` G ) ) = .0. )
76 2 75 syl 
 |-  ( ph -> ( F ` ( 0g ` G ) ) = .0. )
77 76 ad4antr 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ r = ( 0g ` Q ) ) -> ( F ` ( 0g ` G ) ) = .0. )
78 68 74 77 3eqtrd 
 |-  ( ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) /\ r = ( 0g ` Q ) ) -> ( J ` r ) = .0. )
79 65 78 impbida 
 |-  ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ( ( J ` r ) = .0. <-> r = ( 0g ` Q ) ) )
80 1 69 3 4 5 49 ghmquskerlem2 
 |-  ( ( ph /\ r e. ( Base ` Q ) ) -> E. x e. r ( J ` r ) = ( F ` x ) )
81 79 80 r19.29a 
 |-  ( ( ph /\ r e. ( Base ` Q ) ) -> ( ( J ` r ) = .0. <-> r = ( 0g ` Q ) ) )
82 81 pm5.32da 
 |-  ( ph -> ( ( r e. ( Base ` Q ) /\ ( J ` r ) = .0. ) <-> ( r e. ( Base ` Q ) /\ r = ( 0g ` Q ) ) ) )
83 simpr 
 |-  ( ( ph /\ r = ( 0g ` Q ) ) -> r = ( 0g ` Q ) )
84 4 qusgrp 
 |-  ( K e. ( NrmSGrp ` G ) -> Q e. Grp )
85 13 84 syl 
 |-  ( ph -> Q e. Grp )
86 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
87 eqid 
 |-  ( 0g ` Q ) = ( 0g ` Q )
88 86 87 grpidcl 
 |-  ( Q e. Grp -> ( 0g ` Q ) e. ( Base ` Q ) )
89 85 88 syl 
 |-  ( ph -> ( 0g ` Q ) e. ( Base ` Q ) )
90 89 adantr 
 |-  ( ( ph /\ r = ( 0g ` Q ) ) -> ( 0g ` Q ) e. ( Base ` Q ) )
91 83 90 eqeltrd 
 |-  ( ( ph /\ r = ( 0g ` Q ) ) -> r e. ( Base ` Q ) )
92 91 ex 
 |-  ( ph -> ( r = ( 0g ` Q ) -> r e. ( Base ` Q ) ) )
93 92 pm4.71rd 
 |-  ( ph -> ( r = ( 0g ` Q ) <-> ( r e. ( Base ` Q ) /\ r = ( 0g ` Q ) ) ) )
94 82 93 bitr4d 
 |-  ( ph -> ( ( r e. ( Base ` Q ) /\ ( J ` r ) = .0. ) <-> r = ( 0g ` Q ) ) )
95 2 adantr 
 |-  ( ( ph /\ q e. ( Base ` Q ) ) -> F e. ( G GrpHom H ) )
96 95 imaexd 
 |-  ( ( ph /\ q e. ( Base ` Q ) ) -> ( F " q ) e. _V )
97 96 uniexd 
 |-  ( ( ph /\ q e. ( Base ` Q ) ) -> U. ( F " q ) e. _V )
98 5 a1i 
 |-  ( ph -> J = ( q e. ( Base ` Q ) |-> U. ( F " q ) ) )
99 22 36 fnfvelrnd 
 |-  ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ( F ` x ) e. ran F )
100 6 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ran F = ( Base ` H ) )
101 99 100 eleqtrd 
 |-  ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ( F ` x ) e. ( Base ` H ) )
102 38 101 eqeltrd 
 |-  ( ( ( ( ph /\ r e. ( Base ` Q ) ) /\ x e. r ) /\ ( J ` r ) = ( F ` x ) ) -> ( J ` r ) e. ( Base ` H ) )
103 102 80 r19.29a 
 |-  ( ( ph /\ r e. ( Base ` Q ) ) -> ( J ` r ) e. ( Base ` H ) )
104 97 98 103 fmpt2d 
 |-  ( ph -> J : ( Base ` Q ) --> ( Base ` H ) )
105 104 ffnd 
 |-  ( ph -> J Fn ( Base ` Q ) )
106 fniniseg 
 |-  ( J Fn ( Base ` Q ) -> ( r e. ( `' J " { .0. } ) <-> ( r e. ( Base ` Q ) /\ ( J ` r ) = .0. ) ) )
107 105 106 syl 
 |-  ( ph -> ( r e. ( `' J " { .0. } ) <-> ( r e. ( Base ` Q ) /\ ( J ` r ) = .0. ) ) )
108 velsn 
 |-  ( r e. { ( 0g ` Q ) } <-> r = ( 0g ` Q ) )
109 108 a1i 
 |-  ( ph -> ( r e. { ( 0g ` Q ) } <-> r = ( 0g ` Q ) ) )
110 94 107 109 3bitr4d 
 |-  ( ph -> ( r e. ( `' J " { .0. } ) <-> r e. { ( 0g ` Q ) } ) )
111 110 eqrdv 
 |-  ( ph -> ( `' J " { .0. } ) = { ( 0g ` Q ) } )
112 86 18 87 1 kerf1ghm 
 |-  ( J e. ( Q GrpHom H ) -> ( J : ( Base ` Q ) -1-1-> ( Base ` H ) <-> ( `' J " { .0. } ) = { ( 0g ` Q ) } ) )
113 112 biimpar 
 |-  ( ( J e. ( Q GrpHom H ) /\ ( `' J " { .0. } ) = { ( 0g ` Q ) } ) -> J : ( Base ` Q ) -1-1-> ( Base ` H ) )
114 7 111 113 syl2anc 
 |-  ( ph -> J : ( Base ` Q ) -1-1-> ( Base ` H ) )
115 f1f1orn 
 |-  ( J : ( Base ` Q ) -1-1-> ( Base ` H ) -> J : ( Base ` Q ) -1-1-onto-> ran J )
116 114 115 syl 
 |-  ( ph -> J : ( Base ` Q ) -1-1-onto-> ran J )
117 simpr 
 |-  ( ( ph /\ x e. ( Base ` G ) ) -> x e. ( Base ` G ) )
118 ovex 
 |-  ( G ~QG K ) e. _V
119 118 ecelqsi 
 |-  ( x e. ( Base ` G ) -> [ x ] ( G ~QG K ) e. ( ( Base ` G ) /. ( G ~QG K ) ) )
120 117 119 syl 
 |-  ( ( ph /\ x e. ( Base ` G ) ) -> [ x ] ( G ~QG K ) e. ( ( Base ` G ) /. ( G ~QG K ) ) )
121 27 adantr 
 |-  ( ( ph /\ x e. ( Base ` G ) ) -> ( ( Base ` G ) /. ( G ~QG K ) ) = ( Base ` Q ) )
122 120 121 eleqtrd 
 |-  ( ( ph /\ x e. ( Base ` G ) ) -> [ x ] ( G ~QG K ) e. ( Base ` Q ) )
123 elqsi 
 |-  ( r e. ( ( Base ` G ) /. ( G ~QG K ) ) -> E. x e. ( Base ` G ) r = [ x ] ( G ~QG K ) )
124 51 123 syl 
 |-  ( ( ph /\ r e. ( Base ` Q ) ) -> E. x e. ( Base ` G ) r = [ x ] ( G ~QG K ) )
125 simpr 
 |-  ( ( ( ph /\ x e. ( Base ` G ) ) /\ r = [ x ] ( G ~QG K ) ) -> r = [ x ] ( G ~QG K ) )
126 125 fveq2d 
 |-  ( ( ( ph /\ x e. ( Base ` G ) ) /\ r = [ x ] ( G ~QG K ) ) -> ( J ` r ) = ( J ` [ x ] ( G ~QG K ) ) )
127 2 adantr 
 |-  ( ( ph /\ x e. ( Base ` G ) ) -> F e. ( G GrpHom H ) )
128 1 127 3 4 5 117 ghmquskerlem1 
 |-  ( ( ph /\ x e. ( Base ` G ) ) -> ( J ` [ x ] ( G ~QG K ) ) = ( F ` x ) )
129 128 adantr 
 |-  ( ( ( ph /\ x e. ( Base ` G ) ) /\ r = [ x ] ( G ~QG K ) ) -> ( J ` [ x ] ( G ~QG K ) ) = ( F ` x ) )
130 126 129 eqtrd 
 |-  ( ( ( ph /\ x e. ( Base ` G ) ) /\ r = [ x ] ( G ~QG K ) ) -> ( J ` r ) = ( F ` x ) )
131 130 3impa 
 |-  ( ( ph /\ x e. ( Base ` G ) /\ r = [ x ] ( G ~QG K ) ) -> ( J ` r ) = ( F ` x ) )
132 131 eqeq1d 
 |-  ( ( ph /\ x e. ( Base ` G ) /\ r = [ x ] ( G ~QG K ) ) -> ( ( J ` r ) = y <-> ( F ` x ) = y ) )
133 122 124 132 rexxfrd2 
 |-  ( ph -> ( E. r e. ( Base ` Q ) ( J ` r ) = y <-> E. x e. ( Base ` G ) ( F ` x ) = y ) )
134 fvelrnb 
 |-  ( J Fn ( Base ` Q ) -> ( y e. ran J <-> E. r e. ( Base ` Q ) ( J ` r ) = y ) )
135 105 134 syl 
 |-  ( ph -> ( y e. ran J <-> E. r e. ( Base ` Q ) ( J ` r ) = y ) )
136 fvelrnb 
 |-  ( F Fn ( Base ` G ) -> ( y e. ran F <-> E. x e. ( Base ` G ) ( F ` x ) = y ) )
137 21 136 syl 
 |-  ( ph -> ( y e. ran F <-> E. x e. ( Base ` G ) ( F ` x ) = y ) )
138 133 135 137 3bitr4rd 
 |-  ( ph -> ( y e. ran F <-> y e. ran J ) )
139 138 eqrdv 
 |-  ( ph -> ran F = ran J )
140 139 6 eqtr3d 
 |-  ( ph -> ran J = ( Base ` H ) )
141 140 f1oeq3d 
 |-  ( ph -> ( J : ( Base ` Q ) -1-1-onto-> ran J <-> J : ( Base ` Q ) -1-1-onto-> ( Base ` H ) ) )
142 116 141 mpbid 
 |-  ( ph -> J : ( Base ` Q ) -1-1-onto-> ( Base ` H ) )
143 86 18 isgim 
 |-  ( J e. ( Q GrpIso H ) <-> ( J e. ( Q GrpHom H ) /\ J : ( Base ` Q ) -1-1-onto-> ( Base ` H ) ) )
144 7 142 143 sylanbrc 
 |-  ( ph -> J e. ( Q GrpIso H ) )