Metamath Proof Explorer

Theorem unitscyglem3

Description: Lemma for unitscyg. (Contributed by metakunt, 14-Jul-2025)

Ref Expression
Hypotheses unitscyglem1.1 
|- B = ( Base ` G )
unitscyglem1.2 
|- .^ = ( .g ` G )
unitscyglem1.3 
|- ( ph -> G e. Grp )
unitscyglem1.4 
|- ( ph -> B e. Fin )
unitscyglem1.5 
|- ( ph -> A. n e. NN ( # ` { x e. B | ( n .^ x ) = ( 0g ` G ) } ) <_ n )
Assertion unitscyglem3 
|- ( ph -> A. d e. NN ( ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) ) )

Proof

Step Hyp Ref Expression
1 unitscyglem1.1 
 |-  B = ( Base ` G )
2 unitscyglem1.2 
 |-  .^ = ( .g ` G )
3 unitscyglem1.3 
 |-  ( ph -> G e. Grp )
4 unitscyglem1.4 
 |-  ( ph -> B e. Fin )
5 unitscyglem1.5 
 |-  ( ph -> A. n e. NN ( # ` { x e. B | ( n .^ x ) = ( 0g ` G ) } ) <_ n )
6 breq1 
 |-  ( d = c -> ( d || ( # ` B ) <-> c || ( # ` B ) ) )
7 eqeq2 
 |-  ( d = c -> ( ( ( od ` G ) ` x ) = d <-> ( ( od ` G ) ` x ) = c ) )
8 7 rabbidv 
 |-  ( d = c -> { x e. B | ( ( od ` G ) ` x ) = d } = { x e. B | ( ( od ` G ) ` x ) = c } )
9 8 neeq1d 
 |-  ( d = c -> ( { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) <-> { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) )
10 6 9 anbi12d 
 |-  ( d = c -> ( ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) <-> ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) ) )
11 8 fveq2d 
 |-  ( d = c -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) )
12 fveq2 
 |-  ( d = c -> ( phi ` d ) = ( phi ` c ) )
13 11 12 eqeq12d 
 |-  ( d = c -> ( ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) <-> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) )
14 10 13 imbi12d 
 |-  ( d = c -> ( ( ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) ) <-> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) )
15 14 imbi2d 
 |-  ( d = c -> ( ( ph -> ( ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) ) ) <-> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) )
16 simplr 
 |-  ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) -> ph )
17 simplll 
 |-  ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) -> d e. NN )
18 16 17 jca 
 |-  ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) -> ( ph /\ d e. NN ) )
19 breq1 
 |-  ( c = e -> ( c < d <-> e < d ) )
20 breq1 
 |-  ( c = e -> ( c || ( # ` B ) <-> e || ( # ` B ) ) )
21 eqeq2 
 |-  ( c = e -> ( ( ( od ` G ) ` x ) = c <-> ( ( od ` G ) ` x ) = e ) )
22 21 rabbidv 
 |-  ( c = e -> { x e. B | ( ( od ` G ) ` x ) = c } = { x e. B | ( ( od ` G ) ` x ) = e } )
23 22 neeq1d 
 |-  ( c = e -> ( { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) <-> { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) )
24 20 23 anbi12d 
 |-  ( c = e -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) <-> ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) ) )
25 22 fveq2d 
 |-  ( c = e -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) )
26 fveq2 
 |-  ( c = e -> ( phi ` c ) = ( phi ` e ) )
27 25 26 eqeq12d 
 |-  ( c = e -> ( ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) <-> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) )
28 24 27 imbi12d 
 |-  ( c = e -> ( ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) <-> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) )
29 28 imbi2d 
 |-  ( c = e -> ( ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) <-> ( ph -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) ) )
30 19 29 imbi12d 
 |-  ( c = e -> ( ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) <-> ( e < d -> ( ph -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) ) ) )
31 simpr 
 |-  ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) -> A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) )
32 31 adantr 
 |-  ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) -> A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) )
33 32 adantr 
 |-  ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) -> A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) )
34 33 adantr 
 |-  ( ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) /\ e e. NN ) -> A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) )
35 simpr 
 |-  ( ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) /\ e e. NN ) -> e e. NN )
36 30 34 35 rspcdva 
 |-  ( ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) /\ e e. NN ) -> ( e < d -> ( ph -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) ) )
37 simp-5r 
 |-  ( ( ( ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) /\ e e. NN ) /\ ( e < d -> ( ph -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) ) ) /\ e < d ) -> ph )
38 simpr 
 |-  ( ( ( ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) /\ e e. NN ) /\ ( e < d -> ( ph -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) ) ) /\ e < d ) -> e < d )
39 simplr 
 |-  ( ( ( ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) /\ e e. NN ) /\ ( e < d -> ( ph -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) ) ) /\ e < d ) -> ( e < d -> ( ph -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) ) )
40 38 39 mpd 
 |-  ( ( ( ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) /\ e e. NN ) /\ ( e < d -> ( ph -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) ) ) /\ e < d ) -> ( ph -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) )
41 37 40 mpd 
 |-  ( ( ( ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) /\ e e. NN ) /\ ( e < d -> ( ph -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) ) ) /\ e < d ) -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) )
42 41 ex 
 |-  ( ( ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) /\ e e. NN ) /\ ( e < d -> ( ph -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) ) ) -> ( e < d -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) )
43 42 ex 
 |-  ( ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) /\ e e. NN ) -> ( ( e < d -> ( ph -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) ) -> ( e < d -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) ) )
44 36 43 mpd 
 |-  ( ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) /\ e e. NN ) -> ( e < d -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) )
45 44 ralrimiva 
 |-  ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) -> A. e e. NN ( e < d -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) )
46 nfv 
 |-  F/ c ( e < d -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) )
47 nfv 
 |-  F/ e ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) )
48 breq1 
 |-  ( e = c -> ( e < d <-> c < d ) )
49 breq1 
 |-  ( e = c -> ( e || ( # ` B ) <-> c || ( # ` B ) ) )
50 eqeq2 
 |-  ( e = c -> ( ( ( od ` G ) ` x ) = e <-> ( ( od ` G ) ` x ) = c ) )
51 50 rabbidv 
 |-  ( e = c -> { x e. B | ( ( od ` G ) ` x ) = e } = { x e. B | ( ( od ` G ) ` x ) = c } )
52 51 neeq1d 
 |-  ( e = c -> ( { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) <-> { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) )
53 49 52 anbi12d 
 |-  ( e = c -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) <-> ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) ) )
54 51 fveq2d 
 |-  ( e = c -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) )
55 fveq2 
 |-  ( e = c -> ( phi ` e ) = ( phi ` c ) )
56 54 55 eqeq12d 
 |-  ( e = c -> ( ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) <-> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) )
57 53 56 imbi12d 
 |-  ( e = c -> ( ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) <-> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) )
58 48 57 imbi12d 
 |-  ( e = c -> ( ( e < d -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) <-> ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) )
59 46 47 58 cbvralw 
 |-  ( A. e e. NN ( e < d -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) <-> A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) )
60 59 biimpi 
 |-  ( A. e e. NN ( e < d -> ( ( e || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = e } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = e } ) = ( phi ` e ) ) ) -> A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) )
61 45 60 syl 
 |-  ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) -> A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) )
62 18 61 jca 
 |-  ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) -> ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) )
63 simprl 
 |-  ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) -> d || ( # ` B ) )
64 62 63 jca 
 |-  ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) -> ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) )
65 simprr 
 |-  ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) -> { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) )
66 64 65 jca 
 |-  ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) -> ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) )
67 rabn0 
 |-  ( { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) <-> E. x e. B ( ( od ` G ) ` x ) = d )
68 67 biimpi 
 |-  ( { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) -> E. x e. B ( ( od ` G ) ` x ) = d )
69 68 adantl 
 |-  ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) -> E. x e. B ( ( od ` G ) ` x ) = d )
70 simp-4l 
 |-  ( ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ E. x e. B ( ( od ` G ) ` x ) = d ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) )
71 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ E. x e. B ( ( od ` G ) ` x ) = d ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> d || ( # ` B ) )
72 simplr 
 |-  ( ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ E. x e. B ( ( od ` G ) ` x ) = d ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> a e. B )
73 70 71 72 jca31 
 |-  ( ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ E. x e. B ( ( od ` G ) ` x ) = d ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) )
74 simpr 
 |-  ( ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ E. x e. B ( ( od ` G ) ` x ) = d ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> ( ( od ` G ) ` a ) = d )
75 73 74 jca 
 |-  ( ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ E. x e. B ( ( od ` G ) ` x ) = d ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) )
76 nfcv 
 |-  F/_ x B
77 nfcv 
 |-  F/_ z B
78 nfv 
 |-  F/ z ( ( od ` G ) ` x ) = d
79 nfv 
 |-  F/ x ( ( od ` G ) ` z ) = d
80 fveqeq2 
 |-  ( x = z -> ( ( ( od ` G ) ` x ) = d <-> ( ( od ` G ) ` z ) = d ) )
81 76 77 78 79 80 cbvrabw 
 |-  { x e. B | ( ( od ` G ) ` x ) = d } = { z e. B | ( ( od ` G ) ` z ) = d }
82 81 a1i 
 |-  ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> { x e. B | ( ( od ` G ) ` x ) = d } = { z e. B | ( ( od ` G ) ` z ) = d } )
83 82 fveq2d 
 |-  ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( # ` { z e. B | ( ( od ` G ) ` z ) = d } ) )
84 3 ad5antr 
 |-  ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> G e. Grp )
85 4 ad5antr 
 |-  ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> B e. Fin )
86 nfv 
 |-  F/ z ( n .^ x ) = ( 0g ` G )
87 nfv 
 |-  F/ x ( n .^ z ) = ( 0g ` G )
88 oveq2 
 |-  ( x = z -> ( n .^ x ) = ( n .^ z ) )
89 88 eqeq1d 
 |-  ( x = z -> ( ( n .^ x ) = ( 0g ` G ) <-> ( n .^ z ) = ( 0g ` G ) ) )
90 76 77 86 87 89 cbvrabw 
 |-  { x e. B | ( n .^ x ) = ( 0g ` G ) } = { z e. B | ( n .^ z ) = ( 0g ` G ) }
91 90 a1i 
 |-  ( ph -> { x e. B | ( n .^ x ) = ( 0g ` G ) } = { z e. B | ( n .^ z ) = ( 0g ` G ) } )
92 91 fveq2d 
 |-  ( ph -> ( # ` { x e. B | ( n .^ x ) = ( 0g ` G ) } ) = ( # ` { z e. B | ( n .^ z ) = ( 0g ` G ) } ) )
93 92 breq1d 
 |-  ( ph -> ( ( # ` { x e. B | ( n .^ x ) = ( 0g ` G ) } ) <_ n <-> ( # ` { z e. B | ( n .^ z ) = ( 0g ` G ) } ) <_ n ) )
94 93 ralbidv 
 |-  ( ph -> ( A. n e. NN ( # ` { x e. B | ( n .^ x ) = ( 0g ` G ) } ) <_ n <-> A. n e. NN ( # ` { z e. B | ( n .^ z ) = ( 0g ` G ) } ) <_ n ) )
95 94 biimpd 
 |-  ( ph -> ( A. n e. NN ( # ` { x e. B | ( n .^ x ) = ( 0g ` G ) } ) <_ n -> A. n e. NN ( # ` { z e. B | ( n .^ z ) = ( 0g ` G ) } ) <_ n ) )
96 5 95 mpd 
 |-  ( ph -> A. n e. NN ( # ` { z e. B | ( n .^ z ) = ( 0g ` G ) } ) <_ n )
97 96 ad5antr 
 |-  ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> A. n e. NN ( # ` { z e. B | ( n .^ z ) = ( 0g ` G ) } ) <_ n )
98 simp-5r 
 |-  ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> d e. NN )
99 simpllr 
 |-  ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> d || ( # ` B ) )
100 simplr 
 |-  ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> a e. B )
101 simpr 
 |-  ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> ( ( od ` G ) ` a ) = d )
102 nfv 
 |-  F/ x ( ( od ` G ) ` z ) = c
103 nfv 
 |-  F/ z ( ( od ` G ) ` x ) = c
104 fveqeq2 
 |-  ( z = x -> ( ( ( od ` G ) ` z ) = c <-> ( ( od ` G ) ` x ) = c ) )
105 77 76 102 103 104 cbvrabw 
 |-  { z e. B | ( ( od ` G ) ` z ) = c } = { x e. B | ( ( od ` G ) ` x ) = c }
106 eqcom 
 |-  ( { z e. B | ( ( od ` G ) ` z ) = c } = { x e. B | ( ( od ` G ) ` x ) = c } <-> { x e. B | ( ( od ` G ) ` x ) = c } = { z e. B | ( ( od ` G ) ` z ) = c } )
107 105 106 mpbi 
 |-  { x e. B | ( ( od ` G ) ` x ) = c } = { z e. B | ( ( od ` G ) ` z ) = c }
108 107 neeq1i 
 |-  ( { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) <-> { z e. B | ( ( od ` G ) ` z ) = c } =/= (/) )
109 108 anbi2i 
 |-  ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) <-> ( c || ( # ` B ) /\ { z e. B | ( ( od ` G ) ` z ) = c } =/= (/) ) )
110 107 fveq2i 
 |-  ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( # ` { z e. B | ( ( od ` G ) ` z ) = c } )
111 110 eqeq1i 
 |-  ( ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) <-> ( # ` { z e. B | ( ( od ` G ) ` z ) = c } ) = ( phi ` c ) )
112 109 111 imbi12i 
 |-  ( ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) <-> ( ( c || ( # ` B ) /\ { z e. B | ( ( od ` G ) ` z ) = c } =/= (/) ) -> ( # ` { z e. B | ( ( od ` G ) ` z ) = c } ) = ( phi ` c ) ) )
113 112 imbi2i 
 |-  ( ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) <-> ( c < d -> ( ( c || ( # ` B ) /\ { z e. B | ( ( od ` G ) ` z ) = c } =/= (/) ) -> ( # ` { z e. B | ( ( od ` G ) ` z ) = c } ) = ( phi ` c ) ) ) )
114 113 biimpi 
 |-  ( ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) -> ( c < d -> ( ( c || ( # ` B ) /\ { z e. B | ( ( od ` G ) ` z ) = c } =/= (/) ) -> ( # ` { z e. B | ( ( od ` G ) ` z ) = c } ) = ( phi ` c ) ) ) )
115 114 ralimi 
 |-  ( A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) -> A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { z e. B | ( ( od ` G ) ` z ) = c } =/= (/) ) -> ( # ` { z e. B | ( ( od ` G ) ` z ) = c } ) = ( phi ` c ) ) ) )
116 115 adantl 
 |-  ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) -> A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { z e. B | ( ( od ` G ) ` z ) = c } =/= (/) ) -> ( # ` { z e. B | ( ( od ` G ) ` z ) = c } ) = ( phi ` c ) ) ) )
117 116 adantr 
 |-  ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) -> A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { z e. B | ( ( od ` G ) ` z ) = c } =/= (/) ) -> ( # ` { z e. B | ( ( od ` G ) ` z ) = c } ) = ( phi ` c ) ) ) )
118 117 adantr 
 |-  ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) -> A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { z e. B | ( ( od ` G ) ` z ) = c } =/= (/) ) -> ( # ` { z e. B | ( ( od ` G ) ` z ) = c } ) = ( phi ` c ) ) ) )
119 118 adantr 
 |-  ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { z e. B | ( ( od ` G ) ` z ) = c } =/= (/) ) -> ( # ` { z e. B | ( ( od ` G ) ` z ) = c } ) = ( phi ` c ) ) ) )
120 1 2 84 85 97 98 99 100 101 119 unitscyglem2 
 |-  ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> ( # ` { z e. B | ( ( od ` G ) ` z ) = d } ) = ( phi ` d ) )
121 83 120 eqtrd 
 |-  ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) )
122 75 121 syl 
 |-  ( ( ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ E. x e. B ( ( od ` G ) ` x ) = d ) /\ a e. B ) /\ ( ( od ` G ) ` a ) = d ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) )
123 nfv 
 |-  F/ a ( ( od ` G ) ` x ) = d
124 nfv 
 |-  F/ x ( ( od ` G ) ` a ) = d
125 fveqeq2 
 |-  ( x = a -> ( ( ( od ` G ) ` x ) = d <-> ( ( od ` G ) ` a ) = d ) )
126 123 124 125 cbvrexw 
 |-  ( E. x e. B ( ( od ` G ) ` x ) = d <-> E. a e. B ( ( od ` G ) ` a ) = d )
127 126 biimpi 
 |-  ( E. x e. B ( ( od ` G ) ` x ) = d -> E. a e. B ( ( od ` G ) ` a ) = d )
128 127 adantl 
 |-  ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ E. x e. B ( ( od ` G ) ` x ) = d ) -> E. a e. B ( ( od ` G ) ` a ) = d )
129 122 128 r19.29a 
 |-  ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ E. x e. B ( ( od ` G ) ` x ) = d ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) )
130 129 ex 
 |-  ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) -> ( E. x e. B ( ( od ` G ) ` x ) = d -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) ) )
131 130 adantr 
 |-  ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) -> ( E. x e. B ( ( od ` G ) ` x ) = d -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) ) )
132 69 131 mpd 
 |-  ( ( ( ( ( ph /\ d e. NN ) /\ A. c e. NN ( c < d -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) /\ d || ( # ` B ) ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) )
133 66 132 syl 
 |-  ( ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) /\ ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) )
134 133 ex 
 |-  ( ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) /\ ph ) -> ( ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) ) )
135 134 ex 
 |-  ( ( d e. NN /\ A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) ) -> ( ph -> ( ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) ) ) )
136 135 ex 
 |-  ( d e. NN -> ( A. c e. NN ( c < d -> ( ph -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) ) -> ( ph -> ( ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) ) ) ) )
137 15 136 indstr 
 |-  ( d e. NN -> ( ph -> ( ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) ) ) )
138 137 com12 
 |-  ( ph -> ( d e. NN -> ( ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) ) ) )
139 138 imp 
 |-  ( ( ph /\ d e. NN ) -> ( ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) ) )
140 139 ralrimiva 
 |-  ( ph -> A. d e. NN ( ( d || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = d } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = d } ) = ( phi ` d ) ) )